inductive SnHeadRed : Term → Term → Prop

• beta {t : Term} {A : Ty} {b : Term} : LeanSubst.SN Red t → ((:λ[A] b) :@ t) ~>sn b[%t::LeanSubst.I]
• app {f f' : Term} (a : Term) : f ~>sn f' → (f :@ a) ~>sn (f' :@ a)

def «term_~>sn_» : Lean.TrailingParserDescr

Equations

• «term_~>sn_» = Lean.ParserDescr.trailingNode `«term_~>sn_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~>sn ") (Lean.ParserDescr.cat `term 81))

theorem SnHeadRed.red_compatible {t a b : Term} : t ~>sn a → t ~> b → a = b ∨ ∃ (z : Term), b ~>sn z ∧ LeanSubst.Star Red a z

theorem SN.subterm_app {f a : Term} : LeanSubst.SN Red (f :@ a) → LeanSubst.SN Red f ∧ LeanSubst.SN Red a

theorem SN.lam {t : Term} {A : Ty} : LeanSubst.SN Red t ↔ LeanSubst.SN Red (:λ[A] t)

theorem SN.neutral_app {f a : Term} : Neutral f → LeanSubst.SN Red f → LeanSubst.SN Red a → LeanSubst.SN Red (f :@ a)

theorem SN.weak_head_expansion {t b : Term} {A : Ty} : LeanSubst.SN Red t → LeanSubst.SN Red (b[%t::LeanSubst.I]) → LeanSubst.SN Red ((:λ[A] b) :@ t)

