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

(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. x :

2.

x1:

. x1<x

Y((

f,x. if x=

0

1 else x

f(x-1) fi),x1)

if x=

0

1 else x

Y((

f,x. if x=

0

1 else x

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

By:	SplitOnConclITE

Generated subgoal:

1 3. x = 0
xY((f,x. if x=0 1 else xf(x-1) fi),x-1)
3 steps

About:

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

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