At: switch normal safety11 1. E: TaggedEventStruct 2. x: |E| List 3. y: |E| List 4. y x 5. ||y||||x|| 6. i:. i < ||y|| y[i] = x[i] 7. i: (||y||-1) 8. (is-send(E)(x[i]) is-send(E)(x[(i+1)]) (x[i] =msg=(E) x[(i+1)]))
& ((x@0,y:||x||.
x@0 < y
& is-send(E)(x[x@0])
& is-send(E)(x[y])
& x[x@0] delivered at time i+1
& x[y] delivered at time i)
loc(E)(x[i]) = loc(E)(x[(i+1)]))
(is-send(E)(x[i]) is-send(E)(x[(i+1)]) (x[i] =msg=(E) x[(i+1)]))
& ((x,y@0:||y||.
x < y@0
& is-send(E)(y[x])
& is-send(E)(y[y@0])
& y[x] delivered at time i+1
& y[y@0] delivered at time i)
loc(E)(x[i]) = loc(E)(x[(i+1)])) By: RepeatFor 5 (ParallelOp -1)
THEN
All (Unfold `delivered_at`)
THEN
Subst (y[i] = x[i]) -1
THEN
EasyHyp
THEN
Subst (y[(i+1)] = x[(i+1)]) -1
THEN
EasyHyp
THEN
Subst (y[x1] = x[x1]) -1
THEN
EasyHyp
THEN
Subst (y[y@0] = x[y@0]) -1
THEN
EasyHyp Generated subgoals:
x
i:
. i < ||y|| 
y[i] = x[i]
is-send(E)(x[(i+1)]) 
x@0,y:
(is-send(E)(x[i]) 
