Termination w.r.t. Q of the given QTRS could be proven:

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

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

Q is empty.

(1) AAECC Innermost (EQUIVALENT transformation)

We have applied [NOC,AAECCNOC] to switch to innermost. The TRS R 1 is

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)

The TRS R 2 is

a → b
a → c

The signature Sigma is {c, a, b}

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(4) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

We have to consider all minimal (P,Q,R)-chains.

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 5 SCCs with 10 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

We have to consider all minimal (P,Q,R)-chains.

(8) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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))

R is empty.
The set Q consists of the following terms:

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

We have to consider all minimal (P,Q,R)-chains.

(10) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

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

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• DIV(s(x), y, s(z)) → DIV(x, y, z)
  The graph contains the following edges 1 > 1, 2 >= 2, 3 > 3

• DIV(x, y, 0) → DIVISIBLE(x, y)
  The graph contains the following edges 1 >= 1, 2 >= 2

• DIVISIBLE(s(x), s(y)) → DIV(s(x), s(y), s(y))
  The graph contains the following edges 1 >= 1, 2 >= 2, 2 >= 3

(13) TRUE

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GE(s(x), s(y)) → GE(x, y)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

We have to consider all minimal (P,Q,R)-chains.

(15) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GE(s(x), s(y)) → GE(x, y)

R is empty.
The set Q consists of the following terms:

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

We have to consider all minimal (P,Q,R)-chains.

(17) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

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

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GE(s(x), s(y)) → GE(x, y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• GE(s(x), s(y)) → GE(x, y)
  The graph contains the following edges 1 > 1, 2 > 2

(20) TRUE

(21) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUS(s(x), y) → PLUS(x, y)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

We have to consider all minimal (P,Q,R)-chains.

(22) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(23) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUS(s(x), y) → PLUS(x, y)

R is empty.
The set Q consists of the following terms:

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

We have to consider all minimal (P,Q,R)-chains.

(24) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

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

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PLUS(s(x), y) → PLUS(x, y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• PLUS(s(x), y) → PLUS(x, y)
  The graph contains the following edges 1 > 1, 2 >= 2

(27) TRUE

(28) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFTIMES(false, x, y) → TIMES(y, p(x))
TIMES(x, y) → IFTIMES(ge(0, x), x, y)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

We have to consider all minimal (P,Q,R)-chains.

(29) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(30) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFTIMES(false, x, y) → TIMES(y, p(x))
TIMES(x, y) → IFTIMES(ge(0, x), x, y)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(y)) → false
p(s(x)) → x
p(0) → s(s(0))

The set Q consists of the following terms:

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

We have to consider all minimal (P,Q,R)-chains.

(31) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

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

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFTIMES(false, x, y) → TIMES(y, p(x))
TIMES(x, y) → IFTIMES(ge(0, x), x, y)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(y)) → false
p(s(x)) → x
p(0) → s(s(0))

The set Q consists of the following terms:

p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(33) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule TIMES(x, y) → IFTIMES(ge(0, x), x, y) at position [0] we obtained the following new rules [LPAR04]:

TIMES(0, y1) → IFTIMES(true, 0, y1)
TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IFTIMES(false, x, y) → TIMES(y, p(x))
TIMES(0, y1) → IFTIMES(true, 0, y1)
TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(y)) → false
p(s(x)) → x
p(0) → s(s(0))

The set Q consists of the following terms:

p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(35) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(36) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, x, y) → TIMES(y, p(x))

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(y)) → false
p(s(x)) → x
p(0) → s(s(0))

The set Q consists of the following terms:

p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(37) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(38) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, x, y) → TIMES(y, p(x))

The TRS R consists of the following rules:

p(s(x)) → x
p(0) → s(s(0))

The set Q consists of the following terms:

p(s(x0))
p(0)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(39) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

(40) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, x, y) → TIMES(y, p(x))

The TRS R consists of the following rules:

p(s(x)) → x
p(0) → s(s(0))

The set Q consists of the following terms:

p(s(x0))
p(0)

We have to consider all minimal (P,Q,R)-chains.

(41) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IFTIMES(false, x, y) → TIMES(y, p(x)) we obtained the following new rules [LPAR04]:

IFTIMES(false, s(z0), z1) → TIMES(z1, p(s(z0)))

(42) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, s(z0), z1) → TIMES(z1, p(s(z0)))

The TRS R consists of the following rules:

p(s(x)) → x
p(0) → s(s(0))

The set Q consists of the following terms:

p(s(x0))
p(0)

