(13steps)
PrintForm
Definitions
mb
automata
3
Sections
GenAutomata
Doc
At:
decls
mng
rename
member
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 }
v
[[d]] rho(y)
By:
Decide d.lbl =
y
Generated subgoals:
1
9.
d.lbl =
y
v
[[d]] rho(y)
2
9.
d.lbl =
y
v
[[d]] rho(y)
About:
(13steps)
PrintForm
Definitions
mb
automata
3
Sections
GenAutomata
Doc
y
v 
[[d]] rho(y)
d.lbl = y v [[d]] rho(y)
d:{d:dec()| d ds1 }. [[d]] rho(x)
d:dec(). d ds2 
d.lbl = y mk_dec(x, d.typ) ds1 ds2 } v [[d]] rho(y) y y v [[d]] rho(y)d.lbl = y v [[d]] rho(y)
