---

Step * 2 1 1 of Lemma coded-code-seq1


1. k : ℤ@i
2. ¬k + 1 < 1
3. (k + 1) - 1 ≠ 0
4. 0 < k
5. ∀s:ℕk ⟶ ℕ. ∀[n:ℕk]. (coded-seq1(k - 1;code-seq1(k;s);n) = (s n) ∈ ℤ)
6. s : ℕk + 1 ⟶ ℕ@i
7. n : ℕk + 1
⊢ let y,m = coded-pair(code-pair(code-seq1((k + 1) - 1;s);s ((k + 1) - 1))) 
  in if (n =z (k + 1) - 1) then m else coded-seq1((k + 1) - 1 - 1;y;n) fi 
= (s n)
∈ ℤ
BY
{ ((RWO "coded-code-pair" 0 THENA Auto) THEN Reduce 0 THEN AutoSplit) }

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}@i
2.  \mneg{}k  +  1  <  1
3.  (k  +  1)  -  1  \mneq{}  0
4.  0  <  k
5.  \mforall{}s:\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}.  \mforall{}[n:\mBbbN{}k].  (coded-seq1(k  -  1;code-seq1(k;s);n)  =  (s  n))
6.  s  :  \mBbbN{}k  +  1  {}\mrightarrow{}  \mBbbN{}@i
7.  n  :  \mBbbN{}k  +  1
\mvdash{}  let  y,m  =  coded-pair(code-pair(code-seq1((k  +  1)  -  1;s);s  ((k  +  1)  -  1))) 
    in  if  (n  =\msubz{}  (k  +  1)  -  1)  then  m  else  coded-seq1((k  +  1)  -  1  -  1;y;n)  fi 
=  (s  n)


By

---

Latex:
((RWO  "coded-code-pair"  0  THENA  Auto)  THEN  Reduce  0  THEN  AutoSplit)

---

Home Index