WORST_CASE(Omega(n^1),?)
proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 1399 ms]
(2) CpxRelTRS
(3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) SlicingProof [LOWER BOUND(ID), 9 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 40 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 1004 ms]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 47 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 33 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 80 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 78 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 109 ms]
        (26) typed CpxTrs


----------------------------------------

(0)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   PROD(z0) -> c1(PRODITER(z0, s(0)))
   PRODITER(z0, z1) -> c2(IFPROD(isempty(z0), z0, z1), ISEMPTY(z0))
   IFPROD(true, z0, z1) -> c3
   IFPROD(false, z0, z1) -> c4(PRODITER(tail(z0), times(z1, head(z0))), TAIL(z0))
   IFPROD(false, z0, z1) -> c5(PRODITER(tail(z0), times(z1, head(z0))), TIMES(z1, head(z0)), HEAD(z0))
   PLUS(0, z0) -> c6
   PLUS(s(z0), z1) -> c7(PLUS(z0, z1))
   TIMES(z0, z1) -> c8(TIMESITER(z0, z1, 0, 0))
   TIMESITER(z0, z1, z2, z3) -> c9(IFTIMES(ge(z3, z0), z0, z1, z2, z3), GE(z3, z0))
   IFTIMES(true, z0, z1, z2, z3) -> c10
   IFTIMES(false, z0, z1, z2, z3) -> c11(TIMESITER(z0, z1, plus(z1, z2), s(z3)), PLUS(z1, z2))
   ISEMPTY(nil) -> c12
   ISEMPTY(cons(z0, z1)) -> c13
   HEAD(nil) -> c14
   HEAD(cons(z0, z1)) -> c15
   TAIL(nil) -> c16
   TAIL(cons(z0, z1)) -> c17
   GE(z0, 0) -> c18
   GE(0, s(z0)) -> c19
   GE(s(z0), s(z1)) -> c20(GE(z0, z1))
   A -> c21
   A -> c22

