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

At: tag by msg fusion lemma

E:TaggedEventStruct, P,I:((|E| List)Prop). (P refines Causal(E)) ((I No-dup-send(E) Tag-by-msg(E)) fuses P) ((I No-dup-send(E)) fuses P)
By:
Unfolds [`prop_and`;`fusion_condition`] 0
THEN
Reduce 0
THEN
Unfold `str_trace` 0
THEN
Try (Fold `trace_property` 0)
THEN
BackThruSomeHyp
Generated subgoal:

11. E: TaggedEventStruct
2. P: (|E| List)Prop
3. I: (|E| List)Prop
4. P refines Causal(E)
5. tr:|E| List. (m:Label. P( < tr > _m)) I(tr) & No-dup-send(E)(tr) & Tag-by-msg(E)(tr) P(tr)
6. tr: |E| List
7. m:Label. P( < tr > _m)
8. I(tr)
9. No-dup-send(E)(tr)
Tag-by-msg(E)(tr)

About:
listapplyfunctionpropimpliesall

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