(5steps)
PrintForm
Definitions
Lemmas
mb
automata
3
Sections
GenAutomata
Doc
At:
decls
mng
functionality
sigma
ds1,ds2:Collection(dec()), rho:Decl, r:(
[[ds1]] rho). ds1 = ds2
r
(
[[ds2]] rho)
By:
Unfold `sigma` 0
THEN
UnivCD
Generated subgoal:
1
1.
ds1:
Collection(dec())
2.
ds2:
Collection(dec())
3.
rho:
Decl
4.
r:
l:Label
decl_type([[ds1]] rho;l)
5.
ds1 = ds2
r
l:Label
decl_type([[ds2]] rho;l)
About:
(5steps)
PrintForm
Definitions
Lemmas
mb
automata
3
Sections
GenAutomata
Doc