2. P : L:(T List)
(||L||-1)
3. m : (T List)
4.
L:T List, i:(||L||-1).
4. P(L,i)
P(swap(L;i;i+1),i) & m(swap(L;i;i+1))<m(L)
5. L : T List
6.
0<||L||
L':T List.
(L guarded_permutation(T;
L,i. P(L,i)) L') & (i:(||L'||-1). P(L',i))(||L||-1)
L:T List, i:(||L||-1).
P(swap(L;i;i+1),i) & m(swap(L;i;i+1))<m(L)
0<||L||
L':T List.
(L guarded_permutation(T;L,i. P(L,i)) L') & (i:(||L'||-1). P(L',i))| By: |
|
| 1 |
L guarded_permutation(T;L,i. P(L,i)) nil | 1 step |
About:
 |  |  |  |  |  |  |  |  |  |
 |  |  |  |  |  |