is mentioned by

Thm* r:rel(), ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc_pred( < r > ;ds;da;de) tc(r;ds;da;de)	[tc_pred_singleton]
Def tc_eff(ef;ds;de) == tc_smt(ef.smt;ds; < ef.typ > ;de)	[tc_eff]

In prior sections: mb automata 2 mb automata 3 mb automata 1

Try larger context: GenAutomata