is mentioned by

Thm* M:sm{i:l}(), l1,l2:M.action List, s,s':M.state. trace_reachable(M;s;l1 @ l2;s') (x:M.state. trace_reachable(M;s;l1;x) & trace_reachable(M;x;l2;s'))	[trace_reachable_append]
Def (M -tr- > s) == s0:M.state. M.init(s0) & trace_reachable(M;s0;tr;s)	[reachable_via]
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]
Def (f o M) == mk_sm(M.da o f, M.ds, M.init, s1,a,s2. l:Label. kind(a) = f(l) & M.trans(s1, < l,value(a) > ,s2))	[sm_a_rename]

In prior sections: core fun 1 int 2 mb nat num thy 1 mb list 1

Try larger context: GenAutomata