||tr||

j:||tr||. ls < j is-send(E)(tr[j])

n:, i,j:||tr||. ij is-send(E)(tr[i]) is-send(E)(tr[j]) (i switchR(tr)^n ls) (j (switchR(tr)^*) ls)

1	6. i: ||tr|| 7. j: ||tr|| 8. ij 9. is-send(E)(tr[i]) 10. is-send(E)(tr[j]) 11. i switchR(tr)^0 ls j (switchR(tr)^*) ls
2	6. n: 7. 0 < n 8. i,j:||tr||. ij is-send(E)(tr[i]) is-send(E)(tr[j]) (i switchR(tr)^n-1 ls) (j (switchR(tr)^*) ls) 9. i: ||tr|| 10. j: ||tr|| 11. ij 12. is-send(E)(tr[i]) 13. is-send(E)(tr[j]) 14. i switchR(tr)^n ls j (switchR(tr)^*) ls

About: