At: strong switch inv decomposable 1 1
1. E: TaggedEventStruct
2. tr: |E| List
3. switch_inv(E)(tr)
4. Causal(E)(tr)
5. AD-normal(E)(tr)
6. No-dup-deliver(E)(tr)
7. 
tr = nil
ls:
||tr||. is-send(E)(tr[ls]) & (
j:||tr||. ls < j 
is-send(E)(tr[j]))
By:
Inst
Thm* L:T List, P:(||L||
Prop).
(x:||L||. Dec(P(x))) (i:||L||. P(i)) (i:||L||. P(i) & (j:||L||. i < j P(j)))
[|E|;tr;
i.is-send(E)(tr[i])]
THEN
All Reduce
THEN
BackThru
Thm* E:EventStruct, L:|E| List.
L = nil Causal(E)(L) (i:||L||. is-send(E)(L[i]))
Generated subgoals:None
About:
