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