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

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

is-send(E)(x[i]) loc(E)(x[i]) = loc(E)(x[(i+1)])
By:
Decide (is-send(E)(x[i]))
THEN
SimpConcl
Generated subgoal:

19. is-send(E)(x[i])
loc(E)(x[i]) = loc(E)(x[(i+1)])

About:
listassertnatural_numberaddsubtractapplyequalor

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