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 [[d]] rho == Case(d) Case x : s = > x:[[s]] rho	[dec_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]
Def st_app1(s1;s2) == Case(s1) Case a;b = > if st_eq(a;s2) < b > else < > fi Default = > < >	[st_app1]
Def term_eq(a;b) == Case(a) Case x;y = > Case(b) Case x';y' = > term_eq(x;x')term_eq(y;y') Case tree_leaf(x) = > false Default = > True Case tree_leaf(x) = > Case(b) Case x';y' = > false Case tree_leaf(x') = > (x=x') Default = > True Default = > True (recursive)	[term_eq]
Def vc_concl(v) == Case(v) Case vc_imp(x) = > x.concl Case vc_qimp(x) = > x.concl Default = > False	[vc_concl]
Def vc_hyp(v) == Case(v) Case vc_imp(x) = > x.hyp Case vc_qimp(x) = > x.hyp Default = > False	[vc_hyp]

In prior sections: mb basic mb tree mb automata 1

Try larger context: GenAutomata