mb structures Sections GenAutomata Doc

Def b == if b True else False fi

is 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 No-dup-send(E)(tr) == i,j:||tr||. (is-send(E)(tr[i])) (is-send(E)(tr[j])) (tr[i] =msg=(E) tr[j]) i = j[no_duplicate_send]
Def Macro is-deliver(E)(x) == (is-send(E)(x))[event_is_deliver]
Def DecidableEquiv == T:TypeE:TTEquivRel(T)((_1 E _2))Top[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

mb structures Sections GenAutomata Doc