(4steps 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 wf 1
1. k : {2...}
2. g : {2..k}
3. x : {2..k}
4. xx<k
  split_factor1(g; x)  {2..k}
By: Inst: Thm*  i,j:{2...}. i<ij & j<ij Using:[x | x] ...w

Generated subgoal:

1 5. x<xx & x<xx
  split_factor1(g; x)  {2..k}
2 steps

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

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