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

At: switch inv rel closure lemma1 1 2
1. E: EventStruct
2. tr: |E| List
3. ls: ||tr||
4. is-send(E)(tr[ls])
5. j:||tr||. ls < j is-send(E)(tr[j])
6. n:, i,j:||tr||. ij is-send(E)(tr[i]) is-send(E)(tr[j]) (i switchR(tr)^n ls) (j (switchR(tr)^*) ls)

i,j:||tr||. ij is-send(E)(tr[j]) (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls)
By:
Auto
THEN
Unfold `rel_star` -1
THEN
Reduce -1
THEN
ExRepD
Generated subgoal:

17. i: ||tr||
8. j: ||tr||
9. ij
10. is-send(E)(tr[j])
11. n:
12. i switchR(tr)^n ls
j (switchR(tr)^*) ls

About:
listassertnatural_numberless_thanapplyimpliesall

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