mb automata 2 Sections GenAutomata Doc

Def eq_relname(a;b) == Case(a) Case eq(x) = > Case(b) Case eq(x') = > st_eq(x;x') Case x' = > false Default = > false Case x = > Case(b) Case eq(x') = > false Case x' = > x = x' Default = > false Default = > false

is mentioned by

Thm* a,b:relname(). eq_relname(a;b) a = b[assert_eq_relname]

Try larger context: GenAutomata

mb automata 2 Sections GenAutomata Doc