def Trm.reducible (t : Trm) : Prop

Equations

• t.reducible = ∃ (t' : Trm), beta_red t t'

def Trm.normal (t : Trm) : Prop

Equations

• t.normal = ¬t.reducible

theorem Trm.normal_has_no_proper_multi_red (t : Trm) : t.normal → ∀ (t' : Trm), multi_red t t' → t = t'

def Trm.normalizable (t : Trm) : Prop

Equations

• t.normalizable = ∃ (t' : Trm), multi_red t t' ∧ t'.normal

def Trm.strongly_normalizable (t : Trm) : Prop

Equations

• t.strongly_normalizable = ∀ (f : ℕ → Trm), (f 0 = t ∧ ∀ (n : ℕ), beta_red (f n) (f n.succ)) → False

inductive Trm.SN : Trm → Prop

• sn {t : Trm} : (∀ (t' : Trm), beta_red t t' → t'.SN) → t.SN

theorem Trm.strongly_normalizable_iff_SN (t : Trm) : t.strongly_normalizable ↔ t.SN

theorem Trm.beta_red_preserves_SN (t : Trm) : t.SN → ∀ (t' : Trm), beta_red t t' → t'.SN

theorem Trm.multi_red_preserves_SN (t t' : Trm) : t.SN → multi_red t t' → t'.SN

theorem Trm.SN_app1 (t s : Trm) : s.lc → (t @ s).SN → t.SN

theorem Trm.normal_is_unique (t t1 t2 : Trm) : (multi_red t t1 ∧ t1.normal) ∧ multi_red t t2 ∧ t2.normal → t1 = t2

def Trm.SC : Typ → Set Trm

Equations

• Trm.SC Typ.typ_base = {t : Trm | t.lc ∧ t.SN}
• Trm.SC (t1 -> t2) = {t : Trm | t.lc ∧ ∀ (u : Trm), u.lc ∧ u ∈ Trm.SC t1 → (t @ u) ∈ Trm.SC t2}

theorem Trm.SC_regular (A : Typ) (t : Trm) : t ∈ Trm.SC A → t.lc

def Trm.neutral : Trm → Prop

Equations

• (€a).neutral = (true = true)
• ($a).neutral = (true = true)
• (λ a,a_1).neutral = (false = true)
• (a @ a_1).neutral = (true = true)

theorem Trm.CR2 (A : Typ) (t t' : Trm) : t ∈ Trm.SC A → multi_red t t' → t' ∈ Trm.SC A

theorem Trm.CR_1_3 (A : Typ) (t : Trm) : (t ∈ Trm.SC A → t.SN) ∧ (t.lc → t.neutral → (∀ (t' : Trm), beta_red t t' → t' ∈ Trm.SC A) → t ∈ Trm.SC A)

def Trm.CR1 (A : Typ) (t : Trm) : t ∈ Trm.SC A → t.SN

Equations

• ⋯ = ⋯

def Trm.CR3 (A : Typ) (t : Trm) : t.lc → t.neutral → (∀ (t' : Trm), beta_red t t' → t' ∈ Trm.SC A) → t ∈ Trm.SC A

Equations

• ⋯ = ⋯

theorem Trm.SC_var (A : Typ) (x : ℕ) : ($x) ∈ Trm.SC A

theorem Trm.SC_lambda (A1 A2 : Typ) (t : Trm) : (λ A1,t).lc → (∀ (u : Trm), ∀ x ∉ t.fv, u ∈ Trm.SC A1 → ([x // u] t.open₀ ($x)) ∈ Trm.SC A2) → (λ A1,t) ∈ Trm.SC (A1 -> A2)

theorem Trm.SC_lambda_term (A1 A2 : Typ) (t : Trm) : (λ A1,t).lc → (∀ u ∈ Trm.SC A1, t.open₀ u ∈ Trm.SC A2) → (λ A1,t) ∈ Trm.SC (A1 -> A2)

theorem Trm.SC_subst {Γ : context} (t : Trm) (A : Typ) : typing Γ t A → ∀ (f : { x : ℕ // x ∈ context_terms Γ } → Trm), (∀ (x : ℕ) (h : x ∈ context_terms Γ), f ⟨x, h⟩ ∈ Trm.SC (Trm.context_type Γ ⟨x, h⟩)) → Trm.multi_subst (context_terms Γ) f t ∈ Trm.SC A

theorem Trm.strong_normalization (t : Trm) (T : Typ) : typing [] t T → t.SN