(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
  all
  (m:hnum. all
  (m:hnum. (n:hnum. equal
  (m:hnum. (n:hnum. (lt(m,n)
  (m:hnum. (n:hnum. ,exists
  (m:hnum. (n:hnum. ,(P:hnum  hbool. and
  (m:hnum. (n:hnum. ,(P:hnum  hbool. (all
  (m:hnum. (n:hnum. ,(P:hnum  hbool. ((n:hnum. implies(P(suc(n)),P(n)))
  (m:hnum. (n:hnum. ,(P:hnum  hbool. ,and(P(m),not(P(n))))))))
By: HN THEN StrongAuto

Generated subgoal:

1 1. m : 
2. n : 
  (m<n) = (P:. ((n:. (P(n+1))(P(n)))(P(m))P(n)))
22 steps

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

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