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

Innermost Termination of R to be shown.

`   R`
`     ↳Dependency Pair Analysis`

R contains the following Dependency Pairs:

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

Furthermore, R contains one SCC.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Usable Rules (Innermost)`

Dependency Pair:

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

Rule:

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

Strategy:

innermost

As we are in the innermost case, we can delete all 1 non-usable-rules.

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

Dependency Pair:

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

Rule:

none

Strategy:

innermost

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

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

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

Dependency Pair:

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

Rule:

none

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)) =  1 + 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, f00, f10, a}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

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

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.

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