Nuprl Lemma : nat-ind-boot

P:

. (((P 0)

(

n:

. ((P n)

(P (n + 1)))))

(

n:

. (P n)))

Proof

Definitions occuring in Statement : nat:

, prop:

, all:

x:A. B[x], implies: P

Q, and: P

Q, apply: f a, function: x:A

B[x], add: n + m, natural_number: $n
Definitions : all:

x:A. B[x], nat:

, prop:

, implies: P

Q, and: P

Q, member: t

T, le: A

B, not:

A, false: False, so_lambda:

x.t[x], uall:

[x:A]. B[x], so_apply: x[s]
Lemmas : nat_wf, le_wf, all_wf, test-nat-bootstrap
\mforall{}P:\mBbbN{} {}\mrightarrow{} \mBbbP{}. (((P 0) \mwedge{} (\mforall{}n:\mBbbN{}. ((P n) {}\mRightarrow{} (P (n + 1))))) {}\mRightarrow{} (\mforall{}n:\mBbbN{}. (P n))) Date html generated: 2013_03_20-AM-09_46_11 Last ObjectModification: 2012_11_27-AM-10_31_57 Home Index