At: causal fusion 1 1 1
1. E: TaggedEventStruct
2. tr: |E| List
3.
m:Label. Causal(E)( < tr > _m)
4. True
5. tr': |E| List
6. tr'
tr
7. x: |E|
8. (x
tr')
9.
tr':|E| List. tr'
< tr > _tag(E)(x) 
(
x
tr'.(
y
tr'.is-send(E)(y) & (y =msg=(E) x)))
< tr' > _tag(E)(x)
< tr > _tag(E)(x)
By:
Unfold `tag_sublist` 0
THEN
BackThru
Thm*
P:(T

), L2,L1:T List. L1
L2 
filter(P;L1)
filter(P;L2)
Generated subgoals:None
About: