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

At: decls mng member 1
1. ds1: Collection(dec())
2. ds2: Collection(dec())
3. x: Label
4. rho: Decl
5. v: [[d]] rho for d {d:dec()| d ds1 }(x)
6. d:dec(). d ds2 d.lbl = x d ds1

v [[d]] rho for d {d:dec()| d ds2 }(x)
By:
All (Unfold `dall`)
THEN
All Reduce
Generated subgoal:

15. v: d:{d:dec()| d ds1 }. [[d]] rho(x)
6. d:dec(). d ds2 d.lbl = x d ds1
v (d:{d:dec()| d ds2 }. [[d]] rho(x))

About:
setisectapplyequalmemberimpliesall

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