E:EventStruct, tr:|E| List, ls,i:
||tr||.
is-send(E)(tr[ls]) 
(i (switchR(tr)^*) ls) is-send(E)(tr[i])R,R2:(T
TProp).
Trans(T)(R2(_1,_2)) (x,y:T. (x R y) (x R2 y)) (x,y:T. (x (R^*) y) (x R2 y) 
x = y)| Theorem | Name |
|
Thm* E:EventStruct, tr:|E| List, ls,i:||tr||.
is-send(E)(tr[ls]) (i (switchR(tr)^*) ls) is-send(E)(tr[i]) | [switch_inv_rel_closure_send] |
| cites | |
|
Thm* R,R2:(TTProp).
Trans(T)(R2(_1,_2)) (x,y:T. (x R y) (x R2 y)) (x,y:T. (x (R^*) y) (x R2 y) x = y) | [rel_star_closure] |