E:TaggedEventStruct. tag_splitable(E;adR(E))R:(T
TProp), x,y,z:T. (x (R^*) y) 
(y (R^*) z) (x (R^*) z)x,y:T, R:(TTProp). x = y (x (R^*) y)R:(TTProp), x,y:T. (x R y) (x (R^*) y)P:(AAProp), f:(A
), L1,L2:A List.
(L1 swap adjacent[P(x,y)] L2)
(filter(f;L1) swap adjacent[P(x,y)] filter(f;L2)) 
filter(f;L1) = filter(f;L2)