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

Termination of R to be shown.

`   R`
`     ↳Overlay and local confluence Check`

The TRS is overlay and locally confluent (all critical pairs are trivially joinable).Hence, we can switch to innermost.

`   R`
`     ↳OC`
`       →TRS2`
`         ↳Dependency Pair Analysis`

R contains the following Dependency Pairs:

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

Furthermore, R contains one SCC.

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

Dependency Pairs:

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

Rule:

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

Strategy:

innermost

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

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

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

Dependency Pairs:

F01(f10(a, x), y) -> F00(x, f11(a, y))
F00(f11(a, x), y) -> F01(f10(x, f10(a, y)), a)
F00(f10(a, x), y) -> F00(x, f10(a, y))

Rules:

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

Strategy:

innermost

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_00(x1, x2)) =  x1 + x2 POL(f_10(x1, x2)) =  x1 + x2 POL(F_01(x1, x2)) =  x1 + x2 POL(a) =  0

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

The result of this processor delivers one new DP problem.

`   R`
`     ↳OC`
`       →TRS2`
`         ↳DPs`
`           →DP Problem 1`
`             ↳SemLab`
`             ...`
`               →DP Problem 3`
`                 ↳Unlabel`

Dependency Pairs:

F00(f11(a, x), y) -> F01(f10(x, f10(a, y)), a)
F00(f10(a, x), y) -> F00(x, f10(a, y))
F01(f10(a, x), y) -> F00(x, f11(a, y))

Rule:

none

Strategy:

innermost

Removed all semantic labels.

`   R`
`     ↳OC`
`       →TRS2`
`         ↳DPs`
`           →DP Problem 1`
`             ↳SemLab`
`             ...`
`               →DP Problem 4`
`                 ↳Remaining Obligation(s)`

The following remains to be proven:
Dependency Pairs:

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

Rule:

none

Strategy:

innermost

Termination of R could not be shown.
Duration:
0:02 minutes