**Term Rewriting System** *R*:

**[***x*, *y*]

minus(minus(*x*)) -> *x*

minux(+(*x*, *y*)) -> +(minus(*y*), minus(*x*))

+(minus(*x*), +(*x*, *y*)) -> *y*

+(+(*x*, *y*), minus(*y*)) -> *x*

**Termination** of *R* to be shown.

R

↳**Dependency Pair Analysis**

*R* contains the following *Dependency Pairs:
*

MINUX(+(*x*, *y*)) -> +'(minus(*y*), minus(*x*))

MINUX(+(*x*, *y*)) -> MINUS(*y*)

MINUX(+(*x*, *y*)) -> MINUS(*x*)

*R* contains **no** SCCs.

**Termination** of *R* successfully shown.

Duration:

0:00 minutes