---

Step * of Lemma finite-nat-seq-to-list-prop1

∀[f:finite-nat-seq()]
  ((||finite-nat-seq-to-list(f)|| = (fst(f)) ∈ ℕ) ∧ (∀i:ℕfst(f). (finite-nat-seq-to-list(f)[i] = ((snd(f)) i) ∈ ℕ)))
BY
{ ((D 0 THENA Auto)
   THEN (D (-1) THENA Auto)
   THEN RepUR ``finite-nat-seq-to-list`` 0
   THEN (NatInd (-2) THENA Auto)
   THEN (D 0 THENA Auto)
   THEN Reduce 0) }

1
1. n : ℤ
2. f1 : ℕ0 ⟶ ℕ
⊢ (0 = 0 ∈ ℕ) ∧ (∀i:ℕ0. (⊥ = (f1 i) ∈ ℕ))

2
1. n : ℤ
2. 0 < n
3. ∀f1:ℕn - 1 ⟶ ℕ
     ((||primrec(n - 1;[];λi,r. (r @ [f1 i]))|| = (n - 1) ∈ ℕ)
     ∧ (∀i:ℕn - 1. (primrec(n - 1;[];λi,r. (r @ [f1 i]))[i] = (f1 i) ∈ ℕ)))
4. f1 : ℕn ⟶ ℕ
⊢ (||primrec(n;[];λi,r. (r @ [f1 i]))|| = n ∈ ℕ) ∧ (∀i:ℕn. (primrec(n;[];λi,r. (r @ [f1 i]))[i] = (f1 i) ∈ ℕ))

---

Latex:

---

Latex:
\mforall{}[f:finite-nat-seq()]
    ((||finite-nat-seq-to-list(f)||  =  (fst(f)))
    \mwedge{}  (\mforall{}i:\mBbbN{}fst(f).  (finite-nat-seq-to-list(f)[i]  =  ((snd(f))  i))))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (D  (-1)  THENA  Auto)
  THEN  RepUR  ``finite-nat-seq-to-list``  0
  THEN  (NatInd  (-2)  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  Reduce  0)

---

Home Index