Nuprl - Proof: partial sort exists 2 1 1

(8steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: partial sort exists 2 1 1

1. T : Type
2. T List
3. P : T

T

4.

x,y:T. P(x,y)

P(y,x)
5. L1 : T List
6. i :

(||L1||-1)
7. P(L1[i],L1[(i+1)])

P(swap(L1;i;i+1)[i],swap(L1;i;i+1)[(i+1)])

By:	RWO Thm* L:T List, i,j,x:\|\|L\|\|. swap(L;i;j)[x] = L[((i, j)(x))] 0 THEN Unfold `flip` 0 THEN Reduce 0 THEN Repeat SplitOnConclITE

Generated subgoal:

1 8. i = i
9. i+1 = i
10. i+1 = i+1
P(L1[(i+1)],L1[i])
1 step

About:

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

(8steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc