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