**Term Rewriting System** *R*:

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

(*x*, *x*) -> e

(e, *x*) -> *x*

(*x*, .(*x*, *y*)) -> *y*

(/(*x*, *y*), *x*) -> *y*

/(*x*, *x*) -> e

/(*x*, e) -> *x*

/(.(*y*, *x*), *x*) -> *y*

/(*x*, (*y*, *x*)) -> *y*

.(e, *x*) -> *x*

.(*x*, e) -> *x*

.(*x*, (*x*, *y*)) -> *y*

.(/(*y*, *x*), *x*) -> *y*

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

R

↳**Dependency Pair Analysis**

*R* contains **no** *Dependency Pairs* and therefore no SCCs.

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

Duration:

0:00 minutes