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

At: P causal iff 1
1. 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)
By: AssertBY (||tr'||||tr||) (BackThru Thm* l1,l2:T List. l1 l2 ||l1||||l2||)
Generated subgoal:

110. ||tr'||||tr||
y:|E|. (i:. i < ||tr'|| & y = tr'[i]) & is-send(E)(y) & (y =msg=(E) x)

About:
listassertnatural_numberless_thanapplyequalandallexists

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