is mentioned by

Def ioa_mentions_trace(A) == (e:eff(). e A.eff & mentions_trace(e.smt.term)) (p:pre(). p A.pre & rel_mentions_trace(p.rel)) (r:rel(). r A.init & rel_mentions_trace(r))	[ioa_mentions_trace]
Def tc_smt(s;ds;da;de) == mk_dec(s.lbl, s.typ) ds & s.typ term_types(ds;da;de;s.term)	[tc_smt]

In prior sections: mb automata 2

Try larger context: GenAutomata