mb automata 3 Sections GenAutomata Doc

Def closed_rel(r) == rel_free_vars(r) = nil

is mentioned by

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]

Try larger context: GenAutomata

mb automata 3 Sections GenAutomata Doc