Certification Problem
Input (TPDB TRS_Innermost/Mixed_innermost/innermost2)
The rewrite relation of the following TRS is considered.
|
g(c,g(a(x),y)) |
→ |
g(f(a(b)),g(a(y),x)) |
(1) |
|
f(a(x)) |
→ |
c |
(2) |
|
a(b) |
→ |
d |
(3) |
The evaluation strategy is innermost.Property / Task
Prove or disprove termination.Answer / Result
Yes.Proof (by AProVE @ termCOMP 2023)
1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [g(x1, x2)] |
= |
2 · x1 + 2 · x2
|
| [c] |
= |
1 |
| [a(x1)] |
= |
1 + 1 · x1
|
| [f(x1)] |
= |
1 · x1
|
| [b] |
= |
0 |
| [d] |
= |
0 |
all of the following rules can be deleted.
1.1 Dependency Pair Transformation
The following set of initial dependency pairs has been identified.
|
g#(c,g(a(x),y)) |
→ |
g#(f(a(b)),g(a(y),x)) |
(4) |
|
g#(c,g(a(x),y)) |
→ |
f#(a(b)) |
(5) |
|
g#(c,g(a(x),y)) |
→ |
g#(a(y),x) |
(6) |
1.1.1 Dependency Graph Processor
The dependency pairs are split into 0
components.