At: switch inv rel closure lemma1112111 1. E: EventStruct 2. tr: |E| List 3. ls: ||tr|| 4. is-send(E)(tr[ls]) 5. j:||tr||. ls < j is-send(E)(tr[j]) 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 15. n = 0 16. z: ||tr|| 17. is-send(E)(tr[i]) 18. is-send(E)(tr[z]) 19. i < z & tr[z] somewhere delivered before tr[i] z < i & tr[i] somewhere delivered before tr[z] 20. z switchR(tr)^n-1 ls 21. i (switchR(tr)^*) ls 22. z (switchR(tr)^*) ls 23. zj
j (switchR(tr)^*) ls By: Using [`i',z] BackThruSomeHyp Generated subgoals:
||tr||
j:
is-send(E)(tr[j])
j 
z < i & tr[i] somewhere delivered before tr[z]
j (switchR(tr)^*) ls