mb automata 3 Sections GenAutomata Doc

Def rel_mng_2(r; rho; ds; da; de; e; s; s'; a; tr) == list_accum(x,t.x([[t]] 1of(e) s s' a tr);[[r.name]] rho 2of(e) ;r.args)

is mentioned by

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,da,de,e,s,s',a,tr:Top. rel_mng_2(rel_unprime(r); rho; ds; da; de; e; s; s'; a; tr) ~ [[r]] rho ds da de e s a tr[rel_mng_2_unprime]
Thm* r:rel(), rho,ds,da,de,e,s,s',a,tr:Top. rel_mng_2((r)'; rho; ds; da; de; e; s; s'; a; tr) ~ [[r]] rho ds da de e s' a tr[rel_mng_2_addprime]
Def pred_mng_2(p; rho; ds; da; de; e; s; s'; a; tr) == r:rel(). r p rel_mng_2(r; rho; ds; da; de; e; s; s'; a; tr)[pred_mng_2]

Try larger context: GenAutomata

mb automata 3 Sections GenAutomata Doc