0 QTRS
↳1 AAECC Innermost (⇔)
↳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 Narrowing (⇔)
↳34 QDP
↳35 DependencyGraphProof (⇔)
↳36 QDP
↳37 UsableRulesProof (⇔)
↳38 QDP
↳39 QReductionProof (⇔)
↳40 QDP
↳41 Instantiation (⇔)
↳42 QDP
↳43 Instantiation (⇔)
↳44 QDP
↳45 UsableRulesProof (⇔)
↳46 QDP
↳47 Rewriting (⇔)
↳48 QDP
↳49 UsableRulesProof (⇔)
↳50 QDP
↳51 QReductionProof (⇔)
↳52 QDP
↳53 ForwardInstantiation (⇔)
↳54 QDP
↳55 ForwardInstantiation (⇔)
↳56 QDP
↳57 QDPSizeChangeProof (⇔)
↳58 TRUE
↳59 QDP
↳60 UsableRulesProof (⇔)
↳61 QDP
↳62 QReductionProof (⇔)
↳63 QDP
↳64 NonInfProof (⇔)
↳65 QDP
↳66 DependencyGraphProof (⇔)
↳67 TRUE
lcm(x, y) → lcmIter(x, y, 0, times(x, y))
lcmIter(x, y, z, u) → if(or(ge(0, x), ge(z, u)), x, y, z, u)
if(true, x, y, z, u) → z
if(false, x, y, z, u) → if2(divisible(z, y), x, y, z, u)
if2(true, x, y, z, u) → z
if2(false, x, y, z, u) → lcmIter(x, y, plus(x, z), u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → ifTimes(ge(0, x), x, y)
ifTimes(true, x, y) → 0
ifTimes(false, x, y) → plus(y, times(y, p(x)))
p(s(x)) → x
p(0) → s(s(0))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false
div(s(x), y, s(z)) → div(x, y, z)
a → b
a → c
if(true, x, y, z, u) → z
if(false, x, y, z, u) → if2(divisible(z, y), x, y, z, u)
if2(true, x, y, z, u) → z
if2(false, x, y, z, u) → lcmIter(x, y, plus(x, z), u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → ifTimes(ge(0, x), x, y)
ifTimes(true, x, y) → 0
ifTimes(false, x, y) → plus(y, times(y, p(x)))
p(s(x)) → x
p(0) → s(s(0))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false
div(s(x), y, s(z)) → div(x, y, z)
lcm(x, y) → lcmIter(x, y, 0, times(x, y))
lcmIter(x, y, z, u) → if(or(ge(0, x), ge(z, u)), x, y, z, u)
a → b
a → c
lcm(x, y) → lcmIter(x, y, 0, times(x, y))
lcmIter(x, y, z, u) → if(or(ge(0, x), ge(z, u)), x, y, z, u)
if(true, x, y, z, u) → z
if(false, x, y, z, u) → if2(divisible(z, y), x, y, z, u)
if2(true, x, y, z, u) → z
if2(false, x, y, z, u) → lcmIter(x, y, plus(x, z), u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → ifTimes(ge(0, x), x, y)
ifTimes(true, x, y) → 0
ifTimes(false, x, y) → plus(y, times(y, p(x)))
p(s(x)) → x
p(0) → s(s(0))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false
div(s(x), y, s(z)) → div(x, y, z)
a → b
a → c
lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a
LCM(x, y) → LCMITER(x, y, 0, times(x, y))
LCM(x, y) → TIMES(x, y)
LCMITER(x, y, z, u) → IF(or(ge(0, x), ge(z, u)), x, y, z, u)
LCMITER(x, y, z, u) → OR(ge(0, x), ge(z, u))
LCMITER(x, y, z, u) → GE(0, x)
LCMITER(x, y, z, u) → GE(z, u)
IF(false, x, y, z, u) → IF2(divisible(z, y), x, y, z, u)
IF(false, x, y, z, u) → DIVISIBLE(z, y)
IF2(false, x, y, z, u) → LCMITER(x, y, plus(x, z), u)
IF2(false, x, y, z, u) → PLUS(x, z)
PLUS(s(x), y) → PLUS(x, y)
TIMES(x, y) → IFTIMES(ge(0, x), x, y)
TIMES(x, y) → GE(0, x)
IFTIMES(false, x, y) → PLUS(y, times(y, p(x)))
IFTIMES(false, x, y) → TIMES(y, p(x))
IFTIMES(false, x, y) → P(x)
GE(s(x), s(y)) → GE(x, y)
DIVISIBLE(s(x), s(y)) → DIV(s(x), s(y), s(y))
DIV(x, y, 0) → DIVISIBLE(x, y)
DIV(s(x), y, s(z)) → DIV(x, y, z)
lcm(x, y) → lcmIter(x, y, 0, times(x, y))
lcmIter(x, y, z, u) → if(or(ge(0, x), ge(z, u)), x, y, z, u)
if(true, x, y, z, u) → z
if(false, x, y, z, u) → if2(divisible(z, y), x, y, z, u)
if2(true, x, y, z, u) → z
if2(false, x, y, z, u) → lcmIter(x, y, plus(x, z), u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → ifTimes(ge(0, x), x, y)
ifTimes(true, x, y) → 0
ifTimes(false, x, y) → plus(y, times(y, p(x)))
p(s(x)) → x
p(0) → s(s(0))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false
div(s(x), y, s(z)) → div(x, y, z)
a → b
a → c
lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a
DIV(s(x), y, s(z)) → DIV(x, y, z)
DIV(x, y, 0) → DIVISIBLE(x, y)
DIVISIBLE(s(x), s(y)) → DIV(s(x), s(y), s(y))
lcm(x, y) → lcmIter(x, y, 0, times(x, y))
lcmIter(x, y, z, u) → if(or(ge(0, x), ge(z, u)), x, y, z, u)
if(true, x, y, z, u) → z
if(false, x, y, z, u) → if2(divisible(z, y), x, y, z, u)
if2(true, x, y, z, u) → z
if2(false, x, y, z, u) → lcmIter(x, y, plus(x, z), u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → ifTimes(ge(0, x), x, y)
ifTimes(true, x, y) → 0
ifTimes(false, x, y) → plus(y, times(y, p(x)))
p(s(x)) → x
p(0) → s(s(0))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false
div(s(x), y, s(z)) → div(x, y, z)
a → b
a → c
lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a
DIV(s(x), y, s(z)) → DIV(x, y, z)
DIV(x, y, 0) → DIVISIBLE(x, y)
DIVISIBLE(s(x), s(y)) → DIV(s(x), s(y), s(y))
lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a
lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a
DIV(s(x), y, s(z)) → DIV(x, y, z)
DIV(x, y, 0) → DIVISIBLE(x, y)
DIVISIBLE(s(x), s(y)) → DIV(s(x), s(y), s(y))
From the DPs we obtained the following set of size-change graphs:
GE(s(x), s(y)) → GE(x, y)
lcm(x, y) → lcmIter(x, y, 0, times(x, y))
lcmIter(x, y, z, u) → if(or(ge(0, x), ge(z, u)), x, y, z, u)
if(true, x, y, z, u) → z
if(false, x, y, z, u) → if2(divisible(z, y), x, y, z, u)
if2(true, x, y, z, u) → z
if2(false, x, y, z, u) → lcmIter(x, y, plus(x, z), u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → ifTimes(ge(0, x), x, y)
ifTimes(true, x, y) → 0
ifTimes(false, x, y) → plus(y, times(y, p(x)))
p(s(x)) → x
p(0) → s(s(0))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false
div(s(x), y, s(z)) → div(x, y, z)
a → b
a → c
lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a
GE(s(x), s(y)) → GE(x, y)
lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a
lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a
GE(s(x), s(y)) → GE(x, y)
From the DPs we obtained the following set of size-change graphs:
PLUS(s(x), y) → PLUS(x, y)
lcm(x, y) → lcmIter(x, y, 0, times(x, y))
lcmIter(x, y, z, u) → if(or(ge(0, x), ge(z, u)), x, y, z, u)
if(true, x, y, z, u) → z
if(false, x, y, z, u) → if2(divisible(z, y), x, y, z, u)
if2(true, x, y, z, u) → z
if2(false, x, y, z, u) → lcmIter(x, y, plus(x, z), u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → ifTimes(ge(0, x), x, y)
ifTimes(true, x, y) → 0
ifTimes(false, x, y) → plus(y, times(y, p(x)))
p(s(x)) → x
p(0) → s(s(0))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false
div(s(x), y, s(z)) → div(x, y, z)
a → b
a → c
lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a
PLUS(s(x), y) → PLUS(x, y)
lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a
lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a
PLUS(s(x), y) → PLUS(x, y)
From the DPs we obtained the following set of size-change graphs:
IFTIMES(false, x, y) → TIMES(y, p(x))
TIMES(x, y) → IFTIMES(ge(0, x), x, y)
lcm(x, y) → lcmIter(x, y, 0, times(x, y))
lcmIter(x, y, z, u) → if(or(ge(0, x), ge(z, u)), x, y, z, u)
if(true, x, y, z, u) → z
if(false, x, y, z, u) → if2(divisible(z, y), x, y, z, u)
if2(true, x, y, z, u) → z
if2(false, x, y, z, u) → lcmIter(x, y, plus(x, z), u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → ifTimes(ge(0, x), x, y)
ifTimes(true, x, y) → 0
ifTimes(false, x, y) → plus(y, times(y, p(x)))
p(s(x)) → x
p(0) → s(s(0))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false
div(s(x), y, s(z)) → div(x, y, z)
a → b
a → c
lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a
IFTIMES(false, x, y) → TIMES(y, p(x))
TIMES(x, y) → IFTIMES(ge(0, x), x, y)
ge(x, 0) → true
ge(0, s(y)) → false
p(s(x)) → x
p(0) → s(s(0))
lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a
lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a
IFTIMES(false, x, y) → TIMES(y, p(x))
TIMES(x, y) → IFTIMES(ge(0, x), x, y)
ge(x, 0) → true
ge(0, s(y)) → false
p(s(x)) → x
p(0) → s(s(0))
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
TIMES(0, y1) → IFTIMES(true, 0, y1)
TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, x, y) → TIMES(y, p(x))
TIMES(0, y1) → IFTIMES(true, 0, y1)
TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
ge(x, 0) → true
ge(0, s(y)) → false
p(s(x)) → x
p(0) → s(s(0))
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, x, y) → TIMES(y, p(x))
ge(x, 0) → true
ge(0, s(y)) → false
p(s(x)) → x
p(0) → s(s(0))
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, x, y) → TIMES(y, p(x))
p(s(x)) → x
p(0) → s(s(0))
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, x, y) → TIMES(y, p(x))
p(s(x)) → x
p(0) → s(s(0))
p(s(x0))
p(0)
IFTIMES(false, s(z0), z1) → TIMES(z1, p(s(z0)))
TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, s(z0), z1) → TIMES(z1, p(s(z0)))
p(s(x)) → x
p(0) → s(s(0))
p(s(x0))
p(0)
IFTIMES(false, s(z0), z1) → TIMES(z1, p(s(z0)))
TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, s(z0), z1) → TIMES(z1, p(s(z0)))
p(s(x)) → x
p(0) → s(s(0))
p(s(x0))
p(0)
TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, s(z0), z1) → TIMES(z1, p(s(z0)))
p(s(x)) → x
p(s(x0))
p(0)
IFTIMES(false, s(z0), z1) → TIMES(z1, z0)
TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, s(z0), z1) → TIMES(z1, z0)
p(s(x)) → x
p(s(x0))
p(0)
TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, s(z0), z1) → TIMES(z1, z0)
p(s(x0))
p(0)
p(s(x0))
p(0)
TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, s(z0), z1) → TIMES(z1, z0)
IFTIMES(false, s(x0), s(y_0)) → TIMES(s(y_0), x0)
TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, s(x0), s(y_0)) → TIMES(s(y_0), x0)
TIMES(s(x0), s(y_1)) → IFTIMES(false, s(x0), s(y_1))
IFTIMES(false, s(x0), s(y_0)) → TIMES(s(y_0), x0)
TIMES(s(x0), s(y_1)) → IFTIMES(false, s(x0), s(y_1))
From the DPs we obtained the following set of size-change graphs:
IF(false, x, y, z, u) → IF2(divisible(z, y), x, y, z, u)
IF2(false, x, y, z, u) → LCMITER(x, y, plus(x, z), u)
LCMITER(x, y, z, u) → IF(or(ge(0, x), ge(z, u)), x, y, z, u)
lcm(x, y) → lcmIter(x, y, 0, times(x, y))
lcmIter(x, y, z, u) → if(or(ge(0, x), ge(z, u)), x, y, z, u)
if(true, x, y, z, u) → z
if(false, x, y, z, u) → if2(divisible(z, y), x, y, z, u)
if2(true, x, y, z, u) → z
if2(false, x, y, z, u) → lcmIter(x, y, plus(x, z), u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → ifTimes(ge(0, x), x, y)
ifTimes(true, x, y) → 0
ifTimes(false, x, y) → plus(y, times(y, p(x)))
p(s(x)) → x
p(0) → s(s(0))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(0, y, s(z)) → false
div(s(x), y, s(z)) → div(x, y, z)
a → b
a → c
lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a
IF(false, x, y, z, u) → IF2(divisible(z, y), x, y, z, u)
IF2(false, x, y, z, u) → LCMITER(x, y, plus(x, z), u)
LCMITER(x, y, z, u) → IF(or(ge(0, x), ge(z, u)), x, y, z, u)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(s(x), y, s(z)) → div(x, y, z)
div(0, y, s(z)) → false
lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
a
lcm(x0, x1)
lcmIter(x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
times(x0, x1)
ifTimes(true, x0, x1)
ifTimes(false, x0, x1)
p(s(x0))
p(0)
a
IF(false, x, y, z, u) → IF2(divisible(z, y), x, y, z, u)
IF2(false, x, y, z, u) → LCMITER(x, y, plus(x, z), u)
LCMITER(x, y, z, u) → IF(or(ge(0, x), ge(z, u)), x, y, z, u)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(s(x), y, s(z)) → div(x, y, z)
div(0, y, s(z)) → false
plus(0, x0)
plus(s(x0), x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))
(1) (IF(or(ge(0, x8), ge(x10, x11)), x8, x9, x10, x11)=IF(false, x12, x13, x14, x15) ⇒ IF(false, x12, x13, x14, x15)≥IF2(divisible(x14, x13), x12, x13, x14, x15))
(2) (0=x50∧ge(x50, x8)=x48∧ge(x10, x11)=x49∧or(x48, x49)=false ⇒ IF(false, x8, x9, x10, x11)≥IF2(divisible(x10, x9), x8, x9, x10, x11))
(3) (x52=false∧0=x50∧ge(x50, x8)=false∧ge(x10, x11)=x52 ⇒ IF(false, x8, x9, x10, x11)≥IF2(divisible(x10, x9), x8, x9, x10, x11))
(4) (0=x50∧ge(x50, x8)=false∧ge(x10, x11)=false ⇒ IF(false, x8, x9, x10, x11)≥IF2(divisible(x10, x9), x8, x9, x10, x11))
(5) (false=false∧0=0∧ge(x10, x11)=false ⇒ IF(false, s(x54), x9, x10, x11)≥IF2(divisible(x10, x9), s(x54), x9, x10, x11))
(6) (ge(x56, x55)=false∧0=s(x56)∧ge(x10, x11)=false∧(∀x57,x58,x59:ge(x56, x55)=false∧0=x56∧ge(x57, x58)=false ⇒ IF(false, x55, x59, x57, x58)≥IF2(divisible(x57, x59), x55, x59, x57, x58)) ⇒ IF(false, s(x55), x9, x10, x11)≥IF2(divisible(x10, x9), s(x55), x9, x10, x11))
(7) (ge(x10, x11)=false ⇒ IF(false, s(x54), x9, x10, x11)≥IF2(divisible(x10, x9), s(x54), x9, x10, x11))
(8) (false=false ⇒ IF(false, s(x54), x9, 0, s(x61))≥IF2(divisible(0, x9), s(x54), x9, 0, s(x61)))
(9) (ge(x63, x62)=false∧(∀x64,x65:ge(x63, x62)=false ⇒ IF(false, s(x64), x65, x63, x62)≥IF2(divisible(x63, x65), s(x64), x65, x63, x62)) ⇒ IF(false, s(x54), x9, s(x63), s(x62))≥IF2(divisible(s(x63), x9), s(x54), x9, s(x63), s(x62)))
(10) (IF(false, s(x54), x9, 0, s(x61))≥IF2(divisible(0, x9), s(x54), x9, 0, s(x61)))
(11) (IF(false, s(x54), x9, x63, x62)≥IF2(divisible(x63, x9), s(x54), x9, x63, x62) ⇒ IF(false, s(x54), x9, s(x63), s(x62))≥IF2(divisible(s(x63), x9), s(x54), x9, s(x63), s(x62)))
(12) (IF2(divisible(x18, x17), x16, x17, x18, x19)=IF2(false, x20, x21, x22, x23) ⇒ IF2(false, x20, x21, x22, x23)≥LCMITER(x20, x21, plus(x20, x22), x23))
(13) (divisible(x18, x17)=false ⇒ IF2(false, x16, x17, x18, x19)≥LCMITER(x16, x17, plus(x16, x18), x19))
(14) (div(s(x68), s(x67), s(x67))=false ⇒ IF2(false, x16, s(x67), s(x68), x19)≥LCMITER(x16, s(x67), plus(x16, s(x68)), x19))
(15) (s(x68)=x69∧s(x67)=x70∧s(x67)=x71∧div(x69, x70, x71)=false ⇒ IF2(false, x16, s(x67), s(x68), x19)≥LCMITER(x16, s(x67), plus(x16, s(x68)), x19))
(16) (divisible(x73, x72)=false∧s(x68)=x73∧s(x67)=x72∧s(x67)=0 ⇒ IF2(false, x16, s(x67), s(x68), x19)≥LCMITER(x16, s(x67), plus(x16, s(x68)), x19))
(17) (div(x76, x75, x74)=false∧s(x68)=s(x76)∧s(x67)=x75∧s(x67)=s(x74)∧(∀x77,x78,x79,x80:div(x76, x75, x74)=false∧s(x77)=x76∧s(x78)=x75∧s(x78)=x74 ⇒ IF2(false, x79, s(x78), s(x77), x80)≥LCMITER(x79, s(x78), plus(x79, s(x77)), x80)) ⇒ IF2(false, x16, s(x67), s(x68), x19)≥LCMITER(x16, s(x67), plus(x16, s(x68)), x19))
(18) (false=false∧s(x68)=0∧s(x67)=x82∧s(x67)=s(x81) ⇒ IF2(false, x16, s(x67), s(x68), x19)≥LCMITER(x16, s(x67), plus(x16, s(x68)), x19))
(19) (IF2(false, x16, s(x74), s(x76), x19)≥LCMITER(x16, s(x74), plus(x16, s(x76)), x19))
(20) (LCMITER(x36, x37, plus(x36, x38), x39)=LCMITER(x40, x41, x42, x43) ⇒ LCMITER(x40, x41, x42, x43)≥IF(or(ge(0, x40), ge(x42, x43)), x40, x41, x42, x43))
(21) (LCMITER(x36, x37, x42, x39)≥IF(or(ge(0, x36), ge(x42, x39)), x36, x37, x42, x39))
POL(0) = 0
POL(IF(x1, x2, x3, x4, x5)) = -1 + x1 + x2 - x4 + x5
POL(IF2(x1, x2, x3, x4, x5)) = -1 - x4 + x5
POL(LCMITER(x1, x2, x3, x4)) = -1 + x1 - x3 + x4
POL(c) = -2
POL(div(x1, x2, x3)) = 0
POL(divisible(x1, x2)) = 1
POL(false) = 0
POL(ge(x1, x2)) = 0
POL(or(x1, x2)) = x2
POL(plus(x1, x2)) = x1 + x2
POL(s(x1)) = 1 + x1
POL(true) = 0
The following pairs are in Pbound:
IF(false, x, y, z, u) → IF2(divisible(z, y), x, y, z, u)
The following rules are usable:
IF(false, x, y, z, u) → IF2(divisible(z, y), x, y, z, u)
y → plus(0, y)
s(plus(x, y)) → plus(s(x), y)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
IF2(false, x, y, z, u) → LCMITER(x, y, plus(x, z), u)
LCMITER(x, y, z, u) → IF(or(ge(0, x), ge(z, u)), x, y, z, u)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
or(true, y) → true
or(false, y) → y
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
divisible(0, s(y)) → true
divisible(s(x), s(y)) → div(s(x), s(y), s(y))
div(x, y, 0) → divisible(x, y)
div(s(x), y, s(z)) → div(x, y, z)
div(0, y, s(z)) → false
plus(0, x0)
plus(s(x0), x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
or(true, x0)
or(false, x0)
divisible(0, s(x0))
divisible(s(x0), s(x1))
div(x0, x1, 0)
div(0, x0, s(x1))
div(s(x0), x1, s(x2))