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 NonInfProof (⇔)
↳27 QDP
↳28 DependencyGraphProof (⇔)
↳29 TRUE
minus(x, y) → cond(equal(min(x, y), y), x, y)
cond(true, x, y) → s(minus(x, s(y)))
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
minus(x, y) → cond(equal(min(x, y), y), x, y)
cond(true, x, y) → s(minus(x, s(y)))
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
minus(x0, x1)
cond(true, x0, x1)
min(0, x0)
min(x0, 0)
min(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
MINUS(x, y) → COND(equal(min(x, y), y), x, y)
MINUS(x, y) → EQUAL(min(x, y), y)
MINUS(x, y) → MIN(x, y)
COND(true, x, y) → MINUS(x, s(y))
MIN(s(u), s(v)) → MIN(u, v)
EQUAL(s(x), s(y)) → EQUAL(x, y)
minus(x, y) → cond(equal(min(x, y), y), x, y)
cond(true, x, y) → s(minus(x, s(y)))
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
minus(x0, x1)
cond(true, x0, x1)
min(0, x0)
min(x0, 0)
min(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
EQUAL(s(x), s(y)) → EQUAL(x, y)
minus(x, y) → cond(equal(min(x, y), y), x, y)
cond(true, x, y) → s(minus(x, s(y)))
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
minus(x0, x1)
cond(true, x0, x1)
min(0, x0)
min(x0, 0)
min(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
EQUAL(s(x), s(y)) → EQUAL(x, y)
minus(x0, x1)
cond(true, x0, x1)
min(0, x0)
min(x0, 0)
min(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
minus(x0, x1)
cond(true, x0, x1)
min(0, x0)
min(x0, 0)
min(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
EQUAL(s(x), s(y)) → EQUAL(x, y)
From the DPs we obtained the following set of size-change graphs:
MIN(s(u), s(v)) → MIN(u, v)
minus(x, y) → cond(equal(min(x, y), y), x, y)
cond(true, x, y) → s(minus(x, s(y)))
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
minus(x0, x1)
cond(true, x0, x1)
min(0, x0)
min(x0, 0)
min(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
MIN(s(u), s(v)) → MIN(u, v)
minus(x0, x1)
cond(true, x0, x1)
min(0, x0)
min(x0, 0)
min(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
minus(x0, x1)
cond(true, x0, x1)
min(0, x0)
min(x0, 0)
min(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
MIN(s(u), s(v)) → MIN(u, v)
From the DPs we obtained the following set of size-change graphs:
COND(true, x, y) → MINUS(x, s(y))
MINUS(x, y) → COND(equal(min(x, y), y), x, y)
minus(x, y) → cond(equal(min(x, y), y), x, y)
cond(true, x, y) → s(minus(x, s(y)))
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
minus(x0, x1)
cond(true, x0, x1)
min(0, x0)
min(x0, 0)
min(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
COND(true, x, y) → MINUS(x, s(y))
MINUS(x, y) → COND(equal(min(x, y), y), x, y)
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
minus(x0, x1)
cond(true, x0, x1)
min(0, x0)
min(x0, 0)
min(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
minus(x0, x1)
cond(true, x0, x1)
COND(true, x, y) → MINUS(x, s(y))
MINUS(x, y) → COND(equal(min(x, y), y), x, y)
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
min(0, x0)
min(x0, 0)
min(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
(1) (COND(equal(min(x2, x3), x3), x2, x3)=COND(true, x4, x5) ⇒ COND(true, x4, x5)≥MINUS(x4, s(x5)))
(2) (min(x2, x3)=x12∧equal(x12, x3)=true ⇒ COND(true, x2, x3)≥MINUS(x2, s(x3)))
(3) (true=true∧min(x2, 0)=0 ⇒ COND(true, x2, 0)≥MINUS(x2, s(0)))
(4) (equal(x16, x15)=true∧min(x2, s(x15))=s(x16)∧(∀x17:equal(x16, x15)=true∧min(x17, x15)=x16 ⇒ COND(true, x17, x15)≥MINUS(x17, s(x15))) ⇒ COND(true, x2, s(x15))≥MINUS(x2, s(s(x15))))
(5) (0=x18∧min(x2, x18)=0 ⇒ COND(true, x2, 0)≥MINUS(x2, s(0)))
(6) (equal(x16, x15)=true∧s(x15)=x23∧min(x2, x23)=s(x16)∧(∀x17:equal(x16, x15)=true∧min(x17, x15)=x16 ⇒ COND(true, x17, x15)≥MINUS(x17, s(x15))) ⇒ COND(true, x2, s(x15))≥MINUS(x2, s(s(x15))))
(7) (0=0∧0=x19 ⇒ COND(true, 0, 0)≥MINUS(0, s(0)))
(8) (0=0 ⇒ COND(true, x20, 0)≥MINUS(x20, s(0)))
(9) (COND(true, 0, 0)≥MINUS(0, s(0)))
(10) (COND(true, x20, 0)≥MINUS(x20, s(0)))
(11) (s(min(x27, x26))=s(x16)∧equal(x16, x15)=true∧s(x15)=s(x26)∧(∀x17:equal(x16, x15)=true∧min(x17, x15)=x16 ⇒ COND(true, x17, x15)≥MINUS(x17, s(x15)))∧(∀x28,x29,x30:min(x27, x26)=s(x28)∧equal(x28, x29)=true∧s(x29)=x26∧(∀x30:equal(x28, x29)=true∧min(x30, x29)=x28 ⇒ COND(true, x30, x29)≥MINUS(x30, s(x29))) ⇒ COND(true, x27, s(x29))≥MINUS(x27, s(s(x29)))) ⇒ COND(true, s(x27), s(x15))≥MINUS(s(x27), s(s(x15))))
(12) (min(x27, x26)=x16∧equal(x16, x15)=true∧x15=x26∧(∀x28,x29:min(x27, x26)=s(x28)∧equal(x28, x29)=true∧s(x29)=x26 ⇒ COND(true, x27, s(x29))≥MINUS(x27, s(s(x29)))) ⇒ COND(true, s(x27), s(x15))≥MINUS(s(x27), s(s(x15))))
(13) (true=true∧min(x27, x26)=0∧0=x26∧(∀x28,x29:min(x27, x26)=s(x28)∧equal(x28, x29)=true∧s(x29)=x26 ⇒ COND(true, x27, s(x29))≥MINUS(x27, s(s(x29)))) ⇒ COND(true, s(x27), s(0))≥MINUS(s(x27), s(s(0))))
(14) (equal(x34, x33)=true∧min(x27, x26)=s(x34)∧s(x33)=x26∧(∀x28,x29:min(x27, x26)=s(x28)∧equal(x28, x29)=true∧s(x29)=x26 ⇒ COND(true, x27, s(x29))≥MINUS(x27, s(s(x29))))∧(∀x35,x36,x37,x38:equal(x34, x33)=true∧min(x35, x36)=x34∧x33=x36∧(∀x37,x38:min(x35, x36)=s(x37)∧equal(x37, x38)=true∧s(x38)=x36 ⇒ COND(true, x35, s(x38))≥MINUS(x35, s(s(x38)))) ⇒ COND(true, s(x35), s(x33))≥MINUS(s(x35), s(s(x33)))) ⇒ COND(true, s(x27), s(s(x33)))≥MINUS(s(x27), s(s(s(x33)))))
(15) (min(x27, x26)=0∧0=x26 ⇒ COND(true, s(x27), s(0))≥MINUS(s(x27), s(s(0))))
(16) (COND(true, x27, s(x33))≥MINUS(x27, s(s(x33)))∧(∀x35,x36,x37,x38:equal(x34, x33)=true∧min(x35, x36)=x34∧x33=x36∧(∀x37,x38:min(x35, x36)=s(x37)∧equal(x37, x38)=true∧s(x38)=x36 ⇒ COND(true, x35, s(x38))≥MINUS(x35, s(s(x38)))) ⇒ COND(true, s(x35), s(x33))≥MINUS(s(x35), s(s(x33)))) ⇒ COND(true, s(x27), s(s(x33)))≥MINUS(s(x27), s(s(s(x33)))))
(17) (0=0∧0=x39 ⇒ COND(true, s(0), s(0))≥MINUS(s(0), s(s(0))))
(18) (0=0 ⇒ COND(true, s(x40), s(0))≥MINUS(s(x40), s(s(0))))
(19) (COND(true, s(0), s(0))≥MINUS(s(0), s(s(0))))
(20) (COND(true, s(x40), s(0))≥MINUS(s(x40), s(s(0))))
(21) (COND(true, x27, s(x33))≥MINUS(x27, s(s(x33))) ⇒ COND(true, s(x27), s(s(x33)))≥MINUS(s(x27), s(s(s(x33)))))
(22) (MINUS(x6, s(x7))=MINUS(x8, x9) ⇒ MINUS(x8, x9)≥COND(equal(min(x8, x9), x9), x8, x9))
(23) (MINUS(x6, s(x7))≥COND(equal(min(x6, s(x7)), s(x7)), x6, s(x7)))
POL(0) = 0
POL(COND(x1, x2, x3)) = -1 - x1 + x2 - x3
POL(MINUS(x1, x2)) = -1 + x1 - x2
POL(c) = -2
POL(equal(x1, x2)) = 0
POL(false) = 0
POL(min(x1, x2)) = 0
POL(s(x1)) = 1 + x1
POL(true) = 0
The following pairs are in Pbound:
COND(true, x, y) → MINUS(x, s(y))
The following rules are usable:
COND(true, x, y) → MINUS(x, s(y))
false → equal(s(x), 0)
true → equal(0, 0)
equal(x, y) → equal(s(x), s(y))
false → equal(0, s(y))
MINUS(x, y) → COND(equal(min(x, y), y), x, y)
min(0, v) → 0
min(u, 0) → 0
min(s(u), s(v)) → s(min(u, v))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
min(0, x0)
min(x0, 0)
min(s(x0), s(x1))
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))