def WeakValue : Term → Bool

Equations

• WeakValue (:λ[a] a_1) = true
• WeakValue x✝ = false

def WeakNormalization.VR : Ty → Term → Prop

Equations

• WeakNormalization.VR (A -t> B) (:λ[a] b) = ∀ (a : Term), WeakNormalization.VR A a → ∃ (v : Term), LeanSubst.Star Red (b[%a::LeanSubst.I]) v ∧ WeakNormalization.VR B v
• WeakNormalization.VR x✝¹ x✝ = False

def WeakNormalization.ER : Ty → Term → Prop

Equations

• WeakNormalization.ER x✝¹ x✝ = ∃ (v : Term), LeanSubst.Star Red x✝ v ∧ WeakNormalization.VR x✝¹ v

theorem WeakNormalization.VR.sound {A : Ty} {t : Term} : VR A t → WeakValue t = true

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

Equations

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

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

Equations

• Γ ⊨w t : A = ∀ (σ : LeanSubst.Subst Term), WeakNormalization.GR Γ σ → WeakNormalization.ER A (t[σ])

def WeakNormalization.«term_⊨w_:_» : Lean.TrailingParserDescr

Equations

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

theorem WeakNormalization.fundamental {Γ : List Ty} {t : Term} {A : Ty} : Γ ⊢ t : A → Γ ⊨w t : A

theorem weak_termination {t : Term} {A : Ty} : [] ⊢ t : A → ∃ (v : Term), LeanSubst.Star Red t v ∧ WeakValue v = true

theorem consistency_lemma {t : Term} : [] ⊢ t : ⊤ → WeakValue t = true → False

theorem consistency {t : Term} : ¬[] ⊢ t : ⊤