2.6. Examples
The named constants mirror the L0 constants, but can now be written with
ordinary variable names.
def I : L1 := L1[λx. x]def T : L1 := L1[λx. λy. x]def F : L1 := L1[λx. λy. y]def N : L1 := L1[λb. b {F} {T}]def N' : L1 := L1[λb. λx. λy. b y x]def A : L1 := L1[λb. λc. b c {F}]def M : L1 := L1[λb. λx. λy. y b x]def Z : L1 := L1[λf. λx. x]def S : L1 := L1[λn. λf. λx. f (n f x)]def Plus : L1 := L1[λn. λm. n {S} m]example : L1.toL0 L1[λx. x] = L0[λ 0] := ⊢ (lam "x" (var "x")).toL0 = (L0.var 0).lam All goals completed! 🐙example : L1.toL0 L1[λx. λy. x] = L0[λ λ 1] := ⊢ (lam "x" (lam "y" (var "x"))).toL0 = (L0.var 1).lam.lam All goals completed! 🐙example : L1.toL0 L1[λx. λy. y] = L0[λ λ 0] := ⊢ (lam "x" (lam "y" (var "y"))).toL0 = (L0.var 0).lam.lam All goals completed! 🐙example : L1.toL0 L1[λx. λx. x] = L0[λ λ 0] := ⊢ (lam "x" (lam "x" (var "x"))).toL0 = (L0.var 0).lam.lam All goals completed! 🐙example : L1.toL0 L1[x] = L0[x] := ⊢ (var "x").toL0 = L0.free "x" All goals completed! 🐙example : L1[λx. x] =α₁ L1[λy. y] := ⊢ lam "x" (var "x") =α₁ lam "y" (var "y") All goals completed! 🐙example : L1[(λx. x) (λy. y)] →β₁ L1[λz. z] := ⊢ (lam "x" (var "x")).app (lam "y" (var "y")) →β₁ lam "z" (var "z") All goals completed! 🐙example : L1[(λx. x) (λy. y)] →β₁* L1[λz. z] := ⊢ (lam "x" (var "x")).app (lam "y" (var "y")) →β₁* lam "z" (var "z") All goals completed! 🐙example : L1.NormalForm I := ⊢ I.NormalForm All goals completed! 🐙example : L1.NormalForm T := ⊢ T.NormalForm All goals completed! 🐙example : L1.NormalForm F := ⊢ F.NormalForm All goals completed! 🐙example : L1.NormalForm N := ⊢ N.NormalForm All goals completed! 🐙example : L1.NormalForm N' := ⊢ N'.NormalForm All goals completed! 🐙example : L1.NormalForm A := ⊢ A.NormalForm All goals completed! 🐙example : L1.NormalForm M := ⊢ M.NormalForm All goals completed! 🐙example : L1[{I} x] →β₁ L1[x] := ⊢ I.app (var "x") →β₁ var "x" All goals completed! 🐙example : L1[{I} x] →β₁* L1[x] := ⊢ I.app (var "x") →β₁* var "x" rt_step { All goals completed! 🐙 }example : L1[{T} x y] →β₁* L1[x] := ⊢ (T.app (var "x")).app (var "y") →β₁* var "x" All goals completed! 🐙example : L1[{F} x y] →β₁* L1[y] := ⊢ (F.app (var "x")).app (var "y") →β₁* var "y" All goals completed! 🐙example : L1[{N} {F}] →β₁* L1[{T}] := ⊢ N.app F →β₁* T calc
_ = L1[{N} {F}] := ⊢ N.app F = N.app F All goals completed! 🐙
_ = L1[(λb. b {F} {T}) {F}] := ⊢ N.app F = (lam "b" (((var "b").app F).app T)).app F All goals completed! 🐙
_ →β₁ L1[{F} {F} {T}] := ⊢ (lam "b" (((var "b").app F).app T)).app F →β₁ (F.app F).app T All goals completed! 🐙
_ = L1[(λx. λy. y) {F} {T}] := ⊢ (F.app F).app T = ((lam "x" (lam "y" (var "y"))).app F).app T All goals completed! 🐙
_ →β₁ L1[(λy. y) {T}] := ⊢ ((lam "x" (lam "y" (var "y"))).app F).app T →β₁ (lam "y" (var "y")).app T All goals completed! 🐙
_ →β₁ L1[{T}] := ⊢ (lam "y" (var "y")).app T →β₁ T All goals completed! 🐙example : L1[{N} {T}] →β₁* L1[{F}] := ⊢ N.app T →β₁* F calc
_ = L1[{N} {T}] := ⊢ N.app T = N.app T All goals completed! 🐙
_ = L1[(λb. b {F} {T}) {T}] := ⊢ N.app T = (lam "b" (((var "b").app F).app T)).app T All goals completed! 🐙
_ →β₁ L1[{T} {F} {T}] := ⊢ (lam "b" (((var "b").app F).app T)).app T →β₁ (T.app F).app T All goals completed! 🐙
_ = L1[(λx. λy. x) {F} {T}] := ⊢ (T.app F).app T = ((lam "x" (lam "y" (var "x"))).app F).app T All goals completed! 🐙
_ →β₁ L1[(λy. {F}) {T}] := ⊢ ((lam "x" (lam "y" (var "x"))).app F).app T →β₁ (lam "y" F).app T All goals completed! 🐙
_ →β₁ L1[{F}] := ⊢ (lam "y" F).app T →β₁ F All goals completed! 🐙example : L1[{N} {F}] →β₁* L1[{T}] := ⊢ N.app F →β₁* T calc
_ = L1[{N} {F}] := ⊢ N.app F = N.app F All goals completed! 🐙
_ = L1[(λb. b {F} {T}) {F}] := ⊢ N.app F = (lam "b" (((var "b").app F).app T)).app F All goals completed! 🐙
_ →β₁ L1[{F} {F} {T}] := ⊢ (lam "b" (((var "b").app F).app T)).app F →β₁ (F.app F).app T All goals completed! 🐙
_ = L1[(λx. λy. y) {F} {T}] := ⊢ (F.app F).app T = ((lam "x" (lam "y" (var "y"))).app F).app T All goals completed! 🐙
_ →β₁ L1[(λy. y) {T}] := ⊢ ((lam "x" (lam "y" (var "y"))).app F).app T →β₁ (lam "y" (var "y")).app T All goals completed! 🐙
_ →β₁ L1[{T}] := ⊢ (lam "y" (var "y")).app T →β₁ T All goals completed! 🐙example : L1[{N'} {T}] →β₁* L1[{F}] := ⊢ N'.app T →β₁* F All goals completed! 🐙example : L1[{N'} {F}] →β₁* L1[{T}] := ⊢ N'.app F →β₁* T All goals completed! 🐙example : L1[{N} {T}] →β₁* L1[{F}] := ⊢ N.app T →β₁* F All goals completed! 🐙example : L1[{N} {F}] →β₁* L1[{T}] := ⊢ N.app F →β₁* T All goals completed! 🐙example : L1[{N'} {T}] →β₁* L1[{F}] := ⊢ N'.app T →β₁* F All goals completed! 🐙example : L1[{N'} {F}] →β₁* L1[{T}] := ⊢ N'.app F →β₁* T All goals completed! 🐙example : L1[{A} {T} {T}] →β₁* L1[{T}] := ⊢ (A.app T).app T →β₁* T All goals completed! 🐙example : L1[{A} {T} {F}] →β₁* L1[{F}] := ⊢ (A.app T).app F →β₁* F All goals completed! 🐙example : L1[{A} {F} {T}] →β₁* L1[{F}] := ⊢ (A.app F).app T →β₁* F All goals completed! 🐙example : L1[{A} {F} {F}] →β₁* L1[{F}] := ⊢ (A.app F).app F →β₁* F All goals completed! 🐙example : L1[(λx. x) y] ⟶₁ L1[y] := ⊢ (lam "x" (var "x")).app (var "y") ⟶₁ var "y"
⊢ SubstIn [] "x" (var "y") (var "x") (var "y")
All goals completed! 🐙example : L1[(λx. x) y] ⟶₁* L1[y] := ⊢ (lam "x" (var "x")).app (var "y") ⟶₁* var "y"
rt_step {
⊢ SubstIn [] "x" (var "y") (var "x") (var "y")
All goals completed! 🐙
}example : Normal L1[λx. x] := ⊢ (lam "x" (var "x")).Normal
⊢ (var "x").Normal
⊢ (var "x").Neutral
All goals completed! 🐙example : Neutral L1[x y] := ⊢ ((var "x").app (var "y")).Neutral
⊢ (var "x").Neutral⊢ (var "y").Normal
⊢ (var "x").Neutral All goals completed! 🐙
⊢ (var "y").Normal ⊢ (var "y").Neutral
All goals completed! 🐙end L1