Termination w.r.t. Q of the given QTRS could be proven:

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

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

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

P(a(x0), p(a(b(x1)), x2)) → P(a(b(a(x2))), p(a(a(x1)), x2))
P(a(x0), p(a(b(x1)), x2)) → P(a(a(x1)), x2)

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(3) QDPSizeChangeProof (EQUIVALENT transformation)

We used the following order and afs together with the size-change analysis [AAECC05] to show that there are no infinite chains for this DP problem.

Order:Combined order from the following AFS and order.
p(x1, x2)  =  p(x1, x2)
a(x1)  =  x1
b(x1)  =  b(x1)

Recursive path order with status [RPO].
Quasi-Precedence:

[p₂, b₁]

Status:

p₂: [2,1]
b₁: [1]

AFS:
p(x1, x2)  =  p(x1, x2)
a(x1)  =  x1
b(x1)  =  b(x1)

From the DPs we obtained the following set of size-change graphs:

• P(a(x0), p(a(b(x1)), x2)) → P(a(b(a(x2))), p(a(a(x1)), x2)) (allowed arguments on rhs = {1, 2})
  The graph contains the following edges 2 > 2

• P(a(x0), p(a(b(x1)), x2)) → P(a(a(x1)), x2) (allowed arguments on rhs = {1, 2})
  The graph contains the following edges 2 > 1, 2 > 2

We oriented the following set of usable rules [AAECC05,FROCOS05].

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

(4) TRUE