is mentioned by

Thm* r1,r2:rel(), ds,daa:Collection(dec()), da:Collection(SimpleType), de:sig(), rho:Decl, e:{[[de]] rho}, s1,s2:{[[ds]] rho}, a:[[da]] rho, tr:trace_env([[daa]] rho). trace_consistent_rel(rho;daa;tr.proj;r1) trace_consistent_rel(rho;daa;tr.proj;r2) tc(r1;ds;da;de) tc(r2;ds;da;de) r1.name = r2.name ||r1.args|| = ||r2.args|| (i:. i < ||r1.args|| [[r1.args[i]]] 1of(e) s1 a tr = [[r2.args[i]]] 1of(e) s1 s2 a tr [[rel_arg_typ(r1.name;i;de)]] rho) ([[r1]] rho ds da de e s1 a tr rel_mng_2(r2; rho; ds; da; de; e; s1; s2; a; tr))	[rel_mng_2_iff]
Thm* r:rel(), i:, ds,da:Collection(dec()), st1:Collection(SimpleType), de:sig(), rho:Decl, s:{[[ds]] rho}, e:{1of([[de]] rho)}, a:[[st1]] rho, tr:trace_env([[da]] rho). trace_consistent_rel(rho;da;tr.proj;r) tc(r;ds;st1;de) i < ||r.args|| [[r.args[i]]] e s a tr [[rel_arg_typ(r.name;i;de)]] rho	[rel_arg_typing]
Thm* r:rel(), i:, ds,da:Collection(dec()), st1:Collection(SimpleType), de:sig(), rho:Decl, s,s':{[[ds]] rho}, e:{1of([[de]] rho)}, a:[[st1]] rho, tr:trace_env([[da]] rho). trace_consistent_rel(rho;da;tr.proj;r) tc(r;ds;st1;de) i < ||r.args|| [[r.args[i]]] e s s' a tr [[rel_arg_typ(r.name;i;de)]] rho	[rel_arg_typing2]

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

Try larger context: GenAutomata