t.term_subst2(as;t);r.args))t.(t)';r.args))t.unprime(t);r.args))t.term_subst(as;t);r.args))
nil ; a.as' [(f(a)) / map(f;as')] (recursive)
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] |
In prior sections: list 1 mb list 1 mb list 2 mb automata 1
Try larger context:
GenAutomata