Step * 2 1 of Lemma coded-code-seq1


1. : ℤ
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. : ℕ1 ⟶ ℕ
6. : ℕ1
⊢ let y,m coded-pair(code-seq1(k 1;s)) 
  in if (n =z (k 1) 1) then else coded-seq1((k 1) 1;y;n) fi 
(s n)
∈ ℤ
BY
xxx(Unfold `code-seq1` THEN (RWO "primrec-unroll" THENA Auto) THEN Fold `code-seq1` THEN AutoSplit)xxx }

1
1. : ℤ
2. ¬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. : ℕ1 ⟶ ℕ
7. : ℕ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 else coded-seq1((k 1) 1;y;n) fi 
(s n)
∈ ℤ


Latex:


Latex:

1.  k  :  \mBbbZ{}
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{}
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:
xxx(Unfold  `code-seq1`  0
        THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
        THEN  Fold  `code-seq1`  0
        THEN  AutoSplit)xxx




Home Index