Term Rewriting System R:
[x]
f(f(x, a), a) -> f(f(f(a, f(a, a)), x), a)

Termination of R to be shown.

`   R`
`     ↳Dependency Pair Analysis`

R contains the following Dependency Pairs:

F(f(x, a), a) -> F(f(f(a, f(a, a)), x), a)
F(f(x, a), a) -> F(f(a, f(a, a)), x)
F(f(x, a), a) -> F(a, f(a, a))
F(f(x, a), a) -> F(a, a)

Furthermore, R contains one SCC.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Semantic Labelling`

Dependency Pair:

F(f(x, a), a) -> F(f(f(a, f(a, a)), x), a)

Rule:

f(f(x, a), a) -> f(f(f(a, f(a, a)), x), a)

Using Semantic Labelling, the DP problem could be transformed. The following model was found:
 F(x0, x1) =  0 f(x0, x1) =  1 a =  1

From the dependency graph we obtain 1 (labeled) SCCs which each result in correspondingDP problem.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳SemLab`
`           →DP Problem 2`
`             ↳Modular Removal of Rules`

Dependency Pair:

F11(f11(x, a), a) -> F11(f11(f11(a, f11(a, a)), x), a)

Rules:

f11(f01(x, a), a) -> f11(f10(f11(a, f11(a, a)), x), a)
f11(f11(x, a), a) -> f11(f11(f11(a, f11(a, a)), x), a)

We have the following set of usable rules: none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
 POL(f_11(x1, x2)) =  x1 + x2 POL(F_11(x1, x2)) =  1 + x1 + x2 POL(a) =  0

We have the following set D of usable symbols: {f11, F11, a}
No Dependency Pairs can be deleted.
2 non usable rules have been deleted.

The result of this processor delivers one new DP problem.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳SemLab`
`           →DP Problem 2`
`             ↳MRR`
`             ...`
`               →DP Problem 3`
`                 ↳Unlabel`

Dependency Pair:

F11(f11(x, a), a) -> F11(f11(f11(a, f11(a, a)), x), a)

Rule:

none

Removed all semantic labels.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳SemLab`
`           →DP Problem 2`
`             ↳MRR`
`             ...`
`               →DP Problem 4`
`                 ↳Instantiation Transformation`

Dependency Pair:

F(f(x, a), a) -> F(f(f(a, f(a, a)), x), a)

Rule:

none

On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule

F(f(x, a), a) -> F(f(f(a, f(a, a)), x), a)
one new Dependency Pair is created:

F(f(f(a, f(a, a)), a), a) -> F(f(f(a, f(a, a)), f(a, f(a, a))), a)

The transformation is resulting in no new DP problems.

Termination of R successfully shown.
Duration:
0:00 minutes