Step
*
2
1
1
2
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
⊢ primrec(n - 1;[];λi,r. (r @ [f1 i])) @ [f1 (n - 1)][i] = (f1 i) ∈ ℕ
BY
{ ((Assert ⌜i = (n - 1) ∈ ℤ⌝⋅ THENA Auto) THEN (Subst ⌜i ~ n - 1⌝ 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) ∈ ℤ
⊢ primrec(n - 1;[];λi,r. (r @ [f1 i])) @ [f1 (n - 1)][n - 1] = (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
\mvdash{} primrec(n - 1;[];\mlambda{}i,r. (r @ [f1 i])) @ [f1 (n - 1)][i] = (f1 i)
By
Latex:
((Assert \mkleeneopen{}i = (n - 1)\mkleeneclose{}\mcdot{} THENA Auto) THEN (Subst \mkleeneopen{}i \msim{} n - 1\mkleeneclose{} 0\mcdot{} THENA Auto))
Home
Index