is mentioned by

Thm* M:sm{i:l}(), f:(LabelLabel), s:(f o M).state. s M.state	[sm_a_rename_state]
Thm* M:sm{i:l}(), a:M.action. kind(a) Label & kind(a) Pattern	[kind_wf2]
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: mb label mb declaration mb record

Try larger context: GenAutomata