PrintForm Definitions mb state machine Sections GenAutomata Doc

At: trace reachable wf

M:sm{i:l}(), l:M.action List, s,s':M.state. trace_reachable(M;s;l;s') Prop
By:
Analyze 0
THEN
Analyze 0
THEN
ListInd -1
THEN
RecUnfold `trace_reachable` 0
THEN
Reduce 0
THEN
Easy
Generated subgoals:

None

About:
listmemberpropall

PrintForm Definitions mb state machine Sections GenAutomata Doc