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

At: no dup fusion 1 1
1. E: TaggedEventStruct
2. tr: |E| List
3. m:Label. No-dup-deliver(E)( < tr > _m)
4. Tag-by-msg(E)(tr)
5. x: |E|
6. y: |E|
7. is-send(E)(x)
8. is-send(E)(y)
9. y =msg=(E) x
10. loc(E)(x) = loc(E)(y)
11. x1,y:|E|. is-send(E)(x1) is-send(E)(y) (y =msg=(E) x1) loc(E)(x1) = loc(E)(y) sublist(|E|;[x1; y]; < tr > _tag(E)(x))
12. sublist(|E|;[x; y]; < tr > _tag(E)(x))

sublist(|E|;[x; y];tr)
By:
ParallelOp -1
THEN
Unfold `tag_sublist` 0
THEN
BackThru Thm* L1,L2:T List, P:(T). sublist(T;L2;filter(P;L1)) sublist(T;L2;L1) & (xL2.P(x))
THEN
Unfold `l_all` 0
THEN
Reduce 0
Generated subgoal:

112. sublist(|E|;[x; y];tr)
13. x1: |E|
14. (x1 [x; y])
tag(E)(x1) = tag(E)(x)

About:
listconsnilassertapplyequalimpliesall

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