Friedman’s A-translation

Peter Selinger

1992

-- Mechanised by Miëtek Bak
-- thanks to András, Ambrus, ames, drvink, Jesper, ncf, and roconnor
-- first-order predicate logic with one sort (naturals) and one predicate (equality)
-- variant with first-order structures for renaming and substitution

{-# OPTIONS --rewriting #-}

module mi.Selinger1992 where

open import mi.FOL public


----------------------------------------------------------------------------------------------------

-- TODO: statement of theorem 1


----------------------------------------------------------------------------------------------------

-- lemma 2

lem2 :  {Þ k} {Γ : Fm§ k} {A}  Þ / Γ  A  PA / Γ  A
lem2 (‵var i)                = ‵var i
lem2 (‵lam d)                = ‵lam (lem2 d)
lem2 (d ‵$ e)                = lem2 d ‵$ lem2 e
lem2 (‵pair d e)             = ‵pair (lem2 d) (lem2 e)
lem2 (‵fst d)                = ‵fst (lem2 d)
lem2 (‵snd d)                = ‵snd (lem2 d)
lem2 (‵left d)               = ‵left (lem2 d)
lem2 (‵right d)              = ‵right (lem2 d)
lem2 (‵either c d e)         = ‵either (lem2 c) (lem2 d) (lem2 e)
lem2 (‵all refl d)           = ‵all refl (lem2 d)
lem2 (‵unall t refl d)       = ‵unall t refl (lem2 d)
lem2 (‵ex t refl d)          = ‵ex t refl (lem2 d)
lem2 (‵letex refl refl d e)  = ‵letex refl refl (lem2 d) (lem2 e)
lem2 (‵abortHA d)            = ‵abort (lem2 d)
lem2 (‵magicPA d)            = ‵magicPA (lem2 d)
lem2 ‵refl                   = ‵refl
lem2 (‵sym d)                = ‵sym (lem2 d)
lem2 (‵trans d e)            = ‵trans (lem2 d) (lem2 e)
lem2 (‵cong f i refl refl d) = ‵cong f i refl refl (lem2 d)
lem2 ‵dis                    = ‵dis
lem2 (‵inj d)                = ‵inj (lem2 d)
lem2 (‵ind refl refl d e)    = ‵ind refl refl (lem2 d) (lem2 e)
lem2 (‵proj i refl)          = ‵proj i refl
lem2 (‵comp g φ refl)        = ‵comp g φ refl
lem2 (‵rec f g)              = ‵rec f g


----------------------------------------------------------------------------------------------------

-- quantifier-free formulas

data IsQFree {k} : Fm k  Set where
  _‵⊃_ :  {A B} (p : IsQFree A) (q : IsQFree B)  IsQFree (A ‵⊃ B)
  _‵∧_ :  {A B} (p : IsQFree A) (q : IsQFree B)  IsQFree (A ‵∧ B)
  _‵∨_ :  {A B} (p : IsQFree A) (q : IsQFree B)  IsQFree (A ‵∨ B)
  ‵⊥  : IsQFree ‵⊥
  _‵=_ :  {t u}  IsQFree (t ‵= u)

-- TODO: lemma 3
-- module _ where
--   open =-Reasoning
--
--   lem3 : ∀ {Þ k} {Γ : Fm§ k} (A : Fm k) {{_ : IsQFree A}} → Σ (Prim k) λ f →
--            Þ / Γ ⊢ A ‵⫗ ‵fun f (tab ‵var) ‵= 𝟘
--   lem3 (A ‵⊃ B) = {!!}
--   lem3 (A ‵∧ B) = {!!}
--   lem3 (A ‵∨ B) = {!!}
--   lem3 ‵⊥      = sig
--                     (ƒconst 1)
--                     (‵pair
--                       (‵lam (abort 0))
--                       (‵lam (‵dis ‵$ (‵lam goal) ‵$ 0)))
--                   where
--                     goal : ∀ {Þ k} {Γ : Fm§ k} →
--                              Þ / Γ , ‵fun (ƒconst 1) (tab ‵var) ‵= 𝟘 ⊢ 𝕊 𝟘 ‵= 𝟘
--                     goal = begin
--                              𝕊 𝟘
--                            =⟨⟩
--                              ‵fun suc (∙ , ‵fun zero ∙)
--                            =⟨ ‵cong suc zero refl refl
--                                  (begin
--                                    ‵fun zero ∙
--                                  =˘⟨ ‵comp zero ∙ refl ⟩
--                                    ‵fun (comp zero ∙) (tab ‵var)
--                                  ∎)
--                                ⟩
--                              ‵fun suc (∙ , ‵fun (comp zero ∙) (tab ‵var))
--                            =˘⟨ ‵comp suc ((∙ , comp zero ∙)) refl ⟩
--                              ‵fun (comp suc (∙ , comp zero ∙)) (tab ‵var)
--                            =⟨⟩
--                              ‵fun (ƒconst 1) (tab ‵var)
--                            =⟨ 0 ⟩
--                              𝟘
--                            ∎
--   lem3 (t ‵= u) = {!!}


----------------------------------------------------------------------------------------------------

-- Π⁰₂ class of formulas

-- TODO: definition of Π⁰₂
-- TODO: lemma 4


----------------------------------------------------------------------------------------------------

-- double negation translation

 :  {k}  Fm k  Fm k
(A ‵⊃ B) ° = A ° ‵⊃ B °
(A ‵∧ B) ° = A ° ‵∧ B °
(A ‵∨ B) ° = ‵¬ ‵¬ (A ° ‵∨ B °)
(‵∀ A)   ° = ‵∀ A °
(‵∃ A)   ° = ‵¬ ‵¬ (‵∃ A °)
‵⊥      ° = ‵⊥
(t ‵= u) ° = ‵¬ ‵¬ (t ‵= u)

_°§ :  {k}  Fm§ k  Fm§ k
       °§ = 
(Γ , A) °§ = Γ °§ , A °

-- TODO: interactions between DNT and renaming/substitution
module _ where
  postulate
    TODO1 :  {k} {A : Fm (suc k)} {t}  A ° [ t /0]Fm  A [ t /0]Fm °
  -- TODO1 = {!!}

  postulate
    TODO2 :  {Þ k} {Γ : Fm§ k} {A}  Þ / wkFm§ Γ °§  A  Þ / wkFm§ (Γ °§)  A
  -- TODO2 = {!!}

  postulate
    TODO3 :  {Þ k} {Γ : Fm§ k} {A t}  Þ / Γ  A [ t /0]Fm °  Þ / Γ  A ° [ t /0]Fm
  -- TODO3 = {!!}

  postulate
    TODO4 :  {Þ k} {Γ : Fm§ k} {A t}  Þ / Γ  ‵∀ (A ° ‵⊃ wkFm A [ t /1]Fm °) 
              Þ / Γ  ‵∀ (A ° ‵⊃ wkFm (A °) [ t /1]Fm)
  -- TODO4 = {!!}

  postulate
    TODO5 :  {Þ k} {Γ : Fm§ k} {A C}  Þ / wkFm§ Γ °§ , A °  wkFm C ° 
              Þ / wkFm§ (Γ °§) , A °  wkFm (C °)
  -- TODO5 = {!!}

-- TODO: lemma 5
module _ where
  open ⫗-Reasoning

  lem5-1 :  {k} {Γ : Fm§ k} {A}  PA / Γ  A ° ‵⫗ A
  lem5-1 {A = A ‵⊃ B} = ‵cong⊃ lem5-1 lem5-1
  lem5-1 {A = A ‵∧ B} = ‵cong∧ lem5-1 lem5-1
  lem5-1 {A = A ‵∨ B} = begin
                          (A ‵∨ B) °
                        ⫗⟨ ‵dn 
                          A ° ‵∨ B °
                        ⫗⟨ ‵cong∨ lem5-1 lem5-1 
                          A ‵∨ B
                        
  lem5-1 {A = ‵∀ A}   = ‵cong∀ lem5-1
  lem5-1 {A = ‵∃ A}   = begin
                          (‵∃ A) °
                        ⫗⟨ ‵dn 
                          ‵∃ A °
                        ⫗⟨ ‵cong∃ lem5-1 
                          ‵∃ A
                        
  lem5-1 {A = ‵⊥}    = ⫗refl
  lem5-1 {A = t ‵= u} = ‵dn

lem5-2 :  {Þ k} {Γ : Fm§ k} {A}  Þ / Γ  ‵¬ ‵¬ (A °) ‵⊃ A °
lem5-2 {A = A ‵⊃ B} = ‵lam (‵lam (lem5-2 ‵$ ‵lam
                         (2 ‵$ ‵lam
                           (1 ‵$ 0 ‵$ 2))))
lem5-2 {A = A ‵∧ B} = ‵lam (‵pair
                         (lem5-2 ‵$ ‵lam
                           (1 ‵$ ‵lam
                             (1 ‵$ ‵fst 0)))
                         (lem5-2 ‵$ ‵lam
                           (1 ‵$ ‵lam
                             (1 ‵$ ‵snd 0))))
lem5-2 {A = A ‵∨ B} = ‵lam (‵join 0)
lem5-2 {A = ‵∀ A}   = ‵lam (‵all refl (lem5-2 ‵$ ‵lam
                         (1 ‵$ ‵lam
                           (1 ‵$ ‵unall (‵tvar 0) (idcutFm (A °)) 0))))
lem5-2 {A = ‵∃ A}   = ‵lam (‵join 0)
lem5-2 {A = ‵⊥}    = ‵lam (0 ‵$ ⊃id)
lem5-2 {A = t ‵= u} = ‵lam (‵join 0)

lem5-3∋ :  {k} {Γ : Fm§ k} {A}  Γ  A  Γ °§  A °
lem5-3∋ zero    = zero
lem5-3∋ (suc i) = suc (lem5-3∋ i)

-- TODO: why does rewriting blow up constraint solver here?
module _ where
  lem5-3 :  {Þ k} {Γ : Fm§ k} {A}  PA / Γ  A  Þ / Γ °§  A °
  lem5-3 (‵var i)                = ‵var (lem5-3∋ i)
  lem5-3 (‵lam d)                = ‵lam (lem5-3 d)
  lem5-3 (d ‵$ e)                = lem5-3 d ‵$ lem5-3 e
  lem5-3 (‵pair d e)             = ‵pair (lem5-3 d) (lem5-3 e)
  lem5-3 (‵fst d)                = ‵fst (lem5-3 d)
  lem5-3 (‵snd d)                = ‵snd (lem5-3 d)
  lem5-3 (‵left d)               = ‵return (‵left (lem5-3 d))
  lem5-3 (‵right d)              = ‵return (‵right (lem5-3 d))
  lem5-3 (‵either c d e)         = lem5-2 ‵$ (lem5-3 c ‵>>= ‵lam (‵either 0
                                     (‵return (‵exch (wk (lem5-3 d))))
                                     (‵return (‵exch (wk (lem5-3 e))))))
  lem5-3 {Γ = Γ} (‵all refl d)
      = ‵all refl (TODO2 {Γ = Γ} (lem5-3 d))

  lem5-3 (‵unall t refl d)       = ‵unall t TODO1 (lem5-3 d)
  lem5-3 (‵ex t refl d)          = ‵return (‵ex t TODO1 (lem5-3 d))

  lem5-3 {Γ = Γ} (‵letex {C = C} refl refl d e)
      = lem5-2 ‵$
          (lem5-3 d ‵>>=
            ‵lam (‵letex refl refl 0
              (‵return (‵exch (wk (TODO5 {Γ = Γ} {C = C} (lem5-3 e)))))))

  lem5-3 (‵magicPA d)            = lem5-2 ‵$ ‵lam (lem5-3 d)
  lem5-3 ‵refl                   = ‵return ‵refl
  lem5-3 (‵sym d)                = lem5-3 d ‵>>= ‵lam
                                     (‵return (‵sym 0))
  lem5-3 (‵trans d e)            = lem5-3 d ‵>>= ‵lam
                                     (wk (lem5-3 e) ‵>>= ‵lam
                                       (‵return (‵trans 1 0)))
  lem5-3 (‵cong f i refl refl d) = lem5-3 d ‵>>= ‵lam
                                     (‵return (‵cong f i refl refl 0))
  lem5-3 ‵dis                    = ‵return ‵dis
  lem5-3 (‵inj d)                = lem5-3 d ‵>>= ‵lam
                                     (‵return (‵inj 0))
  lem5-3 (‵ind refl refl d e)    = ‵ind refl refl (TODO3 (lem5-3 d)) (TODO4 (lem5-3 e))
  lem5-3 (‵proj i refl)          = ‵return (‵proj i refl)
  lem5-3 (‵comp g φ refl)        = ‵return (‵comp g φ refl)
  lem5-3 (‵rec {t = t} f g)      = ‵pair
                                     (‵return (‵fst (‵rec {t = t} f g)))
                                     (‵return (‵snd (‵rec f g)))

-- "Note that the converse of 3 trivially holds wih 1."
lem5-3⁻¹ :  {Þ k} {Γ : Fm§ k} {A}  Þ / Γ °§  A °  PA / Γ  A
lem5-3⁻¹ d = aux (‵fst lem5-1 ‵$ lem2 d)
  where
    aux :  {k} {Γ : Fm§ k} {A}  PA / Γ °§  A  PA / Γ  A
    aux {Γ = }     d = d
    aux {Γ = Γ , C} d = wk (aux (‵lam d)) ‵$ (‵snd lem5-1 ‵$ 0)

-- TODO: "A counterexample for 4 is ¬∀y.A[y/x₀]."
-- lem5-4 : ∀ {k} {Γ : Fm§ k} → ¬ (∀ {A} → HA / Γ , ‵¬ (‵∀ A) ⊢ (‵¬ (‵∀ A)) °)
-- lem5-4 = {!!}


----------------------------------------------------------------------------------------------------

-- A-translation

_ᴬ⟨_⟩ :  {k}  Fm k  Fm k  Fm k
(A ‵⊃ B) ᴬ⟨ T  = A ᴬ⟨ T  ‵⊃ B ᴬ⟨ T 
(A ‵∧ B) ᴬ⟨ T  = A ᴬ⟨ T  ‵∧ B ᴬ⟨ T 
(A ‵∨ B) ᴬ⟨ T  = A ᴬ⟨ T  ‵∨ B ᴬ⟨ T 
(‵∀ A)   ᴬ⟨ T  = ‵∀ A ᴬ⟨ wkFm T 
(‵∃ A)   ᴬ⟨ T  = ‵∃ A ᴬ⟨ wkFm T 
‵⊥      ᴬ⟨ T  = T
(t ‵= u) ᴬ⟨ T  = (t ‵= u) ‵∨ T

_ᴬ⟨_⟩§ :  {k}  Fm§ k  Fm k  Fm§ k
       ᴬ⟨ T ⟩§ = 
(Γ , A) ᴬ⟨ T ⟩§ = Γ ᴬ⟨ T ⟩§ , A ᴬ⟨ T 

-- TODO: interactions between A-translation and renaming/substitution
module _ where
  postulate
    TODO6 :  {k} {A : Fm (suc k)} {T t}  (A ᴬ⟨ wkFm T ) [ t /0]Fm  (A [ t /0]Fm) ᴬ⟨ T 
  -- TODO6 = ?

-- TODO: lemma 6
module _ where
  open 

  -- non-constructive lemma
  aux1 :  {k} {Γ : Fm§ k} {A B C}  PA / Γ  (A ‵∨ C) ‵⊃ (B ‵∨ C) ‵⫗ (A ‵⊃ B) ‵∨ C
  aux1 = ‵pair
           (‵lam (‵either ‵em
             (‵right 0)
             (‵left (‵lam
               (‵either (2 ‵$ (‵left 0))
                 0
                 (‵abort (2 ‵$ 0)))))))
           (‵lam (‵lam (‵either 0
             (‵either 2
               (‵left (0 ‵$ 1))
               (‵right 0))
             (‵right 0))))

  aux2 :  {Þ k} {Γ : Fm§ k} {A B C}  Þ / Γ  (A ‵∨ C) ‵∧ (B ‵∨ C) ‵⫗ (A ‵∧ B) ‵∨ C
  aux2 = ‵pair
           (‵lam (‵either (‵fst 0)
             (‵either (‵snd 1)
               (‵left (‵pair 1 0))
               (‵right 0))
             (‵right 0)))
           (‵lam (‵either 0
             (‵pair (‵left (‵fst 0)) (‵left (‵snd 0)))
             (‵pair (‵right 0) (‵right 0))))

  aux3 :  {Þ k} {Γ : Fm§ k} {A B C}  Þ / Γ  (A ‵∨ C) ‵∨ (B ‵∨ C) ‵⫗ (A ‵∨ B) ‵∨ C
  aux3 = ‵pair
           (‵lam (‵either 0
             (‵either 0
               (‵left (‵left 0))
               (‵right 0))
             (‵either 0
               (‵left (‵right 0))
               (‵right 0))))
           (‵lam (‵either 0
             (‵either 0
               (‵left (‵left 0))
               (‵right (‵left 0)))
             (‵left (‵right 0)))) -- could also be ‵right

  -- non-constructive lemma
  aux4 :  {k} {Γ : Fm§ k} {A C}  PA / Γ  ‵∀ (A ‵∨ wkFm C) ‵⫗ ‵∀ A ‵∨ C
  aux4 {A = A} {C} = ‵pair
                       (‵lam (‵either ‵em
                         (‵right 0)
                         (‵left
                           (‵all refl (‵either (‵unall (‵tvar 0) (idcutFm (A ‵∨ wkFm C)) 1)
                             0
                             (‵abort (1 ‵$ 0)))))))
                       (‵lam (‵either 0
                         (‵all refl (‵left (‵unall (‵tvar 0) (idcutFm A) 0)))
                         (‵all refl (‵right 0))))

  aux5 :  {Þ k} {Γ : Fm§ k} {A C}  Þ / Γ  ‵∃ (A ‵∨ wkFm C) ‵⫗ ‵∃ A ‵∨ C
  aux5 {A = A} {C} = ‵pair
                       (‵lam (‵letex refl refl 0 (‵either 0
                         (‵left (‵ex (‵tvar 0) (idcutFm A) 0))
                         (‵right 0))))
                       (‵lam (‵either 0
                         (‵letex refl refl 0
                           (‵ex (‵tvar 0) (_‵∨_ & idcutFm A  idcutFm (wkFm C)) (‵left 0)))
                         (‵ex 𝟘 -- could also be any other natural
                           ( (subFm (idTm§ , 𝟘) A ‵∨_)
                               & ( eqsubFm idTm§ 𝟘 C
                                  idsubFm C
                                 )
                           )
                           (‵right 0))))

  aux6 :  {Þ k} {Γ : Fm§ k} {C}  Þ / Γ  C ‵⫗ ‵⊥ ‵∨ C
  aux6 = ‵pair
           (‵lam (‵right 0))
           (‵lam (‵either 0 (‵abort 0) 0))

module _ where
  open ⫗-Reasoning

  lem6-1 :  {k} {Γ : Fm§ k} {A T}  PA / Γ  A ᴬ⟨ T  ‵⫗ A ‵∨ T
  lem6-1 {A = A ‵⊃ B} {T} = begin
                              A ᴬ⟨ T  ‵⊃ B ᴬ⟨ T 
                            ⫗⟨ ‵cong⊃ lem6-1 lem6-1 
                              (A ‵∨ T) ‵⊃ (B ‵∨ T)
                            ⫗⟨ aux1 
                              (A ‵⊃ B) ‵∨ T
                            
  lem6-1 {A = A ‵∧ B} {T} = begin
                              A ᴬ⟨ T  ‵∧ B ᴬ⟨ T 
                            ⫗⟨ ‵cong∧ lem6-1 lem6-1 
                              (A ‵∨ T) ‵∧ (B ‵∨ T)
                            ⫗⟨ aux2 
                              (A ‵∧ B) ‵∨ T
                            
  lem6-1 {A = A ‵∨ B} {T} = begin
                              A ᴬ⟨ T  ‵∨ B ᴬ⟨ T 
                            ⫗⟨ ‵cong∨ lem6-1 lem6-1 
                              (A ‵∨ T) ‵∨ (B ‵∨ T)
                            ⫗⟨ aux3 
                              (A ‵∨ B) ‵∨ T
                            
  lem6-1 {A = ‵∀ A}   {T} = begin
                              ‵∀ (A ᴬ⟨ wkFm T )
                            ⫗⟨ ‵cong∀ lem6-1 
                              ‵∀ (A ‵∨ wkFm T)
                            ⫗⟨ aux4 
                              ‵∀ A ‵∨ T
                            
  lem6-1 {A = ‵∃ A}   {T} = begin
                              ‵∃ (A ᴬ⟨ wkFm T )
                            ⫗⟨ ‵cong∃ lem6-1 
                              ‵∃ (A ‵∨ wkFm T)
                            ⫗⟨ aux5 
                              ‵∃ A ‵∨ T
                            
  lem6-1 {A = ‵⊥}    {T} = aux6
  lem6-1 {A = t ‵= u} {T} = ⫗refl

-- lem6-2 : ∀ {Þ k} {Γ : Fm§ k} {A T} → Þ / Γ ⊢ T ‵⊃ A ᴬ⟨ T ⟩
-- lem6-2 {A = A ‵⊃ B}    = ‵lam (‵lam (lem6-2 ‵$ 1)) -- function argument ignored
-- lem6-2 {A = A ‵∧ B}    = ‵lam (‵pair (lem6-2 ‵$ 0) (lem6-2 ‵$ 0))
-- lem6-2 {A = A ‵∨ B}    = ‵lam (‵left (lem6-2 ‵$ 0)) -- could also be ‵right
-- lem6-2 {A = ‵∀ A}      = ‵lam (‵all refl (lem6-2 ‵$ 0))
-- lem6-2 {A = ‵∃ A}  {T} = {!!}
-- -- ‵lam (‵ex 𝟘 (TODO6 {A = A} {T}) (lem6-2 {A = A [ 𝟘 /0]Fm} ‵$ 0)) -- TODO: termination failure
-- lem6-2 {A = ‵⊥}       = ⊃id
-- lem6-2 {A = t ‵= u}    = ‵lam (‵right 0)
--
-- lem6-3∋ : ∀ {k} {Γ : Fm§ k} {A T} → Γ ∋ A → Γ ᴬ⟨ T ⟩§ ∋ A ᴬ⟨ T ⟩
-- lem6-3∋ zero    = zero
-- lem6-3∋ (suc i) = suc (lem6-3∋ i)

-- TODO: "The proof of 3 is a bit tricky where eigenvariable conditions are involved."
-- lem6-3 : ∀ {Þ k} {Γ : Fm§ k} {A T} → Þ / Γ ⊢ A → Þ / Γ ᴬ⟨ T ⟩§ ⊢ A ᴬ⟨ T ⟩
-- lem6-3 (‵var i)                = ‵var (lem6-3∋ i)
-- lem6-3 (‵lam d)                = ‵lam (lem6-3 d)
-- lem6-3 (d ‵$ e)                = lem6-3 d ‵$ lem6-3 e
-- lem6-3 (‵pair d e)             = ‵pair (lem6-3 d) (lem6-3 e)
-- lem6-3 (‵fst d)                = ‵fst (lem6-3 d)
-- lem6-3 (‵snd d)                = ‵snd (lem6-3 d)
-- lem6-3 (‵left d)               = ‵left (lem6-3 d)
-- lem6-3 (‵right d)              = ‵right (lem6-3 d)
-- lem6-3 (‵either c d e)         = ‵either (lem6-3 c) (lem6-3 d) (lem6-3 e)
-- lem6-3 (‵all refl d)           = {!!}
-- lem6-3 (‵unall t refl d)       = {!!}
-- lem6-3 (‵ex t refl d)          = {!!}
-- lem6-3 (‵letex refl refl d e)  = {!!}
-- lem6-3 (‵abort d)              = {!!}
-- lem6-3 (‵magic d)              = {!!}
-- lem6-3 ‵refl                   = ‵left ‵refl
-- lem6-3 (‵sym d)                = ‵either (lem6-3 d)
--                                    (‵left (‵sym 0))
--                                    (‵right 0)
-- lem6-3 (‵trans d e)            = ‵either (lem6-3 d)
--                                    (‵either (wk (lem6-3 e))
--                                      (‵left (‵trans 1 0))
--                                      (‵right 0))
--                                    (‵right 0)
-- lem6-3 (‵cong f i refl refl d) = {!!}
-- lem6-3 ‵dis                    = {!!}
-- lem6-3 (‵inj d)                = {!!}
-- lem6-3 (‵ind refl refl d e)    = {!!}
-- lem6-3 (‵proj i refl)          = {!!}
-- lem6-3 (‵comp g φ refl)        = {!!}
-- lem6-3 (‵rec f g)              = {!!}

-- TODO: "A counterexample for 4 is A = ¬¬T."
-- lem6-4 : ∀ {k} {Γ : Fm§ k} → ¬ (∀ {T} → HA / Γ , ‵¬ ‵¬ T ⊢ (‵¬ ‵¬ T) ᴬ⟨ T ⟩)
-- lem6-4 = {!!}


----------------------------------------------------------------------------------------------------

-- proof of theorem 1

-- TODO: lemma 7
-- TODO: corollary 8
-- TODO: theorem 1


----------------------------------------------------------------------------------------------------

Lorem ipsum dolor sit amet, consectetur adipisicing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.


P. Selinger (1992)

Friedman’s A-translation

Manuscript.