Nuprl - mb_structures Citations of msg

Def =(M)(m_1,m_2) == ((content(M)(m_1)) =(cEQ(M)) (content(M)(m_2)))

sender(M)(m_1) =

sender(M)(m_2)

(uid(M)(m_1)=

uid(M)(m_2))

is mentioned by

Thm* M:MessageStruct. EquivRel(|M|)(_1 =(M) _2) [msg_eq_equiv]

Def =msg=(E)(e_1,e_2) == (msg(E)(e_1)) =(MS(E)) (msg(E)(e_2)) [event_msg_eq]

Try larger context: GenAutomata

`Thm* M:MessageStruct. EquivRel(\|M\|)(_1 =(M) _2)`	[msg_eq_equiv]
`Def =msg=(E)(e_1,e_2) == (msg(E)(e_1)) =(MS(E)) (msg(E)(e_2))`	[event_msg_eq]