---

Step * of Lemma test-nat-bootstrap

P:  . b:P 0. c:n:  P n  (P (n + 1)). n:.  ((n.primrec(n;b;c)) n  P n)
BY
{ (UnivCD THENA Auto) }

1
1. P :   @i'
2. b : P 0@i
3. c : n:  P n  (P (n + 1))@i
4. n : @i
 (n.primrec(n;b;c)) n  P n


\mforall{}P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}.  \mforall{}b:P  0.  \mforall{}c:n:\mBbbN{}  {}\mrightarrow{}  P  n  {}\mrightarrow{}  (P  (n  +  1)).  \mforall{}n:\mBbbN{}.    ((\mlambda{}n.primrec(n;b;c))  n  \mmember{}  P  n)


By

(UnivCD  THENA  Auto)



Home Index