theorem SN.red_app_preservation {f f' a : Term} : f ~>sn f' → LeanSubst.SN Red f → LeanSubst.SN Red a → LeanSubst.SN Red (f' :@ a) → LeanSubst.SN Red (f :@ a)

theorem SN.backward_closure {t' t : Term} : LeanSubst.SN Red t' → t ~>sn t' → LeanSubst.SN Red t

inductive SnVariant : Type

• neu : SnVariant
• nor : SnVariant
• red : SnVariant

@[reducible, inline]

abbrev SnIndices : SnVariant → Type

Equations

• SnIndices SnVariant.neu = Term
• SnIndices SnVariant.nor = Term
• SnIndices SnVariant.red = (Term × Term)

inductive SNi (v : SnVariant) : SnIndices v → Prop

• var {x : Nat} : SNi SnVariant.neu #x
• app {s : SnIndices SnVariant.neu} {t : SnIndices SnVariant.nor} : SNi SnVariant.neu s → SNi SnVariant.nor t → SNi SnVariant.neu (s :@ t)
• lam {t : SnIndices SnVariant.nor} {A : Ty} : SNi SnVariant.nor t → SNi SnVariant.nor (:λ[A] t)
• neu {t : SnIndices SnVariant.neu} : SNi SnVariant.neu t → SNi SnVariant.nor t
• red {t t' : Term} : SNi SnVariant.red (t, t') → SNi SnVariant.nor t' → SNi SnVariant.nor t
• beta {t : SnIndices SnVariant.nor} {A : Ty} {b : Term} : SNi SnVariant.nor t → SNi SnVariant.red ((:λ[A] b) :@ t, b[%t::LeanSubst.I])
• step {s s' t : Term} : SNi SnVariant.red (s, s') → SNi SnVariant.red (s :@ t, s' :@ t)

@[reducible, inline]

abbrev SNi.SnRenameLemmaType (σ : LeanSubst.Subst Term) : LeanSubst.IsRen σ → (v : SnVariant) → (i : SnIndices v) → Prop

Equations

• SNi.SnRenameLemmaType σ x✝ SnVariant.neu t = SNi SnVariant.neu (t[σ])
• SNi.SnRenameLemmaType σ x✝ SnVariant.nor t = SNi SnVariant.nor (t[σ])
• SNi.SnRenameLemmaType σ x✝ SnVariant.red (t, t') = SNi SnVariant.red (t[σ], t'[σ])

theorem SNi.rename {v : SnVariant} {i : SnIndices v} (σ : LeanSubst.Subst Term) (h : LeanSubst.IsRen σ) : SNi v i → SnRenameLemmaType σ h v i

@[reducible, inline]

abbrev SNi.SnAntiRenameLemmaType (σ : LeanSubst.Subst Term) : LeanSubst.IsRen σ → (v : SnVariant) → (i : SnIndices v) → Prop

Equations

• SNi.SnAntiRenameLemmaType σ x✝ SnVariant.neu t = ∀ (z : Term), t = z[σ] → SNi SnVariant.neu z
• SNi.SnAntiRenameLemmaType σ x✝ SnVariant.nor t = ∀ (z : Term), t = z[σ] → SNi SnVariant.nor z
• SNi.SnAntiRenameLemmaType σ x✝ SnVariant.red (t, t') = ∀ (z : Term), t = z[σ] → ∃ (z' : Term), t' = z'[σ] ∧ SNi SnVariant.red (z, z')

theorem SNi.antirename {v : SnVariant} {i : SnIndices v} (σ : LeanSubst.Subst Term) (h : LeanSubst.IsRen σ) : SNi v i → SnAntiRenameLemmaType σ h v i

@[reducible, inline]

abbrev SNi.SnBetaVarLemmaType (v : SnVariant) (i : SnIndices v) : Prop

Equations

• SNi.SnBetaVarLemmaType SnVariant.neu s = ∀ (t : Term) (x : Nat), s = t :@ #x → SNi SnVariant.neu t
• SNi.SnBetaVarLemmaType SnVariant.nor s = ∀ (t : Term) (x : Nat), s = t :@ #x → SNi SnVariant.nor t
• SNi.SnBetaVarLemmaType SnVariant.red x_2 = True

theorem SNi.beta_var {v : SnVariant} {i : SnIndices v} : SNi v i → SnBetaVarLemmaType v i

@[reducible, inline]

abbrev SNi.SnPropertyWeakenLemmaType (v : SnVariant) (i : SnIndices v) : Prop

Equations

• SNi.SnPropertyWeakenLemmaType SnVariant.neu t = Neutral t
• SNi.SnPropertyWeakenLemmaType SnVariant.nor t = True
• SNi.SnPropertyWeakenLemmaType SnVariant.red (t, t') = t ~> t'

theorem SNi.property_weaken {v : SnVariant} {i : SnIndices v} : SNi v i → SnPropertyWeakenLemmaType v i

@[reducible, inline]

abbrev SNi.SnSoundLemmaType (v : SnVariant) (i : SnIndices v) : Prop

Equations

• SNi.SnSoundLemmaType SnVariant.neu t = LeanSubst.SN Red t
• SNi.SnSoundLemmaType SnVariant.nor t = LeanSubst.SN Red t
• SNi.SnSoundLemmaType SnVariant.red (t, t') = t ~>sn t'

theorem SNi.sound {v : SnVariant} {i : SnIndices v} : SNi v i → SnSoundLemmaType v i

def StrongNormalizaton.LR : Ty → Term → Prop

Equations

• StrongNormalizaton.LR ⊤ = fun (t : Term) => SNi SnVariant.nor t
• StrongNormalizaton.LR (A -t> B) = fun (t : Term) => ∀ (σ : LeanSubst.Subst Term) (v : Term), LeanSubst.IsRen σ → StrongNormalizaton.LR A v → StrongNormalizaton.LR B (t[σ] :@ v)

def StrongNormalizaton.GR : List Ty → LeanSubst.Subst Term → Prop

Equations

• StrongNormalizaton.GR x✝¹ x✝ = ∀ (x : Nat) (T : Ty), x✝¹[x]? = some T → StrongNormalizaton.LR T ↑(x✝ x)

def StrongNormalizaton.SemanticTyping (Γ : List Ty) (t : Term) (A : Ty) : Prop

Equations

• Γ ⊨s t : A = ∀ (σ : LeanSubst.Subst Term), StrongNormalizaton.GR Γ σ → StrongNormalizaton.LR A (t[σ])

def StrongNormalizaton.«term_⊨s_:_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem StrongNormalizaton.monotone {A : Ty} {t : Term} (σ : LeanSubst.Subst Term) : LeanSubst.IsRen σ → LR A t → LR A (t[σ])

theorem StrongNormalizaton.cr {A : Ty} : (∀ (t : Term), LR A t → SNi SnVariant.nor t) ∧ (∀ (t : SnIndices SnVariant.neu), SNi SnVariant.neu t → LR A t) ∧ ∀ (t t' : Term), SNi SnVariant.red (t, t') → LR A t' → LR A t

theorem StrongNormalizaton.var {A : Ty} {x : Nat} : LR A #x

theorem StrongNormalizaton.fundamental {Γ : List Ty} {t : Term} {A : Ty} : Γ ⊢ t : A → Γ ⊨s t : A

theorem strong_normalization_inductive {Γ : List Ty} {t : Term} {A : Ty} : Γ ⊢ t : A → SNi SnVariant.nor t

theorem strong_normalization {Γ : List Ty} {t : Term} {A : Ty} : Γ ⊢ t : A → LeanSubst.SN Red t