Certification Problem
Input (TPDB TRS_Standard/AG01/#3.17a)
The rewrite relation of the following TRS is considered.
|
app(nil,k) |
→ |
k |
(1) |
|
app(l,nil) |
→ |
l |
(2) |
|
app(cons(x,l),k) |
→ |
cons(x,app(l,k)) |
(3) |
|
sum(cons(x,nil)) |
→ |
cons(x,nil) |
(4) |
|
sum(cons(x,cons(y,l))) |
→ |
sum(cons(plus(x,y),l)) |
(5) |
|
sum(app(l,cons(x,cons(y,k)))) |
→ |
sum(app(l,sum(cons(x,cons(y,k))))) |
(6) |
|
plus(0,y) |
→ |
y |
(7) |
|
plus(s(x),y) |
→ |
s(plus(x,y)) |
(8) |
|
sum(plus(cons(0,x),cons(y,l))) |
→ |
pred(sum(cons(s(x),cons(y,l)))) |
(9) |
|
pred(cons(s(x),nil)) |
→ |
cons(x,nil) |
(10) |
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
| [app(x1, x2)] |
= |
2 · x1 + 1 · x2
|
| [nil] |
= |
0 |
| [cons(x1, x2)] |
= |
1 · x1 + 1 · x2
|
| [sum(x1)] |
= |
1 · x1
|
| [plus(x1, x2)] |
= |
1 · x1 + 1 · x2
|
| [0] |
= |
2 |
| [s(x1)] |
= |
1 · x1
|
| [pred(x1)] |
= |
1 + 1 · x1
|
all of the following rules can be deleted.
|
plus(0,y) |
→ |
y |
(7) |
|
sum(plus(cons(0,x),cons(y,l))) |
→ |
pred(sum(cons(s(x),cons(y,l)))) |
(9) |
|
pred(cons(s(x),nil)) |
→ |
cons(x,nil) |
(10) |
1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [app(x1, x2)] |
= |
2 · x1 + 2 · x2
|
| [nil] |
= |
1 |
| [cons(x1, x2)] |
= |
1 · x1 + 1 · x2
|
| [sum(x1)] |
= |
1 · x1
|
| [plus(x1, x2)] |
= |
1 · x1 + 1 · x2
|
| [s(x1)] |
= |
1 · x1
|
all of the following rules can be deleted.
|
app(nil,k) |
→ |
k |
(1) |
|
app(l,nil) |
→ |
l |
(2) |
1.1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [app(x1, x2)] |
= |
2 · x1 + 1 · x2
|
| [cons(x1, x2)] |
= |
1 + 2 · x1 + 1 · x2
|
| [sum(x1)] |
= |
1 · x1
|
| [nil] |
= |
0 |
| [plus(x1, x2)] |
= |
1 · x1 + 1 · x2
|
| [s(x1)] |
= |
1 · x1
|
all of the following rules can be deleted.
|
app(cons(x,l),k) |
→ |
cons(x,app(l,k)) |
(3) |
|
sum(cons(x,cons(y,l))) |
→ |
sum(cons(plus(x,y),l)) |
(5) |
1.1.1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [sum(x1)] |
= |
1 · x1
|
| [cons(x1, x2)] |
= |
1 · x1 + 2 · x2
|
| [nil] |
= |
0 |
| [app(x1, x2)] |
= |
1 · x1 + 2 · x2
|
| [plus(x1, x2)] |
= |
2 + 2 · x1 + 2 · x2
|
| [s(x1)] |
= |
1 + 1 · x1
|
all of the following rules can be deleted.
|
plus(s(x),y) |
→ |
s(plus(x,y)) |
(8) |
1.1.1.1.1 Switch to Innermost Termination
The TRS is overlay and locally confluent:
10Hence, it suffices to show innermost termination in the following.
1.1.1.1.1.1 Dependency Pair Transformation
The following set of initial dependency pairs has been identified.
|
sum#(app(l,cons(x,cons(y,k)))) |
→ |
sum#(app(l,sum(cons(x,cons(y,k))))) |
(11) |
|
sum#(app(l,cons(x,cons(y,k)))) |
→ |
sum#(cons(x,cons(y,k))) |
(12) |
1.1.1.1.1.1.1 Dependency Graph Processor
The dependency pairs are split into 0
components.