0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔)
↳16 QDP
↳17 QReductionProof (⇔)
↳18 QDP
↳19 QDPSizeChangeProof (⇔)
↳20 TRUE
↳21 QDP
↳22 UsableRulesProof (⇔)
↳23 QDP
↳24 QReductionProof (⇔)
↳25 QDP
↳26 Instantiation (⇔)
↳27 QDP
↳28 Rewriting (⇔)
↳29 QDP
↳30 UsableRulesProof (⇔)
↳31 QDP
↳32 QReductionProof (⇔)
↳33 QDP
↳34 Instantiation (⇔)
↳35 QDP
↳36 NonInfProof (⇔)
↳37 AND
↳38 QDP
↳39 DependencyGraphProof (⇔)
↳40 TRUE
↳41 QDP
↳42 DependencyGraphProof (⇔)
↳43 TRUE
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
divides(x, y) → div(x, y, y)
div(0, 0, z) → true
div(0, s(x), z) → false
div(s(x), 0, s(z)) → div(s(x), s(z), s(z))
div(s(x), s(y), z) → div(x, y, z)
prime(x) → test(x, s(s(0)))
test(x, y) → if1(gt(x, y), x, y)
if1(true, x, y) → if2(divides(x, y), x, y)
if1(false, x, y) → true
if2(true, x, y) → false
if2(false, x, y) → test(x, s(y))
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
divides(x, y) → div(x, y, y)
div(0, 0, z) → true
div(0, s(x), z) → false
div(s(x), 0, s(z)) → div(s(x), s(z), s(z))
div(s(x), s(y), z) → div(x, y, z)
prime(x) → test(x, s(s(0)))
test(x, y) → if1(gt(x, y), x, y)
if1(true, x, y) → if2(divides(x, y), x, y)
if1(false, x, y) → true
if2(true, x, y) → false
if2(false, x, y) → test(x, s(y))
gt(s(x0), 0)
gt(0, x0)
gt(s(x0), s(x1))
divides(x0, x1)
div(0, 0, x0)
div(0, s(x0), x1)
div(s(x0), 0, s(x1))
div(s(x0), s(x1), x2)
prime(x0)
test(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
GT(s(x), s(y)) → GT(x, y)
DIVIDES(x, y) → DIV(x, y, y)
DIV(s(x), 0, s(z)) → DIV(s(x), s(z), s(z))
DIV(s(x), s(y), z) → DIV(x, y, z)
PRIME(x) → TEST(x, s(s(0)))
TEST(x, y) → IF1(gt(x, y), x, y)
TEST(x, y) → GT(x, y)
IF1(true, x, y) → IF2(divides(x, y), x, y)
IF1(true, x, y) → DIVIDES(x, y)
IF2(false, x, y) → TEST(x, s(y))
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
divides(x, y) → div(x, y, y)
div(0, 0, z) → true
div(0, s(x), z) → false
div(s(x), 0, s(z)) → div(s(x), s(z), s(z))
div(s(x), s(y), z) → div(x, y, z)
prime(x) → test(x, s(s(0)))
test(x, y) → if1(gt(x, y), x, y)
if1(true, x, y) → if2(divides(x, y), x, y)
if1(false, x, y) → true
if2(true, x, y) → false
if2(false, x, y) → test(x, s(y))
gt(s(x0), 0)
gt(0, x0)
gt(s(x0), s(x1))
divides(x0, x1)
div(0, 0, x0)
div(0, s(x0), x1)
div(s(x0), 0, s(x1))
div(s(x0), s(x1), x2)
prime(x0)
test(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
DIV(s(x), s(y), z) → DIV(x, y, z)
DIV(s(x), 0, s(z)) → DIV(s(x), s(z), s(z))
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
divides(x, y) → div(x, y, y)
div(0, 0, z) → true
div(0, s(x), z) → false
div(s(x), 0, s(z)) → div(s(x), s(z), s(z))
div(s(x), s(y), z) → div(x, y, z)
prime(x) → test(x, s(s(0)))
test(x, y) → if1(gt(x, y), x, y)
if1(true, x, y) → if2(divides(x, y), x, y)
if1(false, x, y) → true
if2(true, x, y) → false
if2(false, x, y) → test(x, s(y))
gt(s(x0), 0)
gt(0, x0)
gt(s(x0), s(x1))
divides(x0, x1)
div(0, 0, x0)
div(0, s(x0), x1)
div(s(x0), 0, s(x1))
div(s(x0), s(x1), x2)
prime(x0)
test(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
DIV(s(x), s(y), z) → DIV(x, y, z)
DIV(s(x), 0, s(z)) → DIV(s(x), s(z), s(z))
gt(s(x0), 0)
gt(0, x0)
gt(s(x0), s(x1))
divides(x0, x1)
div(0, 0, x0)
div(0, s(x0), x1)
div(s(x0), 0, s(x1))
div(s(x0), s(x1), x2)
prime(x0)
test(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
gt(s(x0), 0)
gt(0, x0)
gt(s(x0), s(x1))
divides(x0, x1)
div(0, 0, x0)
div(0, s(x0), x1)
div(s(x0), 0, s(x1))
div(s(x0), s(x1), x2)
prime(x0)
test(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
DIV(s(x), s(y), z) → DIV(x, y, z)
DIV(s(x), 0, s(z)) → DIV(s(x), s(z), s(z))
From the DPs we obtained the following set of size-change graphs:
GT(s(x), s(y)) → GT(x, y)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
divides(x, y) → div(x, y, y)
div(0, 0, z) → true
div(0, s(x), z) → false
div(s(x), 0, s(z)) → div(s(x), s(z), s(z))
div(s(x), s(y), z) → div(x, y, z)
prime(x) → test(x, s(s(0)))
test(x, y) → if1(gt(x, y), x, y)
if1(true, x, y) → if2(divides(x, y), x, y)
if1(false, x, y) → true
if2(true, x, y) → false
if2(false, x, y) → test(x, s(y))
gt(s(x0), 0)
gt(0, x0)
gt(s(x0), s(x1))
divides(x0, x1)
div(0, 0, x0)
div(0, s(x0), x1)
div(s(x0), 0, s(x1))
div(s(x0), s(x1), x2)
prime(x0)
test(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
GT(s(x), s(y)) → GT(x, y)
gt(s(x0), 0)
gt(0, x0)
gt(s(x0), s(x1))
divides(x0, x1)
div(0, 0, x0)
div(0, s(x0), x1)
div(s(x0), 0, s(x1))
div(s(x0), s(x1), x2)
prime(x0)
test(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
gt(s(x0), 0)
gt(0, x0)
gt(s(x0), s(x1))
divides(x0, x1)
div(0, 0, x0)
div(0, s(x0), x1)
div(s(x0), 0, s(x1))
div(s(x0), s(x1), x2)
prime(x0)
test(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
GT(s(x), s(y)) → GT(x, y)
From the DPs we obtained the following set of size-change graphs:
TEST(x, y) → IF1(gt(x, y), x, y)
IF1(true, x, y) → IF2(divides(x, y), x, y)
IF2(false, x, y) → TEST(x, s(y))
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
divides(x, y) → div(x, y, y)
div(0, 0, z) → true
div(0, s(x), z) → false
div(s(x), 0, s(z)) → div(s(x), s(z), s(z))
div(s(x), s(y), z) → div(x, y, z)
prime(x) → test(x, s(s(0)))
test(x, y) → if1(gt(x, y), x, y)
if1(true, x, y) → if2(divides(x, y), x, y)
if1(false, x, y) → true
if2(true, x, y) → false
if2(false, x, y) → test(x, s(y))
gt(s(x0), 0)
gt(0, x0)
gt(s(x0), s(x1))
divides(x0, x1)
div(0, 0, x0)
div(0, s(x0), x1)
div(s(x0), 0, s(x1))
div(s(x0), s(x1), x2)
prime(x0)
test(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
TEST(x, y) → IF1(gt(x, y), x, y)
IF1(true, x, y) → IF2(divides(x, y), x, y)
IF2(false, x, y) → TEST(x, s(y))
divides(x, y) → div(x, y, y)
div(0, 0, z) → true
div(0, s(x), z) → false
div(s(x), 0, s(z)) → div(s(x), s(z), s(z))
div(s(x), s(y), z) → div(x, y, z)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
gt(s(x0), 0)
gt(0, x0)
gt(s(x0), s(x1))
divides(x0, x1)
div(0, 0, x0)
div(0, s(x0), x1)
div(s(x0), 0, s(x1))
div(s(x0), s(x1), x2)
prime(x0)
test(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
prime(x0)
test(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
TEST(x, y) → IF1(gt(x, y), x, y)
IF1(true, x, y) → IF2(divides(x, y), x, y)
IF2(false, x, y) → TEST(x, s(y))
divides(x, y) → div(x, y, y)
div(0, 0, z) → true
div(0, s(x), z) → false
div(s(x), 0, s(z)) → div(s(x), s(z), s(z))
div(s(x), s(y), z) → div(x, y, z)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
gt(s(x0), 0)
gt(0, x0)
gt(s(x0), s(x1))
divides(x0, x1)
div(0, 0, x0)
div(0, s(x0), x1)
div(s(x0), 0, s(x1))
div(s(x0), s(x1), x2)
TEST(z0, s(z1)) → IF1(gt(z0, s(z1)), z0, s(z1))
IF1(true, x, y) → IF2(divides(x, y), x, y)
IF2(false, x, y) → TEST(x, s(y))
TEST(z0, s(z1)) → IF1(gt(z0, s(z1)), z0, s(z1))
divides(x, y) → div(x, y, y)
div(0, 0, z) → true
div(0, s(x), z) → false
div(s(x), 0, s(z)) → div(s(x), s(z), s(z))
div(s(x), s(y), z) → div(x, y, z)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
gt(s(x0), 0)
gt(0, x0)
gt(s(x0), s(x1))
divides(x0, x1)
div(0, 0, x0)
div(0, s(x0), x1)
div(s(x0), 0, s(x1))
div(s(x0), s(x1), x2)
IF1(true, x, y) → IF2(div(x, y, y), x, y)
TEST(x, y) → IF1(gt(x, y), x, y)
IF2(false, x, y) → TEST(x, s(y))
IF1(true, x, y) → IF2(div(x, y, y), x, y)
divides(x, y) → div(x, y, y)
div(0, 0, z) → true
div(0, s(x), z) → false
div(s(x), 0, s(z)) → div(s(x), s(z), s(z))
div(s(x), s(y), z) → div(x, y, z)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
gt(s(x0), 0)
gt(0, x0)
gt(s(x0), s(x1))
divides(x0, x1)
div(0, 0, x0)
div(0, s(x0), x1)
div(s(x0), 0, s(x1))
div(s(x0), s(x1), x2)
TEST(x, y) → IF1(gt(x, y), x, y)
IF2(false, x, y) → TEST(x, s(y))
IF1(true, x, y) → IF2(div(x, y, y), x, y)
div(0, 0, z) → true
div(0, s(x), z) → false
div(s(x), 0, s(z)) → div(s(x), s(z), s(z))
div(s(x), s(y), z) → div(x, y, z)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
gt(s(x0), 0)
gt(0, x0)
gt(s(x0), s(x1))
divides(x0, x1)
div(0, 0, x0)
div(0, s(x0), x1)
div(s(x0), 0, s(x1))
div(s(x0), s(x1), x2)
divides(x0, x1)
TEST(x, y) → IF1(gt(x, y), x, y)
IF2(false, x, y) → TEST(x, s(y))
IF1(true, x, y) → IF2(div(x, y, y), x, y)
div(0, 0, z) → true
div(0, s(x), z) → false
div(s(x), 0, s(z)) → div(s(x), s(z), s(z))
div(s(x), s(y), z) → div(x, y, z)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
gt(s(x0), 0)
gt(0, x0)
gt(s(x0), s(x1))
div(0, 0, x0)
div(0, s(x0), x1)
div(s(x0), 0, s(x1))
div(s(x0), s(x1), x2)
TEST(z0, s(z1)) → IF1(gt(z0, s(z1)), z0, s(z1))
IF2(false, x, y) → TEST(x, s(y))
IF1(true, x, y) → IF2(div(x, y, y), x, y)
TEST(z0, s(z1)) → IF1(gt(z0, s(z1)), z0, s(z1))
div(0, 0, z) → true
div(0, s(x), z) → false
div(s(x), 0, s(z)) → div(s(x), s(z), s(z))
div(s(x), s(y), z) → div(x, y, z)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
gt(s(x0), 0)
gt(0, x0)
gt(s(x0), s(x1))
div(0, 0, x0)
div(0, s(x0), x1)
div(s(x0), 0, s(x1))
div(s(x0), s(x1), x2)
(1) (TEST(x2, s(x3))=TEST(x4, x5) ⇒ TEST(x4, x5)≥IF1(gt(x4, x5), x4, x5))
(2) (TEST(x2, s(x3))≥IF1(gt(x2, s(x3)), x2, s(x3)))
(3) (IF2(div(x12, x13, x13), x12, x13)=IF2(false, x14, x15) ⇒ IF2(false, x14, x15)≥TEST(x14, s(x15)))
(4) (x13=x24∧div(x12, x13, x24)=false ⇒ IF2(false, x12, x13)≥TEST(x12, s(x13)))
(5) (false=false∧s(x27)=x26 ⇒ IF2(false, 0, s(x27))≥TEST(0, s(s(x27))))
(6) (div(s(x29), s(x28), s(x28))=false∧0=s(x28)∧(div(s(x29), s(x28), s(x28))=false∧s(x28)=s(x28) ⇒ IF2(false, s(x29), s(x28))≥TEST(s(x29), s(s(x28)))) ⇒ IF2(false, s(x29), 0)≥TEST(s(x29), s(0)))
(7) (div(x32, x31, x30)=false∧s(x31)=x30∧(div(x32, x31, x30)=false∧x31=x30 ⇒ IF2(false, x32, x31)≥TEST(x32, s(x31))) ⇒ IF2(false, s(x32), s(x31))≥TEST(s(x32), s(s(x31))))
(8) (IF2(false, 0, s(x27))≥TEST(0, s(s(x27))))
(9) (div(x32, x31, x30)=false∧s(x31)=x30 ⇒ IF2(false, s(x32), s(x31))≥TEST(s(x32), s(s(x31))))
(10) (false=false∧s(s(x35))=x34 ⇒ IF2(false, s(0), s(s(x35)))≥TEST(s(0), s(s(s(x35)))))
(11) (div(s(x37), s(x36), s(x36))=false∧s(0)=s(x36)∧(div(s(x37), s(x36), s(x36))=false∧s(s(x36))=s(x36) ⇒ IF2(false, s(s(x37)), s(s(x36)))≥TEST(s(s(x37)), s(s(s(x36))))) ⇒ IF2(false, s(s(x37)), s(0))≥TEST(s(s(x37)), s(s(0))))
(12) (div(x40, x39, x38)=false∧s(s(x39))=x38∧(div(x40, x39, x38)=false∧s(x39)=x38 ⇒ IF2(false, s(x40), s(x39))≥TEST(s(x40), s(s(x39)))) ⇒ IF2(false, s(s(x40)), s(s(x39)))≥TEST(s(s(x40)), s(s(s(x39)))))
(13) (IF2(false, s(0), s(s(x35)))≥TEST(s(0), s(s(s(x35)))))
(14) (IF2(false, s(s(x37)), s(0))≥TEST(s(s(x37)), s(s(0))))
(15) (IF2(false, s(s(x40)), s(s(x39)))≥TEST(s(s(x40)), s(s(s(x39)))))
(16) (IF1(gt(x16, x17), x16, x17)=IF1(true, x18, x19) ⇒ IF1(true, x18, x19)≥IF2(div(x18, x19, x19), x18, x19))
(17) (gt(x16, x17)=true ⇒ IF1(true, x16, x17)≥IF2(div(x16, x17, x17), x16, x17))
(18) (true=true ⇒ IF1(true, s(x44), 0)≥IF2(div(s(x44), 0, 0), s(x44), 0))
(19) (gt(x47, x46)=true∧(gt(x47, x46)=true ⇒ IF1(true, x47, x46)≥IF2(div(x47, x46, x46), x47, x46)) ⇒ IF1(true, s(x47), s(x46))≥IF2(div(s(x47), s(x46), s(x46)), s(x47), s(x46)))
(20) (IF1(true, s(x44), 0)≥IF2(div(s(x44), 0, 0), s(x44), 0))
(21) (IF1(true, x47, x46)≥IF2(div(x47, x46, x46), x47, x46) ⇒ IF1(true, s(x47), s(x46))≥IF2(div(s(x47), s(x46), s(x46)), s(x47), s(x46)))
POL(0) = 0
POL(IF1(x1, x2, x3)) = -1 - x1 + x2 - x3
POL(IF2(x1, x2, x3)) = -1 - x1 + x2 - x3
POL(TEST(x1, x2)) = -1 + x1 - x2
POL(c) = -2
POL(div(x1, x2, x3)) = 0
POL(false) = 0
POL(gt(x1, x2)) = 0
POL(s(x1)) = 1 + x1
POL(true) = 0
The following pairs are in Pbound:
IF2(false, x, y) → TEST(x, s(y))
The following rules are usable:
IF1(true, x, y) → IF2(div(x, y, y), x, y)
true → div(0, 0, z)
false → div(0, s(x), z)
div(s(x), s(z), s(z)) → div(s(x), 0, s(z))
div(x, y, z) → div(s(x), s(y), z)
true → gt(s(x), 0)
false → gt(0, y)
gt(x, y) → gt(s(x), s(y))
TEST(x, y) → IF1(gt(x, y), x, y)
IF1(true, x, y) → IF2(div(x, y, y), x, y)
div(0, 0, z) → true
div(0, s(x), z) → false
div(s(x), 0, s(z)) → div(s(x), s(z), s(z))
div(s(x), s(y), z) → div(x, y, z)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
gt(s(x0), 0)
gt(0, x0)
gt(s(x0), s(x1))
div(0, 0, x0)
div(0, s(x0), x1)
div(s(x0), 0, s(x1))
div(s(x0), s(x1), x2)
TEST(x, y) → IF1(gt(x, y), x, y)
IF2(false, x, y) → TEST(x, s(y))
div(0, 0, z) → true
div(0, s(x), z) → false
div(s(x), 0, s(z)) → div(s(x), s(z), s(z))
div(s(x), s(y), z) → div(x, y, z)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
gt(s(x0), 0)
gt(0, x0)
gt(s(x0), s(x1))
div(0, 0, x0)
div(0, s(x0), x1)
div(s(x0), 0, s(x1))
div(s(x0), s(x1), x2)