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

At: switch inv rel closure lemma1

E:EventStruct, tr:|E| List, ls:||tr||. is-send(E)(tr[ls]) (j:||tr||. ls < j is-send(E)(tr[j])) (i,j:||tr||. ij is-send(E)(tr[j]) (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls))
By: RepeatFor 5 (Analyze 0)
Generated subgoal:

11. 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])
i,j:||tr||. ij is-send(E)(tr[j]) (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls)

About:
listassertnatural_numberless_thanapplyimpliesall

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