is mentioned by

Thm* M:sm{i:l}(), I:(M.state(M.action List)Prop). (x:M.state. M.init(x) I(x,nil)) (s0,x:M.state, act:M.action, x':M.state, l:M.action List. M.init(s0) trace_reachable(M;s0;l;x) I(x,l) M.trans(x,act,x') I(x',l @ [act])) (M |= always s,t.I(s,t))	[trace_inv_induction]
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, s,s':M.state. trace_reachable(M;s;[a];s') M.trans(s,a,s')	[trace_reachable_one]
Def (M |= always s,t.P(s;t)) == t:M.action List, s0,s:M.state. M.init(s0) trace_reachable(M;s0;t;s) P(s;t)	[trace_inv]
Def (M -tr- > s) == s0:M.state. M.init(s0) & trace_reachable(M;s0;tr;s)	[reachable_via]

Try larger context: GenAutomata