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

At: switch normal exists 2 3 1
1. E: TaggedEventStruct
2. tr: |E| List
3. switch_inv(E)(tr)
4. No-dup-send(E)(tr)
5. L': |E| List
6. i:(||L'||-1). R_ad_normal(tr)(L'[i],L'[(i+1)])

swap adjacent[R_ad_normal(tr)(x,y)] = > delayableR(E) asyncR(E)
By:
((Unfolds [`rel_implies`;`rel_or`;`R_delayable`;`R_async`] 0) THEN (Unfold `swap_adjacent` 0) THEN (Reduce 0) THEN ExRepD THEN (AssertBY Dec(loc(E)(x[i]) = loc(E)(x[(i+1)]) & is-send(E)(x[i]) & is-send(E)(x[(i+1)]) is-send(E)(x[i]) & is-send(E)(x[(i+1)])) Auto) THEN (Unfold `decidable` -1) THEN (Analyze -1)) THENL [OrRight;OrLeft]
THEN
InstConcl [i]
THEN
SupposeNot
THEN
Analyze -4
THEN
Unfold `R_ad_normal` 0
THEN
Reduce 0
THEN
SimpConcl
THEN
SupposeNot
THEN
AllHyps (h.(Analyze h) THEN (Complete SimpConcl))
Generated subgoals:

None

About:
listassertdecidablenatural_numberaddsubtractapplyequalandorall

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