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 NonInfProof (⇔)
↳29 AND
↳30 QDP
↳31 DependencyGraphProof (⇔)
↳32 TRUE
↳33 QDP
↳34 DependencyGraphProof (⇔)
↳35 TRUE
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
if(true, x, y, z) → z
if(false, x, y, z) → loop(x, double(y), s(z))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
if(true, x, y, z) → z
if(false, x, y, z) → loop(x, double(y), s(z))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
LE(s(x), s(y)) → LE(x, y)
DOUBLE(s(x)) → DOUBLE(x)
LOG(s(x)) → LOOP(s(x), s(0), 0)
LOOP(x, s(y), z) → IF(le(x, s(y)), x, s(y), z)
LOOP(x, s(y), z) → LE(x, s(y))
IF(false, x, y, z) → LOOP(x, double(y), s(z))
IF(false, x, y, z) → DOUBLE(y)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
if(true, x, y, z) → z
if(false, x, y, z) → loop(x, double(y), s(z))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
DOUBLE(s(x)) → DOUBLE(x)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
if(true, x, y, z) → z
if(false, x, y, z) → loop(x, double(y), s(z))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
DOUBLE(s(x)) → DOUBLE(x)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
DOUBLE(s(x)) → DOUBLE(x)
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)
double(0) → 0
double(s(x)) → s(s(double(x)))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
if(true, x, y, z) → z
if(false, x, y, z) → loop(x, double(y), s(z))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
LE(s(x), s(y)) → LE(x, y)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
LE(s(x), s(y)) → LE(x, y)
From the DPs we obtained the following set of size-change graphs:
LOOP(x, s(y), z) → IF(le(x, s(y)), x, s(y), z)
IF(false, x, y, z) → LOOP(x, double(y), s(z))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
if(true, x, y, z) → z
if(false, x, y, z) → loop(x, double(y), s(z))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
LOOP(x, s(y), z) → IF(le(x, s(y)), x, s(y), z)
IF(false, x, y, z) → LOOP(x, double(y), s(z))
double(0) → 0
double(s(x)) → s(s(double(x)))
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))
double(0)
double(s(x0))
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
log(0)
log(s(x0))
loop(x0, s(x1), x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
LOOP(x, s(y), z) → IF(le(x, s(y)), x, s(y), z)
IF(false, x, y, z) → LOOP(x, double(y), s(z))
double(0) → 0
double(s(x)) → s(s(double(x)))
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))
double(0)
double(s(x0))
LOOP(z0, s(x1), s(z2)) → IF(le(z0, s(x1)), z0, s(x1), s(z2))
IF(false, x, y, z) → LOOP(x, double(y), s(z))
LOOP(z0, s(x1), s(z2)) → IF(le(z0, s(x1)), z0, s(x1), s(z2))
double(0) → 0
double(s(x)) → s(s(double(x)))
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))
double(0)
double(s(x0))
(1) (IF(le(x3, s(x4)), x3, s(x4), x5)=IF(false, x6, x7, x8) ⇒ LOOP(x3, s(x4), x5)≥IF(le(x3, s(x4)), x3, s(x4), x5))
(2) (s(x4)=x18∧le(x3, x18)=false ⇒ LOOP(x3, s(x4), x5)≥IF(le(x3, s(x4)), x3, s(x4), x5))
(3) (le(x21, x20)=false∧s(x4)=s(x20)∧(∀x22,x23:le(x21, x20)=false∧s(x22)=x20 ⇒ LOOP(x21, s(x22), x23)≥IF(le(x21, s(x22)), x21, s(x22), x23)) ⇒ LOOP(s(x21), s(x4), x5)≥IF(le(s(x21), s(x4)), s(x21), s(x4), x5))
(4) (false=false∧s(x4)=0 ⇒ LOOP(s(x24), s(x4), x5)≥IF(le(s(x24), s(x4)), s(x24), s(x4), x5))
(5) (le(x21, x20)=false ⇒ LOOP(s(x21), s(x20), x5)≥IF(le(s(x21), s(x20)), s(x21), s(x20), x5))
(6) (le(x27, x26)=false∧(∀x28:le(x27, x26)=false ⇒ LOOP(s(x27), s(x26), x28)≥IF(le(s(x27), s(x26)), s(x27), s(x26), x28)) ⇒ LOOP(s(s(x27)), s(s(x26)), x5)≥IF(le(s(s(x27)), s(s(x26))), s(s(x27)), s(s(x26)), x5))
(7) (false=false ⇒ LOOP(s(s(x29)), s(0), x5)≥IF(le(s(s(x29)), s(0)), s(s(x29)), s(0), x5))
(8) (LOOP(s(x27), s(x26), x5)≥IF(le(s(x27), s(x26)), s(x27), s(x26), x5) ⇒ LOOP(s(s(x27)), s(s(x26)), x5)≥IF(le(s(s(x27)), s(s(x26))), s(s(x27)), s(s(x26)), x5))
(9) (LOOP(s(s(x29)), s(0), x5)≥IF(le(s(s(x29)), s(0)), s(s(x29)), s(0), x5))
(10) (LOOP(x9, double(x10), s(x11))=LOOP(x12, s(x13), x14) ⇒ IF(false, x9, x10, x11)≥LOOP(x9, double(x10), s(x11)))
(11) (double(x10)=s(x13) ⇒ IF(false, x9, x10, x11)≥LOOP(x9, double(x10), s(x11)))
(12) (s(s(double(x30)))=s(x13)∧(∀x31,x32,x33:double(x30)=s(x31) ⇒ IF(false, x32, x30, x33)≥LOOP(x32, double(x30), s(x33))) ⇒ IF(false, x9, s(x30), x11)≥LOOP(x9, double(s(x30)), s(x11)))
(13) (IF(false, x9, s(x30), x11)≥LOOP(x9, double(s(x30)), s(x11)))
POL(0) = 0
POL(IF(x1, x2, x3, x4)) = -1 - x1 + x2 - x3
POL(LOOP(x1, x2, x3)) = -1 + x1 - x2
POL(c) = -2
POL(double(x1)) = 2·x1
POL(false) = 0
POL(le(x1, x2)) = 0
POL(s(x1)) = 1 + x1
POL(true) = 2
The following pairs are in Pbound:
IF(false, x, y, z) → LOOP(x, double(y), s(z))
The following rules are usable:
LOOP(x, s(y), z) → IF(le(x, s(y)), x, s(y), z)
0 → double(0)
s(s(double(x))) → double(s(x))
true → le(0, y)
le(x, y) → le(s(x), s(y))
false → le(s(x), 0)
LOOP(x, s(y), z) → IF(le(x, s(y)), x, s(y), z)
double(0) → 0
double(s(x)) → s(s(double(x)))
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))
double(0)
double(s(x0))
IF(false, x, y, z) → LOOP(x, double(y), s(z))
double(0) → 0
double(s(x)) → s(s(double(x)))
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))
double(0)
double(s(x0))