def StrongNormalizaton.LR : Ty → Term → Prop

Equations

• StrongNormalizaton.LR ⊤ = fun (t : Term) => SNi SnVariant.nor t
• StrongNormalizaton.LR (A -t> B) = fun (t : Term) => ∀ (r : LeanSubst.Ren) (v : Term), StrongNormalizaton.LR A v → StrongNormalizaton.LR B (t[↑r] :@ 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} (r : LeanSubst.Ren) : LR A t → LR A t[↑r]

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