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

At: switch theorem 1
1. E: EventStruct
2. P: (|E| List)Prop
3. A: Type
4. evt: A|E|
5. tg: ALabel
6. tr: A List
7. switchable(E)(P)
8. No-dup-send(E)(map(evt;tr))
9. switch_inv( < A,evt,tg > (E))(tr)
10. m:Label. P(map(evt; < tr > _m))
11. switchable( < A,evt,tg > (E))(P o evt)
12. (switch_inv( < A,evt,tg > (E)) No-dup-send( < A,evt,tg > (E))) fuses P o evt

P(map(evt;tr))
By:
((Unfold `fusion_condition` -1) THEN (Unfold `compose_map` -1) THEN (Reduce -1) THEN (BackThru -1)) THENA (Unfold `str_trace` 0)
THEN
Unfold `prop_and` 0
THEN
Reduce 0
Generated subgoal:

112. tr:Trace( < A,evt,tg > (E)). (m:Label. P(map(evt; < tr > _m))) (switch_inv( < A,evt,tg > (E)) No-dup-send( < A,evt,tg > (E)))(tr) P(map(evt;tr))
No-dup-send( < A,evt,tg > (E))(tr)

About:
listapplyfunctionuniversepropall

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