---

Step * 2 of Lemma code-coded-seq


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 ∈ ℤ
BY
{ xxx((GenConclTerm ⌜coded-pair(x - 1)⌝⋅ THENA Auto) THEN D -2 THEN Reduce 0)xxx }

1
1. x : {1...}
2. v1 : ℕ
3. v2 : ℕ
4. coded-pair(x - 1) = <v1, v2> ∈ (ℕ × ℕ)
⊢ code-seq(v1 + 1;λn.coded-seq1(v1;v2;n)) = x ∈ ℤ

---

Latex:

---

Latex:

1.  x  :  \{1...\}
\mvdash{}  let  k,s  =  let  a,b  =  coded-pair(x  -  1)  in  <a  +  1,  \mlambda{}n.coded-seq1(a;b;n)>  in  code-seq(k;s)  =  x


By

---

Latex:
xxx((GenConclTerm  \mkleeneopen{}coded-pair(x  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  Reduce  0)xxx

---

Home Index