(0) Obligation:

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

times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(nil) → 0
sum(cons(0, xs)) → sum(xs)
sum(cons(s(x), xs)) → s(sum(cons(x, xs)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)

Q is empty.

(1) Overlay + Local Confluence (EQUIVALENT transformation)

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

(2) Obligation:

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

times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(nil) → 0
sum(cons(0, xs)) → sum(xs)
sum(cons(s(x), xs)) → s(sum(cons(x, xs)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(nil)
sum(cons(0, x0))
sum(cons(s(x0), x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

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

TIMES(x, y) → SUM(generate(x, y))
TIMES(x, y) → GENERATE(x, y)
GENERATE(x, y) → GEN(x, y, 0)
GEN(x, y, z) → IF(ge(z, x), x, y, z)
GEN(x, y, z) → GE(z, x)
IF(false, x, y, z) → GEN(x, y, s(z))
SUM(cons(0, xs)) → SUM(xs)
SUM(cons(s(x), xs)) → SUM(cons(x, xs))
GE(s(x), s(y)) → GE(x, y)

The TRS R consists of the following rules:

times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(nil) → 0
sum(cons(0, xs)) → sum(xs)
sum(cons(s(x), xs)) → s(sum(cons(x, xs)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(nil)
sum(cons(0, x0))
sum(cons(s(x0), x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

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

times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(nil) → 0
sum(cons(0, xs)) → sum(xs)
sum(cons(s(x), xs)) → s(sum(cons(x, xs)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(nil)
sum(cons(0, x0))
sum(cons(s(x0), x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

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

(8) Obligation:

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

SUM(cons(s(x), xs)) → SUM(cons(x, xs))
SUM(cons(0, xs)) → SUM(xs)

The TRS R consists of the following rules:

times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(nil) → 0
sum(cons(0, xs)) → sum(xs)
sum(cons(s(x), xs)) → s(sum(cons(x, xs)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(nil)
sum(cons(0, x0))
sum(cons(s(x0), x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

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

(9) Obligation:

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

IF(false, x, y, z) → GEN(x, y, s(z))
GEN(x, y, z) → IF(ge(z, x), x, y, z)

The TRS R consists of the following rules:

times(x, y) → sum(generate(x, y))
generate(x, y) → gen(x, y, 0)
gen(x, y, z) → if(ge(z, x), x, y, z)
if(true, x, y, z) → nil
if(false, x, y, z) → cons(y, gen(x, y, s(z)))
sum(nil) → 0
sum(cons(0, xs)) → sum(xs)
sum(cons(s(x), xs)) → s(sum(cons(x, xs)))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

times(x0, x1)
generate(x0, x1)
gen(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
sum(nil)
sum(cons(0, x0))
sum(cons(s(x0), x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

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