E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2)E:EventStruct. is-send(E) 
|E|
E:EventStruct. loc(E) |E|LabelE:EventStruct. msg(E) |E||MS(E)|
M:MessageStruct(E|M|)(ELabel)(E)Top
is mentioned by
|
Thm* E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2) | [event_msg_eq_equiv] |
|
Thm* E:EventStruct. is-send(E) |E| | [event_is_snd_wf] |
|
Thm* E:EventStruct. loc(E) |E|Label | [event_loc_wf] |
|
Thm* E:EventStruct. msg(E) |E||MS(E)| | [event_msg_wf] |
Try larger context: GenAutomata