---

Step * 2 of Lemma coded-code-seq1


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

1
1. k : ℤ@i
2. (k + 1) - 1 ≠ 0
3. 0 < k
4. ∀s:ℕk ⟶ ℕ. ∀[n:ℕk]. (coded-seq1(k - 1;code-seq1(k;s);n) = (s n) ∈ ℤ)
5. s : ℕk + 1 ⟶ ℕ@i
6. n : ℕk + 1
⊢ let y,m = coded-pair(code-seq1(k + 1;s)) 
  in if (n =z (k + 1) - 1) then m else coded-seq1((k + 1) - 1 - 1;y;n) fi 
= (s n)
∈ ℤ

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:AutoSplit

---

Home Index