PrintForm Definitions mb structures Sections GenAutomata Doc

At: event msg wf

E:EventStruct. msg(E) |E||MS(E)|
By:
Analyze 0
THEN
Unfolds [`event_msg`;`event_msg_str`] 0
THEN
RepeatFor 3 ((Analyze -1) THEN (Reduce 0))
THEN
Trivial
Generated subgoals:

None

About:
functionmemberall

PrintForm Definitions mb structures Sections GenAutomata Doc