0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 QDP
↳5 MRRProof (⇔)
↳6 QDP
↳7 Instantiation (⇔)
↳8 QDP
↳9 Instantiation (⇔)
↳10 QDP
↳11 ForwardInstantiation (⇔)
↳12 QDP
↳13 SemLabProof (⇐)
↳14 QDP
↳15 DependencyGraphProof (⇔)
↳16 QDP
↳17 UsableRulesReductionPairsProof (⇔)
↳18 QDP
↳19 QDPOrderProof (⇔)
↳20 QDP
↳21 PisEmptyProof (⇔)
↳22 TRUE
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 + x1 + 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)), 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)), 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)), 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-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-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.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-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.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.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.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-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-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-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.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-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-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.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-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.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-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-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.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-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.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.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.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-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-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-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.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-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-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.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-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))
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)) = 0
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