t:Term. term_free_vars((t)') ~ term_free_vars(t)
t,vs. term_free_vars(t) @ vs;nil;r.args)f.nil;f.nil;f.nil;v.[v];P.nil;x,y. x @ y;t)
is mentioned by
| Thm* t:Term. term_free_vars((t)') ~ term_free_vars(t) | [term_free_vars_addprime] |
| Def rel_free_vars(r) == reduce(t,vs. term_free_vars(t) @ vs;nil;r.args) | [rel_free_vars] |
| Def closed_term(t) == term_free_vars(t) = nil | [closed_term] |
Try larger context:
GenAutomata