2. L : T List
3. P : T
T
4.
x,y:T. P(x,y) 
P(y,x)
5.
L:T List.
5.
L':T List.
5. (L guarded_permutation(T;
L,i. P(L[i],L[(i+1)])) L')
5. & (
i:
(||L'||-1). P(L'[i],L'[(i+1)]))
L':T List.
(L guarded_permutation(T;L,i. P(L[i],L[(i+1)])) L')
& (i:(||L'||-1). P(L'[i],L'[(i+1)]))
