Certification Problem

Input (TPDB TRS_Standard/Endrullis_06/pair3rotate)

The rewrite relation of the following TRS is considered.

p(a(x0),p(b(x1),p(a(x2),x3)))

→

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

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

p^#(a(x0),p(b(x1),p(a(x2),x3))) → p^#(a(a(x0)),p(b(x1),x3)) (3)

p^#(a(x0),p(b(x1),p(a(x2),x3))) → p^#(x2,p(a(a(x0)),p(b(x1),x3))) (2)

1.1.1 Monotonic Reduction Pair Processor
Using the linear polynomial interpretation over the naturals

[p(x₁, x₂)] = 2 + 2 · x₁ + 1 · x₂

[a(x₁)] = 1 · x₁

[b(x₁)] = 2 · x₁

[p^#(x₁, x₂)] = 2 · x₁ + 1 · x₂

the pair
p^#(a(x0),p(b(x1),p(a(x2),x3))) → p^#(a(a(x0)),p(b(x1),x3)) (3)
and no rules could be deleted.
1.1.1.1 Reduction Pair Processor
Using the linear polynomial interpretation over the rationals with delta = 192

[p^#(x₁, x₂)] = 0 + 4 · x₁ + 4 · x₂

[a(x₁)] = 4 + 1/4 · x₁

[p(x₁, x₂)] = 0 + 4 · x₁ + 4 · x₂

[b(x₁)] = 0 + 0 · x₁

the pair
p^#(a(x0),p(b(x1),p(a(x2),x3))) → p^#(x2,p(a(a(x0)),p(b(x1),x3))) (2)
could be deleted.
1.1.1.1.1 P is empty

There are no pairs anymore.