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 QDPSizeChangeProof (⇔)
↳27 TRUE
↳28 QDP
↳29 UsableRulesProof (⇔)
↳30 QDP
↳31 QReductionProof (⇔)
↳32 QDP
↳33 Instantiation (⇔)
↳34 QDP
↳35 Narrowing (⇔)
↳36 QDP
↳37 DependencyGraphProof (⇔)
↳38 QDP
↳39 Narrowing (⇔)
↳40 QDP
↳41 DependencyGraphProof (⇔)
↳42 QDP
↳43 Instantiation (⇔)
↳44 QDP
↳45 Rewriting (⇔)
↳46 QDP
↳47 Rewriting (⇔)
↳48 QDP
↳49 Rewriting (⇔)
↳50 QDP
↳51 Instantiation (⇔)
↳52 QDP
↳53 Instantiation (⇔)
↳54 QDP
↳55 Instantiation (⇔)
↳56 QDP
↳57 NonInfProof (⇔)
↳58 QDP
↳59 DependencyGraphProof (⇔)
↳60 TRUE
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
log(x, 0) → baseError
log(x, s(0)) → baseError
log(0, s(s(b))) → logZeroError
log(s(x), s(s(b))) → loop(s(x), s(s(b)), s(0), 0)
loop(x, s(s(b)), s(y), z) → if(le(x, s(y)), x, s(s(b)), s(y), z)
if(true, x, b, y, z) → z
if(false, x, b, y, z) → loop(x, b, times(b, y), s(z))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
log(x, 0) → baseError
log(x, s(0)) → baseError
log(0, s(s(b))) → logZeroError
log(s(x), s(s(b))) → loop(s(x), s(s(b)), s(0), 0)
loop(x, s(s(b)), s(y), z) → if(le(x, s(y)), x, s(s(b)), s(y), z)
if(true, x, b, y, z) → z
if(false, x, b, y, z) → loop(x, b, times(b, y), s(z))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
log(x0, 0)
log(x0, s(0))
log(0, s(s(x0)))
log(s(x0), s(s(x1)))
loop(x0, s(s(x1)), s(x2), x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
LE(s(x), s(y)) → LE(x, y)
PLUS(s(x), y) → PLUS(x, y)
TIMES(s(x), y) → PLUS(y, times(x, y))
TIMES(s(x), y) → TIMES(x, y)
LOG(s(x), s(s(b))) → LOOP(s(x), s(s(b)), s(0), 0)
LOOP(x, s(s(b)), s(y), z) → IF(le(x, s(y)), x, s(s(b)), s(y), z)
LOOP(x, s(s(b)), s(y), z) → LE(x, s(y))
IF(false, x, b, y, z) → LOOP(x, b, times(b, y), s(z))
IF(false, x, b, y, z) → TIMES(b, y)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
log(x, 0) → baseError
log(x, s(0)) → baseError
log(0, s(s(b))) → logZeroError
log(s(x), s(s(b))) → loop(s(x), s(s(b)), s(0), 0)
loop(x, s(s(b)), s(y), z) → if(le(x, s(y)), x, s(s(b)), s(y), z)
if(true, x, b, y, z) → z
if(false, x, b, y, z) → loop(x, b, times(b, y), s(z))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
log(x0, 0)
log(x0, s(0))
log(0, s(s(x0)))
log(s(x0), s(s(x1)))
loop(x0, s(s(x1)), s(x2), x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
PLUS(s(x), y) → PLUS(x, y)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
log(x, 0) → baseError
log(x, s(0)) → baseError
log(0, s(s(b))) → logZeroError
log(s(x), s(s(b))) → loop(s(x), s(s(b)), s(0), 0)
loop(x, s(s(b)), s(y), z) → if(le(x, s(y)), x, s(s(b)), s(y), z)
if(true, x, b, y, z) → z
if(false, x, b, y, z) → loop(x, b, times(b, y), s(z))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
log(x0, 0)
log(x0, s(0))
log(0, s(s(x0)))
log(s(x0), s(s(x1)))
loop(x0, s(s(x1)), s(x2), x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
PLUS(s(x), y) → PLUS(x, y)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
log(x0, 0)
log(x0, s(0))
log(0, s(s(x0)))
log(s(x0), s(s(x1)))
loop(x0, s(s(x1)), s(x2), x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
log(x0, 0)
log(x0, s(0))
log(0, s(s(x0)))
log(s(x0), s(s(x1)))
loop(x0, s(s(x1)), s(x2), x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
PLUS(s(x), y) → PLUS(x, y)
From the DPs we obtained the following set of size-change graphs:
TIMES(s(x), y) → TIMES(x, y)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
log(x, 0) → baseError
log(x, s(0)) → baseError
log(0, s(s(b))) → logZeroError
log(s(x), s(s(b))) → loop(s(x), s(s(b)), s(0), 0)
loop(x, s(s(b)), s(y), z) → if(le(x, s(y)), x, s(s(b)), s(y), z)
if(true, x, b, y, z) → z
if(false, x, b, y, z) → loop(x, b, times(b, y), s(z))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
log(x0, 0)
log(x0, s(0))
log(0, s(s(x0)))
log(s(x0), s(s(x1)))
loop(x0, s(s(x1)), s(x2), x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
TIMES(s(x), y) → TIMES(x, y)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
log(x0, 0)
log(x0, s(0))
log(0, s(s(x0)))
log(s(x0), s(s(x1)))
loop(x0, s(s(x1)), s(x2), x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
log(x0, 0)
log(x0, s(0))
log(0, s(s(x0)))
log(s(x0), s(s(x1)))
loop(x0, s(s(x1)), s(x2), x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
TIMES(s(x), y) → TIMES(x, y)
From the DPs we obtained the following set of size-change graphs:
LE(s(x), s(y)) → LE(x, y)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
log(x, 0) → baseError
log(x, s(0)) → baseError
log(0, s(s(b))) → logZeroError
log(s(x), s(s(b))) → loop(s(x), s(s(b)), s(0), 0)
loop(x, s(s(b)), s(y), z) → if(le(x, s(y)), x, s(s(b)), s(y), z)
if(true, x, b, y, z) → z
if(false, x, b, y, z) → loop(x, b, times(b, y), s(z))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
log(x0, 0)
log(x0, s(0))
log(0, s(s(x0)))
log(s(x0), s(s(x1)))
loop(x0, s(s(x1)), s(x2), x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
LE(s(x), s(y)) → LE(x, y)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
log(x0, 0)
log(x0, s(0))
log(0, s(s(x0)))
log(s(x0), s(s(x1)))
loop(x0, s(s(x1)), s(x2), x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
log(x0, 0)
log(x0, s(0))
log(0, s(s(x0)))
log(s(x0), s(s(x1)))
loop(x0, s(s(x1)), s(x2), x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
LE(s(x), s(y)) → LE(x, y)
From the DPs we obtained the following set of size-change graphs:
LOOP(x, s(s(b)), s(y), z) → IF(le(x, s(y)), x, s(s(b)), s(y), z)
IF(false, x, b, y, z) → LOOP(x, b, times(b, y), s(z))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
log(x, 0) → baseError
log(x, s(0)) → baseError
log(0, s(s(b))) → logZeroError
log(s(x), s(s(b))) → loop(s(x), s(s(b)), s(0), 0)
loop(x, s(s(b)), s(y), z) → if(le(x, s(y)), x, s(s(b)), s(y), z)
if(true, x, b, y, z) → z
if(false, x, b, y, z) → loop(x, b, times(b, y), s(z))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
log(x0, 0)
log(x0, s(0))
log(0, s(s(x0)))
log(s(x0), s(s(x1)))
loop(x0, s(s(x1)), s(x2), x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
LOOP(x, s(s(b)), s(y), z) → IF(le(x, s(y)), x, s(s(b)), s(y), z)
IF(false, x, b, y, z) → LOOP(x, b, times(b, y), s(z))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
log(x0, 0)
log(x0, s(0))
log(0, s(s(x0)))
log(s(x0), s(s(x1)))
loop(x0, s(s(x1)), s(x2), x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
log(x0, 0)
log(x0, s(0))
log(0, s(s(x0)))
log(s(x0), s(s(x1)))
loop(x0, s(s(x1)), s(x2), x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
LOOP(x, s(s(b)), s(y), z) → IF(le(x, s(y)), x, s(s(b)), s(y), z)
IF(false, x, b, y, z) → LOOP(x, b, times(b, y), s(z))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
LOOP(z0, s(s(x1)), s(x2), s(z3)) → IF(le(z0, s(x2)), z0, s(s(x1)), s(x2), s(z3))
IF(false, x, b, y, z) → LOOP(x, b, times(b, y), s(z))
LOOP(z0, s(s(x1)), s(x2), s(z3)) → IF(le(z0, s(x2)), z0, s(s(x1)), s(x2), s(z3))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
LOOP(0, s(s(y1)), s(y2), y3) → IF(true, 0, s(s(y1)), s(y2), y3)
LOOP(s(x0), s(s(y1)), s(x1), y3) → IF(le(x0, x1), s(x0), s(s(y1)), s(x1), y3)
IF(false, x, b, y, z) → LOOP(x, b, times(b, y), s(z))
LOOP(0, s(s(y1)), s(y2), y3) → IF(true, 0, s(s(y1)), s(y2), y3)
LOOP(s(x0), s(s(y1)), s(x1), y3) → IF(le(x0, x1), s(x0), s(s(y1)), s(x1), y3)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
LOOP(s(x0), s(s(y1)), s(x1), y3) → IF(le(x0, x1), s(x0), s(s(y1)), s(x1), y3)
IF(false, x, b, y, z) → LOOP(x, b, times(b, y), s(z))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
IF(false, y0, 0, x0, y3) → LOOP(y0, 0, 0, s(y3))
IF(false, y0, s(x0), x1, y3) → LOOP(y0, s(x0), plus(x1, times(x0, x1)), s(y3))
LOOP(s(x0), s(s(y1)), s(x1), y3) → IF(le(x0, x1), s(x0), s(s(y1)), s(x1), y3)
IF(false, y0, 0, x0, y3) → LOOP(y0, 0, 0, s(y3))
IF(false, y0, s(x0), x1, y3) → LOOP(y0, s(x0), plus(x1, times(x0, x1)), s(y3))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
IF(false, y0, s(x0), x1, y3) → LOOP(y0, s(x0), plus(x1, times(x0, x1)), s(y3))
LOOP(s(x0), s(s(y1)), s(x1), y3) → IF(le(x0, x1), s(x0), s(s(y1)), s(x1), y3)
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
IF(false, s(z0), s(s(z1)), s(z2), z3) → LOOP(s(z0), s(s(z1)), plus(s(z2), times(s(z1), s(z2))), s(z3))
LOOP(s(x0), s(s(y1)), s(x1), y3) → IF(le(x0, x1), s(x0), s(s(y1)), s(x1), y3)
IF(false, s(z0), s(s(z1)), s(z2), z3) → LOOP(s(z0), s(s(z1)), plus(s(z2), times(s(z1), s(z2))), s(z3))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
IF(false, s(z0), s(s(z1)), s(z2), z3) → LOOP(s(z0), s(s(z1)), s(plus(z2, times(s(z1), s(z2)))), s(z3))
LOOP(s(x0), s(s(y1)), s(x1), y3) → IF(le(x0, x1), s(x0), s(s(y1)), s(x1), y3)
IF(false, s(z0), s(s(z1)), s(z2), z3) → LOOP(s(z0), s(s(z1)), s(plus(z2, times(s(z1), s(z2)))), s(z3))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
IF(false, s(z0), s(s(z1)), s(z2), z3) → LOOP(s(z0), s(s(z1)), s(plus(z2, plus(s(z2), times(z1, s(z2))))), s(z3))
LOOP(s(x0), s(s(y1)), s(x1), y3) → IF(le(x0, x1), s(x0), s(s(y1)), s(x1), y3)
IF(false, s(z0), s(s(z1)), s(z2), z3) → LOOP(s(z0), s(s(z1)), s(plus(z2, plus(s(z2), times(z1, s(z2))))), s(z3))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
IF(false, s(z0), s(s(z1)), s(z2), z3) → LOOP(s(z0), s(s(z1)), s(plus(z2, s(plus(z2, times(z1, s(z2)))))), s(z3))
LOOP(s(x0), s(s(y1)), s(x1), y3) → IF(le(x0, x1), s(x0), s(s(y1)), s(x1), y3)
IF(false, s(z0), s(s(z1)), s(z2), z3) → LOOP(s(z0), s(s(z1)), s(plus(z2, s(plus(z2, times(z1, s(z2)))))), s(z3))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
LOOP(s(z0), s(s(z1)), s(y_2), s(z3)) → IF(le(z0, y_2), s(z0), s(s(z1)), s(y_2), s(z3))
IF(false, s(z0), s(s(z1)), s(z2), z3) → LOOP(s(z0), s(s(z1)), s(plus(z2, s(plus(z2, times(z1, s(z2)))))), s(z3))
LOOP(s(z0), s(s(z1)), s(y_2), s(z3)) → IF(le(z0, y_2), s(z0), s(s(z1)), s(y_2), s(z3))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
IF(false, s(z0), s(s(z1)), s(z2), s(z3)) → LOOP(s(z0), s(s(z1)), s(plus(z2, s(plus(z2, times(z1, s(z2)))))), s(s(z3)))
LOOP(s(z0), s(s(z1)), s(y_2), s(z3)) → IF(le(z0, y_2), s(z0), s(s(z1)), s(y_2), s(z3))
IF(false, s(z0), s(s(z1)), s(z2), s(z3)) → LOOP(s(z0), s(s(z1)), s(plus(z2, s(plus(z2, times(z1, s(z2)))))), s(s(z3)))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
LOOP(s(z0), s(s(z1)), s(y_2), s(s(z3))) → IF(le(z0, y_2), s(z0), s(s(z1)), s(y_2), s(s(z3)))
IF(false, s(z0), s(s(z1)), s(z2), s(z3)) → LOOP(s(z0), s(s(z1)), s(plus(z2, s(plus(z2, times(z1, s(z2)))))), s(s(z3)))
LOOP(s(z0), s(s(z1)), s(y_2), s(s(z3))) → IF(le(z0, y_2), s(z0), s(s(z1)), s(y_2), s(s(z3)))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)
(1) (IF(le(x4, x6), s(x4), s(s(x5)), s(x6), s(s(x7)))=IF(false, s(x8), s(s(x9)), s(x10), s(x11)) ⇒ IF(false, s(x8), s(s(x9)), s(x10), s(x11))≥LOOP(s(x8), s(s(x9)), s(plus(x10, s(plus(x10, times(x9, s(x10)))))), s(s(x11))))
(2) (le(x4, x6)=false ⇒ IF(false, s(x4), s(s(x5)), s(x6), s(s(x7)))≥LOOP(s(x4), s(s(x5)), s(plus(x6, s(plus(x6, times(x5, s(x6)))))), s(s(s(x7)))))
(3) (le(x26, x25)=false∧(∀x27,x28:le(x26, x25)=false ⇒ IF(false, s(x26), s(s(x27)), s(x25), s(s(x28)))≥LOOP(s(x26), s(s(x27)), s(plus(x25, s(plus(x25, times(x27, s(x25)))))), s(s(s(x28))))) ⇒ IF(false, s(s(x26)), s(s(x5)), s(s(x25)), s(s(x7)))≥LOOP(s(s(x26)), s(s(x5)), s(plus(s(x25), s(plus(s(x25), times(x5, s(s(x25))))))), s(s(s(x7)))))
(4) (false=false ⇒ IF(false, s(s(x29)), s(s(x5)), s(0), s(s(x7)))≥LOOP(s(s(x29)), s(s(x5)), s(plus(0, s(plus(0, times(x5, s(0)))))), s(s(s(x7)))))
(5) (IF(false, s(x26), s(s(x5)), s(x25), s(s(x7)))≥LOOP(s(x26), s(s(x5)), s(plus(x25, s(plus(x25, times(x5, s(x25)))))), s(s(s(x7)))) ⇒ IF(false, s(s(x26)), s(s(x5)), s(s(x25)), s(s(x7)))≥LOOP(s(s(x26)), s(s(x5)), s(plus(s(x25), s(plus(s(x25), times(x5, s(s(x25))))))), s(s(s(x7)))))
(6) (IF(false, s(s(x29)), s(s(x5)), s(0), s(s(x7)))≥LOOP(s(s(x29)), s(s(x5)), s(plus(0, s(plus(0, times(x5, s(0)))))), s(s(s(x7)))))
(7) (LOOP(s(x12), s(s(x13)), s(plus(x14, s(plus(x14, times(x13, s(x14)))))), s(s(x15)))=LOOP(s(x16), s(s(x17)), s(x18), s(s(x19))) ⇒ LOOP(s(x16), s(s(x17)), s(x18), s(s(x19)))≥IF(le(x16, x18), s(x16), s(s(x17)), s(x18), s(s(x19))))
(8) (LOOP(s(x12), s(s(x13)), s(x18), s(s(x15)))≥IF(le(x12, x18), s(x12), s(s(x13)), s(x18), s(s(x15))))
POL(0) = 0
POL(IF(x1, x2, x3, x4, x5)) = -1 + x1 + x2 - x4
POL(LOOP(x1, x2, x3, x4)) = x1 - x3
POL(c) = -1
POL(false) = 1
POL(le(x1, x2)) = 1
POL(plus(x1, x2)) = x1 + x2
POL(s(x1)) = 1 + x1
POL(times(x1, x2)) = 0
POL(true) = 0
The following pairs are in Pbound:
IF(false, s(z0), s(s(z1)), s(z2), s(z3)) → LOOP(s(z0), s(s(z1)), s(plus(z2, s(plus(z2, times(z1, s(z2)))))), s(s(z3)))
The following rules are usable:
IF(false, s(z0), s(s(z1)), s(z2), s(z3)) → LOOP(s(z0), s(s(z1)), s(plus(z2, s(plus(z2, times(z1, s(z2)))))), s(s(z3)))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
y → plus(0, y)
s(plus(x, y)) → plus(s(x), y)
le(s(x), 0) → false
0 → times(0, y)
plus(y, times(x, y)) → times(s(x), y)
LOOP(s(z0), s(s(z1)), s(y_2), s(s(z3))) → IF(le(z0, y_2), s(z0), s(s(z1)), s(y_2), s(s(z3)))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
plus(0, x0)
plus(s(x0), x1)
times(0, x0)
times(s(x0), x1)