Nuprl - mb_structures Citations of event_msg

Def =msg=(E)(e_1,e_2) == (msg(E)(e_1)) =(MS(E)) (msg(E)(e_2))

is mentioned by

Thm* E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2) [event_msg_eq_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]

Try larger context: GenAutomata

mb structures Sections GenAutomata Doc

`Thm* E:EventStruct. EquivRel(\|E\|)(_1 =msg=(E) _2)`	[event_msg_eq_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]