t.term_subst2(as;t);r.args))t.(t)';r.args))t.unprime(t);r.args))t.term_subst(as;t);r.args))is mentioned by
| Def rel_subst2(as;r) == mk_rel(r.name, map(t.term_subst2(as;t);r.args)) | [rel_subst2] |
| Def (r)' == mk_rel(r.name, map(t.(t)';r.args)) | [rel_addprime] |
| Def rel_unprime(r) == mk_rel(r.name, map(t.unprime(t);r.args)) | [rel_unprime] |
| Def rel_subst(as;r) == mk_rel(r.name, map(t.term_subst(as;t);r.args)) | [rel_subst] |
Try larger context:
GenAutomata