Thm* r:rel(), ds:Collection(dec()), da1,da2:Collection(SimpleType), de:sig().
closed_rel(r)  tc(r;ds;da1;de)  tc(r;ds;da2;de) | [tc_closed_rel] |
Thm* r:rel(), rho,ds,da1,da2,de,s,s',e,a1,a2,tr:Top.
closed_rel(r) 
(rel_mng_2(r; rho; ds; da1; de; e; s; s'; a1; tr) ~ rel_mng_2
(r; rho; ds; da2; de; e; s; s'; a2; tr)) | [closed_rel_mng2] |
Thm* r:rel(), rho,ds,da1,da2,de,s,e,a1,a2,tr:Top.
closed_rel(r)  ([[r]] rho ds da1 de e s a1 tr ~ [[r]] rho ds da2 de e s a2 tr) | [closed_rel_mng_sq] |
Thm* r:rel(), i: . closed_rel(r)  i < ||r.args||  closed_term(r.args[i]) | [closed_rel_args] |
Def closed_pred(p) == r:rel(). r p  closed_rel(r) | [closed_pred] |