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

At: switch normal exists 2 1
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)])

switch_inv(E)(L')
By: Assert swap adjacent[R_ad_normal(tr)(x,y)]^* preserves switch_inv(E)
Generated subgoals:

1 swap adjacent[R_ad_normal(tr)(x,y)]^* preserves switch_inv(E)
28. swap adjacent[R_ad_normal(tr)(x,y)]^* preserves switch_inv(E)
switch_inv(E)(L')

About:
listnatural_numberaddsubtractapplyall

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