At: P causal safety1 1. E: EventStruct 2. x: |E| List 3. y: |E| List 4. y x 5. ||y||||x|| 6. i:. i < ||y|| y[i] = x[i] 7. Causal(E)(x)
Causal(E)(y) By: All (h.(Unfold `P_causal` h) THEN (Reduce h))
THEN
ParallelOp -1
THEN
Thin -3
THEN
ParallelOp -1
THEN
Subst (y[i] = x[i]) 0
THEN
EasyHyp
THEN
Subst (y[j] = x[j]) 0
THEN
EasyHyp Generated subgoals:
x
i:
. i < ||y|| 
y[i] = x[i]
Causal(E)(y)
h.(Unfold `P_causal` h) THEN (Reduce h))