At: switch inv safety1 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. switch_inv(E)(x)
switch_inv(E)(y) By: All (h.(Unfold `switch_inv` h) THEN (Unfold `delivered_at` h) THEN (Reduce h))
THEN
RepeatFor 3 ((ParallelOp -1) THEN (Thin -3))
THEN
Subst (y[i] = x[i]) 0
THEN
EasyHyp
THEN
Subst (y[j] = x[j]) 0
THEN
EasyHyp
THEN
Subst (y[k] = x[k]) 0
THEN
EasyHyp
THEN
RepeatFor 6 (ParallelOp -1)
THEN
Subst (y[k'] = x[k']) 0
THEN
EasyHyp Generated subgoals:
x
i:
. i < ||y|| 
y[i] = x[i]
switch_inv(E)(y)
h.(Unfold `switch_inv` h) THEN (Unfold `delivered_at` h) THEN (Reduce h))