Nuprl - Pf switch_normal

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

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)])

swap adjacent[R_ad_normal(tr)(x,y)]^* preserves switch_inv(E)

By: BackThru Thm* P:(TProp), R:(TTProp). R preserves P R^* preserves P THEN Reduce 0 THEN Unfolds [`preserved_by`;`swap_adjacent`] 0 THEN Reduce 0 THEN ExRepD THEN SubstFor y 0 THEN Thin -1 THEN ThinVar `L\'' THEN Thin -4

Generated subgoal:

1 5. x: |E| List
6. switch_inv(E)(x)
7. i: (||x||-1)
8. R_ad_normal(tr)(x[i],x[(i+1)])
switch_inv(E)(swap(x;i;i+1))

About:

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