---

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


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) ∈ ℕ))
BY
{ ((InstHyp [⌜f1⌝] (-2)⋅ THENA Auto) THEN Thin (-3) THEN RepD THEN (RWO "primrec-unroll" 0 THENA Auto) THEN AutoSplit) }

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

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}f1:\mBbbN{}n  -  1  {}\mrightarrow{}  \mBbbN{}
          ((||primrec(n  -  1;[];\mlambda{}i,r.  (r  @  [f1  i]))||  =  (n  -  1))
          \mwedge{}  (\mforall{}i:\mBbbN{}n  -  1.  (primrec(n  -  1;[];\mlambda{}i,r.  (r  @  [f1  i]))[i]  =  (f1  i))))
4.  f1  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}
\mvdash{}  (||primrec(n;[];\mlambda{}i,r.  (r  @  [f1  i]))||  =  n)  \mwedge{}  (\mforall{}i:\mBbbN{}n.  (primrec(n;[];\mlambda{}i,r.  (r  @  [f1  i]))[i]  =  (f1  i)\000C))


By

---

Latex:
((InstHyp  [\mkleeneopen{}f1\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  Thin  (-3)
  THEN  RepD
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index