Certification Problem

Input (TPDB TRS_Standard/Endrullis_06/pair2simple2)

The rewrite relation of the following TRS is considered.

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

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 pair
p#(a(x0),p(a(a(a(x1))),x2)) → p#(a(a(b(x0))),x2) (3)
could be deleted.

1.1.1 Reduction Pair Processor

Using the
prec(a) = 1 stat(a) = lex
prec(p) = 2 stat(p) = lex
prec(b) = 0 stat(b) = lex

π(p#) = 2
π(a) = [1]
π(p) = [2,1]
π(b) = []

the pair
p#(a(x0),p(a(a(a(x1))),x2)) → p#(a(x2),p(a(a(b(x0))),x2)) (2)
could be deleted.

1.1.1.1 P is empty

There are no pairs anymore.