At: P causal switchable0 3 1 2
1. E: EventStruct
2. x: |E| List
3. y: |E| List
4. z: |E| List
5. 
i:
||x||. 
j:||x||. j
i & is-send(E)(x[j]) & (x[j] =msg=(E) x[i])
6. i:||y||. j:||y||. ji & is-send(E)(y[j]) & (y[j] =msg=(E) y[i])
7. (x
x.(yy.
(x =msg=(E) y)))
8. z = (x @ y)
9. i: ||z||
10. ||z|| = ||x||+||y||
11. i < ||x||
j:||z||. ji & is-send(E)(z[j]) & (z[j] =msg=(E) z[i])
By:
AssertBY (z[i] = y[(i-||x||)]) ((HypSubstList 8 0) THEN (RWO "select_append_back" 0))
THEN
InstHyp [i-||x||] 6
THEN
ExRepD
THEN
AssertBY (z[(j+||x||)] = y[j]) ((HypSubstList 8 0) THEN (RWO "select_append_back" 0))
THEN
InstConcl [j+||x||]
THEN
SubstFor z[(j+||x||)] 0
THEN
Try Trivial
THEN
SubstFor z[i] 0
THEN
Try Trivial
Generated subgoals:None
About:
