(7steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc

At: decls mng subtype 1 2
1. ds: Collection(dec())
2. rho: Decl
3. x: Label
4. y: d:{d:dec()| d ds }. [[d]] rho(x)
5. a: SimpleType
6. mk_dec(x, a) ds
7. y [[mk_dec(x, a)]] rho(x)

y [[a]] rho
By:
Unfold `dec_mng` -1
THEN
Unfold `dbase` -1
THEN
Reduce -1
Generated subgoal:

17. y if x = x [[a]] rho else Top fi
y [[a]] rho

About:
setisectapplymember

(7steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc