E:TaggedEventStruct, tr:|E| List, ls:||tr||. switch_inv(E)(tr) (i,j:||tr||. (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls) tag(E)(tr[i]) = tag(E)(tr[j]))

1	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 tag(E)(tr[i]) = tag(E)(tr[j])

About: