foo(0(x1)) → 0(s(p(p(p(s(s(s(p(s(x1))))))))))
foo(s(x1)) → p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))
bar(0(x1)) → 0(p(s(s(s(x1)))))
bar(s(x1)) → p(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(x1)))))
↳ QTRS
↳ DependencyPairsProof
foo(0(x1)) → 0(s(p(p(p(s(s(s(p(s(x1))))))))))
foo(s(x1)) → p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))
bar(0(x1)) → 0(p(s(s(s(x1)))))
bar(s(x1)) → p(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(x1)))))
FOO(s(x1)) → P(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))
FOO(0(x1)) → P(p(p(s(s(s(p(s(x1))))))))
FOO(s(x1)) → P(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))
FOO(s(x1)) → P(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))
FOO(s(x1)) → P(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))
BAR(s(x1)) → P(p(s(s(x1))))
FOO(s(x1)) → P(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))
FOO(s(x1)) → P(s(s(p(s(x1)))))
FOO(s(x1)) → P(s(bar(p(p(s(s(p(s(x1)))))))))
P(p(s(x1))) → P(x1)
BAR(s(x1)) → P(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))
FOO(0(x1)) → P(p(s(s(s(p(s(x1)))))))
FOO(0(x1)) → P(s(x1))
FOO(s(x1)) → P(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))
FOO(s(x1)) → P(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))
FOO(s(x1)) → P(p(s(s(p(s(x1))))))
BAR(0(x1)) → P(s(s(s(x1))))
BAR(s(x1)) → FOO(s(p(p(s(s(x1))))))
FOO(s(x1)) → P(s(x1))
FOO(s(x1)) → P(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))
FOO(0(x1)) → P(s(s(s(p(s(x1))))))
BAR(s(x1)) → P(p(s(s(foo(s(p(p(s(s(x1))))))))))
FOO(s(x1)) → FOO(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))
BAR(s(x1)) → P(s(s(foo(s(p(p(s(s(x1)))))))))
FOO(s(x1)) → BAR(p(p(s(s(p(s(x1)))))))
BAR(s(x1)) → P(s(s(x1)))
foo(0(x1)) → 0(s(p(p(p(s(s(s(p(s(x1))))))))))
foo(s(x1)) → p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))
bar(0(x1)) → 0(p(s(s(s(x1)))))
bar(s(x1)) → p(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(x1)))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
FOO(s(x1)) → P(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))
FOO(0(x1)) → P(p(p(s(s(s(p(s(x1))))))))
FOO(s(x1)) → P(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))
FOO(s(x1)) → P(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))
FOO(s(x1)) → P(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))
BAR(s(x1)) → P(p(s(s(x1))))
FOO(s(x1)) → P(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))
FOO(s(x1)) → P(s(s(p(s(x1)))))
FOO(s(x1)) → P(s(bar(p(p(s(s(p(s(x1)))))))))
P(p(s(x1))) → P(x1)
BAR(s(x1)) → P(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))
FOO(0(x1)) → P(p(s(s(s(p(s(x1)))))))
FOO(0(x1)) → P(s(x1))
FOO(s(x1)) → P(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))
FOO(s(x1)) → P(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))
FOO(s(x1)) → P(p(s(s(p(s(x1))))))
BAR(0(x1)) → P(s(s(s(x1))))
BAR(s(x1)) → FOO(s(p(p(s(s(x1))))))
FOO(s(x1)) → P(s(x1))
FOO(s(x1)) → P(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))
FOO(0(x1)) → P(s(s(s(p(s(x1))))))
BAR(s(x1)) → P(p(s(s(foo(s(p(p(s(s(x1))))))))))
FOO(s(x1)) → FOO(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))
BAR(s(x1)) → P(s(s(foo(s(p(p(s(s(x1)))))))))
FOO(s(x1)) → BAR(p(p(s(s(p(s(x1)))))))
BAR(s(x1)) → P(s(s(x1)))
foo(0(x1)) → 0(s(p(p(p(s(s(s(p(s(x1))))))))))
foo(s(x1)) → p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))
bar(0(x1)) → 0(p(s(s(s(x1)))))
bar(s(x1)) → p(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(x1)))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
P(p(s(x1))) → P(x1)
foo(0(x1)) → 0(s(p(p(p(s(s(s(p(s(x1))))))))))
foo(s(x1)) → p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))
bar(0(x1)) → 0(p(s(s(s(x1)))))
bar(s(x1)) → p(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(x1)))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P(p(s(x1))) → P(x1)
The value of delta used in the strict ordering is 4.
POL(P(x1)) = (2)x_1
POL(p(x1)) = 2 + (2)x_1
POL(s(x1)) = x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
foo(0(x1)) → 0(s(p(p(p(s(s(s(p(s(x1))))))))))
foo(s(x1)) → p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))
bar(0(x1)) → 0(p(s(s(s(x1)))))
bar(s(x1)) → p(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(x1)))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
FOO(s(x1)) → FOO(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))
FOO(s(x1)) → BAR(p(p(s(s(p(s(x1)))))))
BAR(s(x1)) → FOO(s(p(p(s(s(x1))))))
foo(0(x1)) → 0(s(p(p(p(s(s(s(p(s(x1))))))))))
foo(s(x1)) → p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))
bar(0(x1)) → 0(p(s(s(s(x1)))))
bar(s(x1)) → p(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(x1)))))