IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
split factor1 chara111 1. k : {2...}
2. g : {2..k}
3. x : {2..k}
4. xx<k 5. x<xx 6. x<xx 7. h : {2..k}
8. h = split_factor1(g; x)
9. h(xx) = 0
10. h(x) = g(x)+g(xx)+g(xx)
11. u:{2..k}. u = xu = xxh(u) = g(u)
{2..k}(g) = {2..k}(h)
By:
<Unproved Leaf>
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html