x,y. x = y 
[[Q]] rho Case R = > e.R Default = > True
Default = > false Case x = > Case(b) Case eq(x') = > false Case x' = > x =
x' Default = > false Default = > falsex1.inr(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x1])
is mentioned by
| Def [[rn]] rho e == Case(rn) Case eq(Q) = > x,y. x = y [[Q]] rho Case R = > e.R Default = > True | [relname_mng] |
| 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] |
In prior sections: mb automata 1
Try larger context:
GenAutomata