Def exists == p:'a. x:'a. (p(x))

is mentioned by

Thm* all Thm* (k:hnum. all Thm* (k:hnum. (n:hnum. implies Thm* (k:hnum. (n:hnum. (lt(0,n) Thm* (k:hnum. (n:hnum. ,exists Thm* (k:hnum. (n:hnum. ,(r:hnum. exists Thm* (k:hnum. (n:hnum. ,(r:hnum. (q:hnum. and Thm* (k:hnum. (n:hnum. ,(r:hnum. (q:hnum. (equal(k,add(mult(q,n),r)) Thm* (k:hnum. (n:hnum. ,(r:hnum. (q:hnum. ,lt(r,n)))))))	[hda]
Thm* all Thm* (P:hnum  hbool. implies Thm* (P:hnum  hbool. (exists(n:hnum. P(n)) Thm* (P:hnum  hbool. ,exists Thm* (P:hnum  hbool. ,(n:hnum. and Thm* (P:hnum  hbool. ,(n:hnum. (P(n) Thm* (P:hnum  hbool. ,(n:hnum. ,all(m:hnum. implies(lt(m,n),not(P(m))))))))	[hwop]
Thm* all(n:hnum. all(m:hnum. or(lt(n,m),exists(p:hnum. equal(n,add(p,m))))))	[hless_or_eq_add]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. implies Thm* (m:hnum. (n:hnum. (lt(n,m) Thm* (m:hnum. (n:hnum. ,exists(p:hnum. equal(m,add(n,add(p,1)))))))	[hless_add_1]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. implies(lt(n,m),exists(p:hnum. equal(add(p,n),m)))))	[hless_add]
Thm* all(m:hnum. or(equal(m,0),exists(n:hnum. equal(m,suc(n)))))	[hnum_cases]

In prior sections: hol bool hol num hol prim rec

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html