(16steps 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 char a 1 1 1

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(gx)
9. h(xx) = 0
10. h(x) = g(x)+g(xx)+g(xx)
11. u:{2..k}. u = x  u = xx  h(u) = g(u)
  {2..k}(g) = {2..k}(h)


By: <Unproved Leaf>


Generated subgoals:

None

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

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