mb
structures
Sections
GenAutomata
Doc
Def
cEQ(MS) == 1of(2of(MS))
is mentioned by
Thm*
M:MessageStruct. content(M)
|M|
|cEQ(M)|
[msg_content_wf]
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