tr' 
filter(
b.
(b =msg=(E) a);x)
tr':|E| List. tr' x 
(x
tr'.(
ytr'.is-send(E)(y) & (y =msg=(E) x)))b.(b =msg=(E) a);x) y tr:|E| List. tr x & tr' = filter(b.(b =msg=(E) a);tr)P:(T
), L_1,L_2:T List.
L_2 filter(P;L_1) (L_3:T List. L_3 L_1 & L_2 = filter(P;L_3))| 1 | tr' filter(b.(b =msg=(E) a);x) |
About:
 |  |  |  |  |  |  |  |  |