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

At: switch main theorem

E:EventStruct, P:TraceProperty(E), A:Type, evt:(A|E|), tg:(ALabel), tr_u:Trace(E), tr_l:A List. switchable(E)(P) No-dup-send(E)(tr_u) full_switch_inv(E;A;evt;tg;tr_u;tr_l) (m:Label. P(map(evt; < tr_l > _m))) P(tr_u)
By:
Unfolds [`trace_property`;`str_trace`] 0
THEN
Unfold `full_switch_inv` -2
THEN
ExRepD
THEN
Inst Thm* E:EventStruct, P:((|E| List)Prop), A:Type, evt:(A|E|) , tg:(ALabel), tr:A List. switchable(E)(P) No-dup-send(E)(map(evt;tr)) switch_inv( < A,evt,tg > (E))(tr) (m:Label. P(map(evt; < tr > _m))) P(map(evt;tr)) [E;P;A;evt;tg;tr_m]
Generated subgoals:

11. E: EventStruct
2. P: (|E| List)Prop
3. A: Type
4. evt: A|E|
5. tg: ALabel
6. tr_u: |E| List
7. tr_l: A List
8. switchable(E)(P)
9. No-dup-send(E)(tr_u)
10. tr_m: A List
11. tr_l R(tg) tr_m
12. map(evt;tr_m) layerR(E) tr_u
13. switch_inv( < A,evt,tg > (E))(tr_m)
14. m:Label. P(map(evt; < tr_l > _m))
No-dup-send(E)(map(evt;tr_m))
21. E: EventStruct
2. P: (|E| List)Prop
3. A: Type
4. evt: A|E|
5. tg: ALabel
6. tr_u: |E| List
7. tr_l: A List
8. switchable(E)(P)
9. No-dup-send(E)(tr_u)
10. tr_m: A List
11. tr_l R(tg) tr_m
12. map(evt;tr_m) layerR(E) tr_u
13. switch_inv( < A,evt,tg > (E))(tr_m)
14. m:Label. P(map(evt; < tr_l > _m))
15. m: Label
P(map(evt; < tr_m > _m))
31. E: EventStruct
2. P: (|E| List)Prop
3. A: Type
4. evt: A|E|
5. tg: ALabel
6. tr_u: |E| List
7. tr_l: A List
8. switchable(E)(P)
9. No-dup-send(E)(tr_u)
10. tr_m: A List
11. tr_l R(tg) tr_m
12. map(evt;tr_m) layerR(E) tr_u
13. switch_inv( < A,evt,tg > (E))(tr_m)
14. m:Label. P(map(evt; < tr_l > _m))
15. P(map(evt;tr_m))
P(tr_u)

About:
listapplyfunctionuniverseimpliesall

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