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

At: P causal switchable0 2 1 2
1. E: EventStruct
2. x: |E| List
3. y: |E| List
4. tr':|E| List. tr' x (xtr'.(ytr'.is-send(E)(y) & (y =msg=(E) x)))
5. a: |E|
6. y = filter(b.(b =msg=(E) a);x)
7. tr': |E| List
8. tr' y
9. tr:|E| List. tr x & tr' = filter(b.(b =msg=(E) a);tr)

(xtr'.(ytr'.is-send(E)(y) & (y =msg=(E) x)))
By:
ExRepD
THEN
InstHyp [tr] 4
THEN
RepeatFor 3 (ParallelOp -1)
Generated subgoals:

19. tr: |E| List
10. tr x
11. tr' = filter(b.(b =msg=(E) a);tr)
12. x:|E|. (x tr) (ytr.is-send(E)(y) & (y =msg=(E) x))
13. x1: |E|
14. (x1 tr')
(x1 tr)
29. tr: |E| List
10. tr x
11. tr' = filter(b.(b =msg=(E) a);tr)
12. x:|E|. (x tr) (ytr.is-send(E)(y) & (y =msg=(E) x))
13. x1: |E|
14. (x1 tr')
15. (ytr.is-send(E)(y) & (y =msg=(E) x1))
(ytr'.is-send(E)(y) & (y =msg=(E) x1))

About:
listassertlambdaapplyequalimpliesandallexists

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