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

At: sigma decls mng2 1 1 1 1 1
1. da: Collection(dec())
2. rho: Decl
3. k: Label
4. w: [[dec_lookup(da;k)]] rho
5. d: {d:dec()| d da }

w [[d]] rho(k)
By: Analyze -1
Generated subgoal:

15. d: dec()
6. d da
w [[d]] rho(k)

About:
setapplymember

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