is mentioned by

Thm* p:Fmla, rho:Decl, ds,daa:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(), s:{[[ds]] rho}, e:{[[de]] rho}, a1,a2:Top, tr:trace_env([[daa]] rho). trace_consistent_pred(rho;daa;tr.proj;p) tc_pred(p;ds;da1;de) closed_pred(p) ([[p]] rho ds da1 de e s a1 tr [[p]] rho ds da2 de e s a2 tr)	[closed_pred_mng]
Thm* r:rel(), rho:Decl, ds,daa:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(), s:{[[ds]] rho}, e:{[[de]] rho}, a1,a2:Top, tr:trace_env([[daa]] rho). trace_consistent_rel(rho;daa;tr.proj;r) tc(r;ds;da1;de) closed_rel(r) ([[r]] rho ds da1 de e s a1 tr [[r]] rho ds da2 de e s a2 tr)	[closed_rel_mng_2]

In prior sections: mb events mb automata 1 mb automata 2 mb automata 3 mb basic mb declaration

Try larger context: GenAutomata