PrintForm
Definitions
mb
structures
Sections
GenAutomata
Doc
At:
event
loc
wf
E:EventStruct. loc(E)
|E|
Label
By:
Analyze 0
THEN
Unfold `event_loc` 0
THEN
RepeatFor 4 ((Analyze -1) THEN (Reduce 0))
Generated subgoals:
None
About:
PrintForm
Definitions
mb
structures
Sections
GenAutomata
Doc