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

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

d = d {d:dec()| d ds1 }
By:
Analyze -2
THEN
Analyze
Generated subgoal:

17. d: dec()
8. d ds2
9. d.lbl = x
d ds1

About:
assertsetisectapplyequalimpliesall

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