s1,s2,s:SimpleType. s 
st_app1(s1;s2) 
st_eq(s1;s2
s)
Default = > false Case x = > Case(b) Case eq(x') = > false Case x' = > x =
x' Default = > false Default = > false
< b > else < > fi Default = > < > 
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,s:SimpleType. s st_app1(s1;s2) st_eq(s1;s2s) | [member_st_app1] |
| Def eq_relname(a;b) == Case(a) Case eq(x) = > Case(b) Case eq(x') = > st_eq(x;x') Case x' = > false Default = > false Case x = > Case(b) Case eq(x') = > false Case x' = > x = x' Default = > false Default = > false | [eq_relname] |
| Def st_app1(s1;s2) == Case(s1) Case a;b = > if st_eq(a;s2) < b > else < > fi Default = > < > | [st_app1] |
In prior sections: mb automata 1
Try larger context:
GenAutomata