E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2)M:MessageStruct. EquivRel(|M|)(_1 =(M) _2)E:DecidableEquiv. EquivRel(|E|)(_1 =(E) _2)
E:T
T
EquivRel(T)(
(_1 E _2))Topis mentioned by
|
Thm* E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2) | [event_msg_eq_equiv] |
|
Thm* M:MessageStruct. EquivRel(|M|)(_1 =(M) _2) | [msg_eq_equiv] |
|
Thm* E:DecidableEquiv. EquivRel(|E|)(_1 =(E) _2) | [eq_dequiv_equiv] |
|
Def DecidableEquiv == T:TypeE:TTEquivRel(T)((_1 E _2))Top | [dequiv] |
In prior sections: rel 1 mb basic mb nat num thy 1
Try larger context: GenAutomata