mb automata 3 Sections GenAutomata Doc

Def [[rn]] rho e == Case(rn) Case eq(Q) = > x,y. x = y [[Q]] rho Case R = > e.R Default = > True

is mentioned by

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)[rel_mng_2]
Def [[r]] rho ds da de e s a tr == list_accum(x,t.x([[t]] 1of(e) s a tr);[[r.name]] rho 2of(e) ;r.args)[rel_mng]

Try larger context: GenAutomata

mb automata 3 Sections GenAutomata Doc