YES
0 QTRS
↳1 DependencyPairsProof (⇔, 0 ms)
↳2 QDP
↳3 MRRProof (⇔, 0 ms)
↳4 QDP
↳5 QDPOrderProof (⇔, 28 ms)
↳6 QDP
↳7 PisEmptyProof (⇔, 0 ms)
↳8 YES
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)) = 2·x1 + x2
POL(a(x1)) = x1
POL(b(x1)) = x1
POL(p(x1, x2)) = 2 + 2·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 24.
POL(P(x1, x2)) = [4]x1 + x2
POL(a(x1)) = [4] + [4]x1
POL(b(x1)) = 0
POL(p(x1, x2)) = [2]x1 + [1/2]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)))