(8steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

At: causal fusion

E:TaggedEventStruct. PTrue fuses Causal(E)
By:
Unfolds [`PTrue`;`fusion_condition`] 0
THEN
Reduce 0
THEN
Unfold `str_trace` 0
Generated subgoal:

11. E: TaggedEventStruct
2. tr: |E| List
3. m:Label. Causal(E)( < tr > _m)
4. True
Causal(E)(tr)

About:
applyall

(8steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc