mb automata 3 Sections GenAutomata Doc

Def term_eq(a;b) == Case(a) Case x;y = > Case(b) Case x';y' = > term_eq(x;x')term_eq(y;y') Case tree_leaf(x) = > false Default = > True Case tree_leaf(x) = > Case(b) Case x';y' = > false Case tree_leaf(x') = > (x=x') Default = > True Default = > True (recursive)

is mentioned

In prior sections: mb automata 2

Try larger context: GenAutomata

mb automata 3 Sections GenAutomata Doc