---

Step * 1 of Lemma code-coded-seq1


1. k : ℤ@i
2. k ≠ 0
3. 0 < k
4. ∀[x:ℕ]. (code-seq1(k;λn.coded-seq1(k - 1;x;n)) = x ∈ ℤ)
5. x : ℕ
6. v1 : ℕ@i
7. v2 : ℕ@i
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
{ TACTIC:(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)) }

1
1. k : ℤ@i
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 : ℕ@i
8. v2 : ℕ@i
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{}@i
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{}@i
7.  v2  :  \mBbbN{}@i
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:
TACTIC:(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))

---

Home Index