is mentioned by
Thm* p1,p2:Fmla, ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(). p2 p1 ds1 ds2 da1 da2 tc_pred(p1;ds1;da1;de) tc_pred(p2;ds2;da2;de) | [tc_pred_monotone] |
In prior sections: mb collection mb automata 2 mb automata 3
Try larger context:
GenAutomata