2. L : T List
3. P : T
TProp
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. L' : T List
9. guarded_permutation(T;
L,i. Q(L[i],L[(i+1)]))(L,L')
(swap adjacent[P(x,y)]^*)(L,L')TProp
x,y:T. Dec(P(x,y))
x,y:T. P(x,y) P(y,x)
T
x,y:T. Q(x,y) P(x,y)
L,i. Q(L[i],L[(i+1)]))(L,L')
(swap adjacent[P(x,y)]^*)(L,L')| By: |
h.Unfold `guarded_permutation` h)
THEN BackThruLemma' Thm* R1,R2:(TTProp), x,y:T. R1 => R2 (x (R1^*) y) (x (R2^*) y)
THEN Reduce 0 THEN Unfold `rel_implies` 0 THEN Reduce 0 |
| 1 |
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 | 1 step |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |