st_eq(b;b') Default = > false Case tree_leaf(x) = > Case(s2) Case a';b' = > false Case tree_leaf(y) = > InjCase(x; x'. InjCase(y; y'. x' =
y'; b. false); a. InjCase(y; y'. false; b. true)) Default = > false Default = > false (recursive)
is mentioned
In prior sections: mb automata 1 mb automata 2