(4steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: split factor1 wf 1 1

1. k : {2...}
2. g : {2..k}
3. x : {2..k}
4. xx<k
5. x<xx & x<xx
  split_factor1(gx {2..k}


By: Def THEN New:u FunExtensionality


Generated subgoal:

1 6. u : {2..k}
  if u=x g(x)+g(xx)+g(xx) ; u=xx 0 else g(u) fi  

1 step

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

(4steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc