At: switch main theorem31 1. 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))
layerR(E) preserves P By: Unfold `layer_rel` 0
THEN
BackThru
Thm*P:(TProp), R:(TTProp). R preserves P R^* preserves P
THEN
AllHyps (h.(Unfold `b_switchable` h) THEN (Reduce h))
THEN
Repeat
(BackThru
Thm*P:(TProp), R1,R2:(TTProp).
R1 preserves P R2 preserves P R1 R2 preserves P) Generated subgoals:
Prop
m:Label. P(map(evt; < tr_l > _m))
layerR(E) preserves P
R^* preserves P
h.(Unfold `b_switchable` h) THEN (Reduce h))
R2 preserves P)