Nuprl - Pf normal_form

(6steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc

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. ((I J) K) fuses P

(I K) fuses P

By: ParallelOp -1 THEN All (Unfold `str_trace`) THEN ParallelOp -2 THEN Analyze 0 THEN ParallelOp -2 THEN ExRepD THEN InstHyp [tr'] -8

Generated subgoals:

1 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'
20. m: Label
P( < tr' > _m)

2 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')

3 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'
20. P(tr')
P(tr)

About:

(6steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc

1	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'` 20. `m:` `Label` `P( < tr' > _m)`
2	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')`
3	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'` 20. `P(tr')` `P(tr)`