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

At: P no dup iff

E:EventStruct, tr:|E| List. No-dup-deliver(E)(tr) (x,y:|E|. is-send(E)(x) is-send(E)(y) (y =msg=(E) x) loc(E)(x) = loc(E)(y) sublist(|E|;[x; y];tr))
By: Auto
Generated subgoals:

11. E: EventStruct
2. tr: |E| List
3. No-dup-deliver(E)(tr)
4. x: |E|
5. y: |E|
6. is-send(E)(x)
7. is-send(E)(y)
8. y =msg=(E) x
9. loc(E)(x) = loc(E)(y)
sublist(|E|;[x; y];tr)
21. E: EventStruct
2. tr: |E| List
3. x,y:|E|. is-send(E)(x) is-send(E)(y) (y =msg=(E) x) loc(E)(x) = loc(E)(y) sublist(|E|;[x; y];tr)
No-dup-deliver(E)(tr)

About:
listconsnilassertapplyequalimpliesall

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