(6steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc

At: member dec lookup


ds:Collection(dec()), x:Label, T:SimpleType. T dec_lookup(ds;x) mk_dec(x, T) ds

By:
Unfold `dec_lookup` 0
THEN
RW ColMemberC 0
THEN
ExRepD


Generated subgoals:

11. ds: Collection(dec())
2. x: Label
3. T: SimpleType
4. d: dec()
5. d ds
6. d.lbl = x
7. T = d.typ
mk_dec(x, T) ds
21. ds: Collection(dec())
2. x: Label
3. T: SimpleType
4. mk_dec(x, T) ds
d:dec(). d ds & d.lbl = x & T = d.typ

About:
assertequalandallexists

(6steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc