YES
0 QTRS
↳1 DependencyPairsProof (⇔, 0 ms)
↳2 QDP
↳3 DependencyGraphProof (⇔, 0 ms)
↳4 QDP
↳5 MRRProof (⇔, 7 ms)
↳6 QDP
↳7 TransformationProof (⇔, 0 ms)
↳8 QDP
↳9 TransformationProof (⇔, 1 ms)
↳10 QDP
↳11 TransformationProof (⇔, 0 ms)
↳12 QDP
↳13 SemLabProof (⇒, 60 ms)
↳14 QDP
↳15 DependencyGraphProof (⇔, 0 ms)
↳16 QDP
↳17 UsableRulesReductionPairsProof (⇔, 0 ms)
↳18 QDP
↳19 QDPOrderProof (⇔, 0 ms)
↳20 QDP
↳21 PisEmptyProof (⇔, 0 ms)
↳22 YES
p(p(b(a(x0)), x1), p(x2, x3)) → p(p(b(x2), a(a(b(x1)))), p(x3, x0))
P(p(b(a(x0)), x1), p(x2, x3)) → P(p(b(x2), a(a(b(x1)))), p(x3, x0))
P(p(b(a(x0)), x1), p(x2, x3)) → P(b(x2), a(a(b(x1))))
P(p(b(a(x0)), x1), p(x2, x3)) → P(x3, x0)
p(p(b(a(x0)), x1), p(x2, x3)) → p(p(b(x2), a(a(b(x1)))), p(x3, x0))
P(p(b(a(x0)), x1), p(x2, x3)) → P(x3, x0)
P(p(b(a(x0)), x1), p(x2, x3)) → P(p(b(x2), a(a(b(x1)))), p(x3, x0))
p(p(b(a(x0)), x1), p(x2, x3)) → p(p(b(x2), a(a(b(x1)))), p(x3, x0))
P(p(b(a(x0)), x1), p(x2, x3)) → P(x3, x0)
POL(P(x1, x2)) = x1 + x2
POL(a(x1)) = x1
POL(b(x1)) = x1
POL(p(x1, x2)) = 1 + 2·x1 + 2·x2
P(p(b(a(x0)), x1), p(x2, x3)) → P(p(b(x2), a(a(b(x1)))), p(x3, x0))
p(p(b(a(x0)), x1), p(x2, x3)) → p(p(b(x2), a(a(b(x1)))), p(x3, x0))
P(p(b(a(x0)), a(a(b(y_1)))), p(x2, x3)) → P(p(b(x2), a(a(b(a(a(b(y_1))))))), p(x3, x0)) → P(p(b(a(x0)), a(a(b(y_1)))), p(x2, x3)) → P(p(b(x2), a(a(b(a(a(b(y_1))))))), p(x3, x0))
P(p(b(a(x0)), a(a(b(y_1)))), p(x2, x3)) → P(p(b(x2), a(a(b(a(a(b(y_1))))))), p(x3, x0))
p(p(b(a(x0)), x1), p(x2, x3)) → p(p(b(x2), a(a(b(x1)))), p(x3, x0))
P(p(b(a(x0)), a(a(b(a(a(b(y_1))))))), p(x2, x3)) → P(p(b(x2), a(a(b(a(a(b(a(a(b(y_1)))))))))), p(x3, x0)) → P(p(b(a(x0)), a(a(b(a(a(b(y_1))))))), p(x2, x3)) → P(p(b(x2), a(a(b(a(a(b(a(a(b(y_1)))))))))), p(x3, x0))
P(p(b(a(x0)), a(a(b(a(a(b(y_1))))))), p(x2, x3)) → P(p(b(x2), a(a(b(a(a(b(a(a(b(y_1)))))))))), p(x3, x0))
p(p(b(a(x0)), x1), p(x2, x3)) → p(p(b(x2), a(a(b(x1)))), p(x3, x0))
P(p(b(a(x0)), a(a(b(a(a(b(x1))))))), p(a(y_0), x3)) → P(p(b(a(y_0)), a(a(b(a(a(b(a(a(b(x1)))))))))), p(x3, x0)) → P(p(b(a(x0)), a(a(b(a(a(b(x1))))))), p(a(y_0), x3)) → P(p(b(a(y_0)), a(a(b(a(a(b(a(a(b(x1)))))))))), p(x3, x0))
P(p(b(a(x0)), a(a(b(a(a(b(x1))))))), p(a(y_0), x3)) → P(p(b(a(y_0)), a(a(b(a(a(b(a(a(b(x1)))))))))), p(x3, x0))
p(p(b(a(x0)), x1), p(x2, x3)) → p(p(b(x2), a(a(b(x1)))), p(x3, x0))
P.0-0(p.0-1(b.1(a.0(x0)), a.1(a.0(b.1(a.1(a.0(b.0(x1))))))), p.1-0(a.0(y_0), x3)) → P.0-0(p.0-1(b.1(a.0(y_0)), a.1(a.0(b.1(a.1(a.0(b.1(a.1(a.0(b.0(x1)))))))))), p.0-0(x3, x0))
P.0-0(p.0-1(b.1(a.0(x0)), a.1(a.0(b.1(a.1(a.0(b.0(x1))))))), p.1-1(a.0(y_0), x3)) → P.0-0(p.0-1(b.1(a.0(y_0)), a.1(a.0(b.1(a.1(a.0(b.1(a.1(a.0(b.0(x1)))))))))), p.1-0(x3, x0))
P.0-0(p.0-1(b.1(a.0(x0)), a.1(a.0(b.1(a.1(a.0(b.0(x1))))))), p.1-0(a.1(y_0), x3)) → P.0-0(p.0-1(b.1(a.1(y_0)), a.1(a.0(b.1(a.1(a.0(b.1(a.1(a.0(b.0(x1)))))))))), p.0-0(x3, x0))
P.0-0(p.0-1(b.1(a.0(x0)), a.1(a.0(b.1(a.1(a.0(b.0(x1))))))), p.1-1(a.1(y_0), x3)) → P.0-0(p.0-1(b.1(a.1(y_0)), a.1(a.0(b.1(a.1(a.0(b.1(a.1(a.0(b.0(x1)))))))))), p.1-0(x3, x0))
P.0-0(p.0-1(b.1(a.0(x0)), a.1(a.0(b.1(a.1(a.0(b.1(x1))))))), p.1-0(a.0(y_0), x3)) → P.0-0(p.0-1(b.1(a.0(y_0)), a.1(a.0(b.1(a.1(a.0(b.1(a.1(a.0(b.1(x1)))))))))), p.0-0(x3, x0))
P.0-0(p.0-1(b.1(a.0(x0)), a.1(a.0(b.1(a.1(a.0(b.1(x1))))))), p.1-1(a.0(y_0), x3)) → P.0-0(p.0-1(b.1(a.0(y_0)), a.1(a.0(b.1(a.1(a.0(b.1(a.1(a.0(b.1(x1)))))))))), p.1-0(x3, x0))
P.0-0(p.0-1(b.1(a.0(x0)), a.1(a.0(b.1(a.1(a.0(b.1(x1))))))), p.1-0(a.1(y_0), x3)) → P.0-0(p.0-1(b.1(a.1(y_0)), a.1(a.0(b.1(a.1(a.0(b.1(a.1(a.0(b.1(x1)))))))))), p.0-0(x3, x0))
P.0-0(p.0-1(b.1(a.0(x0)), a.1(a.0(b.1(a.1(a.0(b.1(x1))))))), p.1-1(a.1(y_0), x3)) → P.0-0(p.0-1(b.1(a.1(y_0)), a.1(a.0(b.1(a.1(a.0(b.1(a.1(a.0(b.1(x1)))))))))), p.1-0(x3, x0))
P.0-0(p.0-1(b.1(a.1(x0)), a.1(a.0(b.1(a.1(a.0(b.0(x1))))))), p.1-0(a.0(y_0), x3)) → P.0-0(p.0-1(b.1(a.0(y_0)), a.1(a.0(b.1(a.1(a.0(b.1(a.1(a.0(b.0(x1)))))))))), p.0-1(x3, x0))
P.0-0(p.0-1(b.1(a.1(x0)), a.1(a.0(b.1(a.1(a.0(b.0(x1))))))), p.1-1(a.0(y_0), x3)) → P.0-0(p.0-1(b.1(a.0(y_0)), a.1(a.0(b.1(a.1(a.0(b.1(a.1(a.0(b.0(x1)))))))))), p.1-1(x3, x0))
P.0-0(p.0-1(b.1(a.1(x0)), a.1(a.0(b.1(a.1(a.0(b.0(x1))))))), p.1-0(a.1(y_0), x3)) → P.0-0(p.0-1(b.1(a.1(y_0)), a.1(a.0(b.1(a.1(a.0(b.1(a.1(a.0(b.0(x1)))))))))), p.0-1(x3, x0))
P.0-0(p.0-1(b.1(a.1(x0)), a.1(a.0(b.1(a.1(a.0(b.0(x1))))))), p.1-1(a.1(y_0), x3)) → P.0-0(p.0-1(b.1(a.1(y_0)), a.1(a.0(b.1(a.1(a.0(b.1(a.1(a.0(b.0(x1)))))))))), p.1-1(x3, x0))
P.0-0(p.0-1(b.1(a.1(x0)), a.1(a.0(b.1(a.1(a.0(b.1(x1))))))), p.1-0(a.0(y_0), x3)) → P.0-0(p.0-1(b.1(a.0(y_0)), a.1(a.0(b.1(a.1(a.0(b.1(a.1(a.0(b.1(x1)))))))))), p.0-1(x3, x0))
P.0-0(p.0-1(b.1(a.1(x0)), a.1(a.0(b.1(a.1(a.0(b.1(x1))))))), p.1-1(a.0(y_0), x3)) → P.0-0(p.0-1(b.1(a.0(y_0)), a.1(a.0(b.1(a.1(a.0(b.1(a.1(a.0(b.1(x1)))))))))), p.1-1(x3, x0))
P.0-0(p.0-1(b.1(a.1(x0)), a.1(a.0(b.1(a.1(a.0(b.1(x1))))))), p.1-0(a.1(y_0), x3)) → P.0-0(p.0-1(b.1(a.1(y_0)), a.1(a.0(b.1(a.1(a.0(b.1(a.1(a.0(b.1(x1)))))))))), p.0-1(x3, x0))
P.0-0(p.0-1(b.1(a.1(x0)), a.1(a.0(b.1(a.1(a.0(b.1(x1))))))), p.1-1(a.1(y_0), x3)) → P.0-0(p.0-1(b.1(a.1(y_0)), a.1(a.0(b.1(a.1(a.0(b.1(a.1(a.0(b.1(x1)))))))))), p.1-1(x3, x0))
p.0-0(p.0-0(b.1(a.0(x0)), x1), p.0-0(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.0(x1)))), p.0-0(x3, x0))
p.0-0(p.0-0(b.1(a.0(x0)), x1), p.0-1(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.0(x1)))), p.1-0(x3, x0))
p.0-0(p.0-0(b.1(a.0(x0)), x1), p.1-0(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.0(x1)))), p.0-0(x3, x0))
p.0-0(p.0-0(b.1(a.0(x0)), x1), p.1-1(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.0(x1)))), p.1-0(x3, x0))
p.0-0(p.0-1(b.1(a.0(x0)), x1), p.0-0(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.1(x1)))), p.0-0(x3, x0))
p.0-0(p.0-1(b.1(a.0(x0)), x1), p.0-1(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.1(x1)))), p.1-0(x3, x0))
p.0-0(p.0-1(b.1(a.0(x0)), x1), p.1-0(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.1(x1)))), p.0-0(x3, x0))
p.0-0(p.0-1(b.1(a.0(x0)), x1), p.1-1(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.1(x1)))), p.1-0(x3, x0))
p.0-0(p.0-0(b.1(a.1(x0)), x1), p.0-0(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.0(x1)))), p.0-1(x3, x0))
p.0-0(p.0-0(b.1(a.1(x0)), x1), p.0-1(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.0(x1)))), p.1-1(x3, x0))
p.0-0(p.0-0(b.1(a.1(x0)), x1), p.1-0(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.0(x1)))), p.0-1(x3, x0))
p.0-0(p.0-0(b.1(a.1(x0)), x1), p.1-1(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.0(x1)))), p.1-1(x3, x0))
p.0-0(p.0-1(b.1(a.1(x0)), x1), p.0-0(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.1(x1)))), p.0-1(x3, x0))
p.0-0(p.0-1(b.1(a.1(x0)), x1), p.0-1(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.1(x1)))), p.1-1(x3, x0))
p.0-0(p.0-1(b.1(a.1(x0)), x1), p.1-0(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.1(x1)))), p.0-1(x3, x0))
p.0-0(p.0-1(b.1(a.1(x0)), x1), p.1-1(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.1(x1)))), p.1-1(x3, x0))
P.0-0(p.0-1(b.1(a.1(x0)), a.1(a.0(b.1(a.1(a.0(b.1(x1))))))), p.1-1(a.1(y_0), x3)) → P.0-0(p.0-1(b.1(a.1(y_0)), a.1(a.0(b.1(a.1(a.0(b.1(a.1(a.0(b.1(x1)))))))))), p.1-1(x3, x0))
p.0-0(p.0-0(b.1(a.0(x0)), x1), p.0-0(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.0(x1)))), p.0-0(x3, x0))
p.0-0(p.0-0(b.1(a.0(x0)), x1), p.0-1(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.0(x1)))), p.1-0(x3, x0))
p.0-0(p.0-0(b.1(a.0(x0)), x1), p.1-0(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.0(x1)))), p.0-0(x3, x0))
p.0-0(p.0-0(b.1(a.0(x0)), x1), p.1-1(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.0(x1)))), p.1-0(x3, x0))
p.0-0(p.0-1(b.1(a.0(x0)), x1), p.0-0(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.1(x1)))), p.0-0(x3, x0))
p.0-0(p.0-1(b.1(a.0(x0)), x1), p.0-1(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.1(x1)))), p.1-0(x3, x0))
p.0-0(p.0-1(b.1(a.0(x0)), x1), p.1-0(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.1(x1)))), p.0-0(x3, x0))
p.0-0(p.0-1(b.1(a.0(x0)), x1), p.1-1(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.1(x1)))), p.1-0(x3, x0))
p.0-0(p.0-0(b.1(a.1(x0)), x1), p.0-0(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.0(x1)))), p.0-1(x3, x0))
p.0-0(p.0-0(b.1(a.1(x0)), x1), p.0-1(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.0(x1)))), p.1-1(x3, x0))
p.0-0(p.0-0(b.1(a.1(x0)), x1), p.1-0(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.0(x1)))), p.0-1(x3, x0))
p.0-0(p.0-0(b.1(a.1(x0)), x1), p.1-1(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.0(x1)))), p.1-1(x3, x0))
p.0-0(p.0-1(b.1(a.1(x0)), x1), p.0-0(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.1(x1)))), p.0-1(x3, x0))
p.0-0(p.0-1(b.1(a.1(x0)), x1), p.0-1(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.1(x1)))), p.1-1(x3, x0))
p.0-0(p.0-1(b.1(a.1(x0)), x1), p.1-0(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.1(x1)))), p.0-1(x3, x0))
p.0-0(p.0-1(b.1(a.1(x0)), x1), p.1-1(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.1(x1)))), p.1-1(x3, x0))
Used ordering: POLO with Polynomial interpretation [POLO]:
p.0-0(p.0-0(b.1(a.0(x0)), x1), p.0-0(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.0(x1)))), p.0-0(x3, x0))
p.0-0(p.0-0(b.1(a.0(x0)), x1), p.0-1(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.0(x1)))), p.1-0(x3, x0))
p.0-0(p.0-0(b.1(a.0(x0)), x1), p.1-0(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.0(x1)))), p.0-0(x3, x0))
p.0-0(p.0-0(b.1(a.0(x0)), x1), p.1-1(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.0(x1)))), p.1-0(x3, x0))
p.0-0(p.0-1(b.1(a.0(x0)), x1), p.0-0(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.1(x1)))), p.0-0(x3, x0))
p.0-0(p.0-1(b.1(a.0(x0)), x1), p.0-1(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.1(x1)))), p.1-0(x3, x0))
p.0-0(p.0-1(b.1(a.0(x0)), x1), p.1-0(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.1(x1)))), p.0-0(x3, x0))
p.0-0(p.0-1(b.1(a.0(x0)), x1), p.1-1(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.1(x1)))), p.1-0(x3, x0))
p.0-0(p.0-0(b.1(a.1(x0)), x1), p.0-0(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.0(x1)))), p.0-1(x3, x0))
p.0-0(p.0-0(b.1(a.1(x0)), x1), p.0-1(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.0(x1)))), p.1-1(x3, x0))
p.0-0(p.0-0(b.1(a.1(x0)), x1), p.1-0(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.0(x1)))), p.0-1(x3, x0))
p.0-0(p.0-0(b.1(a.1(x0)), x1), p.1-1(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.0(x1)))), p.1-1(x3, x0))
p.0-0(p.0-1(b.1(a.1(x0)), x1), p.0-0(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.1(x1)))), p.0-1(x3, x0))
p.0-0(p.0-1(b.1(a.1(x0)), x1), p.0-1(x2, x3)) → p.0-0(p.0-1(b.0(x2), a.1(a.0(b.1(x1)))), p.1-1(x3, x0))
p.0-0(p.0-1(b.1(a.1(x0)), x1), p.1-0(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.1(x1)))), p.0-1(x3, x0))
p.0-0(p.0-1(b.1(a.1(x0)), x1), p.1-1(x2, x3)) → p.0-0(p.0-1(b.1(x2), a.1(a.0(b.1(x1)))), p.1-1(x3, x0))
POL(P.0-0(x1, x2)) = x1 + x2
POL(a.0(x1)) = x1
POL(a.1(x1)) = x1
POL(b.1(x1)) = x1
POL(p.0-1(x1, x2)) = x1 + x2
POL(p.1-1(x1, x2)) = x1 + x2
P.0-0(p.0-1(b.1(a.1(x0)), a.1(a.0(b.1(a.1(a.0(b.1(x1))))))), p.1-1(a.1(y_0), x3)) → P.0-0(p.0-1(b.1(a.1(y_0)), a.1(a.0(b.1(a.1(a.0(b.1(a.1(a.0(b.1(x1)))))))))), p.1-1(x3, x0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P.0-0(p.0-1(b.1(a.1(x0)), a.1(a.0(b.1(a.1(a.0(b.1(x1))))))), p.1-1(a.1(y_0), x3)) → P.0-0(p.0-1(b.1(a.1(y_0)), a.1(a.0(b.1(a.1(a.0(b.1(a.1(a.0(b.1(x1)))))))))), p.1-1(x3, x0))
POL(P.0-0(x1, x2)) = x1 + x2
POL(a.0(x1)) = x1
POL(a.1(x1)) = 1 + x1
POL(b.1(x1)) = x1
POL(p.0-1(x1, x2)) = x1
POL(p.1-1(x1, x2)) = x1 + x2