Certification Problem
Input (TPDB TRS_Standard/AProVE_04/IJCAR_1)
The rewrite relation of the following TRS is considered.
|
div(0,y) |
→ |
0 |
(1) |
|
div(x,y) |
→ |
quot(x,y,y) |
(2) |
|
quot(0,s(y),z) |
→ |
0 |
(3) |
|
quot(s(x),s(y),z) |
→ |
quot(x,y,z) |
(4) |
|
quot(x,0,s(z)) |
→ |
s(div(x,s(z))) |
(5) |
Property / Task
Prove or disprove termination.Answer / Result
Yes.Proof (by AProVE @ termCOMP 2023)
1 Dependency Pair Transformation
The following set of initial dependency pairs has been identified.
|
div#(x,y) |
→ |
quot#(x,y,y) |
(6) |
|
quot#(s(x),s(y),z) |
→ |
quot#(x,y,z) |
(7) |
|
quot#(x,0,s(z)) |
→ |
div#(x,s(z)) |
(8) |
1.1 Reduction Pair Processor with Usable Rules
Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
| prec(s) |
= |
0 |
|
weight(s) |
= |
1 |
|
|
|
in combination with the following argument filter
| π(div#) |
= |
1 |
| π(quot#) |
= |
1 |
| π(s) |
= |
[1] |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pair
|
quot#(s(x),s(y),z) |
→ |
quot#(x,y,z) |
(7) |
could be deleted.
1.1.1 Reduction Pair Processor with Usable Rules
Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
| prec(0) |
= |
1 |
|
weight(0) |
= |
2 |
|
|
|
| prec(s) |
= |
0 |
|
weight(s) |
= |
1 |
|
|
|
in combination with the following argument filter
| π(div#) |
= |
2 |
| π(quot#) |
= |
2 |
| π(0) |
= |
[] |
| π(s) |
= |
[] |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pair
|
quot#(x,0,s(z)) |
→ |
div#(x,s(z)) |
(8) |
could be deleted.
1.1.1.1 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
|
div#(x,y) |
→ |
quot#(x,y,y) |
(6) |
|
|
| 1 |
≥ |
1 |
| 2 |
≥ |
2 |
| 2 |
≥ |
3 |
As there is no critical graph in the transitive closure, there are no infinite chains.