(23steps total) PrintForm Definitions hol prim rec Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hless def 1 2 1
1. m : 
2. n : 
3. P : 
4. n:. P(n+1)  P(n)
5. P(m)
6. P(n)
  m<n
By: Case (m<n  m = n  m>n) THEN StrongAuto

Generated subgoals:

1 7. m<n
8. m = n
  m>n
1 step
2 7. m = n
  m<n
1 step
3 7. m>n
  m<n
16 steps

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

(23steps total) PrintForm Definitions hol prim rec Sections HOLlib Doc