# Termination of deterministic term rewriting

Consider a simple language:

$$t ::= plus ~ t ~ t ~ | ~ gen ~ t ~ | ~ except ~ N ~ t ~ | ~ N$$

with N constructors plus, gen and except, N being the natural numbers, and $G = \{t_n\}$ a finite, ordered set of terms.

These terms can be evaluated using a small step operational semantics:

$$\frac{G ~ \vdash ~ t_1 \rightarrow t_2}{G ~ \vdash ~ plus ~ t_1 t_3 \rightarrow plus ~ t_2 ~ t_3}$$

$$\frac{G ~ \vdash ~ t_1 \rightarrow t_2}{G ~ \vdash ~ plus ~ n ~ t_1 \rightarrow plus ~ n ~ t_2}$$

$$\frac{}{G ~ \vdash ~ plus ~ n_1 ~ n_2 \rightarrow n_1 + n_2} \\ \text{using the addition on natural numbers}$$

$$\frac{G ~ \vdash ~ t_1 \rightarrow t_2}{G ~ \vdash ~ gen ~ t_1 \rightarrow gen ~ t_2}$$

$$\frac{}{\{t_n\} ~ \vdash ~ gen ~ n \rightarrow except ~ n ~ t_n}$$

$$\frac{G \setminus \{t_n\} ~ \vdash ~ t_1 \rightarrow t_2}{G ~ \vdash ~ except ~ n ~ t_1 \rightarrow except ~ n ~ t_2}$$

$$\frac{}{G ~ \vdash ~ except ~ n ~ m \rightarrow m}$$

The idea is that the stored terms in $G$ might be mutually recursive, but are not allowed to "loop". Hence, everytime, one term is selected from $G$, it is wrapped in an $except$ term that prevents such a loop.

It seems intuitive, that this system (i.e. a function that applies a rule as long as possible) always terminates. But is that so? How does one prove this? I tried to map the evaluation to a CPO, but failed so far.

The problem is proving the supremum of a directed chain: The term might grow and shrink. It may only grow however, when an except node is introduced, which reduces the allowed set $G$. So expansion is clearly limited. Any reduction clearly shrinks the term which is also limited. So I'd need a CPO defined as the product of these two orders that is not defined as usual.

Does anyone have an idea how to solve this?