Certification Problem

Input (TPDB TRS_Standard/Endrullis_06/pair3hard)

The rewrite relation of the following TRS is considered.

p(a(x0),p(x1,p(x2,x3))) → p(x1,p(x0,p(a(x3),x3))) (1)

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.
p#(a(x0),p(x1,p(x2,x3))) → p#(x1,p(x0,p(a(x3),x3))) (2)
p#(a(x0),p(x1,p(x2,x3))) → p#(x0,p(a(x3),x3)) (3)
p#(a(x0),p(x1,p(x2,x3))) → p#(a(x3),x3) (4)

1.1 Reduction Pair Processor

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(p) = 1 weight(p) = 1
in combination with the following argument filter

π(p#) = 2
π(p) = [2]

the pairs
p#(a(x0),p(x1,p(x2,x3))) → p#(x0,p(a(x3),x3)) (3)
p#(a(x0),p(x1,p(x2,x3))) → p#(a(x3),x3) (4)
could be deleted.

1.1.1 Forward Instantiation Processor

We instantiate the pair to the following set of pairs
p#(a(x0),p(a(y_0),p(x2,x3))) → p#(a(y_0),p(x0,p(a(x3),x3))) (5)

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

We obtain the set of labeled pairs
p#10(a0(x0),p10(a0(y_0),p00(x2,x3))) → p#10(a0(y_0),p00(x0,p10(a0(x3),x3))) (6)
p#10(a0(x0),p10(a0(y_0),p01(x2,x3))) → p#10(a0(y_0),p00(x0,p11(a1(x3),x3))) (7)
p#10(a0(x0),p10(a0(y_0),p10(x2,x3))) → p#10(a0(y_0),p00(x0,p10(a0(x3),x3))) (8)
p#10(a0(x0),p10(a0(y_0),p11(x2,x3))) → p#10(a0(y_0),p00(x0,p11(a1(x3),x3))) (9)
p#10(a0(x0),p10(a1(y_0),p00(x2,x3))) → p#10(a1(y_0),p00(x0,p10(a0(x3),x3))) (10)
p#10(a0(x0),p10(a1(y_0),p01(x2,x3))) → p#10(a1(y_0),p00(x0,p11(a1(x3),x3))) (11)
p#10(a0(x0),p10(a1(y_0),p10(x2,x3))) → p#10(a1(y_0),p00(x0,p10(a0(x3),x3))) (12)
p#10(a0(x0),p10(a1(y_0),p11(x2,x3))) → p#10(a1(y_0),p00(x0,p11(a1(x3),x3))) (13)
p#10(a1(x0),p10(a0(y_0),p00(x2,x3))) → p#10(a0(y_0),p10(x0,p10(a0(x3),x3))) (14)
p#10(a1(x0),p10(a0(y_0),p01(x2,x3))) → p#10(a0(y_0),p10(x0,p11(a1(x3),x3))) (15)
p#10(a1(x0),p10(a0(y_0),p10(x2,x3))) → p#10(a0(y_0),p10(x0,p10(a0(x3),x3))) (16)
p#10(a1(x0),p10(a0(y_0),p11(x2,x3))) → p#10(a0(y_0),p10(x0,p11(a1(x3),x3))) (17)
p#10(a1(x0),p10(a1(y_0),p00(x2,x3))) → p#10(a1(y_0),p10(x0,p10(a0(x3),x3))) (18)
p#10(a1(x0),p10(a1(y_0),p01(x2,x3))) → p#10(a1(y_0),p10(x0,p11(a1(x3),x3))) (19)
p#10(a1(x0),p10(a1(y_0),p10(x2,x3))) → p#10(a1(y_0),p10(x0,p10(a0(x3),x3))) (20)
p#10(a1(x0),p10(a1(y_0),p11(x2,x3))) → p#10(a1(y_0),p10(x0,p11(a1(x3),x3))) (21)
and the set of labeled rules:
p10(a0(x0),p00(x1,p00(x2,x3))) → p00(x1,p00(x0,p10(a0(x3),x3))) (22)
p10(a0(x0),p00(x1,p01(x2,x3))) → p00(x1,p00(x0,p11(a1(x3),x3))) (23)
p10(a0(x0),p00(x1,p10(x2,x3))) → p00(x1,p00(x0,p10(a0(x3),x3))) (24)
p10(a0(x0),p00(x1,p11(x2,x3))) → p00(x1,p00(x0,p11(a1(x3),x3))) (25)
p10(a0(x0),p10(x1,p00(x2,x3))) → p10(x1,p00(x0,p10(a0(x3),x3))) (26)
p10(a0(x0),p10(x1,p01(x2,x3))) → p10(x1,p00(x0,p11(a1(x3),x3))) (27)
p10(a0(x0),p10(x1,p10(x2,x3))) → p10(x1,p00(x0,p10(a0(x3),x3))) (28)
p10(a0(x0),p10(x1,p11(x2,x3))) → p10(x1,p00(x0,p11(a1(x3),x3))) (29)
p10(a1(x0),p00(x1,p00(x2,x3))) → p00(x1,p10(x0,p10(a0(x3),x3))) (30)
p10(a1(x0),p00(x1,p01(x2,x3))) → p00(x1,p10(x0,p11(a1(x3),x3))) (31)
p10(a1(x0),p00(x1,p10(x2,x3))) → p00(x1,p10(x0,p10(a0(x3),x3))) (32)
p10(a1(x0),p00(x1,p11(x2,x3))) → p00(x1,p10(x0,p11(a1(x3),x3))) (33)
p10(a1(x0),p10(x1,p00(x2,x3))) → p10(x1,p10(x0,p10(a0(x3),x3))) (34)
p10(a1(x0),p10(x1,p01(x2,x3))) → p10(x1,p10(x0,p11(a1(x3),x3))) (35)
p10(a1(x0),p10(x1,p10(x2,x3))) → p10(x1,p10(x0,p10(a0(x3),x3))) (36)
p10(a1(x0),p10(x1,p11(x2,x3))) → p10(x1,p10(x0,p11(a1(x3),x3))) (37)

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.