IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
split factor2 wf111 1. k : {2...}
2. g : {2..k}
3. x : {2..k}
4. y : {2..k}
5. xy<k 6. x<xy & y<xy 7. u : {2..k}
if u=xg(x)+g(xy) ; u=yg(y)+g(xy) ; u=xy 0 else g(u) fi
By:
SplitOnConclITEs ...
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html