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

At: causal fusion 1
1. E: TaggedEventStruct
2. tr: |E| List
3. m:Label. Causal(E)( < tr > _m)
4. True

Causal(E)(tr)
By:
RWO "P_causal_iff" 0
THEN
Unfold `l_all` 0
THEN
AllHyps (InstHyp [tag(E)(x)])
THEN
RWO "P_causal_iff" -1
Generated subgoal:

15. tr': |E| List
6. tr' tr
7. x: |E|
8. (x tr')
9. tr':|E| List. tr' < tr > _tag(E)(x) (xtr'.(ytr'.is-send(E)(y) & (y =msg=(E) x)))
(ytr'.is-send(E)(y) & (y =msg=(E) x))

About:
listassertapplyandtrueall

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