r:rel(), de:sig(), i:
. tc1(r;de) 
i < ||r.args|| rel_arg_typ(r.name;i;de) 
SimpleType
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
| Thm* r:rel(), de:sig(), i:. tc1(r;de) i < ||r.args|| rel_arg_typ(r.name;i;de) SimpleType | [rel_arg_typ_wf] |
| 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: mb automata 1
Try larger context:
GenAutomata