---

Step * 1 of Lemma code-coded-seq1


1. k : ℤ
2. k ≠ 0
3. 0 < k
4. ∀[x:ℕ]. (code-seq1(k;λn.coded-seq1(k - 1;x;n)) = x ∈ ℤ)
5. x : ℕ
6. v1 : ℕ
7. v2 : ℕ
8. coded-pair(x) = <v1, v2> ∈ (ℕ × ℕ)
⊢ code-seq1(k + 1;λn.if (n =z k) then v2 else coded-seq1(k - 1;v1;n) fi ) = x ∈ ℤ
BY
{ xxx(Unfold `code-seq1` 0
      THEN (RWO "primrec-unroll" 0 THENA Auto)
      THEN Fold `code-seq1` 0
      THEN AutoSplit
      THEN (Subst' (k + 1) - 1 ~ k 0 THENA Auto))xxx }

1
1. k : ℤ
2. ¬k + 1 < 1
3. k ≠ 0
4. 0 < k
5. ∀[x:ℕ]. (code-seq1(k;λn.coded-seq1(k - 1;x;n)) = x ∈ ℤ)
6. x : ℕ
7. v1 : ℕ
8. v2 : ℕ
9. coded-pair(x) = <v1, v2> ∈ (ℕ × ℕ)
⊢ code-pair(code-seq1(k;λn.if (n =z k) then v2 else coded-seq1(k - 1;v1;n) fi );v2) = x ∈ ℤ

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  k  \mneq{}  0
3.  0  <  k
4.  \mforall{}[x:\mBbbN{}].  (code-seq1(k;\mlambda{}n.coded-seq1(k  -  1;x;n))  =  x)
5.  x  :  \mBbbN{}
6.  v1  :  \mBbbN{}
7.  v2  :  \mBbbN{}
8.  coded-pair(x)  =  <v1,  v2>
\mvdash{}  code-seq1(k  +  1;\mlambda{}n.if  (n  =\msubz{}  k)  then  v2  else  coded-seq1(k  -  1;v1;n)  fi  )  =  x


By

---

Latex:
xxx(Unfold  `code-seq1`  0
        THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
        THEN  Fold  `code-seq1`  0
        THEN  AutoSplit
        THEN  (Subst'  (k  +  1)  -  1  \msim{}  k  0  THENA  Auto))xxx

---

Home Index