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