Nuprl - Proof: search property 2 1 2

(21steps total) PrintForm Definitions mb nat Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: search property 2 1 2

1. k :

2. 0<k
3.

P:(

(k-1)

).
3. ((

i:

(k-1). P(i))

0<search(k-1;P))
3. & (0<search(k-1;P)
3. & (

3. & (P(search(k-1;P)-1) & (

j:

(k-1). j<search(k-1;P)-1

P(j)))
4. P :

k

5. ((

i:

(k-1). P(i))

0<search(k-1;P))
5. & (0<search(k-1;P)
5. & (

5. & (P(search(k-1;P)-1) & (

j:

(k-1). j<search(k-1;P)-1

P(j)))
6.

(

i:

(k-1). P(i))

((

i:

k. P(i))

0<search(k;P))

& (0<search(k;P)

P(search(k;P)-1) & (

j:

k. j<search(k;P)-1

P(j)))

By:	AssertBY (0<search(k-1;P)) (ParallelOp -1 THEN EasyHyp) THEN Decide (P(k-1))

Generated subgoals:

1 7. 0<search(k-1;P)
8. P(k-1)
  ((i:k. P(i))  0<search(k;P))
  & (0<search(k;P)  P(search(k;P)-1) & (j:k. j<search(k;P)-1  P(j)))
5 steps

2 7. 0<search(k-1;P)
8. P(k-1)
  ((i:k. P(i))  0<search(k;P))
  & (0<search(k;P)  P(search(k;P)-1) & (j:k. j<search(k;P)-1  P(j)))
5 steps

About:

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

(21steps total) PrintForm Definitions mb nat Sections MarkB generic Doc