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


1. : ℤ
2. n ≠ 0
3. 0 < n
4. f1 : ℕn ⟶ ℕ
5. ||primrec(n 1;[];λi,r. (r [f1 i]))|| (n 1) ∈ ℕ
6. ∀i:ℕ1. (primrec(n 1;[];λi,r. (r [f1 i]))[i] (f1 i) ∈ ℕ)
⊢ ∀i:ℕn. (primrec(n 1;[];λi,r. (r [f1 i])) [f1 (n 1)][i] (f1 i) ∈ ℕ)
BY
((D THENA Auto) THEN (Decide ⌜i < 1⌝⋅ THENA Auto)) }

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

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


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))
\mvdash{}  \mforall{}i:\mBbbN{}n.  (primrec(n  -  1;[];\mlambda{}i,r.  (r  @  [f1  i]))  @  [f1  (n  -  1)][i]  =  (f1  i))


By


Latex:
((D  0  THENA  Auto)  THEN  (Decide  \mkleeneopen{}i  <  n  -  1\mkleeneclose{}\mcdot{}  THENA  Auto))




Home Index