mb
automata
2
Sections
GenAutomata
Doc
Def
rel_free_vars(r) == reduce(
t,vs. term_free_vars(t) @ vs;nil;r.args)
is mentioned by
Thm*
r:rel(). rel_free_vars((r)') = rel_free_vars(r)
[rel_free_vars_addprime]
Try larger context:
GenAutomata
mb
automata
2
Sections
GenAutomata
Doc
r:rel(). rel_free_vars((r)') = rel_free_vars(r)
t,vs. term_free_vars(t) @ vs;nil;r.args)
r:rel(). rel_free_vars((r)') = rel_free_vars(r)