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

At: P causal switchable0 4 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. x@0: |E|
6. is-send(E)(x@0)
7. y = (x @ [x@0])
8. i: ||y||
9. ||y|| = ||x||+||[x@0]||
10. i < ||x||

j:||y||. ji & is-send(E)(y[j]) & (y[j] =msg=(E) y[i])
By:
Reduce -2
THEN
InstConcl [i]
Generated subgoals:

19. ||y|| = ||x||+1
10. i < ||x||
is-send(E)(y[i])
29. ||y|| = ||x||+1
10. i < ||x||
y[i] =msg=(E) y[i]

About:
listconsnilassertintnatural_numberaddless_than
applyequalandallexists

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