---

Step * 1 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. ((-1) + k) = v1 ∈ ℕ
7. code-seq1(k;s) = v2 ∈ ℕ
8. x : ℕv1 + 1
⊢ coded-seq1(v1;code-seq1(k;s);x) = (s x) ∈ ℕ
BY
{ TACTIC:(Subst ⌜v1 ~ k - 1⌝ 0⋅ THENA Auto) }

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(k - 1;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.  ((-1)  +  k)  =  v1
7.  code-seq1(k;s)  =  v2
8.  x  :  \mBbbN{}v1  +  1
\mvdash{}  coded-seq1(v1;code-seq1(k;s);x)  =  (s  x)


By

---

Latex:
TACTIC:(Subst  \mkleeneopen{}v1  \msim{}  k  -  1\mkleeneclose{}  0\mcdot{}  THENA  Auto)

---

Home Index