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 : Trm) (t' : Trm) : t.SN → multi_red t t' → t'.SN

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

theorem Trm.normal_is_unique (t : Trm) (t1 : Trm) (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).neutral = (false = true)
• (a @ a_1).neutral = (true = true)

theorem Trm.CR2 (A : Typ) (t : Trm) (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_lemma (A1 : Typ) (A2 : Typ) (t : Trm) : (λt).lc → (∀ (u : Trm), ∀ x ∉ t.fv, u ∈ Trm.SC A1 → ([x // u] t.open₀ ($x)) ∈ Trm.SC A2) → ∃ (y : ℕ), t.open₀ ($y) ∈ Trm.SC A2

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

theorem Trm.SC_lambda_open (A1 : Typ) (A2 : Typ) (t : Trm) : (λt).lc → (∀ u ∈ Trm.SC A1, t.open₀ u ∈ Trm.SC A2) → (λ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.beta_red_strongly_normalizing (t : Trm) (T : Typ) : typing [] t T → t.SN