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

At: sigma decls mng value2 1 1 2
1. ds: Collection(dec())
2. rho: Decl
3. a: ([[ds]] rho)
4. x: Label
5. mk_dec(kind(a), x) ds
6. value(a) [[dec_lookup(ds;kind(a))]] rho

value(a) [[x]] rho
By: BackThru Thm* sts:Collection(SimpleType), rho:Decl, v:[[sts]] rho, s:SimpleType. s sts v [[s]] rho
Generated subgoal:

1 x dec_lookup(ds;kind(a))

About:
member

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