PrintForm Definitions mb structures Sections GenAutomata Doc

At: msg content wf

M:MessageStruct. content(M) |M||cEQ(M)|
By:
Analyze 0
THEN
Unfolds [`msg_content`;`msg_content_eq`] 0
THEN
RepeatFor 3 ((Analyze -1) THEN (Reduce 0))
THEN
Trivial
Generated subgoals:

None

About:
functionmemberall

PrintForm Definitions mb structures Sections GenAutomata Doc