(9steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

At: ioa all mng action 1 1 1 1 1

1. I: Type
2. A: Iioa{i:l}()
3. rho: Decl
4. de: sig()
5. e: {[[de]] rho}
6. s: l:Labeldecl_type([[ioa_all(I; i.A(i)).da]] rho;l)
7. i: I
8. l: Label
9. x: [[ioa_all(I; i.A(i)).da]] rho(l)
10. d: dec()
11. d A(i).da
12. d.lbl = l

d ioa_all(I; i.A(i)).da

By: Reduce 0

Generated subgoal:

1 d i:I. A(i).da

About:
productapplyfunctionuniverseequal

(9steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc