PrintForm Definitions mb structures Sections GenAutomata Doc

At: event is snd wf

E:EventStruct. is-send(E) |E|
By:
Analyze 0
THEN
Unfold `event_is_snd` 0
THEN
RepeatFor 5 ((Analyze -1) THEN (Reduce 0))
Generated subgoals:

None

About:
boolfunctionmemberall

PrintForm Definitions mb structures Sections GenAutomata Doc