**Term Rewriting System** *R*:

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

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

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

.(i(*x*), *x*) -> 1

.(*x*, i(*x*)) -> 1

.(i(*y*), .(*y*, *z*)) -> *z*

.(*y*, .(i(*y*), *z*)) -> *z*

i(1) -> 1

i(i(*x*)) -> *x*

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

R

↳**Dependency Pair Analysis**

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

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

Duration:

0:00 minutes