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

At: member dec lookup 1 1 1
1. ds: Collection(dec())
2. x: Label
3. T: SimpleType
4. lbl: Label
5. d1: SimpleType
6. < lbl,d1 > ds
7. lbl = x
8. T = d1

mk_dec(x, T) = < lbl,d1 >
By:
Fold `mk_dec` 0
THEN
Analyze
Generated subgoal:

1 x = lbl

About:
pairassertequal

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