By: |
THEN Inst Thm: swap adjacent decomp [A;i;L1] THEN ExRepD |
1 |
2. P : A ![]() ![]() ![]() ![]() 3. f : A ![]() ![]() ![]() 4. L1 : A List 5. L2 : A List 6. i : ![]() 7. P(L1[i],L1[(i+1)]) 8. L2 = swap(L1;i;i+1) 9. X : A List 10. Y : A List 11. L1 = (X @ [L1[i]; L1[(i+1)]] @ Y) 12. swap(L1;i;i+1) = (X @ [L1[(i+1)]; L1[i]] @ Y) ![]() ![]() ![]() ![]() | 8 steps |
About:
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |