At: P causal iff 1 1 2
1. E: EventStruct
2. tr: |E| List
3.
i:
||tr||.
j:
||tr||. j
i & is-send(E)(tr[j]) & (tr[j] =msg=(E) tr[i])
4. tr': |E| List
5. ||tr'||
||tr||
6.
i:
. i < ||tr'|| 
tr'[i] = tr[i]
7. x: |E|
8. i: 
9. i < ||tr'||
10. x = tr'[i]
11. ||tr'||
||tr||
12. j:
||tr||
13. j
i
14. is-send(E)(tr[j])
15. tr[j] =msg=(E) tr[i]
tr[j] =msg=(E) x
By:
Subst (x = tr[i]) 0
THEN
SubstFor x 0
THEN
EasyHyp
Generated subgoals:None
About: