PrintForm Definitions mb hybrid Sections GenAutomata Doc

At: fusion and

E:TaggedEventStruct, I,P,Q:TraceProperty(E). (I fuses P) (I fuses Q) (I fuses (P Q))
By:
Unfolds [`trace_property`;`fusion_condition`;`prop_and`] 0
THEN
Unfold `str_trace` 0
THEN
Reduce 0
THEN
BackThruSomeHyp
THEN
AllHyps (h.(InstHyp [m] h) THEN (Complete Auto))
Generated subgoals:

None

About:
impliesall

PrintForm Definitions mb hybrid Sections GenAutomata Doc