(6steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc

At: normal form fusion

E:TaggedEventStruct, P,I,J,K:TraceProperty(E), R:(Trace(E)Trace(E)Prop). tag_splitable(E;R) (tr_1,tr_2:Trace(E). (tr_1 R tr_2) (tr_2 R tr_1)) R preserves P R preserves K (tr:Trace(E). (I K)(tr) (tr':Trace(E). I(tr') & J(tr') & (tr R tr'))) (((I J) K) fuses P) ((I K) fuses P)
By:
Unfold `tag_splitable` 0
THEN
Unfolds [`str_trace`;`trace_property`] 0
THEN
Try (Unfold `trace_property` 0)
THEN
Try (Fold `trace_property` 0)
Generated subgoal:

11. E: TaggedEventStruct
2. P: (|E| List)Prop
3. I: (|E| List)Prop
4. J: (|E| List)Prop
5. K: (|E| List)Prop
6. R: (|E| List)(|E| List)Prop
7. tr_1,tr_2:|E| List. (tr_1 R tr_2) (m:Label. < tr_1 > _m R < tr_2 > _m)
8. tr_1,tr_2:|E| List. (tr_1 R tr_2) (tr_2 R tr_1)
9. R preserves P
10. R preserves K
11. tr:|E| List. (I K)(tr) (tr':|E| List. I(tr') & J(tr') & (tr R tr'))
12. ((I J) K) fuses P
(I K) fuses P

About:
listapplyfunctionpropimpliesandallexists

(6steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc