Nuprl - Proof: induction

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: induction

P:(

). P(0) & (

. P(n)

P(n+1))

(

. P(n))

By:	RewriteOfThm Thm* all Thm* (P:hnum hbool. implies Thm* (P:hnum hbool. (and(P(0),all(n:hnum. implies(P(n),P(suc(n))))) Thm* (P:hnum hbool. ,all(n:hnum. P(n)))) HNC

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html