E:TaggedEventStruct. (switch-decomposable(E) Tag-by-msg(E) Causal(E) No-dup-send(E)) refines single-tag-decomposable(E)

(Auto THEN (Unfolds [`P_tag_by_msg`;`prop_and`] 0) THEN (Unfolds [`switch_decomposable`;`single_tag_decomposable`;`tr_refines`] 0) THEN (Reduce 0) THEN SplitOrHyps THEN (Try Trivial) THEN ExRepD THEN (Inst Thm* L:T List, P:(||L||Prop). (x:||L||. Dec(P(x))) (i,j:||L||. P(i) i < j P(j)) (L_1,L_2:T List. L = (L_1 @ L_2) & (i:||L||. P(i) ||L_1||i)) [|E|;tr;C(Q)])) THENA (Try (Complete (Auto THEN (Reduce 0))))

1	1. E: TaggedEventStruct 2. tr: |E| List 3. Q: ||tr||Prop 4. i:||tr||. Dec(Q(i)) 5. i: ||tr|| 6. Q(i) 7. i:||tr||. Q(i) is-send(E)(tr[i]) 8. i,j:||tr||. Q(i) Q(j) tag(E)(tr[i]) = tag(E)(tr[j]) 9. i,j:||tr||. Q(i) ij C(Q)(j) 10. i,j:||tr||. (tr[i] =msg=(E) tr[j]) tag(E)(tr[i]) = tag(E)(tr[j]) 11. Causal(E)(tr) 12. No-dup-send(E)(tr) 13. tr = nil x:||tr||. Dec(C(Q)(x))
2	1. E: TaggedEventStruct 2. tr: |E| List 3. Q: ||tr||Prop 4. i:||tr||. Dec(Q(i)) 5. i: ||tr|| 6. Q(i) 7. i:||tr||. Q(i) is-send(E)(tr[i]) 8. i,j:||tr||. Q(i) Q(j) tag(E)(tr[i]) = tag(E)(tr[j]) 9. i,j:||tr||. Q(i) ij C(Q)(j) 10. i,j:||tr||. (tr[i] =msg=(E) tr[j]) tag(E)(tr[i]) = tag(E)(tr[j]) 11. Causal(E)(tr) 12. No-dup-send(E)(tr) 13. tr = nil i,j:||tr||. C(Q)(i) i < j C(Q)(j)
3	1. E: TaggedEventStruct 2. tr: |E| List 3. Q: ||tr||Prop 4. i:||tr||. Dec(Q(i)) 5. i: ||tr|| 6. Q(i) 7. i:||tr||. Q(i) is-send(E)(tr[i]) 8. i,j:||tr||. Q(i) Q(j) tag(E)(tr[i]) = tag(E)(tr[j]) 9. i,j:||tr||. Q(i) ij C(Q)(j) 10. i,j:||tr||. (tr[i] =msg=(E) tr[j]) tag(E)(tr[i]) = tag(E)(tr[j]) 11. Causal(E)(tr) 12. No-dup-send(E)(tr) 13. tr = nil 14. L_1,L_2:|E| List. tr = (L_1 @ L_2) & (i:||tr||. C(Q)(i) ||L_1||i) L_1,L_2:Trace(E). tr = (L_1 @ L_2) & L_2 = nil |E| List & (xL_1.(yL_2.(x =msg=(E) y))) & (m:Label. (xL_2.tag(E)(x) = m))

About: