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

At: ioa all mng action 1
1. I: Type
2. A: Iioa{i:l}()
3. rho: Decl
4. de: sig()
5. e: {[[de]] rho}
6. s: ([[ioa_all(I; i.A(i)).da]] rho)
7. i: I

s [[A(i)]] rho de e.action
By:
Unfolds [`ioa_mng`] 0
THEN
Reduce 0
Generated subgoal:

1 s ([[A(i).da]] rho)

About:
functionuniversemember

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