Examples

              1.5. Examples🔗
              The usual lambda-calculus constants are represented directly as L0 terms.
The examples after the definitions are checked reduction derivations.
def I : L0 := L0[λ 0]def T : L0 := L0[λ λ 1]def F : L0 := L0[λ λ 0]def N : L0 := L0[λ 0 {F} {T}]def N' : L0 := L0[λ λ λ 2 0 1]def A : L0 := L0[λ λ 1 0 {F}]def M : L0 := L0[λ λ λ 0 2 1]example : NormalForm I := by⊢ I.NormalForm normalAll goals completed! 🐙example : NormalForm T := by⊢ T.NormalForm normalAll goals completed! 🐙example : NormalForm F := by⊢ F.NormalForm normalAll goals completed! 🐙example : NormalForm N := by⊢ N.NormalForm normalAll goals completed! 🐙example : NormalForm N' := by⊢ N'.NormalForm normalAll goals completed! 🐙example : NormalForm A := by⊢ A.NormalForm normalAll goals completed! 🐙example : NormalForm M := by⊢ M.NormalForm normalAll goals completed! 🐙example : L0[{I} 3] →β₀ L0[3] := by⊢ I.app (var 3) →β₀ var 3 beta_stepAll goals completed! 🐙example : L0[{I} 3] →β₀* L0[3] := by⊢ I.app (var 3) →β₀* var 3 rt_step { beta_stepAll goals completed! 🐙 }example : L0[{T} 3 4] →β₀* L0[3] := by⊢ (T.app (var 3)).app (var 4) →β₀* var 3 beta_stepsAll goals completed! 🐙example : L0[{F} 3 4] →β₀* L0[4] := by⊢ (F.app (var 3)).app (var 4) →β₀* var 4 beta_stepsAll goals completed! 🐙example : L0[{N} {T}] →β₀* L0[{F}] := by⊢ N.app T →β₀* F calc
    _   = L0[{N} {T}] := by⊢ N.app T = N.app T rflAll goals completed! 🐙
    _   = L0[(λ 0 {F} {T}) {T}] := by⊢ N.app T = (((var 0).app F).app T).lam.app T rflAll goals completed! 🐙
    _  →β₀ L0[{T} {F} {T}] := by⊢ (((var 0).app F).app T).lam.app T →β₀ (T.app F).app T beta_stepAll goals completed! 🐙
    _   = L0[(λ λ 1) {F} {T}] := by⊢ (T.app F).app T = ((var 1).lam.lam.app F).app T rflAll goals completed! 🐙
    _  →β₀ L0[(λ {F}) {T}] := by⊢ ((var 1).lam.lam.app F).app T →β₀ F.lam.app T beta_stepAll goals completed! 🐙
    _  →β₀ L0[{F}] := by⊢ F.lam.app T →β₀ F beta_stepAll goals completed! 🐙example : L0[{N} {F}] →β₀* L0[{T}] := by⊢ N.app F →β₀* T calc
    _   = L0[{N} {F}] := by⊢ N.app F = N.app F rflAll goals completed! 🐙
    _   = L0[(λ 0 {F} {T}) {F}] := by⊢ N.app F = (((var 0).app F).app T).lam.app F rflAll goals completed! 🐙
    _  →β₀ L0[{F} {F} {T}] := by⊢ (((var 0).app F).app T).lam.app F →β₀ (F.app F).app T beta_stepAll goals completed! 🐙
    _   = L0[(λ λ 0) {F} {T}] := by⊢ (F.app F).app T = ((var 0).lam.lam.app F).app T rflAll goals completed! 🐙
    _  →β₀ L0[(λ 0) {T}] := by⊢ ((var 0).lam.lam.app F).app T →β₀ (var 0).lam.app T beta_stepAll goals completed! 🐙
    _  →β₀ L0[{T}] := by⊢ (var 0).lam.app T →β₀ T beta_stepAll goals completed! 🐙example : L0[{N'} {T}] →β₀* L0[{F}] := by⊢ N'.app T →β₀* F beta_stepsAll goals completed! 🐙example : L0[{N'} {F}] →β₀* L0[{T}] := by⊢ N'.app F →β₀* T beta_stepsAll goals completed! 🐙example : L0[{N} {T}] →β₀* L0[{F}] := by⊢ N.app T →β₀* F beta_stepsAll goals completed! 🐙example : L0[{N} {F}] →β₀* L0[{T}] := by⊢ N.app F →β₀* T beta_stepsAll goals completed! 🐙example : L0[{N'} {T}] →β₀* L0[{F}] := by⊢ N'.app T →β₀* F beta_stepsAll goals completed! 🐙example : L0[{N'} {F}] →β₀* L0[{T}] := by⊢ N'.app F →β₀* T beta_stepsAll goals completed! 🐙example : L0[{A} {T} {T}] →β₀* L0[{T}] := by⊢ (A.app T).app T →β₀* T beta_stepsAll goals completed! 🐙example : L0[{A} {T} {F}] →β₀* L0[{F}] := by⊢ (A.app T).app F →β₀* F beta_stepsAll goals completed! 🐙example : L0[{A} {F} {T}] →β₀* L0[{F}] := by⊢ (A.app F).app T →β₀* F beta_stepsAll goals completed! 🐙example : L0[{A} {F} {F}] →β₀* L0[{F}] := by⊢ (A.app F).app F →β₀* F beta_stepsAll goals completed! 🐙def Z : L0 := L0[λ λ 0]def S : L0 := L0[λ λ λ 1 (2 1 0)]def Plus : L0 := L0[λ λ 1 {S} 0]end L0