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

At: member dec lookup 1 1
1. 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) = d
By:
Analyze 4
THEN
All Reduce
Generated subgoal:

14. lbl: Label
5. d1: SimpleType
6. < lbl,d1 > ds
7. lbl = x
8. T = d1
mk_dec(x, T) = < lbl,d1 >

About:
pairassertequal

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