(8steps total) PrintForm Definitions Lemmas NuprlPrimitives Sections NuprlLIB Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc ycomb factorial typing 1
  Y(f,x. if x=0 1 else xf(x-1) fi)  VoidVoid
By: Compute
CoY(f,x. if x=0 1 else xf(x-1) fi)
Co*
Cox.if x=0 1
Cox.else x(x.(f,x. if x=0 1 else xf(x-1) fi)(x(x)))
Cox.else x((x.(f,x. if x=0 1 else xf(x-1) fi)(x(x)))
Cox.else x,x-1) fi

Generated subgoals:

None

About:
ifthenelsevoidnatural_numbersubtractmultiply
lambdaapplyfunctionycombmembermarked_clause_thenmarkup_tag
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

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