is mentioned by
Thm* ![]() | [event_msg_eq_equiv] |
Thm* ![]() | [msg_eq_equiv] |
Thm* ![]() | [eq_dequiv_equiv] |
Def No-dup-send(E)(tr)
== ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [no_duplicate_send] |
Def Macro
is-deliver(E)(x) == ![]() ![]() | [event_is_deliver] |
Def DecidableEquiv == T:Type![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [dequiv] |
In prior sections: bool 1 list 1 mb basic mb nat union mb list 1 mb label mb list 2 rel 1
Try larger context: GenAutomata