is mentioned by

Def rel_arg_typ(rn;i;de) == Case(rn) Case eq(Q) = > Q Case R = > (de.rel(R))[i] Default = > False	[rel_arg_typ]
Def tc1(r;de) == Case(r.name) Case eq(Q) = > ||r.args|| = 2 Case R = > ||de.rel(R)|| = ||r.args|| Default = > False	[tc1]
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)	[st_eq]
Def ts_case(x) var(a)= > v(a) var'(b)= > p(b) opr(f)= > op(f) fvar(x)= > f(x) trace(P)= > t(P) end_ts_case == Case(x) Case ts_var(a) = > v(a) Case ts_pvar(b) = > p(b) Case ts_op(f) = > op(f) Case ts_fvar(x) = > f(x) Case ts_trace(P) = > t(P) Default = >	[ts_case]

In prior sections: mb basic mb tree

Try larger context: GenAutomata