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

At: sigma decls mng value 1
1. ds: Collection(dec())
2. rho: Decl
3. l: Label
4. a1: [[ds]] rho(l)

a1 [[dec_lookup(ds;l)]] rho
By:
All (Unfold `sts_mng`)
THEN
Analyze
THEN
Analyze -1
Generated subgoal:

15. x: SimpleType
6. x dec_lookup(ds;l)
a1 [[x]] rho

About:
applymember

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