(43steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

At: P no dup composable 1 1 1 2 2 1 2
1. E: EventStruct
2. x: |E| List
3. y: |E| List
4. z: |E| List
5. i,j:||x||. is-send(E)(x[i]) is-send(E)(x[j]) (x[j] =msg=(E) x[i]) loc(E)(x[i]) = loc(E)(x[j]) i = j
6. i,j:||y||. is-send(E)(y[i]) is-send(E)(y[j]) (y[j] =msg=(E) y[i]) loc(E)(y[i]) = loc(E)(y[j]) i = j
7. (xx.(yy.(x =msg=(E) y)))
8. z = (x @ y)
9. i: ||z||
10. j: ||z||
11. is-send(E)(z[i])
12. is-send(E)(z[j])
13. z[j] =msg=(E) z[i]
14. loc(E)(z[i]) = loc(E)(z[j])
15. i < j
16. j < ||x||
17. ||z|| = ||x||+||y||
18. z[j] = y[(j-||x||)]
19. i < ||x||
20. z[i] = x[i]

i = j
By:
AllHyps (h.(Unfold `l_all` h) THEN (InstHyp [x[i];y[(j-||x||)]] h))
THEN
Try (BackThru Thm* L:T List, i:||L||. (L[i] L))
Generated subgoal:

17. x@0:|E|. (x@0 x) (y@0:|E|. (y@0 y) (x@0 =msg=(E) y@0))
8. z = (x @ y)
9. i: ||z||
10. j: ||z||
11. is-send(E)(z[i])
12. is-send(E)(z[j])
13. z[j] =msg=(E) z[i]
14. loc(E)(z[i]) = loc(E)(z[j])
15. i < j
16. j < ||x||
17. ||z|| = ||x||+||y||
18. z[j] = y[(j-||x||)]
19. i < ||x||
20. z[i] = x[i]
21. (x[i] =msg=(E) y[(j-||x||)])
i = j

About:
listassertintnatural_numberaddsubtractless_thanapplyequalimpliesall

(43steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc