Certification Problem
Input (TPDB TRS_Standard/Zantema_05/z21)
The rewrite relation of the following TRS is considered.
|
f(f(a,b),x) |
→ |
f(a,f(a,x)) |
(1) |
|
f(f(b,a),x) |
→ |
f(b,f(b,x)) |
(2) |
|
f(x,f(y,z)) |
→ |
f(f(x,y),z) |
(3) |
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.
|
f#(f(a,b),x) |
→ |
f#(a,f(a,x)) |
(4) |
|
f#(f(a,b),x) |
→ |
f#(a,x) |
(5) |
|
f#(f(b,a),x) |
→ |
f#(b,f(b,x)) |
(6) |
|
f#(f(b,a),x) |
→ |
f#(b,x) |
(7) |
|
f#(x,f(y,z)) |
→ |
f#(f(x,y),z) |
(8) |
|
f#(x,f(y,z)) |
→ |
f#(x,y) |
(9) |
1.1 Monotonic Reduction Pair Processor
Using the linear polynomial interpretation over the naturals
| [f(x1, x2)] |
= |
1 · x1 + 1 · x2
|
| [a] |
= |
2 |
| [b] |
= |
2 |
| [f#(x1, x2)] |
= |
2 · x1 + 2 · x2
|
the
pairs
|
f#(f(a,b),x) |
→ |
f#(a,x) |
(5) |
|
f#(f(b,a),x) |
→ |
f#(b,x) |
(7) |
and
no rules
could be deleted.
1.1.1 Monotonic Reduction Pair Processor
Using the linear polynomial interpretation over the naturals
| [f(x1, x2)] |
= |
1 + 1 · x1 + 1 · x2
|
| [a] |
= |
0 |
| [b] |
= |
0 |
| [f#(x1, x2)] |
= |
2 · x1 + 2 · x2
|
the
pair
|
f#(x,f(y,z)) |
→ |
f#(x,y) |
(9) |
and
no rules
could be deleted.
1.1.1.1 Semantic Labeling Processor
The following interpretations form a
model
of the rules.
As carrier we take the set
{0,1}.
Symbols are labeled by the interpretation of their arguments using the interpretations
(modulo 2):
| [a] |
= |
0 |
| [b] |
= |
1 |
| [f(x1, x2)] |
= |
1x1
|
| [f#(x1, x2)] |
= |
0 |
We obtain the set of labeled pairs
|
f#00(f01(a,b),x) |
→ |
f#00(a,f00(a,x)) |
(10) |
|
f#00(x,f00(y,z)) |
→ |
f#00(f00(x,y),z) |
(11) |
|
f#00(x,f01(y,z)) |
→ |
f#01(f00(x,y),z) |
(12) |
|
f#01(x,f10(y,z)) |
→ |
f#00(f01(x,y),z) |
(13) |
|
f#01(x,f11(y,z)) |
→ |
f#01(f01(x,y),z) |
(14) |
|
f#10(x,f00(y,z)) |
→ |
f#10(f10(x,y),z) |
(15) |
|
f#10(x,f01(y,z)) |
→ |
f#11(f10(x,y),z) |
(16) |
|
f#11(x,f10(y,z)) |
→ |
f#10(f11(x,y),z) |
(17) |
|
f#11(x,f11(y,z)) |
→ |
f#11(f11(x,y),z) |
(18) |
|
f#01(f01(a,b),x) |
→ |
f#00(a,f01(a,x)) |
(19) |
|
f#10(f10(b,a),x) |
→ |
f#11(b,f10(b,x)) |
(20) |
|
f#11(f10(b,a),x) |
→ |
f#11(b,f11(b,x)) |
(21) |
and the set of labeled rules:
|
f00(f01(a,b),x) |
→ |
f00(a,f00(a,x)) |
(22) |
|
f01(f01(a,b),x) |
→ |
f00(a,f01(a,x)) |
(23) |
|
f10(f10(b,a),x) |
→ |
f11(b,f10(b,x)) |
(24) |
|
f11(f10(b,a),x) |
→ |
f11(b,f11(b,x)) |
(25) |
|
f00(x,f00(y,z)) |
→ |
f00(f00(x,y),z) |
(26) |
|
f00(x,f01(y,z)) |
→ |
f01(f00(x,y),z) |
(27) |
|
f01(x,f10(y,z)) |
→ |
f00(f01(x,y),z) |
(28) |
|
f01(x,f11(y,z)) |
→ |
f01(f01(x,y),z) |
(29) |
|
f10(x,f00(y,z)) |
→ |
f10(f10(x,y),z) |
(30) |
|
f10(x,f01(y,z)) |
→ |
f11(f10(x,y),z) |
(31) |
|
f11(x,f10(y,z)) |
→ |
f10(f11(x,y),z) |
(32) |
|
f11(x,f11(y,z)) |
→ |
f11(f11(x,y),z) |
(33) |
1.1.1.1.1 Dependency Graph Processor
The dependency pairs are split into 2
components.