---

Step * of Lemma code-coded-seq

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

1
1. x : ℕ@i
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:
TACTIC:(Auto  THEN  Unfold  `coded-seq`  0  THEN  AutoSplit)

---

Home Index