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

At: P causal switchable0 2
1. E: EventStruct

memorylessR(E) preserves Causal(E)
By:
Unfolds [`preserved_by`;`R_memoryless`] 0
THEN
Reduce 0
THEN
ExRepD
THEN
All (RWO "P_causal_iff")
Generated subgoal:

12. 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
(xtr'.(ytr'.is-send(E)(y) & (y =msg=(E) x)))

About:
listassertapplyand

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