Certification Problem
Input (TPDB TRS_Standard/Zantema_05/z22)
The rewrite relation of the following TRS is considered.
|
f(f(f(a,b),c),x) |
→ |
f(b,f(a,f(c,f(b,x)))) |
(1) |
|
f(x,f(y,z)) |
→ |
f(f(x,y),z) |
(2) |
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(f(a,b),c),x) |
→ |
f#(b,f(a,f(c,f(b,x)))) |
(3) |
|
f#(f(f(a,b),c),x) |
→ |
f#(a,f(c,f(b,x))) |
(4) |
|
f#(f(f(a,b),c),x) |
→ |
f#(c,f(b,x)) |
(5) |
|
f#(f(f(a,b),c),x) |
→ |
f#(b,x) |
(6) |
|
f#(x,f(y,z)) |
→ |
f#(f(x,y),z) |
(7) |
|
f#(x,f(y,z)) |
→ |
f#(x,y) |
(8) |
1.1 Monotonic Reduction Pair Processor
Using the linear polynomial interpretation over the naturals
| [f(x1, x2)] |
= |
1 · x1 + 1 · x2
|
| [a] |
= |
1 |
| [b] |
= |
0 |
| [c] |
= |
0 |
| [f#(x1, x2)] |
= |
2 · x1 + 2 · x2
|
the
pairs
|
f#(f(f(a,b),c),x) |
→ |
f#(c,f(b,x)) |
(5) |
|
f#(f(f(a,b),c),x) |
→ |
f#(b,x) |
(6) |
and
no rules
could be deleted.
1.1.1 Reduction Pair Processor
Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
| prec(a) |
= |
1 |
|
weight(a) |
= |
1 |
|
|
|
| prec(b) |
= |
0 |
|
weight(b) |
= |
1 |
|
|
|
in combination with the following argument filter
| π(f#) |
= |
1 |
| π(f) |
= |
1 |
| π(a) |
= |
[] |
| π(b) |
= |
[] |
the
pair
|
f#(f(f(a,b),c),x) |
→ |
f#(b,f(a,f(c,f(b,x)))) |
(3) |
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] |
= |
1 |
| [b] |
= |
0 |
| [c] |
= |
0 |
| [f(x1, x2)] |
= |
0 |
| [f#(x1, x2)] |
= |
0 |
We obtain the set of labeled pairs
|
f#00(f00(f10(a,b),c),x) |
→ |
f#10(a,f00(c,f00(b,x))) |
(9) |
|
f#00(x,f00(y,z)) |
→ |
f#00(f00(x,y),z) |
(10) |
|
f#00(x,f01(y,z)) |
→ |
f#01(f00(x,y),z) |
(11) |
|
f#00(x,f10(y,z)) |
→ |
f#00(f01(x,y),z) |
(12) |
|
f#00(x,f11(y,z)) |
→ |
f#01(f01(x,y),z) |
(13) |
|
f#10(x,f00(y,z)) |
→ |
f#00(f10(x,y),z) |
(14) |
|
f#10(x,f01(y,z)) |
→ |
f#01(f10(x,y),z) |
(15) |
|
f#10(x,f10(y,z)) |
→ |
f#00(f11(x,y),z) |
(16) |
|
f#10(x,f11(y,z)) |
→ |
f#01(f11(x,y),z) |
(17) |
|
f#01(f00(f10(a,b),c),x) |
→ |
f#10(a,f00(c,f01(b,x))) |
(18) |
|
f#00(x,f00(y,z)) |
→ |
f#00(x,y) |
(19) |
|
f#00(x,f01(y,z)) |
→ |
f#00(x,y) |
(20) |
|
f#00(x,f10(y,z)) |
→ |
f#01(x,y) |
(21) |
|
f#00(x,f11(y,z)) |
→ |
f#01(x,y) |
(22) |
|
f#10(x,f00(y,z)) |
→ |
f#10(x,y) |
(23) |
|
f#10(x,f01(y,z)) |
→ |
f#10(x,y) |
(24) |
|
f#10(x,f10(y,z)) |
→ |
f#11(x,y) |
(25) |
|
f#10(x,f11(y,z)) |
→ |
f#11(x,y) |
(26) |
and the set of labeled rules:
|
f00(f00(f10(a,b),c),x) |
→ |
f00(b,f10(a,f00(c,f00(b,x)))) |
(27) |
|
f01(f00(f10(a,b),c),x) |
→ |
f00(b,f10(a,f00(c,f01(b,x)))) |
(28) |
|
f00(x,f00(y,z)) |
→ |
f00(f00(x,y),z) |
(29) |
|
f00(x,f01(y,z)) |
→ |
f01(f00(x,y),z) |
(30) |
|
f00(x,f10(y,z)) |
→ |
f00(f01(x,y),z) |
(31) |
|
f00(x,f11(y,z)) |
→ |
f01(f01(x,y),z) |
(32) |
|
f10(x,f00(y,z)) |
→ |
f00(f10(x,y),z) |
(33) |
|
f10(x,f01(y,z)) |
→ |
f01(f10(x,y),z) |
(34) |
|
f10(x,f10(y,z)) |
→ |
f00(f11(x,y),z) |
(35) |
|
f10(x,f11(y,z)) |
→ |
f01(f11(x,y),z) |
(36) |
1.1.1.1.1 Dependency Graph Processor
The dependency pairs are split into 1
component.