At: switch inv rel closure12 1. E: TaggedEventStruct 2. tr: |E| List 3. ls: ||tr|| 4. switch_inv(E)(tr) 5. i: ||tr|| 6. j: ||tr|| 7. i (switchR(tr)^*) ls 8. j (switchR(tr)^*) ls 9. x,y:||tr||. (x (switchR(tr)^*) y) tag(E)(tr[x]) = tag(E)(tr[y]) x = y
tag(E)(tr[i]) = tag(E)(tr[j]) By: InstHyp [i;ls] -1
THEN
SimpHyp -1
THEN
InstHyp [j;ls] -2
THEN
SimpHyp -1
THEN
SplitOrHyps
THEN
Try (SubstFor i 0)
THEN
Try (SubstFor j 0) Generated subgoals:
||tr||
x,y:
tag(E)(tr[x]) = tag(E)(tr[y]) 
x = y
tag(E)(tr[i]) = tag(E)(tr[j])