E:DecidableEquiv. EquivRel(|E|)(_1 =(E) _2)
C:DecidableEquiv(M
|C|)(MLabel)(M
)TopE:TT
EquivRel(T)(
(_1 E _2))Top
is mentioned by
|
Thm* E:DecidableEquiv. EquivRel(|E|)(_1 =(E) _2) | [eq_dequiv_equiv] |
|
Def MessageStruct == M:TypeC:DecidableEquiv(M|C|)(MLabel)(M)Top | [message_str] |
Try larger context: GenAutomata