Certification Problem
Input (TPDB TRS_Standard/Mixed_TRS/Ex1_Luc04b_GM)
The rewrite relation of the following TRS is considered.
| a__nats |
→ |
cons(0,incr(nats)) |
(1) |
| a__pairs |
→ |
cons(0,incr(odds)) |
(2) |
| a__odds |
→ |
a__incr(a__pairs) |
(3) |
|
a__incr(cons(X,XS)) |
→ |
cons(s(mark(X)),incr(XS)) |
(4) |
|
a__head(cons(X,XS)) |
→ |
mark(X) |
(5) |
|
a__tail(cons(X,XS)) |
→ |
mark(XS) |
(6) |
|
mark(nats) |
→ |
a__nats |
(7) |
|
mark(pairs) |
→ |
a__pairs |
(8) |
|
mark(odds) |
→ |
a__odds |
(9) |
|
mark(incr(X)) |
→ |
a__incr(mark(X)) |
(10) |
|
mark(head(X)) |
→ |
a__head(mark(X)) |
(11) |
|
mark(tail(X)) |
→ |
a__tail(mark(X)) |
(12) |
|
mark(0) |
→ |
0 |
(13) |
|
mark(s(X)) |
→ |
s(mark(X)) |
(14) |
|
mark(nil) |
→ |
nil |
(15) |
|
mark(cons(X1,X2)) |
→ |
cons(mark(X1),X2) |
(16) |
| a__nats |
→ |
nats |
(17) |
| a__pairs |
→ |
pairs |
(18) |
| a__odds |
→ |
odds |
(19) |
|
a__incr(X) |
→ |
incr(X) |
(20) |
|
a__head(X) |
→ |
head(X) |
(21) |
|
a__tail(X) |
→ |
tail(X) |
(22) |
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
| [a__nats] |
= |
0 |
| [cons(x1, x2)] |
= |
2 · x1 + 2 · x2
|
| [0] |
= |
0 |
| [incr(x1)] |
= |
2 · x1
|
| [nats] |
= |
0 |
| [a__pairs] |
= |
0 |
| [odds] |
= |
0 |
| [a__odds] |
= |
0 |
| [a__incr(x1)] |
= |
2 · x1
|
| [s(x1)] |
= |
1 · x1
|
| [mark(x1)] |
= |
2 · x1
|
| [a__head(x1)] |
= |
1 + 1 · x1
|
| [a__tail(x1)] |
= |
1 + 2 · x1
|
| [pairs] |
= |
0 |
| [head(x1)] |
= |
1 + 1 · x1
|
| [tail(x1)] |
= |
1 + 2 · x1
|
| [nil] |
= |
0 |
all of the following rules can be deleted.
|
a__head(cons(X,XS)) |
→ |
mark(X) |
(5) |
|
a__tail(cons(X,XS)) |
→ |
mark(XS) |
(6) |
|
mark(head(X)) |
→ |
a__head(mark(X)) |
(11) |
|
mark(tail(X)) |
→ |
a__tail(mark(X)) |
(12) |
1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [a__nats] |
= |
0 |
| [cons(x1, x2)] |
= |
2 · x1 + 2 · x2
|
| [0] |
= |
0 |
| [incr(x1)] |
= |
2 · x1
|
| [nats] |
= |
0 |
| [a__pairs] |
= |
0 |
| [odds] |
= |
0 |
| [a__odds] |
= |
0 |
| [a__incr(x1)] |
= |
2 · x1
|
| [s(x1)] |
= |
1 · x1
|
| [mark(x1)] |
= |
2 · x1
|
| [pairs] |
= |
0 |
| [nil] |
= |
0 |
| [a__head(x1)] |
= |
1 + 1 · x1
|
| [head(x1)] |
= |
1 · x1
|
| [a__tail(x1)] |
= |
2 + 1 · x1
|
| [tail(x1)] |
= |
2 + 1 · x1
|
all of the following rules can be deleted.
|
a__head(X) |
→ |
head(X) |
(21) |
1.1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [a__nats] |
= |
0 |
| [cons(x1, x2)] |
= |
2 · x1 + 2 · x2
|
| [0] |
= |
0 |
| [incr(x1)] |
= |
2 · x1
|
| [nats] |
= |
0 |
| [a__pairs] |
= |
0 |
| [odds] |
= |
0 |
| [a__odds] |
= |
0 |
| [a__incr(x1)] |
= |
2 · x1
|
| [s(x1)] |
= |
1 · x1
|
| [mark(x1)] |
= |
2 · x1
|
| [pairs] |
= |
0 |
| [nil] |
= |
0 |
| [a__tail(x1)] |
= |
1 + 1 · x1
|
| [tail(x1)] |
= |
1 · x1
|
all of the following rules can be deleted.
|
a__tail(X) |
→ |
tail(X) |
(22) |
1.1.1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [a__nats] |
= |
0 |
| [cons(x1, x2)] |
= |
2 · x1 + 2 · x2
|
| [0] |
= |
0 |
| [incr(x1)] |
= |
2 · x1
|
| [nats] |
= |
0 |
| [a__pairs] |
= |
0 |
| [odds] |
= |
0 |
| [a__odds] |
= |
0 |
| [a__incr(x1)] |
= |
2 · x1
|
| [s(x1)] |
= |
1 · x1
|
| [mark(x1)] |
= |
2 · x1
|
| [pairs] |
= |
0 |
| [nil] |
= |
1 |
all of the following rules can be deleted.
1.1.1.1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [a__nats] |
= |
2 |
| [cons(x1, x2)] |
= |
1 · x1 + 1 · x2
|
| [0] |
= |
0 |
| [incr(x1)] |
= |
2 · x1
|
| [nats] |
= |
1 |
| [a__pairs] |
= |
0 |
| [odds] |
= |
0 |
| [a__odds] |
= |
0 |
| [a__incr(x1)] |
= |
2 · x1
|
| [s(x1)] |
= |
1 · x1
|
| [mark(x1)] |
= |
2 · x1
|
| [pairs] |
= |
0 |
all of the following rules can be deleted.
1.1.1.1.1.1 Dependency Pair Transformation
The following set of initial dependency pairs has been identified.
| a__odds# |
→ |
a__incr#(a__pairs) |
(23) |
| a__odds# |
→ |
a__pairs# |
(24) |
|
a__incr#(cons(X,XS)) |
→ |
mark#(X) |
(25) |
|
mark#(nats) |
→ |
a__nats# |
(26) |
|
mark#(pairs) |
→ |
a__pairs# |
(27) |
|
mark#(odds) |
→ |
a__odds# |
(28) |
|
mark#(incr(X)) |
→ |
a__incr#(mark(X)) |
(29) |
|
mark#(incr(X)) |
→ |
mark#(X) |
(30) |
|
mark#(s(X)) |
→ |
mark#(X) |
(31) |
|
mark#(cons(X1,X2)) |
→ |
mark#(X1) |
(32) |
1.1.1.1.1.1.1 Dependency Graph Processor
The dependency pairs are split into 1
component.