termlist_eq(a.args;b.args)
Case of b; nil true ; x.xs false
x.xs Case of b
nil false
x'.xs' term_eq(x;x')termlist_eq(xs;xs')
(recursive)
is mentioned by
|
Def rel_eq(a;b) == eq_relname(a.name;b.name)termlist_eq(a.args;b.args) | [rel_eq] |
In prior sections: mb automata 2
Try larger context: GenAutomata