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

At: decls mng subtype 1 2 1
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 if x = x [[a]] rho else Top fi

y [[a]] rho
By: EqLblReflexive -1
Generated subgoals:

None

About:
ifthenelsesetisectapplymembertop

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