YES
0 QTRS
↳1 DependencyPairsProof (⇔, 0 ms)
↳2 QDP
↳3 QDPOrderProof (⇔, 0 ms)
↳4 QDP
↳5 TransformationProof (⇔, 0 ms)
↳6 QDP
↳7 SemLabProof (⇒, 103 ms)
↳8 QDP
↳9 DependencyGraphProof (⇔, 0 ms)
↳10 AND
↳11 QDP
↳12 QDPOrderProof (⇔, 0 ms)
↳13 QDP
↳14 PisEmptyProof (⇔, 0 ms)
↳15 YES
↳16 QDP
↳17 QDPOrderProof (⇔, 0 ms)
↳18 QDP
↳19 PisEmptyProof (⇔, 0 ms)
↳20 YES
p(a(x0), p(x1, p(x2, x3))) → p(x1, p(x0, p(a(x3), x3)))
P(a(x0), p(x1, p(x2, x3))) → P(x1, p(x0, p(a(x3), x3)))
P(a(x0), p(x1, p(x2, x3))) → P(x0, p(a(x3), x3))
P(a(x0), p(x1, p(x2, x3))) → P(a(x3), x3)
p(a(x0), p(x1, p(x2, x3))) → p(x1, p(x0, p(a(x3), x3)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P(a(x0), p(x1, p(x2, x3))) → P(x0, p(a(x3), x3))
P(a(x0), p(x1, p(x2, x3))) → P(a(x3), x3)
trivial
dummyConstant=1
p_1=1
p(a(x0), p(x1, p(x2, x3))) → p(x1, p(x0, p(a(x3), x3)))
P(a(x0), p(x1, p(x2, x3))) → P(x1, p(x0, p(a(x3), x3)))
p(a(x0), p(x1, p(x2, x3))) → p(x1, p(x0, p(a(x3), x3)))
P(a(x0), p(a(y_0), p(x2, x3))) → P(a(y_0), p(x0, p(a(x3), x3))) → P(a(x0), p(a(y_0), p(x2, x3))) → P(a(y_0), p(x0, p(a(x3), x3)))
P(a(x0), p(a(y_0), p(x2, x3))) → P(a(y_0), p(x0, p(a(x3), x3)))
p(a(x0), p(x1, p(x2, x3))) → p(x1, p(x0, p(a(x3), x3)))
P.1-0(a.0(x0), p.1-0(a.0(y_0), p.0-0(x2, x3))) → P.1-0(a.0(y_0), p.0-0(x0, p.1-0(a.0(x3), x3)))
P.1-0(a.0(x0), p.1-0(a.0(y_0), p.0-1(x2, x3))) → P.1-0(a.0(y_0), p.0-0(x0, p.1-1(a.1(x3), x3)))
P.1-0(a.0(x0), p.1-0(a.0(y_0), p.1-0(x2, x3))) → P.1-0(a.0(y_0), p.0-0(x0, p.1-0(a.0(x3), x3)))
P.1-0(a.0(x0), p.1-0(a.0(y_0), p.1-1(x2, x3))) → P.1-0(a.0(y_0), p.0-0(x0, p.1-1(a.1(x3), x3)))
P.1-0(a.0(x0), p.1-0(a.1(y_0), p.0-0(x2, x3))) → P.1-0(a.1(y_0), p.0-0(x0, p.1-0(a.0(x3), x3)))
P.1-0(a.0(x0), p.1-0(a.1(y_0), p.0-1(x2, x3))) → P.1-0(a.1(y_0), p.0-0(x0, p.1-1(a.1(x3), x3)))
P.1-0(a.0(x0), p.1-0(a.1(y_0), p.1-0(x2, x3))) → P.1-0(a.1(y_0), p.0-0(x0, p.1-0(a.0(x3), x3)))
P.1-0(a.0(x0), p.1-0(a.1(y_0), p.1-1(x2, x3))) → P.1-0(a.1(y_0), p.0-0(x0, p.1-1(a.1(x3), x3)))
P.1-0(a.1(x0), p.1-0(a.0(y_0), p.0-0(x2, x3))) → P.1-0(a.0(y_0), p.1-0(x0, p.1-0(a.0(x3), x3)))
P.1-0(a.1(x0), p.1-0(a.0(y_0), p.0-1(x2, x3))) → P.1-0(a.0(y_0), p.1-0(x0, p.1-1(a.1(x3), x3)))
P.1-0(a.1(x0), p.1-0(a.0(y_0), p.1-0(x2, x3))) → P.1-0(a.0(y_0), p.1-0(x0, p.1-0(a.0(x3), x3)))
P.1-0(a.1(x0), p.1-0(a.0(y_0), p.1-1(x2, x3))) → P.1-0(a.0(y_0), p.1-0(x0, p.1-1(a.1(x3), x3)))
P.1-0(a.1(x0), p.1-0(a.1(y_0), p.0-0(x2, x3))) → P.1-0(a.1(y_0), p.1-0(x0, p.1-0(a.0(x3), x3)))
P.1-0(a.1(x0), p.1-0(a.1(y_0), p.0-1(x2, x3))) → P.1-0(a.1(y_0), p.1-0(x0, p.1-1(a.1(x3), x3)))
P.1-0(a.1(x0), p.1-0(a.1(y_0), p.1-0(x2, x3))) → P.1-0(a.1(y_0), p.1-0(x0, p.1-0(a.0(x3), x3)))
P.1-0(a.1(x0), p.1-0(a.1(y_0), p.1-1(x2, x3))) → P.1-0(a.1(y_0), p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.0-0(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.0-1(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.1-0(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.1-1(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.0-0(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.0-1(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.1-0(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.1-1(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.0-0(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.0-1(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.1-0(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.1-1(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.0-0(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.0-1(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.1-0(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.1-1(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
P.1-0(a.1(x0), p.1-0(a.1(y_0), p.1-1(x2, x3))) → P.1-0(a.1(y_0), p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.0-0(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.0-1(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.1-0(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.1-1(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.0-0(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.0-1(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.1-0(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.1-1(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.0-0(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.0-1(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.1-0(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.1-1(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.0-0(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.0-1(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.1-0(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.1-1(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P.1-0(a.1(x0), p.1-0(a.1(y_0), p.1-1(x2, x3))) → P.1-0(a.1(y_0), p.1-0(x0, p.1-1(a.1(x3), x3)))
POL(P.1-0(x1, x2)) = x1 + x2
POL(a.1(x1)) = 1 + x1
POL(p.1-0(x1, x2)) = x1
POL(p.1-1(x1, x2)) = 0
p.1-0(a.0(x0), p.0-0(x1, p.0-0(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.0-1(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.1-0(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.1-1(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.0-0(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.0-1(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.1-0(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.1-1(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.0-0(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.0-1(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.1-0(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.1-1(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.0-0(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.0-1(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.1-0(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.1-1(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
P.1-0(a.1(x0), p.1-0(a.1(y_0), p.0-0(x2, x3))) → P.1-0(a.1(y_0), p.1-0(x0, p.1-0(a.0(x3), x3)))
P.1-0(a.1(x0), p.1-0(a.1(y_0), p.1-0(x2, x3))) → P.1-0(a.1(y_0), p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.0-0(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.0-1(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.1-0(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.1-1(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.0-0(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.0-1(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.1-0(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.1-1(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.0-0(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.0-1(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.1-0(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.1-1(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.0-0(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.0-1(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.1-0(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.1-1(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P.1-0(a.1(x0), p.1-0(a.1(y_0), p.0-0(x2, x3))) → P.1-0(a.1(y_0), p.1-0(x0, p.1-0(a.0(x3), x3)))
P.1-0(a.1(x0), p.1-0(a.1(y_0), p.1-0(x2, x3))) → P.1-0(a.1(y_0), p.1-0(x0, p.1-0(a.0(x3), x3)))
POL(P.1-0(x1, x2)) = x1 + x2
POL(a.0(x1)) = 0
POL(a.1(x1)) = 1 + x1
POL(p.0-0(x1, x2)) = 1 + x2
POL(p.0-1(x1, x2)) = 1
POL(p.1-0(x1, x2)) = 1 + x1 + x2
POL(p.1-1(x1, x2)) = 0
p.1-0(a.0(x0), p.0-0(x1, p.0-0(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.0-1(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.1-0(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.1-1(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.0-0(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.0-1(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.1-0(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.1-1(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.0-0(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.0-1(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.1-0(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.1-1(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.1-0(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.0-0(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.0-1(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.1-1(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.0-0(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.0-1(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.1-0(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.0-0(x1, p.1-1(x2, x3))) → p.0-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.0-0(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.0-1(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.1-0(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.0(x0), p.1-0(x1, p.1-1(x2, x3))) → p.1-0(x1, p.0-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.0-0(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.0-1(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.1-0(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.0-0(x1, p.1-1(x2, x3))) → p.0-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.0-0(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.0-1(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.1-0(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-0(a.0(x3), x3)))
p.1-0(a.1(x0), p.1-0(x1, p.1-1(x2, x3))) → p.1-0(x1, p.1-0(x0, p.1-1(a.1(x3), x3)))