---

Step * of Lemma code-coded-seq

∀x:ℕ. (let k,s = coded-seq(x) in code-seq(k;s) = x ∈ ℤ)
BY
{ xxx(Auto THEN Unfold `coded-seq` 0 THEN AutoSplit)xxx }

1
1. x : ℕ
2. x = 0 ∈ ℤ
⊢ code-seq(0;λx.x) = x ∈ ℤ

2
1. x : {1...}
⊢ let k,s = let a,b = coded-pair(x - 1) in <a + 1, λn.coded-seq1(a;b;n)> in code-seq(k;s) = x ∈ ℤ

---

Latex:

---

Latex:
\mforall{}x:\mBbbN{}.  (let  k,s  =  coded-seq(x)  in  code-seq(k;s)  =  x)


By

---

Latex:
xxx(Auto  THEN  Unfold  `coded-seq`  0  THEN  AutoSplit)xxx

---

Home Index