We have to consider all minimal (P,Q,R)-chains.

(43) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IFTIMES(false, x, y) → TIMES(y, p(x)) we obtained the following new rules [LPAR04]:

IFTIMES(false, s(z0), z1) → TIMES(z1, p(s(z0)))

(44) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, s(z0), z1) → TIMES(z1, p(s(z0)))

The TRS R consists of the following rules:

p(s(x)) → x
p(0) → s(s(0))

The set Q consists of the following terms:

p(s(x0))
p(0)

We have to consider all minimal (P,Q,R)-chains.

(45) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(46) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, s(z0), z1) → TIMES(z1, p(s(z0)))

The TRS R consists of the following rules:

p(s(x)) → x

The set Q consists of the following terms:

p(s(x0))
p(0)

We have to consider all minimal (P,Q,R)-chains.

(47) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule IFTIMES(false, s(z0), z1) → TIMES(z1, p(s(z0))) at position [1] we obtained the following new rules [LPAR04]:

IFTIMES(false, s(z0), z1) → TIMES(z1, z0)

(48) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, s(z0), z1) → TIMES(z1, z0)

The TRS R consists of the following rules:

p(s(x)) → x

The set Q consists of the following terms:

p(s(x0))
p(0)

We have to consider all minimal (P,Q,R)-chains.

(49) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(50) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, s(z0), z1) → TIMES(z1, z0)

R is empty.
The set Q consists of the following terms:

p(s(x0))
p(0)

We have to consider all minimal (P,Q,R)-chains.

(51) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

p(s(x0))
p(0)

(52) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, s(z0), z1) → TIMES(z1, z0)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(53) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule IFTIMES(false, s(z0), z1) → TIMES(z1, z0) we obtained the following new rules [LPAR04]:

IFTIMES(false, s(x0), s(y_0)) → TIMES(s(y_0), x0)

(54) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1)
IFTIMES(false, s(x0), s(y_0)) → TIMES(s(y_0), x0)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(55) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule TIMES(s(x0), y1) → IFTIMES(false, s(x0), y1) we obtained the following new rules [LPAR04]:

TIMES(s(x0), s(y_1)) → IFTIMES(false, s(x0), s(y_1))

(56) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(57) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• TIMES(s(x0), s(y_1)) → IFTIMES(false, s(x0), s(y_1))
  The graph contains the following edges 1 >= 2, 2 >= 3

• IFTIMES(false, s(x0), s(y_0)) → TIMES(s(y_0), x0)
  The graph contains the following edges 3 >= 1, 2 > 2

(58) TRUE

(59) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

We have to consider all minimal (P,Q,R)-chains.

(60) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(61) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

We have to consider all minimal (P,Q,R)-chains.

(62) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

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

(63) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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))

We have to consider all minimal (P,Q,R)-chains.

(64) NonInfProof (EQUIVALENT transformation)

The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair IF(false, x, y, z, u) → IF2(divisible(z, y), x, y, z, u) the following chains were created:

• We consider the chain LCMITER(x, y, z, u) → IF(or(ge(0, x), ge(z, u)), x, y, z, u), IF(false, x, y, z, u) → IF2(divisible(z, y), x, y, z, u) which results in the following constraint:
  

  (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))

  
  
  We simplified constraint (1) using rules (I), (II), (III), (VII) which results in the following new constraint:
  

  (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))

  
  
  We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on or(x48, x49)=false which results in the following new constraint:
  

  (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))

  
  
  We simplified constraint (3) using rule (III) which results in the following new constraint:
  

  (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))

  
  
  We simplified constraint (4) using rule (V) (with possible (I) afterwards) using induction on ge(x50, x8)=false which results in the following new constraints:
  

  (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))

  
  
  We simplified constraint (5) using rules (I), (II) which results in the following new constraint:
  

  (7)    (ge(x10, x11)=false ⇒ IF(false, s(x54), x9, x10, x11)≥IF2(divisible(x10, x9), s(x54), x9, x10, x11))

  
  
  We solved constraint (6) using rules (I), (II).We simplified constraint (7) using rule (V) (with possible (I) afterwards) using induction on ge(x10, x11)=false which results in the following new constraints:
  

  (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)))

  
  
  We simplified constraint (8) using rules (I), (II) which results in the following new constraint:
  

  (10)    (IF(false, s(x54), x9, 0, s(x61))≥IF2(divisible(0, x9), s(x54), x9, 0, s(x61)))

  
  
  We simplified constraint (9) using rule (VI) where we applied the induction hypothesis (∀x64,x65:ge(x63, x62)=false ⇒ IF(false, s(x64), x65, x63, x62)≥IF2(divisible(x63, x65), s(x64), x65, x63, x62)) with σ = [x65 / x9, x64 / x54] which results in the following new constraint:
  

  (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)))

  
  
  

