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

At: decls mng singleton 1 1 1 1 2 1
1. l1: Label
2. d3: SimpleType
3. rho: Decl
4. s: l:Labelif l = l1 [[d3]] rho else Top fi
5. x1: Label
6. x: if x1 = l1 [[d3]] rho else Top fi
7. lbl: Label
8. d2: SimpleType
9. < lbl,d2 > = < l1,d3 > dec()
10. lbl = l1
11. d2 = d3
12. x1 = lbl

x [[d2]] rho
By: Subst (x1 ~ l1) 6
Generated subgoals:

1 x1 = l1
26. x: if l1 = l1 [[d3]] rho else Top fi
7. lbl: Label
8. d2: SimpleType
9. < lbl,d2 > = < l1,d3 > dec()
10. lbl = l1
11. d2 = d3
12. x1 = lbl
x [[d2]] rho

About:
pairifthenelseassertfunctionequalmembersqequaltop

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