Rewrite (Calculemus)

Rewrite Module

Rewriting.

Function or value	Description
`rewrite eqs tm` Full Usage: `rewrite eqs tm` Parameters: eqs : `formula<fol> list` - The input list of equation. tm : `term` - The input term. Returns: `term` The input term with all its subterms rewritten at all and repeatedly w.r.t the input list of equations.	Normalize a term w.r.t. a set of equations. eqs : `formula<fol> list` The input list of equation. tm : `term` The input term. Returns: `term` The input term with all its subterms rewritten at all and repeatedly w.r.t the input list of equations. Example `!!!"S(S(S(0))) * S(S(0)) + S(S(S(S(0))))" \|> rewrite !!>[ "0 + x = x"; "S(x) + y = S(x + y)"; "0 * x = 0"; "S(x) * y = y + x * y" ]` Evaluates to ``S(S(S(S(S(S(S(S(S(S(0))))))))))``.
`rewrite1 eqs t` Full Usage: `rewrite1 eqs t` Parameters: eqs : `formula<fol> list` - The input list of equation. t : `term` - The input term. Returns: `term` The input term rewritten at the top level based on the first equation that succeeds to match.	Rewrites a term at the top level with the first element of an equation list that succeeds to match. eqs : `formula<fol> list` The input list of equation. t : `term` The input term. Returns: `term` The input term rewritten at the top level based on the first equation that succeeds to match. Example `rewrite1 !!>["g(c) = 0"; "f(f(x)) = x"] !!!"f(f(f(x)))"` Evaluates to ``f(x)``.