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

At: P causal iff

E:EventStruct, tr:|E| List. Causal(E)(tr) (tr':|E| List. tr' tr (xtr'.(ytr'.is-send(E)(y) & (y =msg=(E) x))))
By:
Unfolds [`P_causal`;`l_all`;`l_exists`] 0
THEN
Unfold `l_member` 0
THEN
Reduce 0
THEN
ExRepD
Generated subgoals:

11. E: EventStruct
2. tr: |E| List
3. i:||tr||. j:||tr||. ji & is-send(E)(tr[j]) & (tr[j] =msg=(E) tr[i])
4. tr': |E| List
5. tr' tr
6. x: |E|
7. i:
8. i < ||tr'||
9. x = tr'[i]
y:|E|. (i:. i < ||tr'|| & y = tr'[i]) & is-send(E)(y) & (y =msg=(E) x)
21. E: EventStruct
2. tr: |E| List
3. tr':|E| List. tr' tr (x:|E|. (i:. i < ||tr'|| & x = tr'[i]) (y:|E|. (i:. i < ||tr'|| & y = tr'[i]) & is-send(E)(y) & (y =msg=(E) x)))
4. i: ||tr||
j:||tr||. ji & is-send(E)(tr[j]) & (tr[j] =msg=(E) tr[i])

About:
listassertnatural_numberless_thanapplyequalimpliesandallexists

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