By: |
((THEN ((All Reduce ((THEN ((Inst Thm* ![]() ![]() ![]() ![]() ((THEN ((RWO Thm* ![]() ![]() ((THEN ((InstHyp [0] -2 ((THEN ((Reduce -1 ((THEN ((InstHyp [1] -3 ((THEN ((Reduce -1 ((THEN ((Inst Thm* ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ((THEN ((WeakSubstFor a 0) (THEN ((WeakSubstFor b 0)) THEN Decide ((i, i+1)(f(0))<(i, i+1)(f(1))) THENL [OrLeft THEN (BackThru Thm* ![]() ![]() ![]() ![]() ![]() ;OrRight] |
1 |
2. L : T List 3. i : ![]() 4. a : T 5. b : T 6. f : ![]() ![]() ![]() ![]() 7. increasing(f;2) 8. ![]() ![]() 9. ||swap(L;i;i+1)|| = ||L|| ![]() ![]() 10. a = L[((i, i+1)(f(0)))] 11. b = L[((i, i+1)(f(1)))] 12. (i, i+1) ![]() ![]() ![]() ![]() ![]() 13. ![]() ![]() ![]() | 1 step |
About:
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() |