tr = nil

||tr||

j:||tr||. ls < j is-send(E)(tr[j])

Q:(||tr||Prop). (i:||tr||. Dec(Q(i))) & (i:||tr||. Q(i)) & (i:||tr||. Q(i) is-send(E)(tr[i])) & (i,j:||tr||. Q(i) Q(j) tag(E)(tr[i]) = tag(E)(tr[j])) & (i,j:||tr||. Q(i) ij C(Q)(j))

AssertBY (i:||tr||. (i (switchR(tr)^*) ls) is-send(E)(tr[i])) ((Inst Thm* E:EventStruct, tr:|E| List, ls,i:||tr||. is-send(E)(tr[ls]) (i (switchR(tr)^*) ls) is-send(E)(tr[i]) [E;tr;ls]) THEN EasyHyp)
THEN
Inst Thm* E:TaggedEventStruct, tr:|E| List, ls:||tr||. switch_inv(E)(tr) (i,j:||tr||. (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls) tag(E)(tr[i]) = tag(E)(tr[j])) [E;tr;ls]
THEN
Thin 3
THEN
Inst Thm* E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2) [E]
THEN
InstConcl [i.i (switchR(tr)^*) ls]
THEN
Reduce 0
THEN
SplitAndConcl
THEN
Try (Complete Auto)
THEN
Try ((InstConcl [ls]) THEN (BackThru Thm* x,y:T, R:(TTProp). x = y (x (R^*) y)))
THEN
Try (Auto THEN (AllHyps (InstHyp [i;j])) THEN (Complete Auto))
THEN
Try (Auto THEN (Complete EasyHyp))
THEN
Thin -2

1

3. Causal(E)(tr) 4. AD-normal(E)(tr) 5. No-dup-deliver(E)(tr) 6. tr = nil 7. ls: ||tr|| 8. is-send(E)(tr[ls]) 9. j:||tr||. ls < j is-send(E)(tr[j]) 10. i:||tr||. (i (switchR(tr)^*) ls) is-send(E)(tr[i]) 11. EquivRel(|E|)(_1 =msg=(E) _2) i,j:||tr||. (i (switchR(tr)^*) ls) ij C(i.i (switchR(tr)^*) ls)(j)

About: