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

At: strong switch inv decomposable 1 2
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
8. 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))
By: ExRepD
Generated subgoal:

18. ls: ||tr||
9. is-send(E)(tr[ls])
10. 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