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

At: strong switch inv decomposable 1
1. E: TaggedEventStruct
2. tr: |E| List
3. switch_inv(E)(tr)
4. Causal(E)(tr)
5. AD-normal(E)(tr)
6. No-dup-deliver(E)(tr)
7. tr = nil

Q:(||tr||Prop). (i:||tr||. Dec(Q(i))) & (i:||tr||. Q(i)) & (i:||tr||. Q(i) is-send(E)(tr[i])) & (i,j:||tr||. Q(i) Q(j) tag(E)(tr[i]) = tag(E)(tr[j])) & (i,j:||tr||. Q(i) ij C(Q)(j))
By: Assert (ls:||tr||. is-send(E)(tr[ls]) & (j:||tr||. ls < j is-send(E)(tr[j])))
Generated subgoals:

1 ls:||tr||. is-send(E)(tr[ls]) & (j:||tr||. ls < j is-send(E)(tr[j]))
28. ls:||tr||. is-send(E)(tr[ls]) & (j:||tr||. ls < j is-send(E)(tr[j]))
Q:(||tr||Prop). (i:||tr||. Dec(Q(i))) & (i:||tr||. Q(i)) & (i:||tr||. Q(i) is-send(E)(tr[i])) & (i,j:||tr||. Q(i) Q(j) tag(E)(tr[i]) = tag(E)(tr[j])) & (i,j:||tr||. Q(i) ij C(Q)(j))

About:
listnilassertdecidablenatural_numberless_thanapplyfunction
equalpropimpliesandallexists

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