Nuprl - Proof: partial sort 2

(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

1. T : Type
2. L : 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

).

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

P(x,y)

L':T List.

(L (swap adjacent[

P(x,y)]^*) L') & (

i:

(||L'||-1). P(L'[i],L'[(i+1)]))

By:	ExRepD THEN Inst Thm: partial sort exists 2 [T;L;Q]

Generated subgoals:

1 6. Q : TT
7. x,y:T. Q(x,y)  P(x,y)
8. x : T
9. y : T
10. Q(x,y)
  Q(y,x)
2 steps

2 6. Q : TT
7. x,y:T. Q(x,y)  P(x,y)
8. L':T List.
8. (L guarded_permutation(T;L,i. Q(L[i],L[(i+1)])) L')
8. & (i:(||L'||-1). Q(L'[i],L'[(i+1)]))
  L':T List.
  (L (swap adjacent[P(x,y)]^*) L') & (i:(||L'||-1). P(L'[i],L'[(i+1)]))
5 steps

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