At: switch inv rel closure lemma1111 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. 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 By: ReduceExp -1
THEN
BackThru
Thm*x,y:T, R:(TTProp). x = y (x (R^*) y)
THEN
SupposeNot
THEN
AllHyps (h.InstHyp [j] h) Generated subgoals:
||tr||
j:
is-send(E)(tr[j])
j
j (switchR(tr)^*) ls
T
h.InstHyp [j] h)