0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 MRRProof (⇔)
↳4 QDP
↳5 QDPOrderProof (⇔)
↳6 QDP
↳7 PisEmptyProof (⇔)
↳8 TRUE
p(a(a(x0)), p(x1, p(a(x2), x3))) → p(x2, p(a(a(b(x1))), p(a(a(x0)), x3)))
P(a(a(x0)), p(x1, p(a(x2), x3))) → P(x2, p(a(a(b(x1))), p(a(a(x0)), x3)))
P(a(a(x0)), p(x1, p(a(x2), x3))) → P(a(a(b(x1))), p(a(a(x0)), x3))
P(a(a(x0)), p(x1, p(a(x2), x3))) → P(a(a(x0)), x3)
p(a(a(x0)), p(x1, p(a(x2), x3))) → p(x2, p(a(a(b(x1))), p(a(a(x0)), x3)))
P(a(a(x0)), p(x1, p(a(x2), x3))) → P(a(a(b(x1))), p(a(a(x0)), x3))
P(a(a(x0)), p(x1, p(a(x2), x3))) → P(a(a(x0)), x3)
POL(P(x1, x2)) = x1 + x2
POL(a(x1)) = x1
POL(b(x1)) = x1
POL(p(x1, x2)) = 1 + x1 + x2
P(a(a(x0)), p(x1, p(a(x2), x3))) → P(x2, p(a(a(b(x1))), p(a(a(x0)), x3)))
p(a(a(x0)), p(x1, p(a(x2), x3))) → p(x2, p(a(a(b(x1))), p(a(a(x0)), x3)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P(a(a(x0)), p(x1, p(a(x2), x3))) → P(x2, p(a(a(b(x1))), p(a(a(x0)), x3)))
The value of delta used in the strict ordering is 3/8.
POL(P(x1, x2)) = x1 + (2)x2
POL(a(x1)) = 1/4 + (4)x1
POL(p(x1, x2)) = (1/4)x1 + (1/2)x2
POL(b(x1)) = 0
p(a(a(x0)), p(x1, p(a(x2), x3))) → p(x2, p(a(a(b(x1))), p(a(a(x0)), x3)))
p(a(a(x0)), p(x1, p(a(x2), x3))) → p(x2, p(a(a(b(x1))), p(a(a(x0)), x3)))