(2steps)
PrintForm
Definitions
mb
state
machine
Sections
GenAutomata
Doc
At:
sm
init
wf
M:sm{i:l}(). M.init
M.state
Prop
By:
Unfolds [`sm`;`sm_state`] 0
Generated subgoal:
1
1.
M:
da:Decl
ds:Decl
({ds}
Prop)
({ds}
(
da)
{ds}
Prop)
M.init
{M.ds}
Prop
About:
(2steps)
PrintForm
Definitions
mb
state
machine
Sections
GenAutomata
Doc
ds:Decl({ds}
Prop)({ds}(
da){ds}Prop)
M.init 
{M.ds}Prop 
M:sm{i:l}(). M.init M.statePropds:Decl({ds}Prop)({ds}(da){ds}Prop) M.init {M.ds}Prop
