Nuprl - Proof: partial sort 2 2 1 1

(10steps 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 2 2 1 1

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

T

Prop
4.

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

x,y:T.

P(x,y)

P(y,x)
6. Q : T

T

7.

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

P(x,y)
8. T List
9. x : T List
10. y : T List
11.

i:

(||x||-1). Q(x[i],x[(i+1)]) & y = swap(x;i;i+1)

x swap adjacent[

P(x,y)] y

By:	Unfold `swap_adjacent` 0 THEN Reduce 0 THEN ParallelOp -1 THEN EasyHyp

Generated subgoals:

None

About:

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

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