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 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 QDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 QDP
↳24 QReductionProof (⇔, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 QDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 QDP
↳31 QReductionProof (⇔, 0 ms)
↳32 QDP
↳33 QDPOrderProof (⇔, 0 ms)
↳34 QDP
↳35 PisEmptyProof (⇔, 0 ms)
↳36 YES
↳37 QDP
↳38 UsableRulesProof (⇔, 0 ms)
↳39 QDP
↳40 QReductionProof (⇔, 0 ms)
↳41 QDP
↳42 TransformationProof (⇔, 0 ms)
↳43 QDP
↳44 DependencyGraphProof (⇔, 0 ms)
↳45 QDP
↳46 TransformationProof (⇔, 0 ms)
↳47 QDP
↳48 TransformationProof (⇔, 0 ms)
↳49 QDP
↳50 TransformationProof (⇔, 0 ms)
↳51 QDP
↳52 TransformationProof (⇔, 0 ms)
↳53 QDP
↳54 DependencyGraphProof (⇔, 0 ms)
↳55 QDP
↳56 UsableRulesProof (⇔, 0 ms)
↳57 QDP
↳58 TransformationProof (⇔, 0 ms)
↳59 QDP
↳60 UsableRulesProof (⇔, 0 ms)
↳61 QDP
↳62 QReductionProof (⇔, 0 ms)
↳63 QDP
↳64 TransformationProof (⇔, 0 ms)
↳65 QDP
↳66 TransformationProof (⇔, 0 ms)
↳67 QDP
↳68 TransformationProof (⇔, 0 ms)
↳69 QDP
↳70 TransformationProof (⇔, 0 ms)
↳71 QDP
↳72 TransformationProof (⇔, 0 ms)
↳73 QDP
↳74 DependencyGraphProof (⇔, 0 ms)
↳75 QDP
↳76 QDPOrderProof (⇔, 0 ms)
↳77 QDP
↳78 DependencyGraphProof (⇔, 0 ms)
↳79 TRUE
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)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
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)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
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))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
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)
LE(s(x), s(y)) → LE(x, y)
INC(s(x)) → INC(x)
LOG(x) → LOGITER(x, 0)
LOGITER(x, y) → IF(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
LOGITER(x, y) → LE(s(0), x)
LOGITER(x, y) → LE(s(s(0)), x)
LOGITER(x, y) → QUOT(x, s(s(0)))
LOGITER(x, y) → INC(y)
IF(true, true, x, y) → LOGITER(x, y)
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)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
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))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
INC(s(x)) → INC(x)
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)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
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))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
INC(s(x)) → INC(x)
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))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
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))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, 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)
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)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
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))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
LE(s(x), s(y)) → LE(x, y)
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))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
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))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
LE(s(x), s(y)) → LE(x, y)
From the DPs we obtained the following set of size-change graphs:
MINUS(s(x), s(y)) → MINUS(x, y)
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)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
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))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
MINUS(s(x), s(y)) → MINUS(x, y)
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))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
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))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, 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))
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)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
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))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
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))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
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
dummyConstant=1
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
LOGITER(x, y) → IF(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
IF(true, true, x, y) → LOGITER(x, y)
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)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
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))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
LOGITER(x, y) → IF(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
IF(true, true, x, y) → LOGITER(x, y)
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
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))
inc(s(x0))
inc(0)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
log(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
LOGITER(x, y) → IF(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
IF(true, true, x, y) → LOGITER(x, y)
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
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))
inc(s(x0))
inc(0)
LOGITER(0, y1) → IF(false, le(s(s(0)), 0), quot(0, s(s(0))), inc(y1)) → LOGITER(0, y1) → IF(false, le(s(s(0)), 0), quot(0, s(s(0))), inc(y1))
LOGITER(s(x1), y1) → IF(le(0, x1), le(s(s(0)), s(x1)), quot(s(x1), s(s(0))), inc(y1)) → LOGITER(s(x1), y1) → IF(le(0, x1), le(s(s(0)), s(x1)), quot(s(x1), s(s(0))), inc(y1))
IF(true, true, x, y) → LOGITER(x, y)
LOGITER(0, y1) → IF(false, le(s(s(0)), 0), quot(0, s(s(0))), inc(y1))
LOGITER(s(x1), y1) → IF(le(0, x1), le(s(s(0)), s(x1)), quot(s(x1), s(s(0))), inc(y1))
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
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))
inc(s(x0))
inc(0)
LOGITER(s(x1), y1) → IF(le(0, x1), le(s(s(0)), s(x1)), quot(s(x1), s(s(0))), inc(y1))
IF(true, true, x, y) → LOGITER(x, y)
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
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))
inc(s(x0))
inc(0)
LOGITER(s(x1), y1) → IF(true, le(s(s(0)), s(x1)), quot(s(x1), s(s(0))), inc(y1)) → LOGITER(s(x1), y1) → IF(true, le(s(s(0)), s(x1)), quot(s(x1), s(s(0))), inc(y1))
IF(true, true, x, y) → LOGITER(x, y)
LOGITER(s(x1), y1) → IF(true, le(s(s(0)), s(x1)), quot(s(x1), s(s(0))), inc(y1))
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
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))
inc(s(x0))
inc(0)
LOGITER(s(x1), y1) → IF(true, le(s(0), x1), quot(s(x1), s(s(0))), inc(y1)) → LOGITER(s(x1), y1) → IF(true, le(s(0), x1), quot(s(x1), s(s(0))), inc(y1))
IF(true, true, x, y) → LOGITER(x, y)
LOGITER(s(x1), y1) → IF(true, le(s(0), x1), quot(s(x1), s(s(0))), inc(y1))
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
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))
inc(s(x0))
inc(0)
LOGITER(s(x1), y1) → IF(true, le(s(0), x1), s(quot(minus(x1, s(0)), s(s(0)))), inc(y1)) → LOGITER(s(x1), y1) → IF(true, le(s(0), x1), s(quot(minus(x1, s(0)), s(s(0)))), inc(y1))
IF(true, true, x, y) → LOGITER(x, y)
LOGITER(s(x1), y1) → IF(true, le(s(0), x1), s(quot(minus(x1, s(0)), s(s(0)))), inc(y1))
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
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))
inc(s(x0))
inc(0)
LOGITER(s(0), y1) → IF(true, false, s(quot(minus(0, s(0)), s(s(0)))), inc(y1)) → LOGITER(s(0), y1) → IF(true, false, s(quot(minus(0, s(0)), s(s(0)))), inc(y1))
LOGITER(s(s(x1)), y1) → IF(true, le(0, x1), s(quot(minus(s(x1), s(0)), s(s(0)))), inc(y1)) → LOGITER(s(s(x1)), y1) → IF(true, le(0, x1), s(quot(minus(s(x1), s(0)), s(s(0)))), inc(y1))
IF(true, true, x, y) → LOGITER(x, y)
LOGITER(s(0), y1) → IF(true, false, s(quot(minus(0, s(0)), s(s(0)))), inc(y1))
LOGITER(s(s(x1)), y1) → IF(true, le(0, x1), s(quot(minus(s(x1), s(0)), s(s(0)))), inc(y1))
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
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))
inc(s(x0))
inc(0)
LOGITER(s(s(x1)), y1) → IF(true, le(0, x1), s(quot(minus(s(x1), s(0)), s(s(0)))), inc(y1))
IF(true, true, x, y) → LOGITER(x, y)
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
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))
inc(s(x0))
inc(0)
LOGITER(s(s(x1)), y1) → IF(true, le(0, x1), s(quot(minus(s(x1), s(0)), s(s(0)))), inc(y1))
IF(true, true, x, y) → LOGITER(x, y)
le(0, y) → true
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)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
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))
inc(s(x0))
inc(0)
LOGITER(s(s(x1)), y1) → IF(true, true, s(quot(minus(s(x1), s(0)), s(s(0)))), inc(y1)) → LOGITER(s(s(x1)), y1) → IF(true, true, s(quot(minus(s(x1), s(0)), s(s(0)))), inc(y1))
IF(true, true, x, y) → LOGITER(x, y)
LOGITER(s(s(x1)), y1) → IF(true, true, s(quot(minus(s(x1), s(0)), s(s(0)))), inc(y1))
le(0, y) → true
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)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
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))
inc(s(x0))
inc(0)
IF(true, true, x, y) → LOGITER(x, y)
LOGITER(s(s(x1)), y1) → IF(true, true, s(quot(minus(s(x1), s(0)), s(s(0)))), inc(y1))
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)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
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))
inc(s(x0))
inc(0)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
IF(true, true, x, y) → LOGITER(x, y)
LOGITER(s(s(x1)), y1) → IF(true, true, s(quot(minus(s(x1), s(0)), s(s(0)))), inc(y1))
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)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
LOGITER(s(s(x1)), y1) → IF(true, true, s(quot(minus(x1, 0), s(s(0)))), inc(y1)) → LOGITER(s(s(x1)), y1) → IF(true, true, s(quot(minus(x1, 0), s(s(0)))), inc(y1))
IF(true, true, x, y) → LOGITER(x, y)
LOGITER(s(s(x1)), y1) → IF(true, true, s(quot(minus(x1, 0), s(s(0)))), inc(y1))
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)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
LOGITER(s(s(x1)), y1) → IF(true, true, s(quot(x1, s(s(0)))), inc(y1)) → LOGITER(s(s(x1)), y1) → IF(true, true, s(quot(x1, s(s(0)))), inc(y1))
IF(true, true, x, y) → LOGITER(x, y)
LOGITER(s(s(x1)), y1) → IF(true, true, s(quot(x1, s(s(0)))), inc(y1))
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)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
IF(true, true, s(y_0), y_1) → LOGITER(s(y_0), y_1) → IF(true, true, s(y_0), y_1) → LOGITER(s(y_0), y_1)
LOGITER(s(s(x1)), y1) → IF(true, true, s(quot(x1, s(s(0)))), inc(y1))
IF(true, true, s(y_0), y_1) → LOGITER(s(y_0), y_1)
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)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
IF(true, true, s(s(y_0)), x1) → LOGITER(s(s(y_0)), x1) → IF(true, true, s(s(y_0)), x1) → LOGITER(s(s(y_0)), x1)
LOGITER(s(s(x1)), y1) → IF(true, true, s(quot(x1, s(s(0)))), inc(y1))
IF(true, true, s(s(y_0)), x1) → LOGITER(s(s(y_0)), x1)
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)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
LOGITER(s(s(0)), y1) → IF(true, true, s(0), inc(y1)) → LOGITER(s(s(0)), y1) → IF(true, true, s(0), inc(y1))
LOGITER(s(s(s(x0))), y1) → IF(true, true, s(s(quot(minus(x0, s(0)), s(s(0))))), inc(y1)) → LOGITER(s(s(s(x0))), y1) → IF(true, true, s(s(quot(minus(x0, s(0)), s(s(0))))), inc(y1))
IF(true, true, s(s(y_0)), x1) → LOGITER(s(s(y_0)), x1)
LOGITER(s(s(0)), y1) → IF(true, true, s(0), inc(y1))
LOGITER(s(s(s(x0))), y1) → IF(true, true, s(s(quot(minus(x0, s(0)), s(s(0))))), inc(y1))
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)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
LOGITER(s(s(s(x0))), y1) → IF(true, true, s(s(quot(minus(x0, s(0)), s(s(0))))), inc(y1))
IF(true, true, s(s(y_0)), x1) → LOGITER(s(s(y_0)), x1)
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)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LOGITER(s(s(s(x0))), y1) → IF(true, true, s(s(quot(minus(x0, s(0)), s(s(0))))), inc(y1))
trivial
s_1=1
0=1
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)))
minus(x, 0) → x
IF(true, true, s(s(y_0)), x1) → LOGITER(s(s(y_0)), x1)
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)))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
minus(x, 0) → x
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
inc(s(x0))
inc(0)