Certification Problem

Input (TPDB TRS_Standard/Zantema_05/z19)

The rewrite relation of the following TRS is considered.

f(f(a,a),x) f(a,f(b,f(a,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(a,a),x) f#(a,f(b,f(a,x))) (3)
f#(f(a,a),x) f#(b,f(a,x)) (4)
f#(f(a,a),x) f#(a,x) (5)
f#(x,f(y,z)) f#(f(x,y),z) (6)
f#(x,f(y,z)) f#(x,y) (7)

1.1 Monotonic Reduction Pair Processor

Using the linear polynomial interpretation over the naturals
[f(x1, x2)] = 1 · x1 + 1 · x2
[a] = 2
[b] = 0
[f#(x1, x2)] = 2 · x1 + 2 · x2
the pairs
f#(f(a,a),x) f#(b,f(a,x)) (4)
f#(f(a,a),x) f#(a,x) (5)
and no rules could be deleted.

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
[f(x1, x2)] = 0
[f#(x1, x2)] = 0

We obtain the set of labeled pairs
f#00(f11(a,a),x) f#10(a,f00(b,f10(a,x))) (8)
f#00(x,f00(y,z)) f#00(f00(x,y),z) (9)
f#00(x,f01(y,z)) f#01(f00(x,y),z) (10)
f#00(x,f10(y,z)) f#00(f01(x,y),z) (11)
f#00(x,f11(y,z)) f#01(f01(x,y),z) (12)
f#10(x,f00(y,z)) f#00(f10(x,y),z) (13)
f#10(x,f01(y,z)) f#01(f10(x,y),z) (14)
f#10(x,f10(y,z)) f#00(f11(x,y),z) (15)
f#10(x,f11(y,z)) f#01(f11(x,y),z) (16)
f#01(f11(a,a),x) f#10(a,f00(b,f11(a,x))) (17)
f#00(x,f00(y,z)) f#00(x,y) (18)
f#00(x,f01(y,z)) f#00(x,y) (19)
f#00(x,f10(y,z)) f#01(x,y) (20)
f#00(x,f11(y,z)) f#01(x,y) (21)
f#10(x,f00(y,z)) f#10(x,y) (22)
f#10(x,f01(y,z)) f#10(x,y) (23)
f#10(x,f10(y,z)) f#11(x,y) (24)
f#10(x,f11(y,z)) f#11(x,y) (25)
and the set of labeled rules:
f00(f11(a,a),x) f10(a,f00(b,f10(a,x))) (26)
f01(f11(a,a),x) f10(a,f00(b,f11(a,x))) (27)
f00(x,f00(y,z)) f00(f00(x,y),z) (28)
f00(x,f01(y,z)) f01(f00(x,y),z) (29)
f00(x,f10(y,z)) f00(f01(x,y),z) (30)
f00(x,f11(y,z)) f01(f01(x,y),z) (31)
f10(x,f00(y,z)) f00(f10(x,y),z) (32)
f10(x,f01(y,z)) f01(f10(x,y),z) (33)
f10(x,f10(y,z)) f00(f11(x,y),z) (34)
f10(x,f11(y,z)) f01(f11(x,y),z) (35)

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.