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

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

mk_dec(x, d.typ) = mk_dec(x, d.typ) {d:dec()| d ds1 }
By:
Fold `member` 0
THEN
Analyze -2
THEN
Analyze
Generated subgoal:

18. d: dec()
9. d ds2
10. d.lbl = y
mk_dec(x, d.typ) ds1

About:
assertsetisectapplyequalimpliesall

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