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

At: P causal switchable0 6 1 1
1. E: EventStruct
2. x: |E| List
3. y: |E| List
4. i:||x||. j:||x||. ji & is-send(E)(x[j]) & (x[j] =msg=(E) x[i])
5. i1: (||x||-1)
6. (x[i1] =msg=(E) x[(i1+1)])
7. is-send(E)(x[i1]) & is-send(E)(x[(i1+1)]) is-send(E)(x[i1]) & is-send(E)(x[(i1+1)])
8. y = swap(x;i1;i1+1)
9. i: ||y||
10. ||swap(x;i1;i1+1)|| = ||x||
11. ||y|| = ||x||
12. ||swap(y;i1;i1+1)|| = ||y||
13. (i1, i1+1) ||x||||x||

j:||y||. ji & is-send(E)(y[j]) & (y[j] =msg=(E) y[i])
By:
InstHyp [(i1, i1+1)(i)] 4
THEN
ExRepD
THEN
InstConcl [(i1, i1+1)(j)]
Generated subgoals:

114. j: ||x||
15. j(i1, i1+1)(i)
16. is-send(E)(x[j])
17. x[j] =msg=(E) x[((i1, i1+1)(i))]
(i1, i1+1)(j)i
214. j: ||x||
15. j(i1, i1+1)(i)
16. is-send(E)(x[j])
17. x[j] =msg=(E) x[((i1, i1+1)(i))]
is-send(E)(y[((i1, i1+1)(j))])
314. j: ||x||
15. j(i1, i1+1)(i)
16. is-send(E)(x[j])
17. x[j] =msg=(E) x[((i1, i1+1)(i))]
y[((i1, i1+1)(j))] =msg=(E) y[i]

About:
listassertintnatural_numberaddsubtractapplyfunction
equalmemberandorallexists

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