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

At: P causal iff 2 1
1. 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||

firstn(i+1;tr) tr
By:
RWO "firstn_is_iseg" 0
THEN
InstConcl [i+1]
Generated subgoals:

None

About:
listassertnatural_numberaddless_thanapplyequalimpliesandallexists

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