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