IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
split factor1 wf111 1. k : {2...}
2. g : {2..k} 3. x : {2..k}
4. xx<k 5. x<xx & x<xx 6. u : {2..k}
if u=xg(x)+g(xx)+g(xx) ; u=xx 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
}
x<k
if u=
x
g(x)+g(x
