Nuprl - Proof: hless def 1

(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

1. m :

2. n :

(m<

n) = (

P:

. ((

n:

. (P(n+1))

(P(n)))

(P(m))

P(n)))

By:	Simpsetp [`bequal`] THEN StrongAuto

Generated subgoals:

1 3. m<n
  P:(). (n:. P(n+1)  P(n)) & P(m) & P(n)
1 step

2 3. P:(). (n:. P(n+1)  P(n)) & P(m) & P(n)
  m<n
20 steps

About:

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

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