M:MessageStruct(E
|M|)(ELabel)(E
)(ELabel)TopM:MessageStruct(E|M|)(ELabel)(E)TopC:DecidableEquiv(M|C|)(MLabel)(M
)TopE:TTEquivRel(T)(
(_1 E _2))TopTopis mentioned by
|
Def TaggedEventStruct
== E:TypeM:MessageStruct(E|M|)(ELabel)(E)(ELabel)Top | [tagged_event_str] |
|
Def EventStruct == E:TypeM:MessageStruct(E|M|)(ELabel)(E)Top | [event_str] |
|
Def MessageStruct == M:TypeC:DecidableEquiv(M|C|)(MLabel)(M)Top | [message_str] |
|
Def DecidableEquiv == T:TypeE:TTEquivRel(T)((_1 E _2))Top | [dequiv] |
|
Def Structure == TypeTop | [struct] |
In prior sections: mb basic
Try larger context: GenAutomata