---

Step * 2 1 of Lemma coded-code-seq1


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)
∈ ℤ
BY
{ TACTIC:(Unfold `code-seq1` 0 THEN (RWO "primrec-unroll" 0 THENA Auto) THEN Fold `code-seq1` 0 THEN AutoSplit) }

1
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)
∈ ℤ

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}@i
2.  (k  +  1)  -  1  \mneq{}  0
3.  0  <  k
4.  \mforall{}s:\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}.  \mforall{}[n:\mBbbN{}k].  (coded-seq1(k  -  1;code-seq1(k;s);n)  =  (s  n))
5.  s  :  \mBbbN{}k  +  1  {}\mrightarrow{}  \mBbbN{}@i
6.  n  :  \mBbbN{}k  +  1
\mvdash{}  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 
=  (s  n)


By

---

Latex:
TACTIC:(Unfold  `code-seq1`  0
                THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
                THEN  Fold  `code-seq1`  0
                THEN  AutoSplit)

---

Home Index