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

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

tr adR(E) L'
By:
Unfold `R_ad` 0
THEN
BackThruLemma' Thm* R1,R2:(TTProp), x,y:T. R1 = > R2 (x (R1^*) y) (x (R2^*) y)
Generated subgoal:

16. i:(||L'||-1). R_ad_normal(tr)(L'[i],L'[(i+1)])
swap adjacent[R_ad_normal(tr)(x,y)] = > delayableR(E) asyncR(E)

About:
listnatural_numberaddsubtractapplyall

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