GenAutomata Sections NuprlLIB Doc

Def trace_reachable(M;s;l;s') == Case of l; nil s = s' M.state ; a.l' x:M.state. M.trans(s,a,x) & trace_reachable(M;x;l';s') (recursive)

is mentioned

In prior sections: mb state machine mb automata 4


GenAutomata Sections NuprlLIB Doc