Nuprl - Proof: search property 2 1 2 1 1

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

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)
6. (

i:

(k-1). P(i))

(0<search(k-1;P))
7. 0<search(k-1;P)
7.

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

j:

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

P(j))
8.

(

i:

(k-1). P(i))
9.

0<search(k-1;P)
10. P(k-1)

search(k;P) = k

By:	Unfold `search` 0 THEN RecUnfold `primrec` 0 THEN Reduce 0 THEN Fold `search` 0 THEN Repeat SplitOnConclITE

Generated subgoals:

None

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