For Pair IF2(false, x, y, z, u) → LCMITER(x, y, plus(x, z), u) the following chains were created:

• We consider the chain 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) which results in the following constraint:
  

  (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))

  
  
  We simplified constraint (12) using rules (I), (II), (III) which results in the following new constraint:
  

  (13)    (divisible(x18, x17)=false ⇒ IF2(false, x16, x17, x18, x19)≥LCMITER(x16, x17, plus(x16, x18), x19))

  
  
  We simplified constraint (13) using rule (V) (with possible (I) afterwards) using induction on divisible(x18, x17)=false which results in the following new constraint:
  

  (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))

  
  
  We simplified constraint (14) using rule (VII) which results in the following new constraint:
  

  (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))

  
  
  We simplified constraint (15) using rule (V) (with possible (I) afterwards) using induction on div(x69, x70, x71)=false which results in the following new constraints:
  

  (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))

  
  
  We solved constraint (16) using rules (I), (II).We simplified constraint (17) using rules (I), (II), (III), (IV) which results in the following new constraint:
  

  (19)    (IF2(false, x16, s(x74), s(x76), x19)≥LCMITER(x16, s(x74), plus(x16, s(x76)), x19))

  
  
  We solved constraint (18) using rules (I), (II).

For Pair LCMITER(x, y, z, u) → IF(or(ge(0, x), ge(z, u)), x, y, z, u) the following chains were created:

• We consider the chain 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) which results in the following constraint:
  

  (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))

  
  
  We simplified constraint (20) using rules (I), (II), (III), (IV) which results in the following new constraint:
  

  (21)    (LCMITER(x36, x37, x42, x39)≥IF(or(ge(0, x36), ge(x42, x39)), x36, x37, x42, x39))

  
  
  

To summarize, we get the following constraints P_≥ for the following pairs.

• IF(false, x, y, z, u) → IF2(divisible(z, y), x, y, z, u)
  
  • (IF(false, s(x54), x9, 0, s(x61))≥IF2(divisible(0, x9), s(x54), x9, 0, s(x61)))
    
  • (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)))
    
  
  
• IF2(false, x, y, z, u) → LCMITER(x, y, plus(x, z), u)
  
  • (IF2(false, x16, s(x74), s(x76), x19)≥LCMITER(x16, s(x74), plus(x16, s(x76)), x19))
    
  
  
• LCMITER(x, y, z, u) → IF(or(ge(0, x), ge(z, u)), x, y, z, u)
  
  • (LCMITER(x36, x37, x42, x39)≥IF(or(ge(0, x36), ge(x42, x39)), x36, x37, x42, x39))
    
  
  

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation [NONINF]:

POL(0) = 0   
POL(IF(x₁, x₂, x₃, x₄, x₅)) = -1 - x₁ + x₃ - x₄ + x₅   
POL(IF2(x₁, x₂, x₃, x₄, x₅)) = -1 - x₁ - x₂ + x₃ - x₄ + x₅   
POL(LCMITER(x₁, x₂, x₃, x₄)) = -1 + x₂ - x₃ + x₄   
POL(c) = -1   
POL(div(x₁, x₂, x₃)) = 0   
POL(divisible(x₁, x₂)) = 0   
POL(false) = 0   
POL(ge(x₁, x₂)) = 0   
POL(or(x₁, x₂)) = 0   
POL(plus(x₁, x₂)) = x₁ + x₂   
POL(s(x₁)) = 1 + x₁   
POL(true) = 0   

The following pairs are in P_>:

IF(false, x, y, z, u) → IF2(divisible(z, y), x, y, z, u)

The following pairs are in P_bound:

IF(false, x, y, z, u) → IF2(divisible(z, y), x, y, z, u)

The following rules are usable:

div(s(x), s(y), s(y)) → divisible(s(x), s(y))
divisible(x, y) → div(x, y, 0)
div(x, y, z) → div(s(x), y, s(z))
true → divisible(0, s(y))
s(plus(x, y)) → plus(s(x), y)
y → plus(0, y)
y → or(false, y)
true → or(true, y)
false → div(0, y, s(z))

(65) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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))

We have to consider all minimal (P,Q,R)-chains.

(66) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(67) TRUE