Term Rewriting System R:
[x, y, z, u, v]
f(f(x, y, z), u, f(x, y, v)) -> f(x, y, f(z, u, v))
f(x, y, y) -> y
f(x, y, g(y)) -> x
f(x, x, y) -> x
f(g(x), x, y) -> y
Innermost Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
F(f(x, y, z), u, f(x, y, v)) -> F(x, y, f(z, u, v))
F(f(x, y, z), u, f(x, y, v)) -> F(z, u, v)
Furthermore, R contains one SCC.
R
↳DPs
→DP Problem 1
↳Size-Change Principle
Dependency Pairs:
F(f(x, y, z), u, f(x, y, v)) -> F(z, u, v)
F(f(x, y, z), u, f(x, y, v)) -> F(x, y, f(z, u, v))
Rules:
f(f(x, y, z), u, f(x, y, v)) -> f(x, y, f(z, u, v))
f(x, y, y) -> y
f(x, y, g(y)) -> x
f(x, x, y) -> x
f(g(x), x, y) -> y
Strategy:
innermost
We number the DPs as follows:
- F(f(x, y, z), u, f(x, y, v)) -> F(z, u, v)
- F(f(x, y, z), u, f(x, y, v)) -> F(x, y, f(z, u, v))
and get the following Size-Change Graph(s): | {2, 1} | , | {2, 1} |
|---|
| 1 | > | 1 |
| 2 | = | 2 |
| 3 | > | 3 |
|
| {2, 1} | , | {2, 1} |
|---|
| 1 | > | 1 |
| 1 | > | 2 |
| 3 | > | 1 |
| 3 | > | 2 |
|
which lead(s) to this/these maximal multigraph(s): | {2, 1} | , | {2, 1} |
|---|
| 1 | > | 1 |
| 2 | = | 2 |
| 3 | > | 3 |
|
| {2, 1} | , | {2, 1} |
|---|
| 1 | > | 1 |
| 1 | > | 2 |
| 3 | > | 1 |
| 3 | > | 2 |
|
DP: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
We obtain no new DP problems.
Innermost Termination of R successfully shown.
Duration:
0:00 minutes