is mentioned by

Def smts_eff_pred(ss;p) == (rp.smts_eff_rel(ss;r))

[smts_eff_pred]

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

Try larger context: GenAutomata