is mentioned by

Def smts_eff(ss;x) == smt_terms( < s ss | s.lbl = x > )	[smts_eff]
Def action_effect(a;es;fs) == < e.smt | e < e es | e.kind = a > > + < mk_smt(f.var, f.var, f.typ) | f < f fs | a f.acts > >	[action_effect]
Def dec_lookup(ds;x) == < d.typ | d < d ds | d.lbl = x > >	[dec_lookup]
Def action_pre(a;ps) == < p.rel | p < p ps | p.kind = a > >	[action_pre]
Def covers_var(A;x) == fr:frame(). fr < fr A.frame | fr.var = x > & (a:Label. (a fr.acts) (ef:eff(). ef < ef A.eff | ef.kind = a & ef.smt.lbl = x > ))	[covers_var]

In prior sections: mb collection

Try larger context: GenAutomata