mb automata 1 Sections GenAutomata Doc

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 by

Thm* s1,s2:SimpleType. st_eq(s1;s2) s1 = s2[assert_st_eq]

Try larger context: GenAutomata

mb automata 1 Sections GenAutomata Doc