---

Step * of Lemma code-coded-seq1

∀[k:ℕ+]. ∀[x:ℕ].  (code-seq1(k;λn.coded-seq1(k - 1;x;n)) = x ∈ ℤ)
BY
{ TACTIC:(InductionOnNat
          THEN Auto
          THEN (Subst' (k + 1) - 1 ~ k 0 THENA Auto)
          THEN RecUnfold `coded-seq1` 0
          THEN AutoSplit
          THEN (GenConclTerm ⌜coded-pair(x)⌝⋅ THENA Auto)
          THEN D -2
          THEN Reduce 0) }

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

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[x:\mBbbN{}].    (code-seq1(k;\mlambda{}n.coded-seq1(k  -  1;x;n))  =  x)


By

---

Latex:
TACTIC:(InductionOnNat
                THEN  Auto
                THEN  (Subst'  (k  +  1)  -  1  \msim{}  k  0  THENA  Auto)
                THEN  RecUnfold  `coded-seq1`  0
                THEN  AutoSplit
                THEN  (GenConclTerm  \mkleeneopen{}coded-pair(x)\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  D  -2
                THEN  Reduce  0)

---

Home Index