---

Step * of Lemma code-coded-seq1

∀[k:ℕ+]. ∀[x:ℕ].  (code-seq1(k;λn.coded-seq1(k - 1;x;n)) = x ∈ ℤ)
BY
{ xxx(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)xxx }

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

---

Latex:

---

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


By

---

Latex:
xxx(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)xxx

---

Home Index