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

At: P causal switchable0 3
1. E: EventStruct

(ternary) composableR(E) preserves Causal(E)
By:
Unfolds [`preserved_by2`;`P_causal`;`R_composable`] 0
THEN
Reduce 0
Generated subgoal:

12. x: |E| List
3. y: |E| List
4. z: |E| List
5. i:||x||. j:||x||. ji & is-send(E)(x[j]) & (x[j] =msg=(E) x[i])
6. i:||y||. j:||y||. ji & is-send(E)(y[j]) & (y[j] =msg=(E) y[i])
7. (xx.(yy.(x =msg=(E) y)))
8. z = (x @ y)
9. i: ||z||
j:||z||. ji & is-send(E)(z[j]) & (z[j] =msg=(E) z[i])

About:
listassertnatural_numberapplyandexists

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