**Term Rewriting System** *R*:

**[***X*]

f(s(*X*), *X*) -> f(*X*, a(*X*))

f(*X*, c(*X*)) -> f(s(*X*), *X*)

f(*X*, *X*) -> c(*X*)

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

R

↳**Dependency Pair Analysis**

*R* contains the following *Dependency Pairs:
*

F(s(*X*), *X*) -> F(*X*, a(*X*))

F(*X*, c(*X*)) -> F(s(*X*), *X*)

*R* contains **no** SCCs.

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

Duration:

0:00 minutes