(17steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: split factor2 char 1 1 a 2

1. k : {2...}
2. g : {2..k}
3. x : {2..k}
4. y : {2..k}
5. xy<k
6. x<y
7. x<xy
8. y<xy
9. h : {2..k}
10. h = split_factor2(gxy)
11. h(xy) = 0
12. h(x) = g(x)+g(xy)
13. h(y) = g(y)+g(xy)
14. u:{2..k}. u = x  u = y  u = xy  h(u) = g(u)
  {x+1..y}(g) = {x+1..y}(h)


By: Analyze ... THEN New:u FunExtensionality THEN BackThru: Hyp:14 ...


Generated subgoals:

None

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

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