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

At: strong switch inv decomposable 1 2 1 1
1. E: TaggedEventStruct
2. tr: |E| List
3. Causal(E)(tr)
4. AD-normal(E)(tr)
5. No-dup-deliver(E)(tr)
6. tr = nil
7. ls: ||tr||
8. is-send(E)(tr[ls])
9. j:||tr||. ls < j is-send(E)(tr[j])
10. i:||tr||. (i (switchR(tr)^*) ls) is-send(E)(tr[i])
11. EquivRel(|E|)(_1 =msg=(E) _2)

i,j:||tr||. (i (switchR(tr)^*) ls) ij C(i.i (switchR(tr)^*) ls)(j)
By:
HideMentioning [`no_duplicate_send`]
THEN
Inst Thm* E:EventStruct, tr:|E| List, ls:||tr||. is-send(E)(tr[ls]) (j:||tr||. ls < j is-send(E)(tr[j])) (i,j:||tr||. ij is-send(E)(tr[j]) (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls)) [E;tr;ls]
THEN
Unfold `message_closure` 0
THEN
Reduce 0
THEN
InductionOnDifference
Generated subgoals:

112. i,j:||tr||. ij is-send(E)(tr[j]) (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls)
i,j:||tr||. 0 = j-i (i (switchR(tr)^*) ls) ij (k:||tr||. (k (switchR(tr)^*) ls) & (tr[k] =msg=(E) tr[j]))
212. i,j:||tr||. ij is-send(E)(tr[j]) (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls)
13. d:
14. 0 < d
15. i,j:||tr||. d-1 = j-i (i (switchR(tr)^*) ls) ij (k:||tr||. (k (switchR(tr)^*) ls) & (tr[k] =msg=(E) tr[j]))
i,j:||tr||. d = j-i (i (switchR(tr)^*) ls) ij (k:||tr||. (k (switchR(tr)^*) ls) & (tr[k] =msg=(E) tr[j]))

About:
listnilassertintnatural_numbersubtractless_thanlambda
applyequalimpliesandallexists

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