Certification Problem
Input (TPDB SRS_Standard/Zantema_04/z091)
The rewrite relation of the following TRS is considered.
|
r0(0(x1)) |
→ |
0(r0(x1)) |
(1) |
|
r0(1(x1)) |
→ |
1(r0(x1)) |
(2) |
|
r0(m(x1)) |
→ |
m(r0(x1)) |
(3) |
|
r1(0(x1)) |
→ |
0(r1(x1)) |
(4) |
|
r1(1(x1)) |
→ |
1(r1(x1)) |
(5) |
|
r1(m(x1)) |
→ |
m(r1(x1)) |
(6) |
|
r0(b(x1)) |
→ |
qr(0(b(x1))) |
(7) |
|
r1(b(x1)) |
→ |
qr(1(b(x1))) |
(8) |
|
0(qr(x1)) |
→ |
qr(0(x1)) |
(9) |
|
1(qr(x1)) |
→ |
qr(1(x1)) |
(10) |
|
m(qr(x1)) |
→ |
ql(m(x1)) |
(11) |
|
0(ql(x1)) |
→ |
ql(0(x1)) |
(12) |
|
1(ql(x1)) |
→ |
ql(1(x1)) |
(13) |
|
b(ql(0(x1))) |
→ |
0(b(r0(x1))) |
(14) |
|
b(ql(1(x1))) |
→ |
1(b(r1(x1))) |
(15) |
Property / Task
Prove or disprove termination.Answer / Result
Yes.Proof (by NaTT @ termCOMP 2023)
1 Dependency Pair Transformation
The following set of initial dependency pairs has been identified.
|
r0#(1(x1)) |
→ |
r0#(x1) |
(16) |
|
0#(qr(x1)) |
→ |
0#(x1) |
(17) |
|
1#(qr(x1)) |
→ |
1#(x1) |
(18) |
|
b#(ql(0(x1))) |
→ |
0#(b(r0(x1))) |
(19) |
|
b#(ql(0(x1))) |
→ |
r0#(x1) |
(20) |
|
r1#(0(x1)) |
→ |
0#(r1(x1)) |
(21) |
|
b#(ql(1(x1))) |
→ |
r1#(x1) |
(22) |
|
r0#(b(x1)) |
→ |
0#(b(x1)) |
(23) |
|
r1#(1(x1)) |
→ |
1#(r1(x1)) |
(24) |
|
r1#(0(x1)) |
→ |
r1#(x1) |
(25) |
|
r1#(b(x1)) |
→ |
1#(b(x1)) |
(26) |
|
m#(qr(x1)) |
→ |
m#(x1) |
(27) |
|
b#(ql(0(x1))) |
→ |
b#(r0(x1)) |
(28) |
|
1#(ql(x1)) |
→ |
1#(x1) |
(29) |
|
b#(ql(1(x1))) |
→ |
b#(r1(x1)) |
(30) |
|
r0#(m(x1)) |
→ |
r0#(x1) |
(31) |
|
r0#(0(x1)) |
→ |
r0#(x1) |
(32) |
|
b#(ql(1(x1))) |
→ |
1#(b(r1(x1))) |
(33) |
|
r0#(m(x1)) |
→ |
m#(r0(x1)) |
(34) |
|
r1#(m(x1)) |
→ |
m#(r1(x1)) |
(35) |
|
r0#(1(x1)) |
→ |
1#(r0(x1)) |
(36) |
|
0#(ql(x1)) |
→ |
0#(x1) |
(37) |
|
r1#(1(x1)) |
→ |
r1#(x1) |
(38) |
|
r1#(m(x1)) |
→ |
r1#(x1) |
(39) |
|
r0#(0(x1)) |
→ |
0#(r0(x1)) |
(40) |
1.1 Dependency Graph Processor
The dependency pairs are split into 6
components.
-
The
1st
component contains the
pair
|
b#(ql(1(x1))) |
→ |
b#(r1(x1)) |
(30) |
|
b#(ql(0(x1))) |
→ |
b#(r0(x1)) |
(28) |
1.1.1 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
| [0#(x1)] |
=
|
0 |
| [1(x1)] |
=
|
x1 + 2 |
| [b(x1)] |
=
|
x1 + 1 |
| [r0(x1)] |
=
|
x1 + 1 |
| [0(x1)] |
=
|
x1 + 2 |
| [ql(x1)] |
=
|
x1 + 0 |
| [r1#(x1)] |
=
|
0 |
| [r1(x1)] |
=
|
x1 + 1 |
| [r0#(x1)] |
=
|
0 |
| [m#(x1)] |
=
|
0 |
| [1#(x1)] |
=
|
0 |
| [b#(x1)] |
=
|
x1 + 0 |
| [qr(x1)] |
=
|
1 |
| [m(x1)] |
=
|
1 |
together with the usable
rules
|
r1(0(x1)) |
→ |
0(r1(x1)) |
(4) |
|
r1(b(x1)) |
→ |
qr(1(b(x1))) |
(8) |
|
r0(0(x1)) |
→ |
0(r0(x1)) |
(1) |
|
r0(m(x1)) |
→ |
m(r0(x1)) |
(3) |
|
r1(1(x1)) |
→ |
1(r1(x1)) |
(5) |
|
1(qr(x1)) |
→ |
qr(1(x1)) |
(10) |
|
r0(b(x1)) |
→ |
qr(0(b(x1))) |
(7) |
|
0(ql(x1)) |
→ |
ql(0(x1)) |
(12) |
|
m(qr(x1)) |
→ |
ql(m(x1)) |
(11) |
|
0(qr(x1)) |
→ |
qr(0(x1)) |
(9) |
|
1(ql(x1)) |
→ |
ql(1(x1)) |
(13) |
|
r1(m(x1)) |
→ |
m(r1(x1)) |
(6) |
|
r0(1(x1)) |
→ |
1(r0(x1)) |
(2) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
|
b#(ql(1(x1))) |
→ |
b#(r1(x1)) |
(30) |
|
b#(ql(0(x1))) |
→ |
b#(r0(x1)) |
(28) |
could be deleted.
1.1.1.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
2nd
component contains the
pair
|
r1#(0(x1)) |
→ |
r1#(x1) |
(25) |
|
r1#(m(x1)) |
→ |
r1#(x1) |
(39) |
|
r1#(1(x1)) |
→ |
r1#(x1) |
(38) |
1.1.2 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
| [0#(x1)] |
=
|
0 |
| [1(x1)] |
=
|
x1 + 1 |
| [b(x1)] |
=
|
1 |
| [r0(x1)] |
=
|
x1 + 37046 |
| [0(x1)] |
=
|
x1 + 1 |
| [ql(x1)] |
=
|
x1 + 0 |
| [r1#(x1)] |
=
|
x1 + 0 |
| [r1(x1)] |
=
|
x1 + 21680 |
| [r0#(x1)] |
=
|
0 |
| [m#(x1)] |
=
|
0 |
| [1#(x1)] |
=
|
0 |
| [b#(x1)] |
=
|
0 |
| [qr(x1)] |
=
|
15922 |
| [m(x1)] |
=
|
x1 + 1 |
together with the usable
rules
|
r1(b(x1)) |
→ |
qr(1(b(x1))) |
(8) |
|
1(qr(x1)) |
→ |
qr(1(x1)) |
(10) |
|
r0(b(x1)) |
→ |
qr(0(b(x1))) |
(7) |
|
0(ql(x1)) |
→ |
ql(0(x1)) |
(12) |
|
0(qr(x1)) |
→ |
qr(0(x1)) |
(9) |
|
1(ql(x1)) |
→ |
ql(1(x1)) |
(13) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
|
r1#(0(x1)) |
→ |
r1#(x1) |
(25) |
|
r1#(m(x1)) |
→ |
r1#(x1) |
(39) |
|
r1#(1(x1)) |
→ |
r1#(x1) |
(38) |
could be deleted.
1.1.2.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
3rd
component contains the
pair
|
r0#(0(x1)) |
→ |
r0#(x1) |
(32) |
|
r0#(m(x1)) |
→ |
r0#(x1) |
(31) |
|
r0#(1(x1)) |
→ |
r0#(x1) |
(16) |
1.1.3 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
| [0#(x1)] |
=
|
0 |
| [1(x1)] |
=
|
x1 + 1 |
| [b(x1)] |
=
|
1 |
| [r0(x1)] |
=
|
x1 + 33138 |
| [0(x1)] |
=
|
x1 + 20977 |
| [ql(x1)] |
=
|
x1 + 0 |
| [r1#(x1)] |
=
|
0 |
| [r1(x1)] |
=
|
x1 + 57798 |
| [r0#(x1)] |
=
|
x1 + 0 |
| [m#(x1)] |
=
|
0 |
| [1#(x1)] |
=
|
0 |
| [b#(x1)] |
=
|
0 |
| [qr(x1)] |
=
|
1324 |
| [m(x1)] |
=
|
x1 + 1 |
together with the usable
rules
|
r1(b(x1)) |
→ |
qr(1(b(x1))) |
(8) |
|
1(qr(x1)) |
→ |
qr(1(x1)) |
(10) |
|
r0(b(x1)) |
→ |
qr(0(b(x1))) |
(7) |
|
0(ql(x1)) |
→ |
ql(0(x1)) |
(12) |
|
0(qr(x1)) |
→ |
qr(0(x1)) |
(9) |
|
1(ql(x1)) |
→ |
ql(1(x1)) |
(13) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
|
r0#(0(x1)) |
→ |
r0#(x1) |
(32) |
|
r0#(m(x1)) |
→ |
r0#(x1) |
(31) |
|
r0#(1(x1)) |
→ |
r0#(x1) |
(16) |
could be deleted.
1.1.3.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
4th
component contains the
pair
1.1.4 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
| [0#(x1)] |
=
|
0 |
| [1(x1)] |
=
|
x1 + 1 |
| [b(x1)] |
=
|
1 |
| [r0(x1)] |
=
|
x1 + 2 |
| [0(x1)] |
=
|
x1 + 1 |
| [ql(x1)] |
=
|
x1 + 0 |
| [r1#(x1)] |
=
|
0 |
| [r1(x1)] |
=
|
x1 + 2 |
| [r0#(x1)] |
=
|
0 |
| [m#(x1)] |
=
|
x1 + 0 |
| [1#(x1)] |
=
|
0 |
| [b#(x1)] |
=
|
0 |
| [qr(x1)] |
=
|
x1 + 1 |
| [m(x1)] |
=
|
x1 + 38145 |
together with the usable
rules
|
1(qr(x1)) |
→ |
qr(1(x1)) |
(10) |
|
0(ql(x1)) |
→ |
ql(0(x1)) |
(12) |
|
0(qr(x1)) |
→ |
qr(0(x1)) |
(9) |
|
1(ql(x1)) |
→ |
ql(1(x1)) |
(13) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
could be deleted.
1.1.4.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
5th
component contains the
pair
|
0#(ql(x1)) |
→ |
0#(x1) |
(37) |
|
0#(qr(x1)) |
→ |
0#(x1) |
(17) |
1.1.5 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
| [0#(x1)] |
=
|
x1 + 0 |
| [1(x1)] |
=
|
x1 + 1 |
| [b(x1)] |
=
|
1 |
| [r0(x1)] |
=
|
x1 + 2 |
| [0(x1)] |
=
|
x1 + 1 |
| [ql(x1)] |
=
|
x1 + 0 |
| [r1#(x1)] |
=
|
0 |
| [r1(x1)] |
=
|
x1 + 2 |
| [r0#(x1)] |
=
|
0 |
| [m#(x1)] |
=
|
0 |
| [1#(x1)] |
=
|
0 |
| [b#(x1)] |
=
|
0 |
| [qr(x1)] |
=
|
x1 + 1 |
| [m(x1)] |
=
|
x1 + 52182 |
together with the usable
rules
|
1(qr(x1)) |
→ |
qr(1(x1)) |
(10) |
|
0(ql(x1)) |
→ |
ql(0(x1)) |
(12) |
|
0(qr(x1)) |
→ |
qr(0(x1)) |
(9) |
|
1(ql(x1)) |
→ |
ql(1(x1)) |
(13) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
could be deleted.
1.1.5.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
6th
component contains the
pair
|
1#(qr(x1)) |
→ |
1#(x1) |
(18) |
|
1#(ql(x1)) |
→ |
1#(x1) |
(29) |
1.1.6 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
| [0#(x1)] |
=
|
0 |
| [1(x1)] |
=
|
x1 + 1 |
| [b(x1)] |
=
|
1 |
| [r0(x1)] |
=
|
x1 + 45991 |
| [0(x1)] |
=
|
x1 + 45990 |
| [ql(x1)] |
=
|
x1 + 1 |
| [r1#(x1)] |
=
|
0 |
| [r1(x1)] |
=
|
x1 + 8406 |
| [r0#(x1)] |
=
|
0 |
| [m#(x1)] |
=
|
0 |
| [1#(x1)] |
=
|
x1 + 0 |
| [b#(x1)] |
=
|
0 |
| [qr(x1)] |
=
|
x1 + 1 |
| [m(x1)] |
=
|
x1 + 1 |
together with the usable
rules
|
1(qr(x1)) |
→ |
qr(1(x1)) |
(10) |
|
0(ql(x1)) |
→ |
ql(0(x1)) |
(12) |
|
0(qr(x1)) |
→ |
qr(0(x1)) |
(9) |
|
1(ql(x1)) |
→ |
ql(1(x1)) |
(13) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
|
1#(qr(x1)) |
→ |
1#(x1) |
(18) |
|
1#(ql(x1)) |
→ |
1#(x1) |
(29) |
could be deleted.
1.1.6.1 Dependency Graph Processor
The dependency pairs are split into 0
components.