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

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

w (d:{d:dec()| d da }. [[d]] rho(k))
By: Analyze
Generated subgoal:

15. d: {d:dec()| d da }
w [[d]] rho(k)

About:
setisectapplymember

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