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

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

tr':|E| List. switch_inv(E)(tr') & AD-normal(E)(tr') & (tr adR(E) tr')
By:
ParallelOp -1
THEN
Try (Fold `trace_property` 0)
Generated subgoals:

15. 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)])
switch_inv(E)(L')
25. 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)])
AD-normal(E)(L')
35. 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'

About:
listnatural_numberaddsubtractapplyandallexists

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