is mentioned by

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)

[trace_reachable]

In prior sections: list 1 prog 1 mb basic mb nat num thy 1 mb list 1

Try larger context: GenAutomata