(10steps)
PrintForm
Definitions
mb
automata
3
Sections
GenAutomata
Doc
At:
decls
mng
member
1
1
1
1.
ds1:
Collection(dec())
2.
ds2:
Collection(dec())
3.
x:
Label
4.
rho:
Decl
5.
v:
d:{d:dec()| d
ds1 }. [[d]] rho(x)
6.
d:dec(). d
ds2
d.lbl = x
d
ds1
7.
d:
{d:dec()| d
ds2 }
v
[[d]] rho(x)
By:
Decide d.lbl =
x
Generated subgoals:
1
8.
d.lbl =
x
v
[[d]] rho(x)
2
8.
d.lbl =
x
v
[[d]] rho(x)
About:
(10steps)
PrintForm
Definitions
mb
automata
3
Sections
GenAutomata
Doc
x
v 
[[d]] rho(x)
d.lbl = x v [[d]] rho(x)
d:{d:dec()| d ds1 }. [[d]] rho(x)
d:dec(). d ds2 
d.lbl = x d ds1 ds2 } v [[d]] rho(x) x x v [[d]] rho(x)d.lbl = x v [[d]] rho(x)
