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

At: P causal switchable0 5 1 1 2 1 2 2
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. loc(E)(x[i1]) = loc(E)(x[(i1+1)])
7. is-send(E)(x[i1])
8. is-send(E)(x[(i1+1)])
9. y = swap(x;i1;i1+1)
10. i: ||y||
11. ||swap(x;i1;i1+1)|| = ||x||
12. ||y|| = ||x||
13. ||swap(y;i1;i1+1)|| = ||y||
14. (i1, i1+1) ||x||||x||
15. is-send(E)(y[i])
16. j: ||x||
17. j(i1, i1+1)(i)
18. is-send(E)(x[j])
19. x[j] =msg=(E) x[((i1, i1+1)(i))]
20. i = i1

(i1, i1+1)(j)i
By:
MoveToConcl -4
THEN
Unfold `flip` 0
THEN
Reduce 0
THEN
Repeat SplitOnConclITE
THEN
AllHyps (h.(HypSubstSq -1 h) THEN Trivial)
Generated subgoals:

117. is-send(E)(x[j])
18. x[j] =msg=(E) x[((i1, i1+1)(i))]
19. i = i1
20. i = i1
21. jif i=i1+1 i1 else i fi
22. j = i1
i1+1i
217. is-send(E)(x[j])
18. x[j] =msg=(E) x[((i1, i1+1)(i))]
19. i = i1
20. i = i1
21. jif i=i1+1 i1 else i fi
22. j = i1
23. j = i1+1
i1i
317. is-send(E)(x[j])
18. x[j] =msg=(E) x[((i1, i1+1)(i))]
19. i = i1
20. i = i1
21. jif i=i1+1 i1 else i fi
22. j = i1
23. j = i1+1
ji

About:
listassertintnatural_numberaddsubtractapplyfunction
equalmemberandallexists

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