E:TaggedEventStruct, P:TraceProperty(E). MCS(E)(P) asyncR(E) preserves P delayableR(E) preserves P (P refines (Causal(E) No-dup-deliver(E))) ((switch_inv(E) No-dup-send(E)) fuses P)

((Unfold `trace_property` 0) THEN (Try (Unfold `trace_property` 0)) THEN (Using [`J',AD-normal(E);`R',adR(E)] (BackThru Thm* E:TaggedEventStruct, P,I,J,K:TraceProperty(E) , R:(Trace(E)Trace(E)Prop). tag_splitable(E;R) (tr_1,tr_2:Trace(E). (tr_1 R tr_2) (tr_2 R tr_1)) R preserves P R preserves K (tr:Trace(E). (I K)(tr) (tr':Trace(E). I(tr') & J(tr') & (tr R tr'))) (((I J) K) fuses P) ((I K) fuses P)))) THENA ((Try (Unfolds [`str_trace`;`trace_property`] 0)) THEN (Try (Fold `trace_property` 0)))

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 (Causal(E) No-dup-deliver(E)) tag_splitable(E;adR(E))
2	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 (Causal(E) No-dup-deliver(E)) tr_1,tr_2:Trace(E). (tr_1 adR(E) tr_2) (tr_2 adR(E) tr_1)
3	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 (Causal(E) No-dup-deliver(E)) adR(E) preserves P
4	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 (Causal(E) No-dup-deliver(E)) adR(E) preserves No-dup-send(E)
5	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 (Causal(E) No-dup-deliver(E)) tr:Trace(E). (switch_inv(E) No-dup-send(E))(tr) (tr':Trace(E). switch_inv(E)(tr') & AD-normal(E)(tr') & (tr adR(E) tr'))
6	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 (Causal(E) No-dup-deliver(E)) ((switch_inv(E) AD-normal(E)) No-dup-send(E)) fuses P

About: