At: switch inv theorem 5 1
1. E: TaggedEventStruct
2. P: (|E| List)
Prop
3. MCS(E)(P)
4. asyncR(E) preserves P
5. delayableR(E) preserves P
6. P refines (
L.Causal(E)(L) & No-dup-deliver(E)(L))
7. tr: |E| List
8. switch_inv(E)(tr)
9. No-dup-send(E)(tr)
10. 
tr':Trace(E). switch_inv(E)(tr') & AD-normal(E)(tr') & (tr adR(E) tr')
tr':|E| List. switch_inv(E)(tr') & AD-normal(E)(tr') & (tr adR(E) tr')
By:
Unfold `str_trace` -1
THEN
ParallelOp -1
THEN
Try (Fold `trace_property` 0)
THEN
Try (Unfold `R_ad` 0)
THEN
EasyHyp
Generated subgoals:None
About:
