---

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


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) ∈ ℕ)
7. i : ℕn
8. ¬i < n - 1
9. i = (n - 1) ∈ ℤ
⊢ primrec(n - 1;[];λi,r. (r @ [f1 i])) @ [f1 (n - 1)][n - 1] = (f1 (n - 1)) ∈ ℕ
BY
{ (RWO "select_append_back" 0 THENA Auto) }

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) ∈ ℕ)
7. i : ℕn
8. ¬i < n - 1
9. i = (n - 1) ∈ ℤ
⊢ [f1 (n - 1)][n - 1 - ||primrec(n - 1;[];λi,r. (r @ [f1 i]))||] = (f1 (n - 1)) ∈ ℕ

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  n  \mneq{}  0
3.  0  <  n
4.  f1  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}
5.  ||primrec(n  -  1;[];\mlambda{}i,r.  (r  @  [f1  i]))||  =  (n  -  1)
6.  \mforall{}i:\mBbbN{}n  -  1.  (primrec(n  -  1;[];\mlambda{}i,r.  (r  @  [f1  i]))[i]  =  (f1  i))
7.  i  :  \mBbbN{}n
8.  \mneg{}i  <  n  -  1
9.  i  =  (n  -  1)
\mvdash{}  primrec(n  -  1;[];\mlambda{}i,r.  (r  @  [f1  i]))  @  [f1  (n  -  1)][n  -  1]  =  (f1  (n  -  1))


By

---

Latex:
(RWO  "select\_append\_back"  0  THENA  Auto)

---

Home Index