mb
structures
Sections
GenAutomata
Doc
Def
sender(MS) == 1of(2of(2of(2of(MS))))
is mentioned by
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))
[msg_eq]
Try larger context:
GenAutomata
mb
structures
Sections
GenAutomata
Doc