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

(Auto THEN (Reduce 0) THEN (AssertBY (switchable( < A,evt,tg > (E))(P o evt)) (BackThru Thm* E:EventStruct, P:((|E| List)Prop), A:Type, f:(A|E|) , t:(ALabel). switchable(E)(P) switchable( < A,f,t > (E))(P o f))) THEN (Inst Thm* E:TaggedEventStruct, P:TraceProperty(E). switchable(E)(P) ((switch_inv(E) No-dup-send(E)) fuses P) [ < A,evt,tg > (E);P o evt])) THENA (Auto THEN (Try (Unfold `trace_property` 0)))
THEN
AllHyps (h. (NthHypSq h) THEN Analyze THEN (Try Trivial) THEN (Unfold `induced_tagged_event_str` 0) THEN (Reduce 0) THEN Trivial)

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

About: