(7steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: prime divs exp 1 2
1. p : 
2. prime(p)
3. b : 
4. z : 
5. p | zb
6. b  0
  p | z
By: Auto
THEN
Inst: 
Thm*  p:. 
Thm*  prime(p)
Thm*  
Thm*  (a,b:, e:({a..b}).
Thm*  (a<b  p | ( i:{a..b}. e(i))  (i:{a..b}. p | e(i)))
Using:[p | 0 | b | e(i):= z] ...

Generated subgoal:

1 7. i:b. p | z
  p | z
1 step

About:
intnatural_numbermultiplyless_thanlambdafunctionimpliesallexists
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

(7steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Search Doc