is mentioned by

Def tc(r;ds;da;de) == Case(r.name) Case eq(Q) = > ||r.args|| = 2 & Q term_types(ds;da;de;r.args[0]) & Q term_types(ds;da;de;r.args[1]) Case R = > ||de.rel(R)|| = ||r.args|| & (i:. i < ||r.args|| (de.rel(R))[i] term_types(ds;da;de;r.args[i])) Default = > False	[tc]
Def [[s]] rho == < op.[[s.fun(op)]] rho,R.[[s.rel(R)]] rho >	[sig_mng]

In prior sections: mb automata 1

Try larger context: GenAutomata