---

Step * 1 of Lemma coded-code-seq


1. k : {1...}
2. s : ℕk ⟶ ℕ@i
3. code-pair(k - 1;code-seq1(k;s)) + 1 ≠ 0
4. v1 : ℕ@i
5. v2 : ℕ@i
6. coded-pair(code-pair((-1) + k;code-seq1(k;s))) = <v1, v2> ∈ (ℕ × ℕ)
⊢ <v1 + 1, λn.coded-seq1(v1;v2;n)> = <k, s> ∈ (k:ℕ × (ℕk ⟶ ℕ))
BY
{ TACTIC:(((RWO "coded-code-pair" (-1) THENM EqHD (-1)) THENA Auto)
          THEN All Reduce
          THEN EqCD
          THEN Auto
          THEN Ext
          THEN Reduce 0
          THEN Auto
          THEN RevHypSubst' (-2) 0) }

1
1. k : {1...}
2. s : ℕk ⟶ ℕ@i
3. code-pair(k - 1;code-seq1(k;s)) + 1 ≠ 0
4. v1 : ℕ@i
5. v2 : ℕ@i
6. ((-1) + k) = v1 ∈ ℕ
7. code-seq1(k;s) = v2 ∈ ℕ
8. x : ℕv1 + 1
⊢ coded-seq1(v1;code-seq1(k;s);x) = (s x) ∈ ℕ

---

Latex:

---

Latex:

1.  k  :  \{1...\}
2.  s  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbN{}@i
3.  code-pair(k  -  1;code-seq1(k;s))  +  1  \mneq{}  0
4.  v1  :  \mBbbN{}@i
5.  v2  :  \mBbbN{}@i
6.  coded-pair(code-pair((-1)  +  k;code-seq1(k;s)))  =  <v1,  v2>
\mvdash{}  <v1  +  1,  \mlambda{}n.coded-seq1(v1;v2;n)>  =  <k,  s>


By

---

Latex:
TACTIC:(((RWO  "coded-code-pair"  (-1)  THENM  EqHD  (-1))  THENA  Auto)
                THEN  All  Reduce
                THEN  EqCD
                THEN  Auto
                THEN  Ext
                THEN  Reduce  0
                THEN  Auto
                THEN  RevHypSubst'  (-2)  0)

---

Home Index