t,vs. term_free_vars(t) @ vs;nil;r.args)s,m. [[s]] rho
m;Prop;l)t,vs. term_vars(t) @ vs;nil;r.args)
k ; a.as' f(a,reduce(f;k;as')) (recursive)
is mentioned by
| Def rel_free_vars(r) == reduce(t,vs. term_free_vars(t) @ vs;nil;r.args) | [rel_free_vars] |
| Def [[l]] rho == reduce(s,m. [[s]] rhom;Prop;l) | [st_list_mng] |
| Def rel_vars(r) == reduce(t,vs. term_vars(t) @ vs;nil;r.args) | [rel_vars] |
In prior sections: mb list 2 list 1 mb list 1 mb label
Try larger context:
GenAutomata