The (relative) TRS S consists of the following rules:

   prod(z0) -> prodIter(z0, s(0))
   prodIter(z0, z1) -> ifProd(isempty(z0), z0, z1)
   ifProd(true, z0, z1) -> z1
   ifProd(false, z0, z1) -> prodIter(tail(z0), times(z1, head(z0)))
   plus(0, z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   times(z0, z1) -> timesIter(z0, z1, 0, 0)
   timesIter(z0, z1, z2, z3) -> ifTimes(ge(z3, z0), z0, z1, z2, z3)
   ifTimes(true, z0, z1, z2, z3) -> z2
   ifTimes(false, z0, z1, z2, z3) -> timesIter(z0, z1, plus(z1, z2), s(z3))
   isempty(nil) -> true
   isempty(cons(z0, z1)) -> false
   head(nil) -> error
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   a -> b
   a -> c

Rewrite Strategy: INNERMOST
----------------------------------------

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

(2)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   PROD(z0) -> c1(PRODITER(z0, s(0)))
   PRODITER(z0, z1) -> c2(IFPROD(isempty(z0), z0, z1), ISEMPTY(z0))
   IFPROD(true, z0, z1) -> c3
   IFPROD(false, z0, z1) -> c4(PRODITER(tail(z0), times(z1, head(z0))), TAIL(z0))
   IFPROD(false, z0, z1) -> c5(PRODITER(tail(z0), times(z1, head(z0))), TIMES(z1, head(z0)), HEAD(z0))
   PLUS(0, z0) -> c6
   PLUS(s(z0), z1) -> c7(PLUS(z0, z1))
   TIMES(z0, z1) -> c8(TIMESITER(z0, z1, 0, 0))
   TIMESITER(z0, z1, z2, z3) -> c9(IFTIMES(ge(z3, z0), z0, z1, z2, z3), GE(z3, z0))
   IFTIMES(true, z0, z1, z2, z3) -> c10
   IFTIMES(false, z0, z1, z2, z3) -> c11(TIMESITER(z0, z1, plus(z1, z2), s(z3)), PLUS(z1, z2))
   ISEMPTY(nil) -> c12
   ISEMPTY(cons(z0, z1)) -> c13
   HEAD(nil) -> c14
   HEAD(cons(z0, z1)) -> c15
   TAIL(nil) -> c16
   TAIL(cons(z0, z1)) -> c17
   GE(z0, 0) -> c18
   GE(0, s(z0)) -> c19
   GE(s(z0), s(z1)) -> c20(GE(z0, z1))
   A -> c21
   A -> c22

The (relative) TRS S consists of the following rules:

   prod(z0) -> prodIter(z0, s(0))
   prodIter(z0, z1) -> ifProd(isempty(z0), z0, z1)
   ifProd(true, z0, z1) -> z1
   ifProd(false, z0, z1) -> prodIter(tail(z0), times(z1, head(z0)))
   plus(0, z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   times(z0, z1) -> timesIter(z0, z1, 0, 0)
   timesIter(z0, z1, z2, z3) -> ifTimes(ge(z3, z0), z0, z1, z2, z3)
   ifTimes(true, z0, z1, z2, z3) -> z2
   ifTimes(false, z0, z1, z2, z3) -> timesIter(z0, z1, plus(z1, z2), s(z3))
   isempty(nil) -> true
   isempty(cons(z0, z1)) -> false
   head(nil) -> error
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   a -> b
   a -> c

Rewrite Strategy: INNERMOST
----------------------------------------

(3) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

(4)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   PROD(z0) -> c1(PRODITER(z0, s(0')))
   PRODITER(z0, z1) -> c2(IFPROD(isempty(z0), z0, z1), ISEMPTY(z0))
   IFPROD(true, z0, z1) -> c3
   IFPROD(false, z0, z1) -> c4(PRODITER(tail(z0), times(z1, head(z0))), TAIL(z0))
   IFPROD(false, z0, z1) -> c5(PRODITER(tail(z0), times(z1, head(z0))), TIMES(z1, head(z0)), HEAD(z0))
   PLUS(0', z0) -> c6
   PLUS(s(z0), z1) -> c7(PLUS(z0, z1))
   TIMES(z0, z1) -> c8(TIMESITER(z0, z1, 0', 0'))
   TIMESITER(z0, z1, z2, z3) -> c9(IFTIMES(ge(z3, z0), z0, z1, z2, z3), GE(z3, z0))
   IFTIMES(true, z0, z1, z2, z3) -> c10
   IFTIMES(false, z0, z1, z2, z3) -> c11(TIMESITER(z0, z1, plus(z1, z2), s(z3)), PLUS(z1, z2))
   ISEMPTY(nil) -> c12
   ISEMPTY(cons(z0, z1)) -> c13
   HEAD(nil) -> c14
   HEAD(cons(z0, z1)) -> c15
   TAIL(nil) -> c16
   TAIL(cons(z0, z1)) -> c17
   GE(z0, 0') -> c18
   GE(0', s(z0)) -> c19
   GE(s(z0), s(z1)) -> c20(GE(z0, z1))
   A -> c21
   A -> c22

The (relative) TRS S consists of the following rules:

   prod(z0) -> prodIter(z0, s(0'))
   prodIter(z0, z1) -> ifProd(isempty(z0), z0, z1)
   ifProd(true, z0, z1) -> z1
   ifProd(false, z0, z1) -> prodIter(tail(z0), times(z1, head(z0)))
   plus(0', z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   times(z0, z1) -> timesIter(z0, z1, 0', 0')
   timesIter(z0, z1, z2, z3) -> ifTimes(ge(z3, z0), z0, z1, z2, z3)
   ifTimes(true, z0, z1, z2, z3) -> z2
   ifTimes(false, z0, z1, z2, z3) -> timesIter(z0, z1, plus(z1, z2), s(z3))
   isempty(nil) -> true
   isempty(cons(z0, z1)) -> false
   head(nil) -> error
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   ge(z0, 0') -> true
   ge(0', s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   a -> b
   a -> c

Rewrite Strategy: INNERMOST
----------------------------------------

(5) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
PLUS/1

----------------------------------------

(6)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   PROD(z0) -> c1(PRODITER(z0, s(0')))
   PRODITER(z0, z1) -> c2(IFPROD(isempty(z0), z0, z1), ISEMPTY(z0))
   IFPROD(true, z0, z1) -> c3
   IFPROD(false, z0, z1) -> c4(PRODITER(tail(z0), times(z1, head(z0))), TAIL(z0))
   IFPROD(false, z0, z1) -> c5(PRODITER(tail(z0), times(z1, head(z0))), TIMES(z1, head(z0)), HEAD(z0))
   PLUS(0') -> c6
   PLUS(s(z0)) -> c7(PLUS(z0))
   TIMES(z0, z1) -> c8(TIMESITER(z0, z1, 0', 0'))
   TIMESITER(z0, z1, z2, z3) -> c9(IFTIMES(ge(z3, z0), z0, z1, z2, z3), GE(z3, z0))
   IFTIMES(true, z0, z1, z2, z3) -> c10
   IFTIMES(false, z0, z1, z2, z3) -> c11(TIMESITER(z0, z1, plus(z1, z2), s(z3)), PLUS(z1))
   ISEMPTY(nil) -> c12
   ISEMPTY(cons(z0, z1)) -> c13
   HEAD(nil) -> c14
   HEAD(cons(z0, z1)) -> c15
   TAIL(nil) -> c16
   TAIL(cons(z0, z1)) -> c17
   GE(z0, 0') -> c18
   GE(0', s(z0)) -> c19
   GE(s(z0), s(z1)) -> c20(GE(z0, z1))
   A -> c21
   A -> c22

The (relative) TRS S consists of the following rules:

   prod(z0) -> prodIter(z0, s(0'))
   prodIter(z0, z1) -> ifProd(isempty(z0), z0, z1)
   ifProd(true, z0, z1) -> z1
   ifProd(false, z0, z1) -> prodIter(tail(z0), times(z1, head(z0)))
   plus(0', z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   times(z0, z1) -> timesIter(z0, z1, 0', 0')
   timesIter(z0, z1, z2, z3) -> ifTimes(ge(z3, z0), z0, z1, z2, z3)
   ifTimes(true, z0, z1, z2, z3) -> z2
   ifTimes(false, z0, z1, z2, z3) -> timesIter(z0, z1, plus(z1, z2), s(z3))
   isempty(nil) -> true
   isempty(cons(z0, z1)) -> false
   head(nil) -> error
   head(cons(z0, z1)) -> z0
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   ge(z0, 0') -> true
   ge(0', s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   a -> b
   a -> c

Rewrite Strategy: INNERMOST
----------------------------------------

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(8)
Obligation:
Innermost TRS:
Rules:
PROD(z0) -> c1(PRODITER(z0, s(0')))
PRODITER(z0, z1) -> c2(IFPROD(isempty(z0), z0, z1), ISEMPTY(z0))
IFPROD(true, z0, z1) -> c3
IFPROD(false, z0, z1) -> c4(PRODITER(tail(z0), times(z1, head(z0))), TAIL(z0))
IFPROD(false, z0, z1) -> c5(PRODITER(tail(z0), times(z1, head(z0))), TIMES(z1, head(z0)), HEAD(z0))
PLUS(0') -> c6
PLUS(s(z0)) -> c7(PLUS(z0))
TIMES(z0, z1) -> c8(TIMESITER(z0, z1, 0', 0'))
TIMESITER(z0, z1, z2, z3) -> c9(IFTIMES(ge(z3, z0), z0, z1, z2, z3), GE(z3, z0))
IFTIMES(true, z0, z1, z2, z3) -> c10
IFTIMES(false, z0, z1, z2, z3) -> c11(TIMESITER(z0, z1, plus(z1, z2), s(z3)), PLUS(z1))
ISEMPTY(nil) -> c12
ISEMPTY(cons(z0, z1)) -> c13
HEAD(nil) -> c14
HEAD(cons(z0, z1)) -> c15
TAIL(nil) -> c16
TAIL(cons(z0, z1)) -> c17
GE(z0, 0') -> c18
GE(0', s(z0)) -> c19
GE(s(z0), s(z1)) -> c20(GE(z0, z1))
A -> c21
A -> c22
prod(z0) -> prodIter(z0, s(0'))
prodIter(z0, z1) -> ifProd(isempty(z0), z0, z1)
ifProd(true, z0, z1) -> z1
ifProd(false, z0, z1) -> prodIter(tail(z0), times(z1, head(z0)))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(z0, z1) -> timesIter(z0, z1, 0', 0')
timesIter(z0, z1, z2, z3) -> ifTimes(ge(z3, z0), z0, z1, z2, z3)
ifTimes(true, z0, z1, z2, z3) -> z2
ifTimes(false, z0, z1, z2, z3) -> timesIter(z0, z1, plus(z1, z2), s(z3))
isempty(nil) -> true
isempty(cons(z0, z1)) -> false
head(nil) -> error
head(cons(z0, z1)) -> z0
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
a -> b
a -> c

Types:
PROD :: nil:cons -> c1
c1 :: c2 -> c1
PRODITER :: nil:cons -> 0':s:error -> c2
s :: 0':s:error -> 0':s:error
0' :: 0':s:error
c2 :: c3:c4:c5 -> c12:c13 -> c2
IFPROD :: true:false -> nil:cons -> 0':s:error -> c3:c4:c5
isempty :: nil:cons -> true:false
ISEMPTY :: nil:cons -> c12:c13
true :: true:false
c3 :: c3:c4:c5
false :: true:false
c4 :: c2 -> c16:c17 -> c3:c4:c5
tail :: nil:cons -> nil:cons
times :: 0':s:error -> 0':s:error -> 0':s:error
head :: nil:cons -> 0':s:error
TAIL :: nil:cons -> c16:c17
c5 :: c2 -> c8 -> c14:c15 -> c3:c4:c5
TIMES :: 0':s:error -> 0':s:error -> c8
HEAD :: nil:cons -> c14:c15
PLUS :: 0':s:error -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c9 -> c8
TIMESITER :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> c9
c9 :: c10:c11 -> c18:c19:c20 -> c9
IFTIMES :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> c10:c11
ge :: 0':s:error -> 0':s:error -> true:false
GE :: 0':s:error -> 0':s:error -> c18:c19:c20
c10 :: c10:c11
c11 :: c9 -> c6:c7 -> c10:c11
plus :: 0':s:error -> 0':s:error -> 0':s:error
nil :: nil:cons
c12 :: c12:c13
cons :: 0':s:error -> nil:cons -> nil:cons
c13 :: c12:c13
c14 :: c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19:c20
c19 :: c18:c19:c20
c20 :: c18:c19:c20 -> c18:c19:c20
A :: c21:c22
c21 :: c21:c22
c22 :: c21:c22
prod :: nil:cons -> 0':s:error
prodIter :: nil:cons -> 0':s:error -> 0':s:error
ifProd :: true:false -> nil:cons -> 0':s:error -> 0':s:error
timesIter :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error
ifTimes :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error
error :: 0':s:error
a :: b:c
b :: b:c
c :: b:c
hole_c11_23 :: c1
hole_nil:cons2_23 :: nil:cons
hole_c23_23 :: c2
hole_0':s:error4_23 :: 0':s:error
hole_c3:c4:c55_23 :: c3:c4:c5
hole_c12:c136_23 :: c12:c13
hole_true:false7_23 :: true:false
hole_c16:c178_23 :: c16:c17
hole_c89_23 :: c8
hole_c14:c1510_23 :: c14:c15
hole_c6:c711_23 :: c6:c7
hole_c912_23 :: c9
hole_c10:c1113_23 :: c10:c11
hole_c18:c19:c2014_23 :: c18:c19:c20
hole_c21:c2215_23 :: c21:c22
hole_b:c16_23 :: b:c
gen_nil:cons17_23 :: Nat -> nil:cons
gen_0':s:error18_23 :: Nat -> 0':s:error
gen_c6:c719_23 :: Nat -> c6:c7
gen_c18:c19:c2020_23 :: Nat -> c18:c19:c20

----------------------------------------

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
PRODITER, PLUS, TIMESITER, ge, GE, plus, prodIter, timesIter

They will be analysed ascendingly in the following order:
PLUS < TIMESITER
ge < TIMESITER
GE < TIMESITER
plus < TIMESITER
ge < timesIter
plus < timesIter

----------------------------------------

(10)
Obligation:
Innermost TRS:
Rules:
PROD(z0) -> c1(PRODITER(z0, s(0')))
PRODITER(z0, z1) -> c2(IFPROD(isempty(z0), z0, z1), ISEMPTY(z0))
IFPROD(true, z0, z1) -> c3
IFPROD(false, z0, z1) -> c4(PRODITER(tail(z0), times(z1, head(z0))), TAIL(z0))
IFPROD(false, z0, z1) -> c5(PRODITER(tail(z0), times(z1, head(z0))), TIMES(z1, head(z0)), HEAD(z0))
PLUS(0') -> c6
PLUS(s(z0)) -> c7(PLUS(z0))
TIMES(z0, z1) -> c8(TIMESITER(z0, z1, 0', 0'))
TIMESITER(z0, z1, z2, z3) -> c9(IFTIMES(ge(z3, z0), z0, z1, z2, z3), GE(z3, z0))
IFTIMES(true, z0, z1, z2, z3) -> c10
IFTIMES(false, z0, z1, z2, z3) -> c11(TIMESITER(z0, z1, plus(z1, z2), s(z3)), PLUS(z1))
ISEMPTY(nil) -> c12
ISEMPTY(cons(z0, z1)) -> c13
HEAD(nil) -> c14
HEAD(cons(z0, z1)) -> c15
TAIL(nil) -> c16
TAIL(cons(z0, z1)) -> c17
GE(z0, 0') -> c18
GE(0', s(z0)) -> c19
GE(s(z0), s(z1)) -> c20(GE(z0, z1))
A -> c21
A -> c22
prod(z0) -> prodIter(z0, s(0'))
prodIter(z0, z1) -> ifProd(isempty(z0), z0, z1)
ifProd(true, z0, z1) -> z1
ifProd(false, z0, z1) -> prodIter(tail(z0), times(z1, head(z0)))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(z0, z1) -> timesIter(z0, z1, 0', 0')
timesIter(z0, z1, z2, z3) -> ifTimes(ge(z3, z0), z0, z1, z2, z3)
ifTimes(true, z0, z1, z2, z3) -> z2
ifTimes(false, z0, z1, z2, z3) -> timesIter(z0, z1, plus(z1, z2), s(z3))
isempty(nil) -> true
isempty(cons(z0, z1)) -> false
head(nil) -> error
head(cons(z0, z1)) -> z0
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
a -> b
a -> c

Types:
PROD :: nil:cons -> c1
c1 :: c2 -> c1
PRODITER :: nil:cons -> 0':s:error -> c2
s :: 0':s:error -> 0':s:error
0' :: 0':s:error
c2 :: c3:c4:c5 -> c12:c13 -> c2
IFPROD :: true:false -> nil:cons -> 0':s:error -> c3:c4:c5
isempty :: nil:cons -> true:false
ISEMPTY :: nil:cons -> c12:c13
true :: true:false
c3 :: c3:c4:c5
false :: true:false
c4 :: c2 -> c16:c17 -> c3:c4:c5
tail :: nil:cons -> nil:cons
times :: 0':s:error -> 0':s:error -> 0':s:error
head :: nil:cons -> 0':s:error
TAIL :: nil:cons -> c16:c17
c5 :: c2 -> c8 -> c14:c15 -> c3:c4:c5
TIMES :: 0':s:error -> 0':s:error -> c8
HEAD :: nil:cons -> c14:c15
PLUS :: 0':s:error -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c9 -> c8
TIMESITER :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> c9
c9 :: c10:c11 -> c18:c19:c20 -> c9
IFTIMES :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> c10:c11
ge :: 0':s:error -> 0':s:error -> true:false
GE :: 0':s:error -> 0':s:error -> c18:c19:c20
c10 :: c10:c11
c11 :: c9 -> c6:c7 -> c10:c11
plus :: 0':s:error -> 0':s:error -> 0':s:error
nil :: nil:cons
c12 :: c12:c13
cons :: 0':s:error -> nil:cons -> nil:cons
c13 :: c12:c13
c14 :: c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19:c20
c19 :: c18:c19:c20
c20 :: c18:c19:c20 -> c18:c19:c20
A :: c21:c22
c21 :: c21:c22
c22 :: c21:c22
prod :: nil:cons -> 0':s:error
prodIter :: nil:cons -> 0':s:error -> 0':s:error
ifProd :: true:false -> nil:cons -> 0':s:error -> 0':s:error
timesIter :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error
ifTimes :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error
error :: 0':s:error
a :: b:c
b :: b:c
c :: b:c
hole_c11_23 :: c1
hole_nil:cons2_23 :: nil:cons
hole_c23_23 :: c2
hole_0':s:error4_23 :: 0':s:error
hole_c3:c4:c55_23 :: c3:c4:c5
hole_c12:c136_23 :: c12:c13
hole_true:false7_23 :: true:false
hole_c16:c178_23 :: c16:c17
hole_c89_23 :: c8
hole_c14:c1510_23 :: c14:c15
hole_c6:c711_23 :: c6:c7
hole_c912_23 :: c9
hole_c10:c1113_23 :: c10:c11
hole_c18:c19:c2014_23 :: c18:c19:c20
hole_c21:c2215_23 :: c21:c22
hole_b:c16_23 :: b:c
gen_nil:cons17_23 :: Nat -> nil:cons
gen_0':s:error18_23 :: Nat -> 0':s:error
gen_c6:c719_23 :: Nat -> c6:c7
gen_c18:c19:c2020_23 :: Nat -> c18:c19:c20


Generator Equations:
gen_nil:cons17_23(0) <=> nil
gen_nil:cons17_23(+(x, 1)) <=> cons(0', gen_nil:cons17_23(x))
gen_0':s:error18_23(0) <=> 0'
gen_0':s:error18_23(+(x, 1)) <=> s(gen_0':s:error18_23(x))
gen_c6:c719_23(0) <=> c6
gen_c6:c719_23(+(x, 1)) <=> c7(gen_c6:c719_23(x))
gen_c18:c19:c2020_23(0) <=> c18
gen_c18:c19:c2020_23(+(x, 1)) <=> c20(gen_c18:c19:c2020_23(x))


The following defined symbols remain to be analysed:
PRODITER, PLUS, TIMESITER, ge, GE, plus, prodIter, timesIter

They will be analysed ascendingly in the following order:
PLUS < TIMESITER
ge < TIMESITER
GE < TIMESITER
plus < TIMESITER
ge < timesIter
plus < timesIter

----------------------------------------

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
PRODITER(gen_nil:cons17_23(n22_23), gen_0':s:error18_23(0)) -> *21_23, rt in Omega(n22_23)

Induction Base:
PRODITER(gen_nil:cons17_23(0), gen_0':s:error18_23(0))

Induction Step:
PRODITER(gen_nil:cons17_23(+(n22_23, 1)), gen_0':s:error18_23(0)) ->_R^Omega(1)
c2(IFPROD(isempty(gen_nil:cons17_23(+(n22_23, 1))), gen_nil:cons17_23(+(n22_23, 1)), gen_0':s:error18_23(0)), ISEMPTY(gen_nil:cons17_23(+(n22_23, 1)))) ->_R^Omega(0)
c2(IFPROD(false, gen_nil:cons17_23(+(1, n22_23)), gen_0':s:error18_23(0)), ISEMPTY(gen_nil:cons17_23(+(1, n22_23)))) ->_R^Omega(1)
c2(c4(PRODITER(tail(gen_nil:cons17_23(+(1, n22_23))), times(gen_0':s:error18_23(0), head(gen_nil:cons17_23(+(1, n22_23))))), TAIL(gen_nil:cons17_23(+(1, n22_23)))), ISEMPTY(gen_nil:cons17_23(+(1, n22_23)))) ->_R^Omega(0)
c2(c4(PRODITER(gen_nil:cons17_23(n22_23), times(gen_0':s:error18_23(0), head(gen_nil:cons17_23(+(1, n22_23))))), TAIL(gen_nil:cons17_23(+(1, n22_23)))), ISEMPTY(gen_nil:cons17_23(+(1, n22_23)))) ->_R^Omega(0)
c2(c4(PRODITER(gen_nil:cons17_23(n22_23), times(gen_0':s:error18_23(0), 0')), TAIL(gen_nil:cons17_23(+(1, n22_23)))), ISEMPTY(gen_nil:cons17_23(+(1, n22_23)))) ->_R^Omega(0)
c2(c4(PRODITER(gen_nil:cons17_23(n22_23), timesIter(gen_0':s:error18_23(0), 0', 0', 0')), TAIL(gen_nil:cons17_23(+(1, n22_23)))), ISEMPTY(gen_nil:cons17_23(+(1, n22_23)))) ->_R^Omega(0)
c2(c4(PRODITER(gen_nil:cons17_23(n22_23), ifTimes(ge(0', gen_0':s:error18_23(0)), gen_0':s:error18_23(0), 0', 0', 0')), TAIL(gen_nil:cons17_23(+(1, n22_23)))), ISEMPTY(gen_nil:cons17_23(+(1, n22_23)))) ->_R^Omega(0)
c2(c4(PRODITER(gen_nil:cons17_23(n22_23), ifTimes(true, gen_0':s:error18_23(0), 0', 0', 0')), TAIL(gen_nil:cons17_23(+(1, n22_23)))), ISEMPTY(gen_nil:cons17_23(+(1, n22_23)))) ->_R^Omega(0)
c2(c4(PRODITER(gen_nil:cons17_23(n22_23), 0'), TAIL(gen_nil:cons17_23(+(1, n22_23)))), ISEMPTY(gen_nil:cons17_23(+(1, n22_23)))) ->_IH
c2(c4(*21_23, TAIL(gen_nil:cons17_23(+(1, n22_23)))), ISEMPTY(gen_nil:cons17_23(+(1, n22_23)))) ->_R^Omega(1)
c2(c4(*21_23, c17), ISEMPTY(gen_nil:cons17_23(+(1, n22_23)))) ->_R^Omega(1)
c2(c4(*21_23, c17), c13)

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(12)
Complex Obligation (BEST)

----------------------------------------

(13)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
PROD(z0) -> c1(PRODITER(z0, s(0')))
PRODITER(z0, z1) -> c2(IFPROD(isempty(z0), z0, z1), ISEMPTY(z0))
IFPROD(true, z0, z1) -> c3
IFPROD(false, z0, z1) -> c4(PRODITER(tail(z0), times(z1, head(z0))), TAIL(z0))
IFPROD(false, z0, z1) -> c5(PRODITER(tail(z0), times(z1, head(z0))), TIMES(z1, head(z0)), HEAD(z0))
PLUS(0') -> c6
PLUS(s(z0)) -> c7(PLUS(z0))
TIMES(z0, z1) -> c8(TIMESITER(z0, z1, 0', 0'))
TIMESITER(z0, z1, z2, z3) -> c9(IFTIMES(ge(z3, z0), z0, z1, z2, z3), GE(z3, z0))
IFTIMES(true, z0, z1, z2, z3) -> c10
IFTIMES(false, z0, z1, z2, z3) -> c11(TIMESITER(z0, z1, plus(z1, z2), s(z3)), PLUS(z1))
ISEMPTY(nil) -> c12
ISEMPTY(cons(z0, z1)) -> c13
HEAD(nil) -> c14
HEAD(cons(z0, z1)) -> c15
TAIL(nil) -> c16
TAIL(cons(z0, z1)) -> c17
GE(z0, 0') -> c18
GE(0', s(z0)) -> c19
GE(s(z0), s(z1)) -> c20(GE(z0, z1))
A -> c21
A -> c22
prod(z0) -> prodIter(z0, s(0'))
prodIter(z0, z1) -> ifProd(isempty(z0), z0, z1)
ifProd(true, z0, z1) -> z1
ifProd(false, z0, z1) -> prodIter(tail(z0), times(z1, head(z0)))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(z0, z1) -> timesIter(z0, z1, 0', 0')
timesIter(z0, z1, z2, z3) -> ifTimes(ge(z3, z0), z0, z1, z2, z3)
ifTimes(true, z0, z1, z2, z3) -> z2
ifTimes(false, z0, z1, z2, z3) -> timesIter(z0, z1, plus(z1, z2), s(z3))
isempty(nil) -> true
isempty(cons(z0, z1)) -> false
head(nil) -> error
head(cons(z0, z1)) -> z0
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
a -> b
a -> c

Types:
PROD :: nil:cons -> c1
c1 :: c2 -> c1
PRODITER :: nil:cons -> 0':s:error -> c2
s :: 0':s:error -> 0':s:error
0' :: 0':s:error
c2 :: c3:c4:c5 -> c12:c13 -> c2
IFPROD :: true:false -> nil:cons -> 0':s:error -> c3:c4:c5
isempty :: nil:cons -> true:false
ISEMPTY :: nil:cons -> c12:c13
true :: true:false
c3 :: c3:c4:c5
false :: true:false
c4 :: c2 -> c16:c17 -> c3:c4:c5
tail :: nil:cons -> nil:cons
times :: 0':s:error -> 0':s:error -> 0':s:error
head :: nil:cons -> 0':s:error
TAIL :: nil:cons -> c16:c17
c5 :: c2 -> c8 -> c14:c15 -> c3:c4:c5
TIMES :: 0':s:error -> 0':s:error -> c8
HEAD :: nil:cons -> c14:c15
PLUS :: 0':s:error -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c9 -> c8
TIMESITER :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> c9
c9 :: c10:c11 -> c18:c19:c20 -> c9
IFTIMES :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> c10:c11
ge :: 0':s:error -> 0':s:error -> true:false
GE :: 0':s:error -> 0':s:error -> c18:c19:c20
c10 :: c10:c11
c11 :: c9 -> c6:c7 -> c10:c11
plus :: 0':s:error -> 0':s:error -> 0':s:error
nil :: nil:cons
c12 :: c12:c13
cons :: 0':s:error -> nil:cons -> nil:cons
c13 :: c12:c13
c14 :: c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19:c20
c19 :: c18:c19:c20
c20 :: c18:c19:c20 -> c18:c19:c20
A :: c21:c22
c21 :: c21:c22
c22 :: c21:c22
prod :: nil:cons -> 0':s:error
prodIter :: nil:cons -> 0':s:error -> 0':s:error
ifProd :: true:false -> nil:cons -> 0':s:error -> 0':s:error
timesIter :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error
ifTimes :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error
error :: 0':s:error
a :: b:c
b :: b:c
c :: b:c
hole_c11_23 :: c1
hole_nil:cons2_23 :: nil:cons
hole_c23_23 :: c2
hole_0':s:error4_23 :: 0':s:error
hole_c3:c4:c55_23 :: c3:c4:c5
hole_c12:c136_23 :: c12:c13
hole_true:false7_23 :: true:false
hole_c16:c178_23 :: c16:c17
hole_c89_23 :: c8
hole_c14:c1510_23 :: c14:c15
hole_c6:c711_23 :: c6:c7
hole_c912_23 :: c9
hole_c10:c1113_23 :: c10:c11
hole_c18:c19:c2014_23 :: c18:c19:c20
hole_c21:c2215_23 :: c21:c22
hole_b:c16_23 :: b:c
gen_nil:cons17_23 :: Nat -> nil:cons
gen_0':s:error18_23 :: Nat -> 0':s:error
gen_c6:c719_23 :: Nat -> c6:c7
gen_c18:c19:c2020_23 :: Nat -> c18:c19:c20


Generator Equations:
gen_nil:cons17_23(0) <=> nil
gen_nil:cons17_23(+(x, 1)) <=> cons(0', gen_nil:cons17_23(x))
gen_0':s:error18_23(0) <=> 0'
gen_0':s:error18_23(+(x, 1)) <=> s(gen_0':s:error18_23(x))
gen_c6:c719_23(0) <=> c6
gen_c6:c719_23(+(x, 1)) <=> c7(gen_c6:c719_23(x))
gen_c18:c19:c2020_23(0) <=> c18
gen_c18:c19:c2020_23(+(x, 1)) <=> c20(gen_c18:c19:c2020_23(x))


The following defined symbols remain to be analysed:
PRODITER, PLUS, TIMESITER, ge, GE, plus, prodIter, timesIter

They will be analysed ascendingly in the following order:
PLUS < TIMESITER
ge < TIMESITER
GE < TIMESITER
plus < TIMESITER
ge < timesIter
plus < timesIter

----------------------------------------

(14) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(15)
BOUNDS(n^1, INF)

----------------------------------------

(16)
Obligation:
Innermost TRS:
Rules:
PROD(z0) -> c1(PRODITER(z0, s(0')))
PRODITER(z0, z1) -> c2(IFPROD(isempty(z0), z0, z1), ISEMPTY(z0))
IFPROD(true, z0, z1) -> c3
IFPROD(false, z0, z1) -> c4(PRODITER(tail(z0), times(z1, head(z0))), TAIL(z0))
IFPROD(false, z0, z1) -> c5(PRODITER(tail(z0), times(z1, head(z0))), TIMES(z1, head(z0)), HEAD(z0))
PLUS(0') -> c6
PLUS(s(z0)) -> c7(PLUS(z0))
TIMES(z0, z1) -> c8(TIMESITER(z0, z1, 0', 0'))
TIMESITER(z0, z1, z2, z3) -> c9(IFTIMES(ge(z3, z0), z0, z1, z2, z3), GE(z3, z0))
IFTIMES(true, z0, z1, z2, z3) -> c10
IFTIMES(false, z0, z1, z2, z3) -> c11(TIMESITER(z0, z1, plus(z1, z2), s(z3)), PLUS(z1))
ISEMPTY(nil) -> c12
ISEMPTY(cons(z0, z1)) -> c13
HEAD(nil) -> c14
HEAD(cons(z0, z1)) -> c15
TAIL(nil) -> c16
TAIL(cons(z0, z1)) -> c17
GE(z0, 0') -> c18
GE(0', s(z0)) -> c19
GE(s(z0), s(z1)) -> c20(GE(z0, z1))
A -> c21
A -> c22
prod(z0) -> prodIter(z0, s(0'))
prodIter(z0, z1) -> ifProd(isempty(z0), z0, z1)
ifProd(true, z0, z1) -> z1
ifProd(false, z0, z1) -> prodIter(tail(z0), times(z1, head(z0)))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(z0, z1) -> timesIter(z0, z1, 0', 0')
timesIter(z0, z1, z2, z3) -> ifTimes(ge(z3, z0), z0, z1, z2, z3)
ifTimes(true, z0, z1, z2, z3) -> z2
ifTimes(false, z0, z1, z2, z3) -> timesIter(z0, z1, plus(z1, z2), s(z3))
isempty(nil) -> true
isempty(cons(z0, z1)) -> false
head(nil) -> error
head(cons(z0, z1)) -> z0
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
a -> b
a -> c

Types:
PROD :: nil:cons -> c1
c1 :: c2 -> c1
PRODITER :: nil:cons -> 0':s:error -> c2
s :: 0':s:error -> 0':s:error
0' :: 0':s:error
c2 :: c3:c4:c5 -> c12:c13 -> c2
IFPROD :: true:false -> nil:cons -> 0':s:error -> c3:c4:c5
isempty :: nil:cons -> true:false
ISEMPTY :: nil:cons -> c12:c13
true :: true:false
c3 :: c3:c4:c5
false :: true:false
c4 :: c2 -> c16:c17 -> c3:c4:c5
tail :: nil:cons -> nil:cons
times :: 0':s:error -> 0':s:error -> 0':s:error
head :: nil:cons -> 0':s:error
TAIL :: nil:cons -> c16:c17
c5 :: c2 -> c8 -> c14:c15 -> c3:c4:c5
TIMES :: 0':s:error -> 0':s:error -> c8
HEAD :: nil:cons -> c14:c15
PLUS :: 0':s:error -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c9 -> c8
TIMESITER :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> c9
c9 :: c10:c11 -> c18:c19:c20 -> c9
IFTIMES :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> c10:c11
ge :: 0':s:error -> 0':s:error -> true:false
GE :: 0':s:error -> 0':s:error -> c18:c19:c20
c10 :: c10:c11
c11 :: c9 -> c6:c7 -> c10:c11
plus :: 0':s:error -> 0':s:error -> 0':s:error
nil :: nil:cons
c12 :: c12:c13
cons :: 0':s:error -> nil:cons -> nil:cons
c13 :: c12:c13
c14 :: c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19:c20
c19 :: c18:c19:c20
c20 :: c18:c19:c20 -> c18:c19:c20
A :: c21:c22
c21 :: c21:c22
c22 :: c21:c22
prod :: nil:cons -> 0':s:error
prodIter :: nil:cons -> 0':s:error -> 0':s:error
ifProd :: true:false -> nil:cons -> 0':s:error -> 0':s:error
timesIter :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error
ifTimes :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error
error :: 0':s:error
a :: b:c
b :: b:c
c :: b:c
hole_c11_23 :: c1
hole_nil:cons2_23 :: nil:cons
hole_c23_23 :: c2
hole_0':s:error4_23 :: 0':s:error
hole_c3:c4:c55_23 :: c3:c4:c5
hole_c12:c136_23 :: c12:c13
hole_true:false7_23 :: true:false
hole_c16:c178_23 :: c16:c17
hole_c89_23 :: c8
hole_c14:c1510_23 :: c14:c15
hole_c6:c711_23 :: c6:c7
hole_c912_23 :: c9
hole_c10:c1113_23 :: c10:c11
hole_c18:c19:c2014_23 :: c18:c19:c20
hole_c21:c2215_23 :: c21:c22
hole_b:c16_23 :: b:c
gen_nil:cons17_23 :: Nat -> nil:cons
gen_0':s:error18_23 :: Nat -> 0':s:error
gen_c6:c719_23 :: Nat -> c6:c7
gen_c18:c19:c2020_23 :: Nat -> c18:c19:c20


Lemmas:
PRODITER(gen_nil:cons17_23(n22_23), gen_0':s:error18_23(0)) -> *21_23, rt in Omega(n22_23)


Generator Equations:
gen_nil:cons17_23(0) <=> nil
gen_nil:cons17_23(+(x, 1)) <=> cons(0', gen_nil:cons17_23(x))
gen_0':s:error18_23(0) <=> 0'
gen_0':s:error18_23(+(x, 1)) <=> s(gen_0':s:error18_23(x))
gen_c6:c719_23(0) <=> c6
gen_c6:c719_23(+(x, 1)) <=> c7(gen_c6:c719_23(x))
gen_c18:c19:c2020_23(0) <=> c18
gen_c18:c19:c2020_23(+(x, 1)) <=> c20(gen_c18:c19:c2020_23(x))


The following defined symbols remain to be analysed:
PLUS, TIMESITER, ge, GE, plus, prodIter, timesIter

They will be analysed ascendingly in the following order:
PLUS < TIMESITER
ge < TIMESITER
GE < TIMESITER
plus < TIMESITER
ge < timesIter
plus < timesIter

----------------------------------------

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
PLUS(gen_0':s:error18_23(n7606_23)) -> gen_c6:c719_23(n7606_23), rt in Omega(1 + n7606_23)

Induction Base:
PLUS(gen_0':s:error18_23(0)) ->_R^Omega(1)
c6

Induction Step:
PLUS(gen_0':s:error18_23(+(n7606_23, 1))) ->_R^Omega(1)
c7(PLUS(gen_0':s:error18_23(n7606_23))) ->_IH
c7(gen_c6:c719_23(c7607_23))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(18)
Obligation:
Innermost TRS:
Rules:
PROD(z0) -> c1(PRODITER(z0, s(0')))
PRODITER(z0, z1) -> c2(IFPROD(isempty(z0), z0, z1), ISEMPTY(z0))
IFPROD(true, z0, z1) -> c3
IFPROD(false, z0, z1) -> c4(PRODITER(tail(z0), times(z1, head(z0))), TAIL(z0))
IFPROD(false, z0, z1) -> c5(PRODITER(tail(z0), times(z1, head(z0))), TIMES(z1, head(z0)), HEAD(z0))
PLUS(0') -> c6
PLUS(s(z0)) -> c7(PLUS(z0))
TIMES(z0, z1) -> c8(TIMESITER(z0, z1, 0', 0'))
TIMESITER(z0, z1, z2, z3) -> c9(IFTIMES(ge(z3, z0), z0, z1, z2, z3), GE(z3, z0))
IFTIMES(true, z0, z1, z2, z3) -> c10
IFTIMES(false, z0, z1, z2, z3) -> c11(TIMESITER(z0, z1, plus(z1, z2), s(z3)), PLUS(z1))
ISEMPTY(nil) -> c12
ISEMPTY(cons(z0, z1)) -> c13
HEAD(nil) -> c14
HEAD(cons(z0, z1)) -> c15
TAIL(nil) -> c16
TAIL(cons(z0, z1)) -> c17
GE(z0, 0') -> c18
GE(0', s(z0)) -> c19
GE(s(z0), s(z1)) -> c20(GE(z0, z1))
A -> c21
A -> c22
prod(z0) -> prodIter(z0, s(0'))
prodIter(z0, z1) -> ifProd(isempty(z0), z0, z1)
ifProd(true, z0, z1) -> z1
ifProd(false, z0, z1) -> prodIter(tail(z0), times(z1, head(z0)))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(z0, z1) -> timesIter(z0, z1, 0', 0')
timesIter(z0, z1, z2, z3) -> ifTimes(ge(z3, z0), z0, z1, z2, z3)
ifTimes(true, z0, z1, z2, z3) -> z2
ifTimes(false, z0, z1, z2, z3) -> timesIter(z0, z1, plus(z1, z2), s(z3))
isempty(nil) -> true
isempty(cons(z0, z1)) -> false
head(nil) -> error
head(cons(z0, z1)) -> z0
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
a -> b
a -> c

Types:
PROD :: nil:cons -> c1
c1 :: c2 -> c1
PRODITER :: nil:cons -> 0':s:error -> c2
s :: 0':s:error -> 0':s:error
0' :: 0':s:error
c2 :: c3:c4:c5 -> c12:c13 -> c2
IFPROD :: true:false -> nil:cons -> 0':s:error -> c3:c4:c5
isempty :: nil:cons -> true:false
ISEMPTY :: nil:cons -> c12:c13
true :: true:false
c3 :: c3:c4:c5
false :: true:false
c4 :: c2 -> c16:c17 -> c3:c4:c5
tail :: nil:cons -> nil:cons
times :: 0':s:error -> 0':s:error -> 0':s:error
head :: nil:cons -> 0':s:error
TAIL :: nil:cons -> c16:c17
c5 :: c2 -> c8 -> c14:c15 -> c3:c4:c5
TIMES :: 0':s:error -> 0':s:error -> c8
HEAD :: nil:cons -> c14:c15
PLUS :: 0':s:error -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c9 -> c8
TIMESITER :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> c9
c9 :: c10:c11 -> c18:c19:c20 -> c9
IFTIMES :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> c10:c11
ge :: 0':s:error -> 0':s:error -> true:false
GE :: 0':s:error -> 0':s:error -> c18:c19:c20
c10 :: c10:c11
c11 :: c9 -> c6:c7 -> c10:c11
plus :: 0':s:error -> 0':s:error -> 0':s:error
nil :: nil:cons
c12 :: c12:c13
cons :: 0':s:error -> nil:cons -> nil:cons
c13 :: c12:c13
c14 :: c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19:c20
c19 :: c18:c19:c20
c20 :: c18:c19:c20 -> c18:c19:c20
A :: c21:c22
c21 :: c21:c22
c22 :: c21:c22
prod :: nil:cons -> 0':s:error
prodIter :: nil:cons -> 0':s:error -> 0':s:error
ifProd :: true:false -> nil:cons -> 0':s:error -> 0':s:error
timesIter :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error
ifTimes :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error
error :: 0':s:error
a :: b:c
b :: b:c
c :: b:c
hole_c11_23 :: c1
hole_nil:cons2_23 :: nil:cons
hole_c23_23 :: c2
hole_0':s:error4_23 :: 0':s:error
hole_c3:c4:c55_23 :: c3:c4:c5
hole_c12:c136_23 :: c12:c13
hole_true:false7_23 :: true:false
hole_c16:c178_23 :: c16:c17
hole_c89_23 :: c8
hole_c14:c1510_23 :: c14:c15
hole_c6:c711_23 :: c6:c7
hole_c912_23 :: c9
hole_c10:c1113_23 :: c10:c11
hole_c18:c19:c2014_23 :: c18:c19:c20
hole_c21:c2215_23 :: c21:c22
hole_b:c16_23 :: b:c
gen_nil:cons17_23 :: Nat -> nil:cons
gen_0':s:error18_23 :: Nat -> 0':s:error
gen_c6:c719_23 :: Nat -> c6:c7
gen_c18:c19:c2020_23 :: Nat -> c18:c19:c20


Lemmas:
PRODITER(gen_nil:cons17_23(n22_23), gen_0':s:error18_23(0)) -> *21_23, rt in Omega(n22_23)
PLUS(gen_0':s:error18_23(n7606_23)) -> gen_c6:c719_23(n7606_23), rt in Omega(1 + n7606_23)


Generator Equations:
gen_nil:cons17_23(0) <=> nil
gen_nil:cons17_23(+(x, 1)) <=> cons(0', gen_nil:cons17_23(x))
gen_0':s:error18_23(0) <=> 0'
gen_0':s:error18_23(+(x, 1)) <=> s(gen_0':s:error18_23(x))
gen_c6:c719_23(0) <=> c6
gen_c6:c719_23(+(x, 1)) <=> c7(gen_c6:c719_23(x))
gen_c18:c19:c2020_23(0) <=> c18
gen_c18:c19:c2020_23(+(x, 1)) <=> c20(gen_c18:c19:c2020_23(x))


The following defined symbols remain to be analysed:
ge, TIMESITER, GE, plus, prodIter, timesIter

They will be analysed ascendingly in the following order:
ge < TIMESITER
GE < TIMESITER
plus < TIMESITER
ge < timesIter
plus < timesIter

----------------------------------------

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ge(gen_0':s:error18_23(n8112_23), gen_0':s:error18_23(n8112_23)) -> true, rt in Omega(0)

Induction Base:
ge(gen_0':s:error18_23(0), gen_0':s:error18_23(0)) ->_R^Omega(0)
true

Induction Step:
ge(gen_0':s:error18_23(+(n8112_23, 1)), gen_0':s:error18_23(+(n8112_23, 1))) ->_R^Omega(0)
ge(gen_0':s:error18_23(n8112_23), gen_0':s:error18_23(n8112_23)) ->_IH
true

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(20)
Obligation:
Innermost TRS:
Rules:
PROD(z0) -> c1(PRODITER(z0, s(0')))
PRODITER(z0, z1) -> c2(IFPROD(isempty(z0), z0, z1), ISEMPTY(z0))
IFPROD(true, z0, z1) -> c3
IFPROD(false, z0, z1) -> c4(PRODITER(tail(z0), times(z1, head(z0))), TAIL(z0))
IFPROD(false, z0, z1) -> c5(PRODITER(tail(z0), times(z1, head(z0))), TIMES(z1, head(z0)), HEAD(z0))
PLUS(0') -> c6
PLUS(s(z0)) -> c7(PLUS(z0))
TIMES(z0, z1) -> c8(TIMESITER(z0, z1, 0', 0'))
TIMESITER(z0, z1, z2, z3) -> c9(IFTIMES(ge(z3, z0), z0, z1, z2, z3), GE(z3, z0))
IFTIMES(true, z0, z1, z2, z3) -> c10
IFTIMES(false, z0, z1, z2, z3) -> c11(TIMESITER(z0, z1, plus(z1, z2), s(z3)), PLUS(z1))
ISEMPTY(nil) -> c12
ISEMPTY(cons(z0, z1)) -> c13
HEAD(nil) -> c14
HEAD(cons(z0, z1)) -> c15
TAIL(nil) -> c16
TAIL(cons(z0, z1)) -> c17
GE(z0, 0') -> c18
GE(0', s(z0)) -> c19
GE(s(z0), s(z1)) -> c20(GE(z0, z1))
A -> c21
A -> c22
prod(z0) -> prodIter(z0, s(0'))
prodIter(z0, z1) -> ifProd(isempty(z0), z0, z1)
ifProd(true, z0, z1) -> z1
ifProd(false, z0, z1) -> prodIter(tail(z0), times(z1, head(z0)))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(z0, z1) -> timesIter(z0, z1, 0', 0')
timesIter(z0, z1, z2, z3) -> ifTimes(ge(z3, z0), z0, z1, z2, z3)
ifTimes(true, z0, z1, z2, z3) -> z2
ifTimes(false, z0, z1, z2, z3) -> timesIter(z0, z1, plus(z1, z2), s(z3))
isempty(nil) -> true
isempty(cons(z0, z1)) -> false
head(nil) -> error
head(cons(z0, z1)) -> z0
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
a -> b
a -> c

Types:
PROD :: nil:cons -> c1
c1 :: c2 -> c1
PRODITER :: nil:cons -> 0':s:error -> c2
s :: 0':s:error -> 0':s:error
0' :: 0':s:error
c2 :: c3:c4:c5 -> c12:c13 -> c2
IFPROD :: true:false -> nil:cons -> 0':s:error -> c3:c4:c5
isempty :: nil:cons -> true:false
ISEMPTY :: nil:cons -> c12:c13
true :: true:false
c3 :: c3:c4:c5
false :: true:false
c4 :: c2 -> c16:c17 -> c3:c4:c5
tail :: nil:cons -> nil:cons
times :: 0':s:error -> 0':s:error -> 0':s:error
head :: nil:cons -> 0':s:error
TAIL :: nil:cons -> c16:c17
c5 :: c2 -> c8 -> c14:c15 -> c3:c4:c5
TIMES :: 0':s:error -> 0':s:error -> c8
HEAD :: nil:cons -> c14:c15
PLUS :: 0':s:error -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c9 -> c8
TIMESITER :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> c9
c9 :: c10:c11 -> c18:c19:c20 -> c9
IFTIMES :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> c10:c11
ge :: 0':s:error -> 0':s:error -> true:false
GE :: 0':s:error -> 0':s:error -> c18:c19:c20
c10 :: c10:c11
c11 :: c9 -> c6:c7 -> c10:c11
plus :: 0':s:error -> 0':s:error -> 0':s:error
nil :: nil:cons
c12 :: c12:c13
cons :: 0':s:error -> nil:cons -> nil:cons
c13 :: c12:c13
c14 :: c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19:c20
c19 :: c18:c19:c20
c20 :: c18:c19:c20 -> c18:c19:c20
A :: c21:c22
c21 :: c21:c22
c22 :: c21:c22
prod :: nil:cons -> 0':s:error
prodIter :: nil:cons -> 0':s:error -> 0':s:error
ifProd :: true:false -> nil:cons -> 0':s:error -> 0':s:error
timesIter :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error
ifTimes :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error
error :: 0':s:error
a :: b:c
b :: b:c
c :: b:c
hole_c11_23 :: c1
hole_nil:cons2_23 :: nil:cons
hole_c23_23 :: c2
hole_0':s:error4_23 :: 0':s:error
hole_c3:c4:c55_23 :: c3:c4:c5
hole_c12:c136_23 :: c12:c13
hole_true:false7_23 :: true:false
hole_c16:c178_23 :: c16:c17
hole_c89_23 :: c8
hole_c14:c1510_23 :: c14:c15
hole_c6:c711_23 :: c6:c7
hole_c912_23 :: c9
hole_c10:c1113_23 :: c10:c11
hole_c18:c19:c2014_23 :: c18:c19:c20
hole_c21:c2215_23 :: c21:c22
hole_b:c16_23 :: b:c
gen_nil:cons17_23 :: Nat -> nil:cons
gen_0':s:error18_23 :: Nat -> 0':s:error
gen_c6:c719_23 :: Nat -> c6:c7
gen_c18:c19:c2020_23 :: Nat -> c18:c19:c20


Lemmas:
PRODITER(gen_nil:cons17_23(n22_23), gen_0':s:error18_23(0)) -> *21_23, rt in Omega(n22_23)
PLUS(gen_0':s:error18_23(n7606_23)) -> gen_c6:c719_23(n7606_23), rt in Omega(1 + n7606_23)
ge(gen_0':s:error18_23(n8112_23), gen_0':s:error18_23(n8112_23)) -> true, rt in Omega(0)


Generator Equations:
gen_nil:cons17_23(0) <=> nil
gen_nil:cons17_23(+(x, 1)) <=> cons(0', gen_nil:cons17_23(x))
gen_0':s:error18_23(0) <=> 0'
gen_0':s:error18_23(+(x, 1)) <=> s(gen_0':s:error18_23(x))
gen_c6:c719_23(0) <=> c6
gen_c6:c719_23(+(x, 1)) <=> c7(gen_c6:c719_23(x))
gen_c18:c19:c2020_23(0) <=> c18
gen_c18:c19:c2020_23(+(x, 1)) <=> c20(gen_c18:c19:c2020_23(x))


The following defined symbols remain to be analysed:
GE, TIMESITER, plus, prodIter, timesIter

They will be analysed ascendingly in the following order:
GE < TIMESITER
plus < TIMESITER
plus < timesIter

----------------------------------------

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
GE(gen_0':s:error18_23(n8704_23), gen_0':s:error18_23(n8704_23)) -> gen_c18:c19:c2020_23(n8704_23), rt in Omega(1 + n8704_23)

Induction Base:
GE(gen_0':s:error18_23(0), gen_0':s:error18_23(0)) ->_R^Omega(1)
c18

Induction Step:
GE(gen_0':s:error18_23(+(n8704_23, 1)), gen_0':s:error18_23(+(n8704_23, 1))) ->_R^Omega(1)
c20(GE(gen_0':s:error18_23(n8704_23), gen_0':s:error18_23(n8704_23))) ->_IH
c20(gen_c18:c19:c2020_23(c8705_23))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(22)
Obligation:
Innermost TRS:
Rules:
PROD(z0) -> c1(PRODITER(z0, s(0')))
PRODITER(z0, z1) -> c2(IFPROD(isempty(z0), z0, z1), ISEMPTY(z0))
IFPROD(true, z0, z1) -> c3
IFPROD(false, z0, z1) -> c4(PRODITER(tail(z0), times(z1, head(z0))), TAIL(z0))
IFPROD(false, z0, z1) -> c5(PRODITER(tail(z0), times(z1, head(z0))), TIMES(z1, head(z0)), HEAD(z0))
PLUS(0') -> c6
PLUS(s(z0)) -> c7(PLUS(z0))
TIMES(z0, z1) -> c8(TIMESITER(z0, z1, 0', 0'))
TIMESITER(z0, z1, z2, z3) -> c9(IFTIMES(ge(z3, z0), z0, z1, z2, z3), GE(z3, z0))
IFTIMES(true, z0, z1, z2, z3) -> c10
IFTIMES(false, z0, z1, z2, z3) -> c11(TIMESITER(z0, z1, plus(z1, z2), s(z3)), PLUS(z1))
ISEMPTY(nil) -> c12
ISEMPTY(cons(z0, z1)) -> c13
HEAD(nil) -> c14
HEAD(cons(z0, z1)) -> c15
TAIL(nil) -> c16
TAIL(cons(z0, z1)) -> c17
GE(z0, 0') -> c18
GE(0', s(z0)) -> c19
GE(s(z0), s(z1)) -> c20(GE(z0, z1))
A -> c21
A -> c22
prod(z0) -> prodIter(z0, s(0'))
prodIter(z0, z1) -> ifProd(isempty(z0), z0, z1)
ifProd(true, z0, z1) -> z1
ifProd(false, z0, z1) -> prodIter(tail(z0), times(z1, head(z0)))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(z0, z1) -> timesIter(z0, z1, 0', 0')
timesIter(z0, z1, z2, z3) -> ifTimes(ge(z3, z0), z0, z1, z2, z3)
ifTimes(true, z0, z1, z2, z3) -> z2
ifTimes(false, z0, z1, z2, z3) -> timesIter(z0, z1, plus(z1, z2), s(z3))
isempty(nil) -> true
isempty(cons(z0, z1)) -> false
head(nil) -> error
head(cons(z0, z1)) -> z0
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
a -> b
a -> c

Types:
PROD :: nil:cons -> c1
c1 :: c2 -> c1
PRODITER :: nil:cons -> 0':s:error -> c2
s :: 0':s:error -> 0':s:error
0' :: 0':s:error
c2 :: c3:c4:c5 -> c12:c13 -> c2
IFPROD :: true:false -> nil:cons -> 0':s:error -> c3:c4:c5
isempty :: nil:cons -> true:false
ISEMPTY :: nil:cons -> c12:c13
true :: true:false
c3 :: c3:c4:c5
false :: true:false
c4 :: c2 -> c16:c17 -> c3:c4:c5
tail :: nil:cons -> nil:cons
times :: 0':s:error -> 0':s:error -> 0':s:error
head :: nil:cons -> 0':s:error
TAIL :: nil:cons -> c16:c17
c5 :: c2 -> c8 -> c14:c15 -> c3:c4:c5
TIMES :: 0':s:error -> 0':s:error -> c8
HEAD :: nil:cons -> c14:c15
PLUS :: 0':s:error -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c9 -> c8
TIMESITER :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> c9
c9 :: c10:c11 -> c18:c19:c20 -> c9
IFTIMES :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> c10:c11
ge :: 0':s:error -> 0':s:error -> true:false
GE :: 0':s:error -> 0':s:error -> c18:c19:c20
c10 :: c10:c11
c11 :: c9 -> c6:c7 -> c10:c11
plus :: 0':s:error -> 0':s:error -> 0':s:error
nil :: nil:cons
c12 :: c12:c13
cons :: 0':s:error -> nil:cons -> nil:cons
c13 :: c12:c13
c14 :: c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19:c20
c19 :: c18:c19:c20
c20 :: c18:c19:c20 -> c18:c19:c20
A :: c21:c22
c21 :: c21:c22
c22 :: c21:c22
prod :: nil:cons -> 0':s:error
prodIter :: nil:cons -> 0':s:error -> 0':s:error
ifProd :: true:false -> nil:cons -> 0':s:error -> 0':s:error
timesIter :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error
ifTimes :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error
error :: 0':s:error
a :: b:c
b :: b:c
c :: b:c
hole_c11_23 :: c1
hole_nil:cons2_23 :: nil:cons
hole_c23_23 :: c2
hole_0':s:error4_23 :: 0':s:error
hole_c3:c4:c55_23 :: c3:c4:c5
hole_c12:c136_23 :: c12:c13
hole_true:false7_23 :: true:false
hole_c16:c178_23 :: c16:c17
hole_c89_23 :: c8
hole_c14:c1510_23 :: c14:c15
hole_c6:c711_23 :: c6:c7
hole_c912_23 :: c9
hole_c10:c1113_23 :: c10:c11
hole_c18:c19:c2014_23 :: c18:c19:c20
hole_c21:c2215_23 :: c21:c22
hole_b:c16_23 :: b:c
gen_nil:cons17_23 :: Nat -> nil:cons
gen_0':s:error18_23 :: Nat -> 0':s:error
gen_c6:c719_23 :: Nat -> c6:c7
gen_c18:c19:c2020_23 :: Nat -> c18:c19:c20


Lemmas:
PRODITER(gen_nil:cons17_23(n22_23), gen_0':s:error18_23(0)) -> *21_23, rt in Omega(n22_23)
PLUS(gen_0':s:error18_23(n7606_23)) -> gen_c6:c719_23(n7606_23), rt in Omega(1 + n7606_23)
ge(gen_0':s:error18_23(n8112_23), gen_0':s:error18_23(n8112_23)) -> true, rt in Omega(0)
GE(gen_0':s:error18_23(n8704_23), gen_0':s:error18_23(n8704_23)) -> gen_c18:c19:c2020_23(n8704_23), rt in Omega(1 + n8704_23)


Generator Equations:
gen_nil:cons17_23(0) <=> nil
gen_nil:cons17_23(+(x, 1)) <=> cons(0', gen_nil:cons17_23(x))
gen_0':s:error18_23(0) <=> 0'
gen_0':s:error18_23(+(x, 1)) <=> s(gen_0':s:error18_23(x))
gen_c6:c719_23(0) <=> c6
gen_c6:c719_23(+(x, 1)) <=> c7(gen_c6:c719_23(x))
gen_c18:c19:c2020_23(0) <=> c18
gen_c18:c19:c2020_23(+(x, 1)) <=> c20(gen_c18:c19:c2020_23(x))


The following defined symbols remain to be analysed:
plus, TIMESITER, prodIter, timesIter

They will be analysed ascendingly in the following order:
plus < TIMESITER
plus < timesIter

----------------------------------------

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
plus(gen_0':s:error18_23(n9713_23), gen_0':s:error18_23(b)) -> gen_0':s:error18_23(+(n9713_23, b)), rt in Omega(0)

Induction Base:
plus(gen_0':s:error18_23(0), gen_0':s:error18_23(b)) ->_R^Omega(0)
gen_0':s:error18_23(b)

Induction Step:
plus(gen_0':s:error18_23(+(n9713_23, 1)), gen_0':s:error18_23(b)) ->_R^Omega(0)
s(plus(gen_0':s:error18_23(n9713_23), gen_0':s:error18_23(b))) ->_IH
s(gen_0':s:error18_23(+(b, c9714_23)))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(24)
Obligation:
Innermost TRS:
Rules:
PROD(z0) -> c1(PRODITER(z0, s(0')))
PRODITER(z0, z1) -> c2(IFPROD(isempty(z0), z0, z1), ISEMPTY(z0))
IFPROD(true, z0, z1) -> c3
IFPROD(false, z0, z1) -> c4(PRODITER(tail(z0), times(z1, head(z0))), TAIL(z0))
IFPROD(false, z0, z1) -> c5(PRODITER(tail(z0), times(z1, head(z0))), TIMES(z1, head(z0)), HEAD(z0))
PLUS(0') -> c6
PLUS(s(z0)) -> c7(PLUS(z0))
TIMES(z0, z1) -> c8(TIMESITER(z0, z1, 0', 0'))
TIMESITER(z0, z1, z2, z3) -> c9(IFTIMES(ge(z3, z0), z0, z1, z2, z3), GE(z3, z0))
IFTIMES(true, z0, z1, z2, z3) -> c10
IFTIMES(false, z0, z1, z2, z3) -> c11(TIMESITER(z0, z1, plus(z1, z2), s(z3)), PLUS(z1))
ISEMPTY(nil) -> c12
ISEMPTY(cons(z0, z1)) -> c13
HEAD(nil) -> c14
HEAD(cons(z0, z1)) -> c15
TAIL(nil) -> c16
TAIL(cons(z0, z1)) -> c17
GE(z0, 0') -> c18
GE(0', s(z0)) -> c19
GE(s(z0), s(z1)) -> c20(GE(z0, z1))
A -> c21
A -> c22
prod(z0) -> prodIter(z0, s(0'))
prodIter(z0, z1) -> ifProd(isempty(z0), z0, z1)
ifProd(true, z0, z1) -> z1
ifProd(false, z0, z1) -> prodIter(tail(z0), times(z1, head(z0)))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(z0, z1) -> timesIter(z0, z1, 0', 0')
timesIter(z0, z1, z2, z3) -> ifTimes(ge(z3, z0), z0, z1, z2, z3)
ifTimes(true, z0, z1, z2, z3) -> z2
ifTimes(false, z0, z1, z2, z3) -> timesIter(z0, z1, plus(z1, z2), s(z3))
isempty(nil) -> true
isempty(cons(z0, z1)) -> false
head(nil) -> error
head(cons(z0, z1)) -> z0
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
a -> b
a -> c

Types:
PROD :: nil:cons -> c1
c1 :: c2 -> c1
PRODITER :: nil:cons -> 0':s:error -> c2
s :: 0':s:error -> 0':s:error
0' :: 0':s:error
c2 :: c3:c4:c5 -> c12:c13 -> c2
IFPROD :: true:false -> nil:cons -> 0':s:error -> c3:c4:c5
isempty :: nil:cons -> true:false
ISEMPTY :: nil:cons -> c12:c13
true :: true:false
c3 :: c3:c4:c5
false :: true:false
c4 :: c2 -> c16:c17 -> c3:c4:c5
tail :: nil:cons -> nil:cons
times :: 0':s:error -> 0':s:error -> 0':s:error
head :: nil:cons -> 0':s:error
TAIL :: nil:cons -> c16:c17
c5 :: c2 -> c8 -> c14:c15 -> c3:c4:c5
TIMES :: 0':s:error -> 0':s:error -> c8
HEAD :: nil:cons -> c14:c15
PLUS :: 0':s:error -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c9 -> c8
TIMESITER :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> c9
c9 :: c10:c11 -> c18:c19:c20 -> c9
IFTIMES :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> c10:c11
ge :: 0':s:error -> 0':s:error -> true:false
GE :: 0':s:error -> 0':s:error -> c18:c19:c20
c10 :: c10:c11
c11 :: c9 -> c6:c7 -> c10:c11
plus :: 0':s:error -> 0':s:error -> 0':s:error
nil :: nil:cons
c12 :: c12:c13
cons :: 0':s:error -> nil:cons -> nil:cons
c13 :: c12:c13
c14 :: c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19:c20
c19 :: c18:c19:c20
c20 :: c18:c19:c20 -> c18:c19:c20
A :: c21:c22
c21 :: c21:c22
c22 :: c21:c22
prod :: nil:cons -> 0':s:error
prodIter :: nil:cons -> 0':s:error -> 0':s:error
ifProd :: true:false -> nil:cons -> 0':s:error -> 0':s:error
timesIter :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error
ifTimes :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error
error :: 0':s:error
a :: b:c
b :: b:c
c :: b:c
hole_c11_23 :: c1
hole_nil:cons2_23 :: nil:cons
hole_c23_23 :: c2
hole_0':s:error4_23 :: 0':s:error
hole_c3:c4:c55_23 :: c3:c4:c5
hole_c12:c136_23 :: c12:c13
hole_true:false7_23 :: true:false
hole_c16:c178_23 :: c16:c17
hole_c89_23 :: c8
hole_c14:c1510_23 :: c14:c15
hole_c6:c711_23 :: c6:c7
hole_c912_23 :: c9
hole_c10:c1113_23 :: c10:c11
hole_c18:c19:c2014_23 :: c18:c19:c20
hole_c21:c2215_23 :: c21:c22
hole_b:c16_23 :: b:c
gen_nil:cons17_23 :: Nat -> nil:cons
gen_0':s:error18_23 :: Nat -> 0':s:error
gen_c6:c719_23 :: Nat -> c6:c7
gen_c18:c19:c2020_23 :: Nat -> c18:c19:c20


Lemmas:
PRODITER(gen_nil:cons17_23(n22_23), gen_0':s:error18_23(0)) -> *21_23, rt in Omega(n22_23)
PLUS(gen_0':s:error18_23(n7606_23)) -> gen_c6:c719_23(n7606_23), rt in Omega(1 + n7606_23)
ge(gen_0':s:error18_23(n8112_23), gen_0':s:error18_23(n8112_23)) -> true, rt in Omega(0)
GE(gen_0':s:error18_23(n8704_23), gen_0':s:error18_23(n8704_23)) -> gen_c18:c19:c2020_23(n8704_23), rt in Omega(1 + n8704_23)
plus(gen_0':s:error18_23(n9713_23), gen_0':s:error18_23(b)) -> gen_0':s:error18_23(+(n9713_23, b)), rt in Omega(0)


Generator Equations:
gen_nil:cons17_23(0) <=> nil
gen_nil:cons17_23(+(x, 1)) <=> cons(0', gen_nil:cons17_23(x))
gen_0':s:error18_23(0) <=> 0'
gen_0':s:error18_23(+(x, 1)) <=> s(gen_0':s:error18_23(x))
gen_c6:c719_23(0) <=> c6
gen_c6:c719_23(+(x, 1)) <=> c7(gen_c6:c719_23(x))
gen_c18:c19:c2020_23(0) <=> c18
gen_c18:c19:c2020_23(+(x, 1)) <=> c20(gen_c18:c19:c2020_23(x))


The following defined symbols remain to be analysed:
TIMESITER, prodIter, timesIter
----------------------------------------

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
prodIter(gen_nil:cons17_23(n11867_23), gen_0':s:error18_23(0)) -> gen_0':s:error18_23(0), rt in Omega(0)

Induction Base:
prodIter(gen_nil:cons17_23(0), gen_0':s:error18_23(0)) ->_R^Omega(0)
ifProd(isempty(gen_nil:cons17_23(0)), gen_nil:cons17_23(0), gen_0':s:error18_23(0)) ->_R^Omega(0)
ifProd(true, gen_nil:cons17_23(0), gen_0':s:error18_23(0)) ->_R^Omega(0)
gen_0':s:error18_23(0)

Induction Step:
prodIter(gen_nil:cons17_23(+(n11867_23, 1)), gen_0':s:error18_23(0)) ->_R^Omega(0)
ifProd(isempty(gen_nil:cons17_23(+(n11867_23, 1))), gen_nil:cons17_23(+(n11867_23, 1)), gen_0':s:error18_23(0)) ->_R^Omega(0)
ifProd(false, gen_nil:cons17_23(+(1, n11867_23)), gen_0':s:error18_23(0)) ->_R^Omega(0)
prodIter(tail(gen_nil:cons17_23(+(1, n11867_23))), times(gen_0':s:error18_23(0), head(gen_nil:cons17_23(+(1, n11867_23))))) ->_R^Omega(0)
prodIter(gen_nil:cons17_23(n11867_23), times(gen_0':s:error18_23(0), head(gen_nil:cons17_23(+(1, n11867_23))))) ->_R^Omega(0)
prodIter(gen_nil:cons17_23(n11867_23), times(gen_0':s:error18_23(0), 0')) ->_R^Omega(0)
prodIter(gen_nil:cons17_23(n11867_23), timesIter(gen_0':s:error18_23(0), 0', 0', 0')) ->_R^Omega(0)
prodIter(gen_nil:cons17_23(n11867_23), ifTimes(ge(0', gen_0':s:error18_23(0)), gen_0':s:error18_23(0), 0', 0', 0')) ->_L^Omega(0)
prodIter(gen_nil:cons17_23(n11867_23), ifTimes(true, gen_0':s:error18_23(0), 0', 0', 0')) ->_R^Omega(0)
prodIter(gen_nil:cons17_23(n11867_23), 0') ->_IH
gen_0':s:error18_23(0)

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(26)
Obligation:
Innermost TRS:
Rules:
PROD(z0) -> c1(PRODITER(z0, s(0')))
PRODITER(z0, z1) -> c2(IFPROD(isempty(z0), z0, z1), ISEMPTY(z0))
IFPROD(true, z0, z1) -> c3
IFPROD(false, z0, z1) -> c4(PRODITER(tail(z0), times(z1, head(z0))), TAIL(z0))
IFPROD(false, z0, z1) -> c5(PRODITER(tail(z0), times(z1, head(z0))), TIMES(z1, head(z0)), HEAD(z0))
PLUS(0') -> c6
PLUS(s(z0)) -> c7(PLUS(z0))
TIMES(z0, z1) -> c8(TIMESITER(z0, z1, 0', 0'))
TIMESITER(z0, z1, z2, z3) -> c9(IFTIMES(ge(z3, z0), z0, z1, z2, z3), GE(z3, z0))
IFTIMES(true, z0, z1, z2, z3) -> c10
IFTIMES(false, z0, z1, z2, z3) -> c11(TIMESITER(z0, z1, plus(z1, z2), s(z3)), PLUS(z1))
ISEMPTY(nil) -> c12
ISEMPTY(cons(z0, z1)) -> c13
HEAD(nil) -> c14
HEAD(cons(z0, z1)) -> c15
TAIL(nil) -> c16
TAIL(cons(z0, z1)) -> c17
GE(z0, 0') -> c18
GE(0', s(z0)) -> c19
GE(s(z0), s(z1)) -> c20(GE(z0, z1))
A -> c21
A -> c22
prod(z0) -> prodIter(z0, s(0'))
prodIter(z0, z1) -> ifProd(isempty(z0), z0, z1)
ifProd(true, z0, z1) -> z1
ifProd(false, z0, z1) -> prodIter(tail(z0), times(z1, head(z0)))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(z0, z1) -> timesIter(z0, z1, 0', 0')
timesIter(z0, z1, z2, z3) -> ifTimes(ge(z3, z0), z0, z1, z2, z3)
ifTimes(true, z0, z1, z2, z3) -> z2
ifTimes(false, z0, z1, z2, z3) -> timesIter(z0, z1, plus(z1, z2), s(z3))
isempty(nil) -> true
isempty(cons(z0, z1)) -> false
head(nil) -> error
head(cons(z0, z1)) -> z0
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
a -> b
a -> c

Types:
PROD :: nil:cons -> c1
c1 :: c2 -> c1
PRODITER :: nil:cons -> 0':s:error -> c2
s :: 0':s:error -> 0':s:error
0' :: 0':s:error
c2 :: c3:c4:c5 -> c12:c13 -> c2
IFPROD :: true:false -> nil:cons -> 0':s:error -> c3:c4:c5
isempty :: nil:cons -> true:false
ISEMPTY :: nil:cons -> c12:c13
true :: true:false
c3 :: c3:c4:c5
false :: true:false
c4 :: c2 -> c16:c17 -> c3:c4:c5
tail :: nil:cons -> nil:cons
times :: 0':s:error -> 0':s:error -> 0':s:error
head :: nil:cons -> 0':s:error
TAIL :: nil:cons -> c16:c17
c5 :: c2 -> c8 -> c14:c15 -> c3:c4:c5
TIMES :: 0':s:error -> 0':s:error -> c8
HEAD :: nil:cons -> c14:c15
PLUS :: 0':s:error -> c6:c7
c6 :: c6:c7
c7 :: c6:c7 -> c6:c7
c8 :: c9 -> c8
TIMESITER :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> c9
c9 :: c10:c11 -> c18:c19:c20 -> c9
IFTIMES :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> c10:c11
ge :: 0':s:error -> 0':s:error -> true:false
GE :: 0':s:error -> 0':s:error -> c18:c19:c20
c10 :: c10:c11
c11 :: c9 -> c6:c7 -> c10:c11
plus :: 0':s:error -> 0':s:error -> 0':s:error
nil :: nil:cons
c12 :: c12:c13
cons :: 0':s:error -> nil:cons -> nil:cons
c13 :: c12:c13
c14 :: c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19:c20
c19 :: c18:c19:c20
c20 :: c18:c19:c20 -> c18:c19:c20
A :: c21:c22
c21 :: c21:c22
c22 :: c21:c22
prod :: nil:cons -> 0':s:error
prodIter :: nil:cons -> 0':s:error -> 0':s:error
ifProd :: true:false -> nil:cons -> 0':s:error -> 0':s:error
timesIter :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error
ifTimes :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error
error :: 0':s:error
a :: b:c
b :: b:c
c :: b:c
hole_c11_23 :: c1
hole_nil:cons2_23 :: nil:cons
hole_c23_23 :: c2
hole_0':s:error4_23 :: 0':s:error
hole_c3:c4:c55_23 :: c3:c4:c5
hole_c12:c136_23 :: c12:c13
hole_true:false7_23 :: true:false
hole_c16:c178_23 :: c16:c17
hole_c89_23 :: c8
hole_c14:c1510_23 :: c14:c15
hole_c6:c711_23 :: c6:c7
hole_c912_23 :: c9
hole_c10:c1113_23 :: c10:c11
hole_c18:c19:c2014_23 :: c18:c19:c20
hole_c21:c2215_23 :: c21:c22
hole_b:c16_23 :: b:c
gen_nil:cons17_23 :: Nat -> nil:cons
gen_0':s:error18_23 :: Nat -> 0':s:error
gen_c6:c719_23 :: Nat -> c6:c7
gen_c18:c19:c2020_23 :: Nat -> c18:c19:c20


Lemmas:
PRODITER(gen_nil:cons17_23(n22_23), gen_0':s:error18_23(0)) -> *21_23, rt in Omega(n22_23)
PLUS(gen_0':s:error18_23(n7606_23)) -> gen_c6:c719_23(n7606_23), rt in Omega(1 + n7606_23)
ge(gen_0':s:error18_23(n8112_23), gen_0':s:error18_23(n8112_23)) -> true, rt in Omega(0)
GE(gen_0':s:error18_23(n8704_23), gen_0':s:error18_23(n8704_23)) -> gen_c18:c19:c2020_23(n8704_23), rt in Omega(1 + n8704_23)
plus(gen_0':s:error18_23(n9713_23), gen_0':s:error18_23(b)) -> gen_0':s:error18_23(+(n9713_23, b)), rt in Omega(0)
prodIter(gen_nil:cons17_23(n11867_23), gen_0':s:error18_23(0)) -> gen_0':s:error18_23(0), rt in Omega(0)


Generator Equations:
gen_nil:cons17_23(0) <=> nil
gen_nil:cons17_23(+(x, 1)) <=> cons(0', gen_nil:cons17_23(x))
gen_0':s:error18_23(0) <=> 0'
gen_0':s:error18_23(+(x, 1)) <=> s(gen_0':s:error18_23(x))
gen_c6:c719_23(0) <=> c6
gen_c6:c719_23(+(x, 1)) <=> c7(gen_c6:c719_23(x))
gen_c18:c19:c2020_23(0) <=> c18
gen_c18:c19:c2020_23(+(x, 1)) <=> c20(gen_c18:c19:c2020_23(x))


The following defined symbols remain to be analysed:
timesIter