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

At: switch inv rel closure send 1 2
1. E: EventStruct
2. tr: |E| List
3. ls: ||tr||
4. i: ||tr||
5. is-send(E)(tr[ls])
6. i (switchR(tr)^*) ls
7. x,y:||tr||. (x (switchR(tr)^*) y) is-send(E)(tr[x]) x = y

is-send(E)(tr[i])
By:
InstHyp [i;ls] -1
THEN
SplitOrHyps
Generated subgoal:

18. i = ls
is-send(E)(tr[i])

About:
listassertnatural_numberapplyequalimpliesorall

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