mb automata 4 Sections GenAutomata Doc

Def c1 c2 == x:T. x c1 x c2

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

mb automata 4 Sections GenAutomata Doc