(1) EquationalDependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,DA_STEIN] we result in the following initial EDP problem:
The TRS P consists of the following rules:

P(a, x) → P(b, g(a))
P(p(a, x), ext) → P(p(b, g(a)), ext)
P(p(a, x), ext) → P(b, g(a))

The TRS R consists of the following rules:

p(a, x) → p(b, g(a))
p(p(a, x), ext) → p(p(b, g(a)), ext)

The set E consists of the following equations:

p(x, y) == p(y, x)
p(p(x, y), z) == p(x, p(y, z))

The set E# consists of the following equations:

P(x, y) == P(y, x)
P(p(x, y), z) == P(x, p(y, z))

We have to consider all minimal (P,E#,R,E)-chains

(3) EDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Equational Dependency Graph [DA_STEIN] contains 1 SCC with 2 less nodes.

(5) EDPPoloProof (EQUIVALENT transformation)

We use the reduction pair processor [DA_STEIN] with a polynomial ordering [POLO]. All Dependency Pairs of this DP problem can be strictly oriented.

P(p(a, x), ext) → P(p(b, g(a)), ext)

With the implicit AFS we had to orient the following set of usable rules of R non-strictly.

p(a, x) → p(b, g(a))
p(p(a, x), ext) → p(p(b, g(a)), ext)

We had to orient the following equations of E# equivalently.

P(x, y) == P(y, x)
P(p(x, y), z) == P(x, p(y, z))

With the implicit AFS we had to orient the following usable equations of E equivalently.

p(p(x, y), z) == p(x, p(y, z))
p(x, y) == p(y, x)

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(P(x₁, x₂)) = 3·x₁ + 3·x₂   
POL(a) = 3   
POL(b) = 0   
POL(g(x₁)) = 2   
POL(p(x₁, x₂)) = x₁ + x₂   

(7) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,E#,R,E) chain.