This variant of integer term rewrite systems results from the automatic translation of imperative programs in Java or C. Each line has the format f1(s1, ..., sn) -> f2(t1, ..., tm) [cond], where f1 and f2 are function symbols, s1, ..., sn, t1, ..., tm are arbitrary terms (in particular, t1, ..., tm can also be/contain arithmetic expressions in infix notation). The constraint cond is a conjunction of arithmetic expressions. Hence, an example system looks like this:
outer(x, r) -> inner(1, 1, x, r) [ x >= 0 && r <= 100000] inner(f, i, x, r) -> inner(f + i, i+1, x, r) [ i <= x ] inner(f, i, x, r) -> outer(x - 1, r + f) [ i > x ] g(cons(x, xs), y) -> g(xs, y + 1) h(xs, y) -> h(cons(0, xs), y - 1) [y > 0]Their semantics are defined by standard (constraint) top-level term rewriting. A rule l -> r [c] can be applied to a term t if there is a substitution σ such that lσ = t and cσ are valid in integer arithmetic. Thus, pre-defined arithmetic operations can always be evaluated, but rewriting is only allowed at the root position. Hence, defined subterms introduced in a right-hand side of a rule below the root are not evaluated. The application then results in the term rσ. So the system f(x) -> g(f(x)) would be considered terminating, because there is no possible infinite sequence of root rewrite steps.