---

Step * of Lemma coded-code-seq

∀k:ℕ. ∀s:ℕk ⟶ ℕ.  (coded-seq(code-seq(k;s)) = <k, s> ∈ (k:ℕ × (ℕk ⟶ ℕ)))
BY
{ (Auto
   THEN Unfolds ``coded-seq code-seq`` 0
   THEN AutoSplit
   THEN Try ((EqCD THEN Auto))
   THEN AutoSplit
   THEN Auto'
   THEN (GenConclTerm ⌜coded-pair((code-pair(k - 1;code-seq1(k;s)) + 1) - 1)⌝⋅ THENM (D -2 THEN Reduce 0))
   THEN Auto
   THEN (RW IntNormC (-1) THENA Auto)) }

1
1. k : {1...}
2. s : ℕk ⟶ ℕ
3. code-pair(k - 1;code-seq1(k;s)) + 1 ≠ 0
4. v1 : ℕ
5. v2 : ℕ
6. coded-pair(code-pair((-1) + k;code-seq1(k;s))) = <v1, v2> ∈ (ℕ × ℕ)
⊢ <v1 + 1, λn.coded-seq1(v1;v2;n)> = <k, s> ∈ (k:ℕ × (ℕk ⟶ ℕ))

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}s:\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}.    (coded-seq(code-seq(k;s))  =  <k,  s>)


By

---

Latex:
(Auto
  THEN  Unfolds  ``coded-seq  code-seq``  0
  THEN  AutoSplit
  THEN  Try  ((EqCD  THEN  Auto))
  THEN  AutoSplit
  THEN  Auto'
  THEN  (GenConclTerm  \mkleeneopen{}coded-pair((code-pair(k  -  1;code-seq1(k;s))  +  1)  -  1)\mkleeneclose{}\mcdot{}
  THENM  (D  -2  THEN  Reduce  0)
  )
  THEN  Auto
  THEN  (RW  IntNormC  (-1)  THENA  Auto))

---

Home Index