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

At: P no dup send enabled 1 1 2 1 1
1. E: EventStruct
2. x: |E| List
3. y: |E| List
4. i,j:||x||. is-send(E)(x[i]) is-send(E)(x[j]) (x[j] =msg=(E) x[i]) loc(E)(x[i]) = loc(E)(x[j]) i = j
5. x@0: |E|
6. is-send(E)(x@0)
7. y = (x @ [x@0])
8. i: ||y||
9. j: ||y||
10. is-send(E)(y[i])
11. y[j] =msg=(E) y[i]
12. loc(E)(y[i]) = loc(E)(y[j])
13. ||y|| = ||x||+1
14. i = ||x||
15. j = ||x||

is-send(E)((x @ [x@0])[||x||])
By: RWO "select_append_back" 0
Generated subgoal:

1 is-send(E)([x@0][(||x||-||x||)])

About:
listconsnilassertintnatural_numberaddsubtractapplyequalimpliesall

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