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

At: P causal switchable0 6
1. E: EventStruct

delayableR(E) preserves Causal(E)
By:
Unfolds [`preserved_by`;`P_causal`;`R_delayable`] 0
THEN
Reduce 0
THEN
Unfold `swap_adjacent` -2
THEN
Reduce -2
THEN
ExRepD
Generated subgoal:

12. 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||
j:||y||. ji & is-send(E)(y[j]) & (y[j] =msg=(E) y[i])

About:
listassertnatural_numberapplyandexists

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