Def st_eq(s1;s2) == Case(s1) Case a;b = > Case(s2) Case a';b' = > st_eq(a;a')
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
Try larger context:
GenAutomata