YES
0 QTRS
↳1 Overlay + Local Confluence (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 QDP
↳10 QReductionProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 QDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 QDP
↳17 QReductionProof (⇔, 0 ms)
↳18 QDP
↳19 QDPOrderProof (⇔, 0 ms)
↳20 QDP
↳21 PisEmptyProof (⇔, 0 ms)
↳22 YES
↳23 QDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 QDP
↳26 QReductionProof (⇔, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
↳30 QDP
↳31 UsableRulesProof (⇔, 0 ms)
↳32 QDP
↳33 QReductionProof (⇔, 0 ms)
↳34 QDP
↳35 QDPSizeChangeProof (⇔, 0 ms)
↳36 YES
↳37 QDP
↳38 UsableRulesProof (⇔, 0 ms)
↳39 QDP
↳40 QReductionProof (⇔, 0 ms)
↳41 QDP
↳42 QDPQMonotonicMRRProof (⇔, 10 ms)
↳43 QDP
↳44 QDPQMonotonicMRRProof (⇔, 13 ms)
↳45 QDP
↳46 TransformationProof (⇔, 0 ms)
↳47 QDP
↳48 TransformationProof (⇔, 0 ms)
↳49 QDP
↳50 UsableRulesProof (⇔, 0 ms)
↳51 QDP
↳52 TransformationProof (⇒, 0 ms)
↳53 QDP
↳54 DependencyGraphProof (⇔, 0 ms)
↳55 QDP
↳56 TransformationProof (⇔, 0 ms)
↳57 QDP
↳58 TransformationProof (⇔, 0 ms)
↳59 QDP
↳60 TransformationProof (⇔, 0 ms)
↳61 QDP
↳62 UsableRulesProof (⇔, 0 ms)
↳63 QDP
↳64 QReductionProof (⇔, 0 ms)
↳65 QDP
↳66 TransformationProof (⇔, 0 ms)
↳67 QDP
↳68 DependencyGraphProof (⇔, 0 ms)
↳69 TRUE
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(0) → 0
inc(s(x)) → s(inc(x))
minus(0, y) → 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(x) → log2(x, 0)
log2(x, y) → if(le(x, 0), le(x, s(0)), x, inc(y))
if(true, b, x, y) → log_undefined
if(false, b, x, y) → if2(b, x, y)
if2(true, x, s(y)) → y
if2(false, x, y) → log2(quot(x, s(s(0))), y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(0) → 0
inc(s(x)) → s(inc(x))
minus(0, y) → 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(x) → log2(x, 0)
log2(x, y) → if(le(x, 0), le(x, s(0)), x, inc(y))
if(true, b, x, y) → log_undefined
if(false, b, x, y) → if2(b, x, y)
if2(true, x, s(y)) → y
if2(false, x, y) → log2(quot(x, s(s(0))), y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
log(x0)
log2(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, s(x1))
if2(false, x0, x1)
LE(s(x), s(y)) → LE(x, y)
INC(s(x)) → INC(x)
MINUS(s(x), s(y)) → MINUS(x, y)
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
QUOT(s(x), s(y)) → MINUS(x, y)
LOG(x) → LOG2(x, 0)
LOG2(x, y) → IF(le(x, 0), le(x, s(0)), x, inc(y))
LOG2(x, y) → LE(x, 0)
LOG2(x, y) → LE(x, s(0))
LOG2(x, y) → INC(y)
IF(false, b, x, y) → IF2(b, x, y)
IF2(false, x, y) → LOG2(quot(x, s(s(0))), y)
IF2(false, x, y) → QUOT(x, s(s(0)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(0) → 0
inc(s(x)) → s(inc(x))
minus(0, y) → 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(x) → log2(x, 0)
log2(x, y) → if(le(x, 0), le(x, s(0)), x, inc(y))
if(true, b, x, y) → log_undefined
if(false, b, x, y) → if2(b, x, y)
if2(true, x, s(y)) → y
if2(false, x, y) → log2(quot(x, s(s(0))), y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
log(x0)
log2(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, s(x1))
if2(false, x0, x1)
MINUS(s(x), s(y)) → MINUS(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(0) → 0
inc(s(x)) → s(inc(x))
minus(0, y) → 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(x) → log2(x, 0)
log2(x, y) → if(le(x, 0), le(x, s(0)), x, inc(y))
if(true, b, x, y) → log_undefined
if(false, b, x, y) → if2(b, x, y)
if2(true, x, s(y)) → y
if2(false, x, y) → log2(quot(x, s(s(0))), y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
log(x0)
log2(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, s(x1))
if2(false, x0, x1)
MINUS(s(x), s(y)) → MINUS(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
log(x0)
log2(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, s(x1))
if2(false, x0, x1)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
log(x0)
log2(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, s(x1))
if2(false, x0, x1)
MINUS(s(x), s(y)) → MINUS(x, y)
From the DPs we obtained the following set of size-change graphs:
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(0) → 0
inc(s(x)) → s(inc(x))
minus(0, y) → 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(x) → log2(x, 0)
log2(x, y) → if(le(x, 0), le(x, s(0)), x, inc(y))
if(true, b, x, y) → log_undefined
if(false, b, x, y) → if2(b, x, y)
if2(true, x, s(y)) → y
if2(false, x, y) → log2(quot(x, s(s(0))), y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
log(x0)
log2(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, s(x1))
if2(false, x0, x1)
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
minus(0, y) → 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
log(x0)
log2(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, s(x1))
if2(false, x0, x1)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
quot(0, s(x0))
quot(s(x0), s(x1))
log(x0)
log2(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, s(x1))
if2(false, x0, x1)
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
minus(0, y) → 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
trivial
s_1=1
0=1
minus(0, y) → 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(0, y) → 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
INC(s(x)) → INC(x)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(0) → 0
inc(s(x)) → s(inc(x))
minus(0, y) → 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(x) → log2(x, 0)
log2(x, y) → if(le(x, 0), le(x, s(0)), x, inc(y))
if(true, b, x, y) → log_undefined
if(false, b, x, y) → if2(b, x, y)
if2(true, x, s(y)) → y
if2(false, x, y) → log2(quot(x, s(s(0))), y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
log(x0)
log2(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, s(x1))
if2(false, x0, x1)
INC(s(x)) → INC(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
log(x0)
log2(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, s(x1))
if2(false, x0, x1)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
log(x0)
log2(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, s(x1))
if2(false, x0, x1)
INC(s(x)) → INC(x)
From the DPs we obtained the following set of size-change graphs:
LE(s(x), s(y)) → LE(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(0) → 0
inc(s(x)) → s(inc(x))
minus(0, y) → 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(x) → log2(x, 0)
log2(x, y) → if(le(x, 0), le(x, s(0)), x, inc(y))
if(true, b, x, y) → log_undefined
if(false, b, x, y) → if2(b, x, y)
if2(true, x, s(y)) → y
if2(false, x, y) → log2(quot(x, s(s(0))), y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
log(x0)
log2(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, s(x1))
if2(false, x0, x1)
LE(s(x), s(y)) → LE(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
log(x0)
log2(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, s(x1))
if2(false, x0, x1)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
log(x0)
log2(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, s(x1))
if2(false, x0, x1)
LE(s(x), s(y)) → LE(x, y)
From the DPs we obtained the following set of size-change graphs:
LOG2(x, y) → IF(le(x, 0), le(x, s(0)), x, inc(y))
IF(false, b, x, y) → IF2(b, x, y)
IF2(false, x, y) → LOG2(quot(x, s(s(0))), y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(0) → 0
inc(s(x)) → s(inc(x))
minus(0, y) → 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(x) → log2(x, 0)
log2(x, y) → if(le(x, 0), le(x, s(0)), x, inc(y))
if(true, b, x, y) → log_undefined
if(false, b, x, y) → if2(b, x, y)
if2(true, x, s(y)) → y
if2(false, x, y) → log2(quot(x, s(s(0))), y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
log(x0)
log2(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, s(x1))
if2(false, x0, x1)
LOG2(x, y) → IF(le(x, 0), le(x, s(0)), x, inc(y))
IF(false, b, x, y) → IF2(b, x, y)
IF2(false, x, y) → LOG2(quot(x, s(s(0))), y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(0, y) → 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(0) → 0
inc(s(x)) → s(inc(x))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
log(x0)
log2(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, s(x1))
if2(false, x0, x1)
log(x0)
log2(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, s(x1))
if2(false, x0, x1)
LOG2(x, y) → IF(le(x, 0), le(x, s(0)), x, inc(y))
IF(false, b, x, y) → IF2(b, x, y)
IF2(false, x, y) → LOG2(quot(x, s(s(0))), y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(0, y) → 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(0) → 0
inc(s(x)) → s(inc(x))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
minus(s(x), s(y)) → minus(x, y)
POL(0) = 2
POL(IF(x1, x2, x3, x4)) = 1 + 2·x3 + x4
POL(IF2(x1, x2, x3)) = 1 + 2·x2 + x3
POL(LOG2(x1, x2)) = 1 + 2·x1 + x2
POL(false) = 2
POL(inc(x1)) = x1
POL(le(x1, x2)) = 2 + x2
POL(minus(x1, x2)) = x1
POL(quot(x1, x2)) = x1
POL(s(x1)) = 1 + 2·x1
POL(true) = 0
LOG2(x, y) → IF(le(x, 0), le(x, s(0)), x, inc(y))
IF(false, b, x, y) → IF2(b, x, y)
IF2(false, x, y) → LOG2(quot(x, s(s(0))), y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(0, y) → 0
minus(x, 0) → x
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(0) → 0
inc(s(x)) → s(inc(x))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, y) → true
POL(0) = 1
POL(IF(x1, x2, x3, x4)) = x1 + x2 + x4
POL(IF2(x1, x2, x3)) = 1 + x1 + x3
POL(LOG2(x1, x2)) = 2 + x2
POL(false) = 1
POL(inc(x1)) = x1
POL(le(x1, x2)) = 1
POL(minus(x1, x2)) = x1
POL(quot(x1, x2)) = 1 + 2·x1
POL(s(x1)) = 1 + x1
POL(true) = 0
LOG2(x, y) → IF(le(x, 0), le(x, s(0)), x, inc(y))
IF(false, b, x, y) → IF2(b, x, y)
IF2(false, x, y) → LOG2(quot(x, s(s(0))), y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(0, y) → 0
minus(x, 0) → x
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(0) → 0
inc(s(x)) → s(inc(x))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
LOG2(s(x0), y1) → IF(false, le(s(x0), s(0)), s(x0), inc(y1)) → LOG2(s(x0), y1) → IF(false, le(s(x0), s(0)), s(x0), inc(y1))
IF(false, b, x, y) → IF2(b, x, y)
IF2(false, x, y) → LOG2(quot(x, s(s(0))), y)
LOG2(s(x0), y1) → IF(false, le(s(x0), s(0)), s(x0), inc(y1))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(0, y) → 0
minus(x, 0) → x
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(0) → 0
inc(s(x)) → s(inc(x))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
LOG2(s(x0), y1) → IF(false, le(x0, 0), s(x0), inc(y1)) → LOG2(s(x0), y1) → IF(false, le(x0, 0), s(x0), inc(y1))
IF(false, b, x, y) → IF2(b, x, y)
IF2(false, x, y) → LOG2(quot(x, s(s(0))), y)
LOG2(s(x0), y1) → IF(false, le(x0, 0), s(x0), inc(y1))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(0, y) → 0
minus(x, 0) → x
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(0) → 0
inc(s(x)) → s(inc(x))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
IF(false, b, x, y) → IF2(b, x, y)
IF2(false, x, y) → LOG2(quot(x, s(s(0))), y)
LOG2(s(x0), y1) → IF(false, le(x0, 0), s(x0), inc(y1))
le(s(x), 0) → false
inc(0) → 0
inc(s(x)) → s(inc(x))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(0, y) → 0
minus(x, 0) → x
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
IF2(false, 0, y1) → LOG2(0, y1) → IF2(false, 0, y1) → LOG2(0, y1)
IF2(false, s(x0), y1) → LOG2(s(quot(minus(x0, s(0)), s(s(0)))), y1) → IF2(false, s(x0), y1) → LOG2(s(quot(minus(x0, s(0)), s(s(0)))), y1)
IF(false, b, x, y) → IF2(b, x, y)
LOG2(s(x0), y1) → IF(false, le(x0, 0), s(x0), inc(y1))
IF2(false, 0, y1) → LOG2(0, y1)
IF2(false, s(x0), y1) → LOG2(s(quot(minus(x0, s(0)), s(s(0)))), y1)
le(s(x), 0) → false
inc(0) → 0
inc(s(x)) → s(inc(x))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(0, y) → 0
minus(x, 0) → x
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
IF2(false, s(x0), y1) → LOG2(s(quot(minus(x0, s(0)), s(s(0)))), y1)
LOG2(s(x0), y1) → IF(false, le(x0, 0), s(x0), inc(y1))
IF(false, b, x, y) → IF2(b, x, y)
le(s(x), 0) → false
inc(0) → 0
inc(s(x)) → s(inc(x))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(0, y) → 0
minus(x, 0) → x
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
IF(false, y_0, s(z0), y_1) → IF2(y_0, s(z0), y_1) → IF(false, y_0, s(z0), y_1) → IF2(y_0, s(z0), y_1)
IF2(false, s(x0), y1) → LOG2(s(quot(minus(x0, s(0)), s(s(0)))), y1)
LOG2(s(x0), y1) → IF(false, le(x0, 0), s(x0), inc(y1))
IF(false, y_0, s(z0), y_1) → IF2(y_0, s(z0), y_1)
le(s(x), 0) → false
inc(0) → 0
inc(s(x)) → s(inc(x))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(0, y) → 0
minus(x, 0) → x
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
IF(false, false, s(x1), x2) → IF2(false, s(x1), x2) → IF(false, false, s(x1), x2) → IF2(false, s(x1), x2)
IF2(false, s(x0), y1) → LOG2(s(quot(minus(x0, s(0)), s(s(0)))), y1)
LOG2(s(x0), y1) → IF(false, le(x0, 0), s(x0), inc(y1))
IF(false, false, s(x1), x2) → IF2(false, s(x1), x2)
le(s(x), 0) → false
inc(0) → 0
inc(s(x)) → s(inc(x))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(0, y) → 0
minus(x, 0) → x
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
LOG2(s(s(x0)), y1) → IF(false, false, s(s(x0)), inc(y1)) → LOG2(s(s(x0)), y1) → IF(false, false, s(s(x0)), inc(y1))
IF2(false, s(x0), y1) → LOG2(s(quot(minus(x0, s(0)), s(s(0)))), y1)
IF(false, false, s(x1), x2) → IF2(false, s(x1), x2)
LOG2(s(s(x0)), y1) → IF(false, false, s(s(x0)), inc(y1))
le(s(x), 0) → false
inc(0) → 0
inc(s(x)) → s(inc(x))
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(0, y) → 0
minus(x, 0) → x
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
IF2(false, s(x0), y1) → LOG2(s(quot(minus(x0, s(0)), s(s(0)))), y1)
IF(false, false, s(x1), x2) → IF2(false, s(x1), x2)
LOG2(s(s(x0)), y1) → IF(false, false, s(s(x0)), inc(y1))
inc(0) → 0
inc(s(x)) → s(inc(x))
minus(0, y) → 0
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, 0) → x
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
IF2(false, s(x0), y1) → LOG2(s(quot(minus(x0, s(0)), s(s(0)))), y1)
IF(false, false, s(x1), x2) → IF2(false, s(x1), x2)
LOG2(s(s(x0)), y1) → IF(false, false, s(s(x0)), inc(y1))
inc(0) → 0
inc(s(x)) → s(inc(x))
minus(0, y) → 0
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, 0) → x
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
IF2(false, s(0), y1) → LOG2(s(quot(0, s(s(0)))), y1) → IF2(false, s(0), y1) → LOG2(s(quot(0, s(s(0)))), y1)
IF(false, false, s(x1), x2) → IF2(false, s(x1), x2)
LOG2(s(s(x0)), y1) → IF(false, false, s(s(x0)), inc(y1))
IF2(false, s(0), y1) → LOG2(s(quot(0, s(s(0)))), y1)
inc(0) → 0
inc(s(x)) → s(inc(x))
minus(0, y) → 0
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
minus(x, 0) → x
inc(0)
inc(s(x0))
minus(0, x0)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))