Nuprl - Proof: hless def 1 2 1 3 1 1 2 2 2

(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 3 1 1 2 2 2

1. m :

2. n :

3. P :

4.

n:

. P(n+1)

P(n)
5. P(m)
6.

P(n)
7. m>n
8. k :

9. 0<k
10. 0

n+k-1

P(n+k-1)

P(n)
11. 0

n+k
12. P(n+k)

P(n+k-1)

By:	InstHyp [n+k-1] 4 THEN StrongAuto

Generated subgoals:

1 0n+k-1
1 step

2 P(n+k-1+1)
1 step

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