Nuprl Basics - Proof: sfa doc ycomb factorial typing 2 1 1 1 2

(8steps total) PrintForm Definitions Lemmas NuprlPrimitives Sections NuprlLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc ycomb factorial typing 2 1 1 1 2

1. x :

2.

x1:

. x1<x

Y((

f,x. if x=

0

1 else x

f(x-1) fi),x1)

3.

x = 0

Y((

f,x. if x=

0

1 else x

f(x-1) fi),x-1)

By:	BackThru: Hyp:2

Generated subgoals:

None

About:

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

(8steps total) PrintForm Definitions Lemmas NuprlPrimitives Sections NuprlLIB Doc