(6steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc

At: normal form fusion 1 2
1. 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. tr:|E| List. (m:Label. P( < tr > _m)) ((I J) K)(tr) P(tr)
13. tr: |E| List
14. m:Label. P( < tr > _m)
15. (I K)(tr)
16. tr': |E| List
17. I(tr')
18. J(tr')
19. tr R tr'

((I J) K)(tr')
By:
All (Unfold `prop_and`)
THEN
All Reduce
THEN
AllHyps (h.(Unfold `preserved_by` h) THEN (BackThruHyp' h))
Generated subgoals:

None

About:
listapplyfunctionpropimpliesandallexists

(6steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc