Step
*
1
of Lemma
primrec-induction
1. [P] : ℕ ⟶ ℙ
2. b : P[0]
3. f : ∀n:ℕ. (P[n]
⇒ P[n + 1])
4. n : ℕ
⊢ P[n]
BY
{ UseWitness ⌜primrec(n;b;f)⌝⋅ }
1
1. P : ℕ ⟶ ℙ
2. b : P[0]
3. f : ∀n:ℕ. (P[n]
⇒ P[n + 1])
4. n : ℕ
⊢ primrec(n;b;f) ∈ P[n]
Latex:
Latex:
1. [P] : \mBbbN{} {}\mrightarrow{} \mBbbP{}
2. b : P[0]
3. f : \mforall{}n:\mBbbN{}. (P[n] {}\mRightarrow{} P[n + 1])
4. n : \mBbbN{}
\mvdash{} P[n]
By
Latex:
UseWitness \mkleeneopen{}primrec(n;b;f)\mkleeneclose{}\mcdot{}
Home
Index