E:TaggedEventStruct, P,I:TraceProperty(E). MCS(E)(P) safetyR(E) preserves I (I refines single-tag-decomposable(E)) (I fuses P)

Unfolds [`tr_refines`;`single_tag_decomposable`;`fusion_condition`] 0
THEN
Unfolds [`memoryless_composable_safety`;`str_trace`;`trace_property`] 0
THEN
Reduce 0
THEN
RepeatFor 6 (Analyze 0)
THEN
ExRepDHyps
THEN
Assert (n:, tr:|E| List. ||tr||n (m:Label. P( < tr > _m)) I(tr) P(tr))
THEN
Try ((Analyze 0) THEN (Using [`n',||tr||] BackThruSomeHyp))
THEN
Try InductionOnNat

1

1. E: TaggedEventStruct 2. P: (|E| List)Prop 3. I: (|E| List)Prop 4. memorylessR(E) preserves P 5. (ternary) composableR(E) preserves P 6. safetyR(E) preserves P 7. safetyR(E) preserves I 8. tr:|E| List. I(tr) tr = nil (L_1,L_2:|E| List. tr = (L_1 @ L_2) & L_2 = nil & (xL_1.(yL_2.(x =msg=(E) y))) & (m:Label. (xL_2.tag(E)(x) = m))) tr:|E| List. ||tr||0 (m:Label. P( < tr > _m)) I(tr) P(tr)

2

1. E: TaggedEventStruct 2. P: (|E| List)Prop 3. I: (|E| List)Prop 4. memorylessR(E) preserves P 5. (ternary) composableR(E) preserves P 6. safetyR(E) preserves P 7. safetyR(E) preserves I 8. tr:|E| List. I(tr) tr = nil (L_1,L_2:|E| List. tr = (L_1 @ L_2) & L_2 = nil & (xL_1.(yL_2.(x =msg=(E) y))) & (m:Label. (xL_2.tag(E)(x) = m))) 9. n: 10. 0 < n 11. tr:|E| List. ||tr||n-1 (m:Label. P( < tr > _m)) I(tr) P(tr) tr:|E| List. ||tr||n (m:Label. P( < tr > _m)) I(tr) P(tr)

About: