| | Who Cites R send enabled? |
|
| R_send_enabled | Def send-enabledR(E)(L_1,L_2) ==  x:|E|.  (is-send(E)(x)) & L_2 = (L_1 @ [x]) |
| | | Thm*  E:EventStruct. send-enabledR(E)  (|E| List)  (|E| List)Prop |
|
| append | Def as @ bs == Case of as; nil  bs ; a.as' [a / (as' @ bs)] (recursive) |
| | | Thm* T:Type, as,bs:T List. (as @ bs) T List |
|
| carrier | Def |S| == 1of(S) |
| | | Thm* S:Structure. |S| Type |
|
| event_is_snd | Def is-send(E) == 1of(2of(2of(2of(2of(E))))) |
| | | Thm* E:EventStruct. is-send(E) |E| |
|
| assert | Def b == if b True else False fi |
| | | Thm* b:. b Prop |
|
| pi1 | Def 1of(t) == t.1 |
| | | Thm* A:Type, B:(AType), p:(a:A B(a)). 1of(p) A |
|
| pi2 | Def 2of(t) == t.2 |
| | | Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p)) |
