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

At: switch inv rel closure 1 1
1. E: TaggedEventStruct
2. tr: |E| List
3. ls: ||tr||
4. switch_inv(E)(tr)
5. i: ||tr||
6. j: ||tr||
7. i (switchR(tr)^*) ls
8. j (switchR(tr)^*) ls
9. x: ||tr||
10. y: ||tr||
11. x switchR(tr) y

tag(E)(tr[x]) = tag(E)(tr[y])
By:
Auto
THEN
Try ((Unfold `switch_inv_rel` -1) THEN (Reduce -1) THEN (Complete Auto))
Generated subgoal:

1 tag(E)(tr[x]) = tag(E)(tr[y])

About:
listnatural_numberapplyequal

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