is mentioned by

Thm* M:sm{i:l}(), P:(M.state(M.action List)Prop). (M |= always s,t.P(s,t)) (M |= s,t.P(s,t) while True) & (M |= initially s,t.P(s,t))	[trace_inv_as_while]
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]
Thm* M:sm{i:l}(), a:M.action. kind(a) Label & kind(a) Pattern	[kind_wf2]
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]

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

Try larger context: GenAutomata