WORST_CASE(Omega(n^1),?)
proof of input_LVVIEB0A0M.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 32.7 s]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 94 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 17 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 94 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 148 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 921 ms]
        (26) typed CpxTrs


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

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


The TRS R consists of the following rules:

   car(cons(x, l)) -> x
   cddr(nil) -> nil
   cddr(cons(x, nil)) -> nil
   cddr(cons(x, cons(y, l))) -> l
   cadr(cons(x, cons(y, l))) -> y
   isZero(0) -> true
   isZero(s(x)) -> false
   plus(x, y) -> ifplus(isZero(x), x, y)
   ifplus(true, x, y) -> y
   ifplus(false, x, y) -> s(plus(p(x), y))
   times(x, y) -> iftimes(isZero(x), x, y)
   iftimes(true, x, y) -> 0
   iftimes(false, x, y) -> plus(y, times(p(x), y))
   p(s(x)) -> x
   p(0) -> 0
   shorter(nil, y) -> true
   shorter(cons(x, l), 0) -> false
   shorter(cons(x, l), s(y)) -> shorter(l, y)
   prod(l) -> if(shorter(l, 0), shorter(l, s(0)), l)
   if(true, b, l) -> s(0)
   if(false, b, l) -> if2(b, l)
   if2(true, l) -> car(l)
   if2(false, l) -> prod(cons(times(car(l), cadr(l)), cddr(l)))

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   car(cons(z0, z1)) -> z0
   cddr(nil) -> nil
   cddr(cons(z0, nil)) -> nil
   cddr(cons(z0, cons(z1, z2))) -> z2
   cadr(cons(z0, cons(z1, z2))) -> z1
   isZero(0) -> true
   isZero(s(z0)) -> false
   plus(z0, z1) -> ifplus(isZero(z0), z0, z1)
   ifplus(true, z0, z1) -> z1
   ifplus(false, z0, z1) -> s(plus(p(z0), z1))
   times(z0, z1) -> iftimes(isZero(z0), z0, z1)
   iftimes(true, z0, z1) -> 0
   iftimes(false, z0, z1) -> plus(z1, times(p(z0), z1))
   p(s(z0)) -> z0
   p(0) -> 0
   shorter(nil, z0) -> true
   shorter(cons(z0, z1), 0) -> false
   shorter(cons(z0, z1), s(z2)) -> shorter(z1, z2)
   prod(z0) -> if(shorter(z0, 0), shorter(z0, s(0)), z0)
   if(true, z0, z1) -> s(0)
   if(false, z0, z1) -> if2(z0, z1)
   if2(true, z0) -> car(z0)
   if2(false, z0) -> prod(cons(times(car(z0), cadr(z0)), cddr(z0)))
Tuples:
   CAR(cons(z0, z1)) -> c
   CDDR(nil) -> c1
   CDDR(cons(z0, nil)) -> c2
   CDDR(cons(z0, cons(z1, z2))) -> c3
   CADR(cons(z0, cons(z1, z2))) -> c4
   ISZERO(0) -> c5
   ISZERO(s(z0)) -> c6
   PLUS(z0, z1) -> c7(IFPLUS(isZero(z0), z0, z1), ISZERO(z0))
   IFPLUS(true, z0, z1) -> c8
   IFPLUS(false, z0, z1) -> c9(PLUS(p(z0), z1), P(z0))
   TIMES(z0, z1) -> c10(IFTIMES(isZero(z0), z0, z1), ISZERO(z0))
   IFTIMES(true, z0, z1) -> c11
   IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(p(z0), z1)), TIMES(p(z0), z1), P(z0))
   P(s(z0)) -> c13
   P(0) -> c14
   SHORTER(nil, z0) -> c15
   SHORTER(cons(z0, z1), 0) -> c16
   SHORTER(cons(z0, z1), s(z2)) -> c17(SHORTER(z1, z2))
   PROD(z0) -> c18(IF(shorter(z0, 0), shorter(z0, s(0)), z0), SHORTER(z0, 0))
   PROD(z0) -> c19(IF(shorter(z0, 0), shorter(z0, s(0)), z0), SHORTER(z0, s(0)))
   IF(true, z0, z1) -> c20
   IF(false, z0, z1) -> c21(IF2(z0, z1))
   IF2(true, z0) -> c22(CAR(z0))
   IF2(false, z0) -> c23(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CAR(z0))
   IF2(false, z0) -> c24(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CADR(z0))
   IF2(false, z0) -> c25(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), CDDR(z0))
S tuples:
   CAR(cons(z0, z1)) -> c
   CDDR(nil) -> c1
   CDDR(cons(z0, nil)) -> c2
   CDDR(cons(z0, cons(z1, z2))) -> c3
   CADR(cons(z0, cons(z1, z2))) -> c4
   ISZERO(0) -> c5
   ISZERO(s(z0)) -> c6
   PLUS(z0, z1) -> c7(IFPLUS(isZero(z0), z0, z1), ISZERO(z0))
   IFPLUS(true, z0, z1) -> c8
   IFPLUS(false, z0, z1) -> c9(PLUS(p(z0), z1), P(z0))
   TIMES(z0, z1) -> c10(IFTIMES(isZero(z0), z0, z1), ISZERO(z0))
   IFTIMES(true, z0, z1) -> c11
   IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(p(z0), z1)), TIMES(p(z0), z1), P(z0))
   P(s(z0)) -> c13
   P(0) -> c14
   SHORTER(nil, z0) -> c15
   SHORTER(cons(z0, z1), 0) -> c16
   SHORTER(cons(z0, z1), s(z2)) -> c17(SHORTER(z1, z2))
   PROD(z0) -> c18(IF(shorter(z0, 0), shorter(z0, s(0)), z0), SHORTER(z0, 0))
   PROD(z0) -> c19(IF(shorter(z0, 0), shorter(z0, s(0)), z0), SHORTER(z0, s(0)))
   IF(true, z0, z1) -> c20
   IF(false, z0, z1) -> c21(IF2(z0, z1))
   IF2(true, z0) -> c22(CAR(z0))
   IF2(false, z0) -> c23(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CAR(z0))
   IF2(false, z0) -> c24(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CADR(z0))
   IF2(false, z0) -> c25(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), CDDR(z0))
K tuples:none
Defined Rule Symbols:   car_1, cddr_1, cadr_1, isZero_1, plus_2, ifplus_3, times_2, iftimes_3, p_1, shorter_2, prod_1, if_3, if2_2

Defined Pair Symbols:   CAR_1, CDDR_1, CADR_1, ISZERO_1, PLUS_2, IFPLUS_3, TIMES_2, IFTIMES_3, P_1, SHORTER_2, PROD_1, IF_3, IF2_2

Compound Symbols:   c, c1, c2, c3, c4, c5, c6, c7_2, c8, c9_2, c10_2, c11, c12_3, c13, c14, c15, c16, c17_1, c18_2, c19_2, c20, c21_1, c22_1, c23_3, c24_3, c25_2


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

(3) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

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

   CAR(cons(z0, z1)) -> c
   CDDR(nil) -> c1
   CDDR(cons(z0, nil)) -> c2
   CDDR(cons(z0, cons(z1, z2))) -> c3
   CADR(cons(z0, cons(z1, z2))) -> c4
   ISZERO(0) -> c5
   ISZERO(s(z0)) -> c6
   PLUS(z0, z1) -> c7(IFPLUS(isZero(z0), z0, z1), ISZERO(z0))
   IFPLUS(true, z0, z1) -> c8
   IFPLUS(false, z0, z1) -> c9(PLUS(p(z0), z1), P(z0))
   TIMES(z0, z1) -> c10(IFTIMES(isZero(z0), z0, z1), ISZERO(z0))
   IFTIMES(true, z0, z1) -> c11
   IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(p(z0), z1)), TIMES(p(z0), z1), P(z0))
   P(s(z0)) -> c13
   P(0) -> c14
   SHORTER(nil, z0) -> c15
   SHORTER(cons(z0, z1), 0) -> c16
   SHORTER(cons(z0, z1), s(z2)) -> c17(SHORTER(z1, z2))
   PROD(z0) -> c18(IF(shorter(z0, 0), shorter(z0, s(0)), z0), SHORTER(z0, 0))
   PROD(z0) -> c19(IF(shorter(z0, 0), shorter(z0, s(0)), z0), SHORTER(z0, s(0)))
   IF(true, z0, z1) -> c20
   IF(false, z0, z1) -> c21(IF2(z0, z1))
   IF2(true, z0) -> c22(CAR(z0))
   IF2(false, z0) -> c23(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CAR(z0))
   IF2(false, z0) -> c24(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CADR(z0))
   IF2(false, z0) -> c25(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), CDDR(z0))

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

   car(cons(z0, z1)) -> z0
   cddr(nil) -> nil
   cddr(cons(z0, nil)) -> nil
   cddr(cons(z0, cons(z1, z2))) -> z2
   cadr(cons(z0, cons(z1, z2))) -> z1
   isZero(0) -> true
   isZero(s(z0)) -> false
   plus(z0, z1) -> ifplus(isZero(z0), z0, z1)
   ifplus(true, z0, z1) -> z1
   ifplus(false, z0, z1) -> s(plus(p(z0), z1))
   times(z0, z1) -> iftimes(isZero(z0), z0, z1)
   iftimes(true, z0, z1) -> 0
   iftimes(false, z0, z1) -> plus(z1, times(p(z0), z1))
   p(s(z0)) -> z0
   p(0) -> 0
   shorter(nil, z0) -> true
   shorter(cons(z0, z1), 0) -> false
   shorter(cons(z0, z1), s(z2)) -> shorter(z1, z2)
   prod(z0) -> if(shorter(z0, 0), shorter(z0, s(0)), z0)
   if(true, z0, z1) -> s(0)
   if(false, z0, z1) -> if2(z0, z1)
   if2(true, z0) -> car(z0)
   if2(false, z0) -> prod(cons(times(car(z0), cadr(z0)), cddr(z0)))

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

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

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

   CAR(cons(z0, z1)) -> c
   CDDR(nil) -> c1
   CDDR(cons(z0, nil)) -> c2
   CDDR(cons(z0, cons(z1, z2))) -> c3
   CADR(cons(z0, cons(z1, z2))) -> c4
   ISZERO(0') -> c5
   ISZERO(s(z0)) -> c6
   PLUS(z0, z1) -> c7(IFPLUS(isZero(z0), z0, z1), ISZERO(z0))
   IFPLUS(true, z0, z1) -> c8
   IFPLUS(false, z0, z1) -> c9(PLUS(p(z0), z1), P(z0))
   TIMES(z0, z1) -> c10(IFTIMES(isZero(z0), z0, z1), ISZERO(z0))
   IFTIMES(true, z0, z1) -> c11
   IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(p(z0), z1)), TIMES(p(z0), z1), P(z0))
   P(s(z0)) -> c13
   P(0') -> c14
   SHORTER(nil, z0) -> c15
   SHORTER(cons(z0, z1), 0') -> c16
   SHORTER(cons(z0, z1), s(z2)) -> c17(SHORTER(z1, z2))
   PROD(z0) -> c18(IF(shorter(z0, 0'), shorter(z0, s(0')), z0), SHORTER(z0, 0'))
   PROD(z0) -> c19(IF(shorter(z0, 0'), shorter(z0, s(0')), z0), SHORTER(z0, s(0')))
   IF(true, z0, z1) -> c20
   IF(false, z0, z1) -> c21(IF2(z0, z1))
   IF2(true, z0) -> c22(CAR(z0))
   IF2(false, z0) -> c23(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CAR(z0))
   IF2(false, z0) -> c24(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CADR(z0))
   IF2(false, z0) -> c25(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), CDDR(z0))

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

   car(cons(z0, z1)) -> z0
   cddr(nil) -> nil
   cddr(cons(z0, nil)) -> nil
   cddr(cons(z0, cons(z1, z2))) -> z2
   cadr(cons(z0, cons(z1, z2))) -> z1
   isZero(0') -> true
   isZero(s(z0)) -> false
   plus(z0, z1) -> ifplus(isZero(z0), z0, z1)
   ifplus(true, z0, z1) -> z1
   ifplus(false, z0, z1) -> s(plus(p(z0), z1))
   times(z0, z1) -> iftimes(isZero(z0), z0, z1)
   iftimes(true, z0, z1) -> 0'
   iftimes(false, z0, z1) -> plus(z1, times(p(z0), z1))
   p(s(z0)) -> z0
   p(0') -> 0'
   shorter(nil, z0) -> true
   shorter(cons(z0, z1), 0') -> false
   shorter(cons(z0, z1), s(z2)) -> shorter(z1, z2)
   prod(z0) -> if(shorter(z0, 0'), shorter(z0, s(0')), z0)
   if(true, z0, z1) -> s(0')
   if(false, z0, z1) -> if2(z0, z1)
   if2(true, z0) -> car(z0)
   if2(false, z0) -> prod(cons(times(car(z0), cadr(z0)), cddr(z0)))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
CAR(cons(z0, z1)) -> c
CDDR(nil) -> c1
CDDR(cons(z0, nil)) -> c2
CDDR(cons(z0, cons(z1, z2))) -> c3
CADR(cons(z0, cons(z1, z2))) -> c4
ISZERO(0') -> c5
ISZERO(s(z0)) -> c6
PLUS(z0, z1) -> c7(IFPLUS(isZero(z0), z0, z1), ISZERO(z0))
IFPLUS(true, z0, z1) -> c8
IFPLUS(false, z0, z1) -> c9(PLUS(p(z0), z1), P(z0))
TIMES(z0, z1) -> c10(IFTIMES(isZero(z0), z0, z1), ISZERO(z0))
IFTIMES(true, z0, z1) -> c11
IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(p(z0), z1)), TIMES(p(z0), z1), P(z0))
P(s(z0)) -> c13
P(0') -> c14
SHORTER(nil, z0) -> c15
SHORTER(cons(z0, z1), 0') -> c16
SHORTER(cons(z0, z1), s(z2)) -> c17(SHORTER(z1, z2))
PROD(z0) -> c18(IF(shorter(z0, 0'), shorter(z0, s(0')), z0), SHORTER(z0, 0'))
PROD(z0) -> c19(IF(shorter(z0, 0'), shorter(z0, s(0')), z0), SHORTER(z0, s(0')))
IF(true, z0, z1) -> c20
IF(false, z0, z1) -> c21(IF2(z0, z1))
IF2(true, z0) -> c22(CAR(z0))
IF2(false, z0) -> c23(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CAR(z0))
IF2(false, z0) -> c24(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CADR(z0))
IF2(false, z0) -> c25(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), CDDR(z0))
car(cons(z0, z1)) -> z0
cddr(nil) -> nil
cddr(cons(z0, nil)) -> nil
cddr(cons(z0, cons(z1, z2))) -> z2
cadr(cons(z0, cons(z1, z2))) -> z1
isZero(0') -> true
isZero(s(z0)) -> false
plus(z0, z1) -> ifplus(isZero(z0), z0, z1)
ifplus(true, z0, z1) -> z1
ifplus(false, z0, z1) -> s(plus(p(z0), z1))
times(z0, z1) -> iftimes(isZero(z0), z0, z1)
iftimes(true, z0, z1) -> 0'
iftimes(false, z0, z1) -> plus(z1, times(p(z0), z1))
p(s(z0)) -> z0
p(0') -> 0'
shorter(nil, z0) -> true
shorter(cons(z0, z1), 0') -> false
shorter(cons(z0, z1), s(z2)) -> shorter(z1, z2)
prod(z0) -> if(shorter(z0, 0'), shorter(z0, s(0')), z0)
if(true, z0, z1) -> s(0')
if(false, z0, z1) -> if2(z0, z1)
if2(true, z0) -> car(z0)
if2(false, z0) -> prod(cons(times(car(z0), cadr(z0)), cddr(z0)))

Types:
CAR :: cons:nil -> c
cons :: 0':s -> cons:nil -> cons:nil
c :: c
CDDR :: cons:nil -> c1:c2:c3
nil :: cons:nil
c1 :: c1:c2:c3
c2 :: c1:c2:c3
c3 :: c1:c2:c3
CADR :: cons:nil -> c4
c4 :: c4
ISZERO :: 0':s -> c5:c6
0' :: 0':s
c5 :: c5:c6
s :: 0':s -> 0':s
c6 :: c5:c6
PLUS :: 0':s -> 0':s -> c7
c7 :: c8:c9 -> c5:c6 -> c7
IFPLUS :: true:false -> 0':s -> 0':s -> c8:c9
isZero :: 0':s -> true:false
true :: true:false
c8 :: c8:c9
false :: true:false
c9 :: c7 -> c13:c14 -> c8:c9
p :: 0':s -> 0':s
P :: 0':s -> c13:c14
TIMES :: 0':s -> 0':s -> c10
c10 :: c11:c12 -> c5:c6 -> c10
IFTIMES :: true:false -> 0':s -> 0':s -> c11:c12
c11 :: c11:c12
c12 :: c7 -> c10 -> c13:c14 -> c11:c12
times :: 0':s -> 0':s -> 0':s
c13 :: c13:c14
c14 :: c13:c14
SHORTER :: cons:nil -> 0':s -> c15:c16:c17
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
PROD :: cons:nil -> c18:c19
c18 :: c20:c21 -> c15:c16:c17 -> c18:c19
IF :: true:false -> true:false -> cons:nil -> c20:c21
shorter :: cons:nil -> 0':s -> true:false
c19 :: c20:c21 -> c15:c16:c17 -> c18:c19
c20 :: c20:c21
c21 :: c22:c23:c24:c25 -> c20:c21
IF2 :: true:false -> cons:nil -> c22:c23:c24:c25
c22 :: c -> c22:c23:c24:c25
c23 :: c18:c19 -> c10 -> c -> c22:c23:c24:c25
car :: cons:nil -> 0':s
cadr :: cons:nil -> 0':s
cddr :: cons:nil -> cons:nil
c24 :: c18:c19 -> c10 -> c4 -> c22:c23:c24:c25
c25 :: c18:c19 -> c1:c2:c3 -> c22:c23:c24:c25
plus :: 0':s -> 0':s -> 0':s
ifplus :: true:false -> 0':s -> 0':s -> 0':s
iftimes :: true:false -> 0':s -> 0':s -> 0':s
prod :: cons:nil -> 0':s
if :: true:false -> true:false -> cons:nil -> 0':s
if2 :: true:false -> cons:nil -> 0':s
hole_c1_26 :: c
hole_cons:nil2_26 :: cons:nil
hole_0':s3_26 :: 0':s
hole_c1:c2:c34_26 :: c1:c2:c3
hole_c45_26 :: c4
hole_c5:c66_26 :: c5:c6
hole_c77_26 :: c7
hole_c8:c98_26 :: c8:c9
hole_true:false9_26 :: true:false
hole_c13:c1410_26 :: c13:c14
hole_c1011_26 :: c10
hole_c11:c1212_26 :: c11:c12
hole_c15:c16:c1713_26 :: c15:c16:c17
hole_c18:c1914_26 :: c18:c19
hole_c20:c2115_26 :: c20:c21
hole_c22:c23:c24:c2516_26 :: c22:c23:c24:c25
gen_cons:nil17_26 :: Nat -> cons:nil
gen_0':s18_26 :: Nat -> 0':s
gen_c15:c16:c1719_26 :: Nat -> c15:c16:c17

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
PLUS, TIMES, times, SHORTER, PROD, shorter, plus, prod

They will be analysed ascendingly in the following order:
PLUS < TIMES
times < TIMES
TIMES < PROD
times < PROD
plus < times
times < prod
SHORTER < PROD
shorter < PROD
shorter < prod

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

(10)
Obligation:
Innermost TRS:
Rules:
CAR(cons(z0, z1)) -> c
CDDR(nil) -> c1
CDDR(cons(z0, nil)) -> c2
CDDR(cons(z0, cons(z1, z2))) -> c3
CADR(cons(z0, cons(z1, z2))) -> c4
ISZERO(0') -> c5
ISZERO(s(z0)) -> c6
PLUS(z0, z1) -> c7(IFPLUS(isZero(z0), z0, z1), ISZERO(z0))
IFPLUS(true, z0, z1) -> c8
IFPLUS(false, z0, z1) -> c9(PLUS(p(z0), z1), P(z0))
TIMES(z0, z1) -> c10(IFTIMES(isZero(z0), z0, z1), ISZERO(z0))
IFTIMES(true, z0, z1) -> c11
IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(p(z0), z1)), TIMES(p(z0), z1), P(z0))
P(s(z0)) -> c13
P(0') -> c14
SHORTER(nil, z0) -> c15
SHORTER(cons(z0, z1), 0') -> c16
SHORTER(cons(z0, z1), s(z2)) -> c17(SHORTER(z1, z2))
PROD(z0) -> c18(IF(shorter(z0, 0'), shorter(z0, s(0')), z0), SHORTER(z0, 0'))
PROD(z0) -> c19(IF(shorter(z0, 0'), shorter(z0, s(0')), z0), SHORTER(z0, s(0')))
IF(true, z0, z1) -> c20
IF(false, z0, z1) -> c21(IF2(z0, z1))
IF2(true, z0) -> c22(CAR(z0))
IF2(false, z0) -> c23(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CAR(z0))
IF2(false, z0) -> c24(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CADR(z0))
IF2(false, z0) -> c25(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), CDDR(z0))
car(cons(z0, z1)) -> z0
cddr(nil) -> nil
cddr(cons(z0, nil)) -> nil
cddr(cons(z0, cons(z1, z2))) -> z2
cadr(cons(z0, cons(z1, z2))) -> z1
isZero(0') -> true
isZero(s(z0)) -> false
plus(z0, z1) -> ifplus(isZero(z0), z0, z1)
ifplus(true, z0, z1) -> z1
ifplus(false, z0, z1) -> s(plus(p(z0), z1))
times(z0, z1) -> iftimes(isZero(z0), z0, z1)
iftimes(true, z0, z1) -> 0'
iftimes(false, z0, z1) -> plus(z1, times(p(z0), z1))
p(s(z0)) -> z0
p(0') -> 0'
shorter(nil, z0) -> true
shorter(cons(z0, z1), 0') -> false
shorter(cons(z0, z1), s(z2)) -> shorter(z1, z2)
prod(z0) -> if(shorter(z0, 0'), shorter(z0, s(0')), z0)
if(true, z0, z1) -> s(0')
if(false, z0, z1) -> if2(z0, z1)
if2(true, z0) -> car(z0)
if2(false, z0) -> prod(cons(times(car(z0), cadr(z0)), cddr(z0)))

Types:
CAR :: cons:nil -> c
cons :: 0':s -> cons:nil -> cons:nil
c :: c
CDDR :: cons:nil -> c1:c2:c3
nil :: cons:nil
c1 :: c1:c2:c3
c2 :: c1:c2:c3
c3 :: c1:c2:c3
CADR :: cons:nil -> c4
c4 :: c4
ISZERO :: 0':s -> c5:c6
0' :: 0':s
c5 :: c5:c6
s :: 0':s -> 0':s
c6 :: c5:c6
PLUS :: 0':s -> 0':s -> c7
c7 :: c8:c9 -> c5:c6 -> c7
IFPLUS :: true:false -> 0':s -> 0':s -> c8:c9
isZero :: 0':s -> true:false
true :: true:false
c8 :: c8:c9
false :: true:false
c9 :: c7 -> c13:c14 -> c8:c9
p :: 0':s -> 0':s
P :: 0':s -> c13:c14
TIMES :: 0':s -> 0':s -> c10
c10 :: c11:c12 -> c5:c6 -> c10
IFTIMES :: true:false -> 0':s -> 0':s -> c11:c12
c11 :: c11:c12
c12 :: c7 -> c10 -> c13:c14 -> c11:c12
times :: 0':s -> 0':s -> 0':s
c13 :: c13:c14
c14 :: c13:c14
SHORTER :: cons:nil -> 0':s -> c15:c16:c17
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
PROD :: cons:nil -> c18:c19
c18 :: c20:c21 -> c15:c16:c17 -> c18:c19
IF :: true:false -> true:false -> cons:nil -> c20:c21
shorter :: cons:nil -> 0':s -> true:false
c19 :: c20:c21 -> c15:c16:c17 -> c18:c19
c20 :: c20:c21
c21 :: c22:c23:c24:c25 -> c20:c21
IF2 :: true:false -> cons:nil -> c22:c23:c24:c25
c22 :: c -> c22:c23:c24:c25
c23 :: c18:c19 -> c10 -> c -> c22:c23:c24:c25
car :: cons:nil -> 0':s
cadr :: cons:nil -> 0':s
cddr :: cons:nil -> cons:nil
c24 :: c18:c19 -> c10 -> c4 -> c22:c23:c24:c25
c25 :: c18:c19 -> c1:c2:c3 -> c22:c23:c24:c25
plus :: 0':s -> 0':s -> 0':s
ifplus :: true:false -> 0':s -> 0':s -> 0':s
iftimes :: true:false -> 0':s -> 0':s -> 0':s
prod :: cons:nil -> 0':s
if :: true:false -> true:false -> cons:nil -> 0':s
if2 :: true:false -> cons:nil -> 0':s
hole_c1_26 :: c
hole_cons:nil2_26 :: cons:nil
hole_0':s3_26 :: 0':s
hole_c1:c2:c34_26 :: c1:c2:c3
hole_c45_26 :: c4
hole_c5:c66_26 :: c5:c6
hole_c77_26 :: c7
hole_c8:c98_26 :: c8:c9
hole_true:false9_26 :: true:false
hole_c13:c1410_26 :: c13:c14
hole_c1011_26 :: c10
hole_c11:c1212_26 :: c11:c12
hole_c15:c16:c1713_26 :: c15:c16:c17
hole_c18:c1914_26 :: c18:c19
hole_c20:c2115_26 :: c20:c21
hole_c22:c23:c24:c2516_26 :: c22:c23:c24:c25
gen_cons:nil17_26 :: Nat -> cons:nil
gen_0':s18_26 :: Nat -> 0':s
gen_c15:c16:c1719_26 :: Nat -> c15:c16:c17


Generator Equations:
gen_cons:nil17_26(0) <=> nil
gen_cons:nil17_26(+(x, 1)) <=> cons(0', gen_cons:nil17_26(x))
gen_0':s18_26(0) <=> 0'
gen_0':s18_26(+(x, 1)) <=> s(gen_0':s18_26(x))
gen_c15:c16:c1719_26(0) <=> c15
gen_c15:c16:c1719_26(+(x, 1)) <=> c17(gen_c15:c16:c1719_26(x))


The following defined symbols remain to be analysed:
PLUS, TIMES, times, SHORTER, PROD, shorter, plus, prod

They will be analysed ascendingly in the following order:
PLUS < TIMES
times < TIMES
TIMES < PROD
times < PROD
plus < times
times < prod
SHORTER < PROD
shorter < PROD
shorter < prod

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
PLUS(gen_0':s18_26(n21_26), gen_0':s18_26(b)) -> *20_26, rt in Omega(n21_26)

Induction Base:
PLUS(gen_0':s18_26(0), gen_0':s18_26(b))

Induction Step:
PLUS(gen_0':s18_26(+(n21_26, 1)), gen_0':s18_26(b)) ->_R^Omega(1)
c7(IFPLUS(isZero(gen_0':s18_26(+(n21_26, 1))), gen_0':s18_26(+(n21_26, 1)), gen_0':s18_26(b)), ISZERO(gen_0':s18_26(+(n21_26, 1)))) ->_R^Omega(0)
c7(IFPLUS(false, gen_0':s18_26(+(1, n21_26)), gen_0':s18_26(b)), ISZERO(gen_0':s18_26(+(1, n21_26)))) ->_R^Omega(1)
c7(c9(PLUS(p(gen_0':s18_26(+(1, n21_26))), gen_0':s18_26(b)), P(gen_0':s18_26(+(1, n21_26)))), ISZERO(gen_0':s18_26(+(1, n21_26)))) ->_R^Omega(0)
c7(c9(PLUS(gen_0':s18_26(n21_26), gen_0':s18_26(b)), P(gen_0':s18_26(+(1, n21_26)))), ISZERO(gen_0':s18_26(+(1, n21_26)))) ->_IH
c7(c9(*20_26, P(gen_0':s18_26(+(1, n21_26)))), ISZERO(gen_0':s18_26(+(1, n21_26)))) ->_R^Omega(1)
c7(c9(*20_26, c13), ISZERO(gen_0':s18_26(+(1, n21_26)))) ->_R^Omega(1)
c7(c9(*20_26, c13), c6)

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:
CAR(cons(z0, z1)) -> c
CDDR(nil) -> c1
CDDR(cons(z0, nil)) -> c2
CDDR(cons(z0, cons(z1, z2))) -> c3
CADR(cons(z0, cons(z1, z2))) -> c4
ISZERO(0') -> c5
ISZERO(s(z0)) -> c6
PLUS(z0, z1) -> c7(IFPLUS(isZero(z0), z0, z1), ISZERO(z0))
IFPLUS(true, z0, z1) -> c8
IFPLUS(false, z0, z1) -> c9(PLUS(p(z0), z1), P(z0))
TIMES(z0, z1) -> c10(IFTIMES(isZero(z0), z0, z1), ISZERO(z0))
IFTIMES(true, z0, z1) -> c11
IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(p(z0), z1)), TIMES(p(z0), z1), P(z0))
P(s(z0)) -> c13
P(0') -> c14
SHORTER(nil, z0) -> c15
SHORTER(cons(z0, z1), 0') -> c16
SHORTER(cons(z0, z1), s(z2)) -> c17(SHORTER(z1, z2))
PROD(z0) -> c18(IF(shorter(z0, 0'), shorter(z0, s(0')), z0), SHORTER(z0, 0'))
PROD(z0) -> c19(IF(shorter(z0, 0'), shorter(z0, s(0')), z0), SHORTER(z0, s(0')))
IF(true, z0, z1) -> c20
IF(false, z0, z1) -> c21(IF2(z0, z1))
IF2(true, z0) -> c22(CAR(z0))
IF2(false, z0) -> c23(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CAR(z0))
IF2(false, z0) -> c24(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CADR(z0))
IF2(false, z0) -> c25(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), CDDR(z0))
car(cons(z0, z1)) -> z0
cddr(nil) -> nil
cddr(cons(z0, nil)) -> nil
cddr(cons(z0, cons(z1, z2))) -> z2
cadr(cons(z0, cons(z1, z2))) -> z1
isZero(0') -> true
isZero(s(z0)) -> false
plus(z0, z1) -> ifplus(isZero(z0), z0, z1)
ifplus(true, z0, z1) -> z1
ifplus(false, z0, z1) -> s(plus(p(z0), z1))
times(z0, z1) -> iftimes(isZero(z0), z0, z1)
iftimes(true, z0, z1) -> 0'
iftimes(false, z0, z1) -> plus(z1, times(p(z0), z1))
p(s(z0)) -> z0
p(0') -> 0'
shorter(nil, z0) -> true
shorter(cons(z0, z1), 0') -> false
shorter(cons(z0, z1), s(z2)) -> shorter(z1, z2)
prod(z0) -> if(shorter(z0, 0'), shorter(z0, s(0')), z0)
if(true, z0, z1) -> s(0')
if(false, z0, z1) -> if2(z0, z1)
if2(true, z0) -> car(z0)
if2(false, z0) -> prod(cons(times(car(z0), cadr(z0)), cddr(z0)))

Types:
CAR :: cons:nil -> c
cons :: 0':s -> cons:nil -> cons:nil
c :: c
CDDR :: cons:nil -> c1:c2:c3
nil :: cons:nil
c1 :: c1:c2:c3
c2 :: c1:c2:c3
c3 :: c1:c2:c3
CADR :: cons:nil -> c4
c4 :: c4
ISZERO :: 0':s -> c5:c6
0' :: 0':s
c5 :: c5:c6
s :: 0':s -> 0':s
c6 :: c5:c6
PLUS :: 0':s -> 0':s -> c7
c7 :: c8:c9 -> c5:c6 -> c7
IFPLUS :: true:false -> 0':s -> 0':s -> c8:c9
isZero :: 0':s -> true:false
true :: true:false
c8 :: c8:c9
false :: true:false
c9 :: c7 -> c13:c14 -> c8:c9
p :: 0':s -> 0':s
P :: 0':s -> c13:c14
TIMES :: 0':s -> 0':s -> c10
c10 :: c11:c12 -> c5:c6 -> c10
IFTIMES :: true:false -> 0':s -> 0':s -> c11:c12
c11 :: c11:c12
c12 :: c7 -> c10 -> c13:c14 -> c11:c12
times :: 0':s -> 0':s -> 0':s
c13 :: c13:c14
c14 :: c13:c14
SHORTER :: cons:nil -> 0':s -> c15:c16:c17
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
PROD :: cons:nil -> c18:c19
c18 :: c20:c21 -> c15:c16:c17 -> c18:c19
IF :: true:false -> true:false -> cons:nil -> c20:c21
shorter :: cons:nil -> 0':s -> true:false
c19 :: c20:c21 -> c15:c16:c17 -> c18:c19
c20 :: c20:c21
c21 :: c22:c23:c24:c25 -> c20:c21
IF2 :: true:false -> cons:nil -> c22:c23:c24:c25
c22 :: c -> c22:c23:c24:c25
c23 :: c18:c19 -> c10 -> c -> c22:c23:c24:c25
car :: cons:nil -> 0':s
cadr :: cons:nil -> 0':s
cddr :: cons:nil -> cons:nil
c24 :: c18:c19 -> c10 -> c4 -> c22:c23:c24:c25
c25 :: c18:c19 -> c1:c2:c3 -> c22:c23:c24:c25
plus :: 0':s -> 0':s -> 0':s
ifplus :: true:false -> 0':s -> 0':s -> 0':s
iftimes :: true:false -> 0':s -> 0':s -> 0':s
prod :: cons:nil -> 0':s
if :: true:false -> true:false -> cons:nil -> 0':s
if2 :: true:false -> cons:nil -> 0':s
hole_c1_26 :: c
hole_cons:nil2_26 :: cons:nil
hole_0':s3_26 :: 0':s
hole_c1:c2:c34_26 :: c1:c2:c3
hole_c45_26 :: c4
hole_c5:c66_26 :: c5:c6
hole_c77_26 :: c7
hole_c8:c98_26 :: c8:c9
hole_true:false9_26 :: true:false
hole_c13:c1410_26 :: c13:c14
hole_c1011_26 :: c10
hole_c11:c1212_26 :: c11:c12
hole_c15:c16:c1713_26 :: c15:c16:c17
hole_c18:c1914_26 :: c18:c19
hole_c20:c2115_26 :: c20:c21
hole_c22:c23:c24:c2516_26 :: c22:c23:c24:c25
gen_cons:nil17_26 :: Nat -> cons:nil
gen_0':s18_26 :: Nat -> 0':s
gen_c15:c16:c1719_26 :: Nat -> c15:c16:c17


Generator Equations:
gen_cons:nil17_26(0) <=> nil
gen_cons:nil17_26(+(x, 1)) <=> cons(0', gen_cons:nil17_26(x))
gen_0':s18_26(0) <=> 0'
gen_0':s18_26(+(x, 1)) <=> s(gen_0':s18_26(x))
gen_c15:c16:c1719_26(0) <=> c15
gen_c15:c16:c1719_26(+(x, 1)) <=> c17(gen_c15:c16:c1719_26(x))


The following defined symbols remain to be analysed:
PLUS, TIMES, times, SHORTER, PROD, shorter, plus, prod

They will be analysed ascendingly in the following order:
PLUS < TIMES
times < TIMES
TIMES < PROD
times < PROD
plus < times
times < prod
SHORTER < PROD
shorter < PROD
shorter < prod

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
CAR(cons(z0, z1)) -> c
CDDR(nil) -> c1
CDDR(cons(z0, nil)) -> c2
CDDR(cons(z0, cons(z1, z2))) -> c3
CADR(cons(z0, cons(z1, z2))) -> c4
ISZERO(0') -> c5
ISZERO(s(z0)) -> c6
PLUS(z0, z1) -> c7(IFPLUS(isZero(z0), z0, z1), ISZERO(z0))
IFPLUS(true, z0, z1) -> c8
IFPLUS(false, z0, z1) -> c9(PLUS(p(z0), z1), P(z0))
TIMES(z0, z1) -> c10(IFTIMES(isZero(z0), z0, z1), ISZERO(z0))
IFTIMES(true, z0, z1) -> c11
IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(p(z0), z1)), TIMES(p(z0), z1), P(z0))
P(s(z0)) -> c13
P(0') -> c14
SHORTER(nil, z0) -> c15
SHORTER(cons(z0, z1), 0') -> c16
SHORTER(cons(z0, z1), s(z2)) -> c17(SHORTER(z1, z2))
PROD(z0) -> c18(IF(shorter(z0, 0'), shorter(z0, s(0')), z0), SHORTER(z0, 0'))
PROD(z0) -> c19(IF(shorter(z0, 0'), shorter(z0, s(0')), z0), SHORTER(z0, s(0')))
IF(true, z0, z1) -> c20
IF(false, z0, z1) -> c21(IF2(z0, z1))
IF2(true, z0) -> c22(CAR(z0))
IF2(false, z0) -> c23(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CAR(z0))
IF2(false, z0) -> c24(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CADR(z0))
IF2(false, z0) -> c25(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), CDDR(z0))
car(cons(z0, z1)) -> z0
cddr(nil) -> nil
cddr(cons(z0, nil)) -> nil
cddr(cons(z0, cons(z1, z2))) -> z2
cadr(cons(z0, cons(z1, z2))) -> z1
isZero(0') -> true
isZero(s(z0)) -> false
plus(z0, z1) -> ifplus(isZero(z0), z0, z1)
ifplus(true, z0, z1) -> z1
ifplus(false, z0, z1) -> s(plus(p(z0), z1))
times(z0, z1) -> iftimes(isZero(z0), z0, z1)
iftimes(true, z0, z1) -> 0'
iftimes(false, z0, z1) -> plus(z1, times(p(z0), z1))
p(s(z0)) -> z0
p(0') -> 0'
shorter(nil, z0) -> true
shorter(cons(z0, z1), 0') -> false
shorter(cons(z0, z1), s(z2)) -> shorter(z1, z2)
prod(z0) -> if(shorter(z0, 0'), shorter(z0, s(0')), z0)
if(true, z0, z1) -> s(0')
if(false, z0, z1) -> if2(z0, z1)
if2(true, z0) -> car(z0)
if2(false, z0) -> prod(cons(times(car(z0), cadr(z0)), cddr(z0)))

Types:
CAR :: cons:nil -> c
cons :: 0':s -> cons:nil -> cons:nil
c :: c
CDDR :: cons:nil -> c1:c2:c3
nil :: cons:nil
c1 :: c1:c2:c3
c2 :: c1:c2:c3
c3 :: c1:c2:c3
CADR :: cons:nil -> c4
c4 :: c4
ISZERO :: 0':s -> c5:c6
0' :: 0':s
c5 :: c5:c6
s :: 0':s -> 0':s
c6 :: c5:c6
PLUS :: 0':s -> 0':s -> c7
c7 :: c8:c9 -> c5:c6 -> c7
IFPLUS :: true:false -> 0':s -> 0':s -> c8:c9
isZero :: 0':s -> true:false
true :: true:false
c8 :: c8:c9
false :: true:false
c9 :: c7 -> c13:c14 -> c8:c9
p :: 0':s -> 0':s
P :: 0':s -> c13:c14
TIMES :: 0':s -> 0':s -> c10
c10 :: c11:c12 -> c5:c6 -> c10
IFTIMES :: true:false -> 0':s -> 0':s -> c11:c12
c11 :: c11:c12
c12 :: c7 -> c10 -> c13:c14 -> c11:c12
times :: 0':s -> 0':s -> 0':s
c13 :: c13:c14
c14 :: c13:c14
SHORTER :: cons:nil -> 0':s -> c15:c16:c17
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
PROD :: cons:nil -> c18:c19
c18 :: c20:c21 -> c15:c16:c17 -> c18:c19
IF :: true:false -> true:false -> cons:nil -> c20:c21
shorter :: cons:nil -> 0':s -> true:false
c19 :: c20:c21 -> c15:c16:c17 -> c18:c19
c20 :: c20:c21
c21 :: c22:c23:c24:c25 -> c20:c21
IF2 :: true:false -> cons:nil -> c22:c23:c24:c25
c22 :: c -> c22:c23:c24:c25
c23 :: c18:c19 -> c10 -> c -> c22:c23:c24:c25
car :: cons:nil -> 0':s
cadr :: cons:nil -> 0':s
cddr :: cons:nil -> cons:nil
c24 :: c18:c19 -> c10 -> c4 -> c22:c23:c24:c25
c25 :: c18:c19 -> c1:c2:c3 -> c22:c23:c24:c25
plus :: 0':s -> 0':s -> 0':s
ifplus :: true:false -> 0':s -> 0':s -> 0':s
iftimes :: true:false -> 0':s -> 0':s -> 0':s
prod :: cons:nil -> 0':s
if :: true:false -> true:false -> cons:nil -> 0':s
if2 :: true:false -> cons:nil -> 0':s
hole_c1_26 :: c
hole_cons:nil2_26 :: cons:nil
hole_0':s3_26 :: 0':s
hole_c1:c2:c34_26 :: c1:c2:c3
hole_c45_26 :: c4
hole_c5:c66_26 :: c5:c6
hole_c77_26 :: c7
hole_c8:c98_26 :: c8:c9
hole_true:false9_26 :: true:false
hole_c13:c1410_26 :: c13:c14
hole_c1011_26 :: c10
hole_c11:c1212_26 :: c11:c12
hole_c15:c16:c1713_26 :: c15:c16:c17
hole_c18:c1914_26 :: c18:c19
hole_c20:c2115_26 :: c20:c21
hole_c22:c23:c24:c2516_26 :: c22:c23:c24:c25
gen_cons:nil17_26 :: Nat -> cons:nil
gen_0':s18_26 :: Nat -> 0':s
gen_c15:c16:c1719_26 :: Nat -> c15:c16:c17


Lemmas:
PLUS(gen_0':s18_26(n21_26), gen_0':s18_26(b)) -> *20_26, rt in Omega(n21_26)


Generator Equations:
gen_cons:nil17_26(0) <=> nil
gen_cons:nil17_26(+(x, 1)) <=> cons(0', gen_cons:nil17_26(x))
gen_0':s18_26(0) <=> 0'
gen_0':s18_26(+(x, 1)) <=> s(gen_0':s18_26(x))
gen_c15:c16:c1719_26(0) <=> c15
gen_c15:c16:c1719_26(+(x, 1)) <=> c17(gen_c15:c16:c1719_26(x))


The following defined symbols remain to be analysed:
SHORTER, TIMES, times, PROD, shorter, plus, prod

They will be analysed ascendingly in the following order:
times < TIMES
TIMES < PROD
times < PROD
plus < times
times < prod
SHORTER < PROD
shorter < PROD
shorter < prod

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
SHORTER(gen_cons:nil17_26(n3405_26), gen_0':s18_26(n3405_26)) -> gen_c15:c16:c1719_26(n3405_26), rt in Omega(1 + n3405_26)

Induction Base:
SHORTER(gen_cons:nil17_26(0), gen_0':s18_26(0)) ->_R^Omega(1)
c15

Induction Step:
SHORTER(gen_cons:nil17_26(+(n3405_26, 1)), gen_0':s18_26(+(n3405_26, 1))) ->_R^Omega(1)
c17(SHORTER(gen_cons:nil17_26(n3405_26), gen_0':s18_26(n3405_26))) ->_IH
c17(gen_c15:c16:c1719_26(c3406_26))

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:
CAR(cons(z0, z1)) -> c
CDDR(nil) -> c1
CDDR(cons(z0, nil)) -> c2
CDDR(cons(z0, cons(z1, z2))) -> c3
CADR(cons(z0, cons(z1, z2))) -> c4
ISZERO(0') -> c5
ISZERO(s(z0)) -> c6
PLUS(z0, z1) -> c7(IFPLUS(isZero(z0), z0, z1), ISZERO(z0))
IFPLUS(true, z0, z1) -> c8
IFPLUS(false, z0, z1) -> c9(PLUS(p(z0), z1), P(z0))
TIMES(z0, z1) -> c10(IFTIMES(isZero(z0), z0, z1), ISZERO(z0))
IFTIMES(true, z0, z1) -> c11
IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(p(z0), z1)), TIMES(p(z0), z1), P(z0))
P(s(z0)) -> c13
P(0') -> c14
SHORTER(nil, z0) -> c15
SHORTER(cons(z0, z1), 0') -> c16
SHORTER(cons(z0, z1), s(z2)) -> c17(SHORTER(z1, z2))
PROD(z0) -> c18(IF(shorter(z0, 0'), shorter(z0, s(0')), z0), SHORTER(z0, 0'))
PROD(z0) -> c19(IF(shorter(z0, 0'), shorter(z0, s(0')), z0), SHORTER(z0, s(0')))
IF(true, z0, z1) -> c20
IF(false, z0, z1) -> c21(IF2(z0, z1))
IF2(true, z0) -> c22(CAR(z0))
IF2(false, z0) -> c23(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CAR(z0))
IF2(false, z0) -> c24(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CADR(z0))
IF2(false, z0) -> c25(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), CDDR(z0))
car(cons(z0, z1)) -> z0
cddr(nil) -> nil
cddr(cons(z0, nil)) -> nil
cddr(cons(z0, cons(z1, z2))) -> z2
cadr(cons(z0, cons(z1, z2))) -> z1
isZero(0') -> true
isZero(s(z0)) -> false
plus(z0, z1) -> ifplus(isZero(z0), z0, z1)
ifplus(true, z0, z1) -> z1
ifplus(false, z0, z1) -> s(plus(p(z0), z1))
times(z0, z1) -> iftimes(isZero(z0), z0, z1)
iftimes(true, z0, z1) -> 0'
iftimes(false, z0, z1) -> plus(z1, times(p(z0), z1))
p(s(z0)) -> z0
p(0') -> 0'
shorter(nil, z0) -> true
shorter(cons(z0, z1), 0') -> false
shorter(cons(z0, z1), s(z2)) -> shorter(z1, z2)
prod(z0) -> if(shorter(z0, 0'), shorter(z0, s(0')), z0)
if(true, z0, z1) -> s(0')
if(false, z0, z1) -> if2(z0, z1)
if2(true, z0) -> car(z0)
if2(false, z0) -> prod(cons(times(car(z0), cadr(z0)), cddr(z0)))

Types:
CAR :: cons:nil -> c
cons :: 0':s -> cons:nil -> cons:nil
c :: c
CDDR :: cons:nil -> c1:c2:c3
nil :: cons:nil
c1 :: c1:c2:c3
c2 :: c1:c2:c3
c3 :: c1:c2:c3
CADR :: cons:nil -> c4
c4 :: c4
ISZERO :: 0':s -> c5:c6
0' :: 0':s
c5 :: c5:c6
s :: 0':s -> 0':s
c6 :: c5:c6
PLUS :: 0':s -> 0':s -> c7
c7 :: c8:c9 -> c5:c6 -> c7
IFPLUS :: true:false -> 0':s -> 0':s -> c8:c9
isZero :: 0':s -> true:false
true :: true:false
c8 :: c8:c9
false :: true:false
c9 :: c7 -> c13:c14 -> c8:c9
p :: 0':s -> 0':s
P :: 0':s -> c13:c14
TIMES :: 0':s -> 0':s -> c10
c10 :: c11:c12 -> c5:c6 -> c10
IFTIMES :: true:false -> 0':s -> 0':s -> c11:c12
c11 :: c11:c12
c12 :: c7 -> c10 -> c13:c14 -> c11:c12
times :: 0':s -> 0':s -> 0':s
c13 :: c13:c14
c14 :: c13:c14
SHORTER :: cons:nil -> 0':s -> c15:c16:c17
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
PROD :: cons:nil -> c18:c19
c18 :: c20:c21 -> c15:c16:c17 -> c18:c19
IF :: true:false -> true:false -> cons:nil -> c20:c21
shorter :: cons:nil -> 0':s -> true:false
c19 :: c20:c21 -> c15:c16:c17 -> c18:c19
c20 :: c20:c21
c21 :: c22:c23:c24:c25 -> c20:c21
IF2 :: true:false -> cons:nil -> c22:c23:c24:c25
c22 :: c -> c22:c23:c24:c25
c23 :: c18:c19 -> c10 -> c -> c22:c23:c24:c25
car :: cons:nil -> 0':s
cadr :: cons:nil -> 0':s
cddr :: cons:nil -> cons:nil
c24 :: c18:c19 -> c10 -> c4 -> c22:c23:c24:c25
c25 :: c18:c19 -> c1:c2:c3 -> c22:c23:c24:c25
plus :: 0':s -> 0':s -> 0':s
ifplus :: true:false -> 0':s -> 0':s -> 0':s
iftimes :: true:false -> 0':s -> 0':s -> 0':s
prod :: cons:nil -> 0':s
if :: true:false -> true:false -> cons:nil -> 0':s
if2 :: true:false -> cons:nil -> 0':s
hole_c1_26 :: c
hole_cons:nil2_26 :: cons:nil
hole_0':s3_26 :: 0':s
hole_c1:c2:c34_26 :: c1:c2:c3
hole_c45_26 :: c4
hole_c5:c66_26 :: c5:c6
hole_c77_26 :: c7
hole_c8:c98_26 :: c8:c9
hole_true:false9_26 :: true:false
hole_c13:c1410_26 :: c13:c14
hole_c1011_26 :: c10
hole_c11:c1212_26 :: c11:c12
hole_c15:c16:c1713_26 :: c15:c16:c17
hole_c18:c1914_26 :: c18:c19
hole_c20:c2115_26 :: c20:c21
hole_c22:c23:c24:c2516_26 :: c22:c23:c24:c25
gen_cons:nil17_26 :: Nat -> cons:nil
gen_0':s18_26 :: Nat -> 0':s
gen_c15:c16:c1719_26 :: Nat -> c15:c16:c17


Lemmas:
PLUS(gen_0':s18_26(n21_26), gen_0':s18_26(b)) -> *20_26, rt in Omega(n21_26)
SHORTER(gen_cons:nil17_26(n3405_26), gen_0':s18_26(n3405_26)) -> gen_c15:c16:c1719_26(n3405_26), rt in Omega(1 + n3405_26)


Generator Equations:
gen_cons:nil17_26(0) <=> nil
gen_cons:nil17_26(+(x, 1)) <=> cons(0', gen_cons:nil17_26(x))
gen_0':s18_26(0) <=> 0'
gen_0':s18_26(+(x, 1)) <=> s(gen_0':s18_26(x))
gen_c15:c16:c1719_26(0) <=> c15
gen_c15:c16:c1719_26(+(x, 1)) <=> c17(gen_c15:c16:c1719_26(x))


The following defined symbols remain to be analysed:
shorter, TIMES, times, PROD, plus, prod

They will be analysed ascendingly in the following order:
times < TIMES
TIMES < PROD
times < PROD
plus < times
times < prod
shorter < PROD
shorter < prod

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
shorter(gen_cons:nil17_26(n4534_26), gen_0':s18_26(n4534_26)) -> true, rt in Omega(0)

Induction Base:
shorter(gen_cons:nil17_26(0), gen_0':s18_26(0)) ->_R^Omega(0)
true

Induction Step:
shorter(gen_cons:nil17_26(+(n4534_26, 1)), gen_0':s18_26(+(n4534_26, 1))) ->_R^Omega(0)
shorter(gen_cons:nil17_26(n4534_26), gen_0':s18_26(n4534_26)) ->_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:
CAR(cons(z0, z1)) -> c
CDDR(nil) -> c1
CDDR(cons(z0, nil)) -> c2
CDDR(cons(z0, cons(z1, z2))) -> c3
CADR(cons(z0, cons(z1, z2))) -> c4
ISZERO(0') -> c5
ISZERO(s(z0)) -> c6
PLUS(z0, z1) -> c7(IFPLUS(isZero(z0), z0, z1), ISZERO(z0))
IFPLUS(true, z0, z1) -> c8
IFPLUS(false, z0, z1) -> c9(PLUS(p(z0), z1), P(z0))
TIMES(z0, z1) -> c10(IFTIMES(isZero(z0), z0, z1), ISZERO(z0))
IFTIMES(true, z0, z1) -> c11
IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(p(z0), z1)), TIMES(p(z0), z1), P(z0))
P(s(z0)) -> c13
P(0') -> c14
SHORTER(nil, z0) -> c15
SHORTER(cons(z0, z1), 0') -> c16
SHORTER(cons(z0, z1), s(z2)) -> c17(SHORTER(z1, z2))
PROD(z0) -> c18(IF(shorter(z0, 0'), shorter(z0, s(0')), z0), SHORTER(z0, 0'))
PROD(z0) -> c19(IF(shorter(z0, 0'), shorter(z0, s(0')), z0), SHORTER(z0, s(0')))
IF(true, z0, z1) -> c20
IF(false, z0, z1) -> c21(IF2(z0, z1))
IF2(true, z0) -> c22(CAR(z0))
IF2(false, z0) -> c23(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CAR(z0))
IF2(false, z0) -> c24(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CADR(z0))
IF2(false, z0) -> c25(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), CDDR(z0))
car(cons(z0, z1)) -> z0
cddr(nil) -> nil
cddr(cons(z0, nil)) -> nil
cddr(cons(z0, cons(z1, z2))) -> z2
cadr(cons(z0, cons(z1, z2))) -> z1
isZero(0') -> true
isZero(s(z0)) -> false
plus(z0, z1) -> ifplus(isZero(z0), z0, z1)
ifplus(true, z0, z1) -> z1
ifplus(false, z0, z1) -> s(plus(p(z0), z1))
times(z0, z1) -> iftimes(isZero(z0), z0, z1)
iftimes(true, z0, z1) -> 0'
iftimes(false, z0, z1) -> plus(z1, times(p(z0), z1))
p(s(z0)) -> z0
p(0') -> 0'
shorter(nil, z0) -> true
shorter(cons(z0, z1), 0') -> false
shorter(cons(z0, z1), s(z2)) -> shorter(z1, z2)
prod(z0) -> if(shorter(z0, 0'), shorter(z0, s(0')), z0)
if(true, z0, z1) -> s(0')
if(false, z0, z1) -> if2(z0, z1)
if2(true, z0) -> car(z0)
if2(false, z0) -> prod(cons(times(car(z0), cadr(z0)), cddr(z0)))

Types:
CAR :: cons:nil -> c
cons :: 0':s -> cons:nil -> cons:nil
c :: c
CDDR :: cons:nil -> c1:c2:c3
nil :: cons:nil
c1 :: c1:c2:c3
c2 :: c1:c2:c3
c3 :: c1:c2:c3
CADR :: cons:nil -> c4
c4 :: c4
ISZERO :: 0':s -> c5:c6
0' :: 0':s
c5 :: c5:c6
s :: 0':s -> 0':s
c6 :: c5:c6
PLUS :: 0':s -> 0':s -> c7
c7 :: c8:c9 -> c5:c6 -> c7
IFPLUS :: true:false -> 0':s -> 0':s -> c8:c9
isZero :: 0':s -> true:false
true :: true:false
c8 :: c8:c9
false :: true:false
c9 :: c7 -> c13:c14 -> c8:c9
p :: 0':s -> 0':s
P :: 0':s -> c13:c14
TIMES :: 0':s -> 0':s -> c10
c10 :: c11:c12 -> c5:c6 -> c10
IFTIMES :: true:false -> 0':s -> 0':s -> c11:c12
c11 :: c11:c12
c12 :: c7 -> c10 -> c13:c14 -> c11:c12
times :: 0':s -> 0':s -> 0':s
c13 :: c13:c14
c14 :: c13:c14
SHORTER :: cons:nil -> 0':s -> c15:c16:c17
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
PROD :: cons:nil -> c18:c19
c18 :: c20:c21 -> c15:c16:c17 -> c18:c19
IF :: true:false -> true:false -> cons:nil -> c20:c21
shorter :: cons:nil -> 0':s -> true:false
c19 :: c20:c21 -> c15:c16:c17 -> c18:c19
c20 :: c20:c21
c21 :: c22:c23:c24:c25 -> c20:c21
IF2 :: true:false -> cons:nil -> c22:c23:c24:c25
c22 :: c -> c22:c23:c24:c25
c23 :: c18:c19 -> c10 -> c -> c22:c23:c24:c25
car :: cons:nil -> 0':s
cadr :: cons:nil -> 0':s
cddr :: cons:nil -> cons:nil
c24 :: c18:c19 -> c10 -> c4 -> c22:c23:c24:c25
c25 :: c18:c19 -> c1:c2:c3 -> c22:c23:c24:c25
plus :: 0':s -> 0':s -> 0':s
ifplus :: true:false -> 0':s -> 0':s -> 0':s
iftimes :: true:false -> 0':s -> 0':s -> 0':s
prod :: cons:nil -> 0':s
if :: true:false -> true:false -> cons:nil -> 0':s
if2 :: true:false -> cons:nil -> 0':s
hole_c1_26 :: c
hole_cons:nil2_26 :: cons:nil
hole_0':s3_26 :: 0':s
hole_c1:c2:c34_26 :: c1:c2:c3
hole_c45_26 :: c4
hole_c5:c66_26 :: c5:c6
hole_c77_26 :: c7
hole_c8:c98_26 :: c8:c9
hole_true:false9_26 :: true:false
hole_c13:c1410_26 :: c13:c14
hole_c1011_26 :: c10
hole_c11:c1212_26 :: c11:c12
hole_c15:c16:c1713_26 :: c15:c16:c17
hole_c18:c1914_26 :: c18:c19
hole_c20:c2115_26 :: c20:c21
hole_c22:c23:c24:c2516_26 :: c22:c23:c24:c25
gen_cons:nil17_26 :: Nat -> cons:nil
gen_0':s18_26 :: Nat -> 0':s
gen_c15:c16:c1719_26 :: Nat -> c15:c16:c17


Lemmas:
PLUS(gen_0':s18_26(n21_26), gen_0':s18_26(b)) -> *20_26, rt in Omega(n21_26)
SHORTER(gen_cons:nil17_26(n3405_26), gen_0':s18_26(n3405_26)) -> gen_c15:c16:c1719_26(n3405_26), rt in Omega(1 + n3405_26)
shorter(gen_cons:nil17_26(n4534_26), gen_0':s18_26(n4534_26)) -> true, rt in Omega(0)


Generator Equations:
gen_cons:nil17_26(0) <=> nil
gen_cons:nil17_26(+(x, 1)) <=> cons(0', gen_cons:nil17_26(x))
gen_0':s18_26(0) <=> 0'
gen_0':s18_26(+(x, 1)) <=> s(gen_0':s18_26(x))
gen_c15:c16:c1719_26(0) <=> c15
gen_c15:c16:c1719_26(+(x, 1)) <=> c17(gen_c15:c16:c1719_26(x))


The following defined symbols remain to be analysed:
plus, TIMES, times, PROD, prod

They will be analysed ascendingly in the following order:
times < TIMES
TIMES < PROD
times < PROD
plus < times
times < prod

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
plus(gen_0':s18_26(n5238_26), gen_0':s18_26(b)) -> gen_0':s18_26(+(n5238_26, b)), rt in Omega(0)

Induction Base:
plus(gen_0':s18_26(0), gen_0':s18_26(b)) ->_R^Omega(0)
ifplus(isZero(gen_0':s18_26(0)), gen_0':s18_26(0), gen_0':s18_26(b)) ->_R^Omega(0)
ifplus(true, gen_0':s18_26(0), gen_0':s18_26(b)) ->_R^Omega(0)
gen_0':s18_26(b)

Induction Step:
plus(gen_0':s18_26(+(n5238_26, 1)), gen_0':s18_26(b)) ->_R^Omega(0)
ifplus(isZero(gen_0':s18_26(+(n5238_26, 1))), gen_0':s18_26(+(n5238_26, 1)), gen_0':s18_26(b)) ->_R^Omega(0)
ifplus(false, gen_0':s18_26(+(1, n5238_26)), gen_0':s18_26(b)) ->_R^Omega(0)
s(plus(p(gen_0':s18_26(+(1, n5238_26))), gen_0':s18_26(b))) ->_R^Omega(0)
s(plus(gen_0':s18_26(n5238_26), gen_0':s18_26(b))) ->_IH
s(gen_0':s18_26(+(b, c5239_26)))

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

(22)
Obligation:
Innermost TRS:
Rules:
CAR(cons(z0, z1)) -> c
CDDR(nil) -> c1
CDDR(cons(z0, nil)) -> c2
CDDR(cons(z0, cons(z1, z2))) -> c3
CADR(cons(z0, cons(z1, z2))) -> c4
ISZERO(0') -> c5
ISZERO(s(z0)) -> c6
PLUS(z0, z1) -> c7(IFPLUS(isZero(z0), z0, z1), ISZERO(z0))
IFPLUS(true, z0, z1) -> c8
IFPLUS(false, z0, z1) -> c9(PLUS(p(z0), z1), P(z0))
TIMES(z0, z1) -> c10(IFTIMES(isZero(z0), z0, z1), ISZERO(z0))
IFTIMES(true, z0, z1) -> c11
IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(p(z0), z1)), TIMES(p(z0), z1), P(z0))
P(s(z0)) -> c13
P(0') -> c14
SHORTER(nil, z0) -> c15
SHORTER(cons(z0, z1), 0') -> c16
SHORTER(cons(z0, z1), s(z2)) -> c17(SHORTER(z1, z2))
PROD(z0) -> c18(IF(shorter(z0, 0'), shorter(z0, s(0')), z0), SHORTER(z0, 0'))
PROD(z0) -> c19(IF(shorter(z0, 0'), shorter(z0, s(0')), z0), SHORTER(z0, s(0')))
IF(true, z0, z1) -> c20
IF(false, z0, z1) -> c21(IF2(z0, z1))
IF2(true, z0) -> c22(CAR(z0))
IF2(false, z0) -> c23(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CAR(z0))
IF2(false, z0) -> c24(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CADR(z0))
IF2(false, z0) -> c25(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), CDDR(z0))
car(cons(z0, z1)) -> z0
cddr(nil) -> nil
cddr(cons(z0, nil)) -> nil
cddr(cons(z0, cons(z1, z2))) -> z2
cadr(cons(z0, cons(z1, z2))) -> z1
isZero(0') -> true
isZero(s(z0)) -> false
plus(z0, z1) -> ifplus(isZero(z0), z0, z1)
ifplus(true, z0, z1) -> z1
ifplus(false, z0, z1) -> s(plus(p(z0), z1))
times(z0, z1) -> iftimes(isZero(z0), z0, z1)
iftimes(true, z0, z1) -> 0'
iftimes(false, z0, z1) -> plus(z1, times(p(z0), z1))
p(s(z0)) -> z0
p(0') -> 0'
shorter(nil, z0) -> true
shorter(cons(z0, z1), 0') -> false
shorter(cons(z0, z1), s(z2)) -> shorter(z1, z2)
prod(z0) -> if(shorter(z0, 0'), shorter(z0, s(0')), z0)
if(true, z0, z1) -> s(0')
if(false, z0, z1) -> if2(z0, z1)
if2(true, z0) -> car(z0)
if2(false, z0) -> prod(cons(times(car(z0), cadr(z0)), cddr(z0)))

Types:
CAR :: cons:nil -> c
cons :: 0':s -> cons:nil -> cons:nil
c :: c
CDDR :: cons:nil -> c1:c2:c3
nil :: cons:nil
c1 :: c1:c2:c3
c2 :: c1:c2:c3
c3 :: c1:c2:c3
CADR :: cons:nil -> c4
c4 :: c4
ISZERO :: 0':s -> c5:c6
0' :: 0':s
c5 :: c5:c6
s :: 0':s -> 0':s
c6 :: c5:c6
PLUS :: 0':s -> 0':s -> c7
c7 :: c8:c9 -> c5:c6 -> c7
IFPLUS :: true:false -> 0':s -> 0':s -> c8:c9
isZero :: 0':s -> true:false
true :: true:false
c8 :: c8:c9
false :: true:false
c9 :: c7 -> c13:c14 -> c8:c9
p :: 0':s -> 0':s
P :: 0':s -> c13:c14
TIMES :: 0':s -> 0':s -> c10
c10 :: c11:c12 -> c5:c6 -> c10
IFTIMES :: true:false -> 0':s -> 0':s -> c11:c12
c11 :: c11:c12
c12 :: c7 -> c10 -> c13:c14 -> c11:c12
times :: 0':s -> 0':s -> 0':s
c13 :: c13:c14
c14 :: c13:c14
SHORTER :: cons:nil -> 0':s -> c15:c16:c17
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
PROD :: cons:nil -> c18:c19
c18 :: c20:c21 -> c15:c16:c17 -> c18:c19
IF :: true:false -> true:false -> cons:nil -> c20:c21
shorter :: cons:nil -> 0':s -> true:false
c19 :: c20:c21 -> c15:c16:c17 -> c18:c19
c20 :: c20:c21
c21 :: c22:c23:c24:c25 -> c20:c21
IF2 :: true:false -> cons:nil -> c22:c23:c24:c25
c22 :: c -> c22:c23:c24:c25
c23 :: c18:c19 -> c10 -> c -> c22:c23:c24:c25
car :: cons:nil -> 0':s
cadr :: cons:nil -> 0':s
cddr :: cons:nil -> cons:nil
c24 :: c18:c19 -> c10 -> c4 -> c22:c23:c24:c25
c25 :: c18:c19 -> c1:c2:c3 -> c22:c23:c24:c25
plus :: 0':s -> 0':s -> 0':s
ifplus :: true:false -> 0':s -> 0':s -> 0':s
iftimes :: true:false -> 0':s -> 0':s -> 0':s
prod :: cons:nil -> 0':s
if :: true:false -> true:false -> cons:nil -> 0':s
if2 :: true:false -> cons:nil -> 0':s
hole_c1_26 :: c
hole_cons:nil2_26 :: cons:nil
hole_0':s3_26 :: 0':s
hole_c1:c2:c34_26 :: c1:c2:c3
hole_c45_26 :: c4
hole_c5:c66_26 :: c5:c6
hole_c77_26 :: c7
hole_c8:c98_26 :: c8:c9
hole_true:false9_26 :: true:false
hole_c13:c1410_26 :: c13:c14
hole_c1011_26 :: c10
hole_c11:c1212_26 :: c11:c12
hole_c15:c16:c1713_26 :: c15:c16:c17
hole_c18:c1914_26 :: c18:c19
hole_c20:c2115_26 :: c20:c21
hole_c22:c23:c24:c2516_26 :: c22:c23:c24:c25
gen_cons:nil17_26 :: Nat -> cons:nil
gen_0':s18_26 :: Nat -> 0':s
gen_c15:c16:c1719_26 :: Nat -> c15:c16:c17


Lemmas:
PLUS(gen_0':s18_26(n21_26), gen_0':s18_26(b)) -> *20_26, rt in Omega(n21_26)
SHORTER(gen_cons:nil17_26(n3405_26), gen_0':s18_26(n3405_26)) -> gen_c15:c16:c1719_26(n3405_26), rt in Omega(1 + n3405_26)
shorter(gen_cons:nil17_26(n4534_26), gen_0':s18_26(n4534_26)) -> true, rt in Omega(0)
plus(gen_0':s18_26(n5238_26), gen_0':s18_26(b)) -> gen_0':s18_26(+(n5238_26, b)), rt in Omega(0)


Generator Equations:
gen_cons:nil17_26(0) <=> nil
gen_cons:nil17_26(+(x, 1)) <=> cons(0', gen_cons:nil17_26(x))
gen_0':s18_26(0) <=> 0'
gen_0':s18_26(+(x, 1)) <=> s(gen_0':s18_26(x))
gen_c15:c16:c1719_26(0) <=> c15
gen_c15:c16:c1719_26(+(x, 1)) <=> c17(gen_c15:c16:c1719_26(x))


The following defined symbols remain to be analysed:
times, TIMES, PROD, prod

They will be analysed ascendingly in the following order:
times < TIMES
TIMES < PROD
times < PROD
times < prod

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
times(gen_0':s18_26(n8153_26), gen_0':s18_26(b)) -> gen_0':s18_26(*(n8153_26, b)), rt in Omega(0)

Induction Base:
times(gen_0':s18_26(0), gen_0':s18_26(b)) ->_R^Omega(0)
iftimes(isZero(gen_0':s18_26(0)), gen_0':s18_26(0), gen_0':s18_26(b)) ->_R^Omega(0)
iftimes(true, gen_0':s18_26(0), gen_0':s18_26(b)) ->_R^Omega(0)
0'

Induction Step:
times(gen_0':s18_26(+(n8153_26, 1)), gen_0':s18_26(b)) ->_R^Omega(0)
iftimes(isZero(gen_0':s18_26(+(n8153_26, 1))), gen_0':s18_26(+(n8153_26, 1)), gen_0':s18_26(b)) ->_R^Omega(0)
iftimes(false, gen_0':s18_26(+(1, n8153_26)), gen_0':s18_26(b)) ->_R^Omega(0)
plus(gen_0':s18_26(b), times(p(gen_0':s18_26(+(1, n8153_26))), gen_0':s18_26(b))) ->_R^Omega(0)
plus(gen_0':s18_26(b), times(gen_0':s18_26(n8153_26), gen_0':s18_26(b))) ->_IH
plus(gen_0':s18_26(b), gen_0':s18_26(*(c8154_26, b))) ->_L^Omega(0)
gen_0':s18_26(+(b, *(n8153_26, b)))

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:
CAR(cons(z0, z1)) -> c
CDDR(nil) -> c1
CDDR(cons(z0, nil)) -> c2
CDDR(cons(z0, cons(z1, z2))) -> c3
CADR(cons(z0, cons(z1, z2))) -> c4
ISZERO(0') -> c5
ISZERO(s(z0)) -> c6
PLUS(z0, z1) -> c7(IFPLUS(isZero(z0), z0, z1), ISZERO(z0))
IFPLUS(true, z0, z1) -> c8
IFPLUS(false, z0, z1) -> c9(PLUS(p(z0), z1), P(z0))
TIMES(z0, z1) -> c10(IFTIMES(isZero(z0), z0, z1), ISZERO(z0))
IFTIMES(true, z0, z1) -> c11
IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(p(z0), z1)), TIMES(p(z0), z1), P(z0))
P(s(z0)) -> c13
P(0') -> c14
SHORTER(nil, z0) -> c15
SHORTER(cons(z0, z1), 0') -> c16
SHORTER(cons(z0, z1), s(z2)) -> c17(SHORTER(z1, z2))
PROD(z0) -> c18(IF(shorter(z0, 0'), shorter(z0, s(0')), z0), SHORTER(z0, 0'))
PROD(z0) -> c19(IF(shorter(z0, 0'), shorter(z0, s(0')), z0), SHORTER(z0, s(0')))
IF(true, z0, z1) -> c20
IF(false, z0, z1) -> c21(IF2(z0, z1))
IF2(true, z0) -> c22(CAR(z0))
IF2(false, z0) -> c23(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CAR(z0))
IF2(false, z0) -> c24(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CADR(z0))
IF2(false, z0) -> c25(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), CDDR(z0))
car(cons(z0, z1)) -> z0
cddr(nil) -> nil
cddr(cons(z0, nil)) -> nil
cddr(cons(z0, cons(z1, z2))) -> z2
cadr(cons(z0, cons(z1, z2))) -> z1
isZero(0') -> true
isZero(s(z0)) -> false
plus(z0, z1) -> ifplus(isZero(z0), z0, z1)
ifplus(true, z0, z1) -> z1
ifplus(false, z0, z1) -> s(plus(p(z0), z1))
times(z0, z1) -> iftimes(isZero(z0), z0, z1)
iftimes(true, z0, z1) -> 0'
iftimes(false, z0, z1) -> plus(z1, times(p(z0), z1))
p(s(z0)) -> z0
p(0') -> 0'
shorter(nil, z0) -> true
shorter(cons(z0, z1), 0') -> false
shorter(cons(z0, z1), s(z2)) -> shorter(z1, z2)
prod(z0) -> if(shorter(z0, 0'), shorter(z0, s(0')), z0)
if(true, z0, z1) -> s(0')
if(false, z0, z1) -> if2(z0, z1)
if2(true, z0) -> car(z0)
if2(false, z0) -> prod(cons(times(car(z0), cadr(z0)), cddr(z0)))

Types:
CAR :: cons:nil -> c
cons :: 0':s -> cons:nil -> cons:nil
c :: c
CDDR :: cons:nil -> c1:c2:c3
nil :: cons:nil
c1 :: c1:c2:c3
c2 :: c1:c2:c3
c3 :: c1:c2:c3
CADR :: cons:nil -> c4
c4 :: c4
ISZERO :: 0':s -> c5:c6
0' :: 0':s
c5 :: c5:c6
s :: 0':s -> 0':s
c6 :: c5:c6
PLUS :: 0':s -> 0':s -> c7
c7 :: c8:c9 -> c5:c6 -> c7
IFPLUS :: true:false -> 0':s -> 0':s -> c8:c9
isZero :: 0':s -> true:false
true :: true:false
c8 :: c8:c9
false :: true:false
c9 :: c7 -> c13:c14 -> c8:c9
p :: 0':s -> 0':s
P :: 0':s -> c13:c14
TIMES :: 0':s -> 0':s -> c10
c10 :: c11:c12 -> c5:c6 -> c10
IFTIMES :: true:false -> 0':s -> 0':s -> c11:c12
c11 :: c11:c12
c12 :: c7 -> c10 -> c13:c14 -> c11:c12
times :: 0':s -> 0':s -> 0':s
c13 :: c13:c14
c14 :: c13:c14
SHORTER :: cons:nil -> 0':s -> c15:c16:c17
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
PROD :: cons:nil -> c18:c19
c18 :: c20:c21 -> c15:c16:c17 -> c18:c19
IF :: true:false -> true:false -> cons:nil -> c20:c21
shorter :: cons:nil -> 0':s -> true:false
c19 :: c20:c21 -> c15:c16:c17 -> c18:c19
c20 :: c20:c21
c21 :: c22:c23:c24:c25 -> c20:c21
IF2 :: true:false -> cons:nil -> c22:c23:c24:c25
c22 :: c -> c22:c23:c24:c25
c23 :: c18:c19 -> c10 -> c -> c22:c23:c24:c25
car :: cons:nil -> 0':s
cadr :: cons:nil -> 0':s
cddr :: cons:nil -> cons:nil
c24 :: c18:c19 -> c10 -> c4 -> c22:c23:c24:c25
c25 :: c18:c19 -> c1:c2:c3 -> c22:c23:c24:c25
plus :: 0':s -> 0':s -> 0':s
ifplus :: true:false -> 0':s -> 0':s -> 0':s
iftimes :: true:false -> 0':s -> 0':s -> 0':s
prod :: cons:nil -> 0':s
if :: true:false -> true:false -> cons:nil -> 0':s
if2 :: true:false -> cons:nil -> 0':s
hole_c1_26 :: c
hole_cons:nil2_26 :: cons:nil
hole_0':s3_26 :: 0':s
hole_c1:c2:c34_26 :: c1:c2:c3
hole_c45_26 :: c4
hole_c5:c66_26 :: c5:c6
hole_c77_26 :: c7
hole_c8:c98_26 :: c8:c9
hole_true:false9_26 :: true:false
hole_c13:c1410_26 :: c13:c14
hole_c1011_26 :: c10
hole_c11:c1212_26 :: c11:c12
hole_c15:c16:c1713_26 :: c15:c16:c17
hole_c18:c1914_26 :: c18:c19
hole_c20:c2115_26 :: c20:c21
hole_c22:c23:c24:c2516_26 :: c22:c23:c24:c25
gen_cons:nil17_26 :: Nat -> cons:nil
gen_0':s18_26 :: Nat -> 0':s
gen_c15:c16:c1719_26 :: Nat -> c15:c16:c17


Lemmas:
PLUS(gen_0':s18_26(n21_26), gen_0':s18_26(b)) -> *20_26, rt in Omega(n21_26)
SHORTER(gen_cons:nil17_26(n3405_26), gen_0':s18_26(n3405_26)) -> gen_c15:c16:c1719_26(n3405_26), rt in Omega(1 + n3405_26)
shorter(gen_cons:nil17_26(n4534_26), gen_0':s18_26(n4534_26)) -> true, rt in Omega(0)
plus(gen_0':s18_26(n5238_26), gen_0':s18_26(b)) -> gen_0':s18_26(+(n5238_26, b)), rt in Omega(0)
times(gen_0':s18_26(n8153_26), gen_0':s18_26(b)) -> gen_0':s18_26(*(n8153_26, b)), rt in Omega(0)


Generator Equations:
gen_cons:nil17_26(0) <=> nil
gen_cons:nil17_26(+(x, 1)) <=> cons(0', gen_cons:nil17_26(x))
gen_0':s18_26(0) <=> 0'
gen_0':s18_26(+(x, 1)) <=> s(gen_0':s18_26(x))
gen_c15:c16:c1719_26(0) <=> c15
gen_c15:c16:c1719_26(+(x, 1)) <=> c17(gen_c15:c16:c1719_26(x))


The following defined symbols remain to be analysed:
TIMES, PROD, prod

They will be analysed ascendingly in the following order:
TIMES < PROD

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
TIMES(gen_0':s18_26(n12695_26), gen_0':s18_26(0)) -> *20_26, rt in Omega(n12695_26)

Induction Base:
TIMES(gen_0':s18_26(0), gen_0':s18_26(0))

Induction Step:
TIMES(gen_0':s18_26(+(n12695_26, 1)), gen_0':s18_26(0)) ->_R^Omega(1)
c10(IFTIMES(isZero(gen_0':s18_26(+(n12695_26, 1))), gen_0':s18_26(+(n12695_26, 1)), gen_0':s18_26(0)), ISZERO(gen_0':s18_26(+(n12695_26, 1)))) ->_R^Omega(0)
c10(IFTIMES(false, gen_0':s18_26(+(1, n12695_26)), gen_0':s18_26(0)), ISZERO(gen_0':s18_26(+(1, n12695_26)))) ->_R^Omega(1)
c10(c12(PLUS(gen_0':s18_26(0), times(p(gen_0':s18_26(+(1, n12695_26))), gen_0':s18_26(0))), TIMES(p(gen_0':s18_26(+(1, n12695_26))), gen_0':s18_26(0)), P(gen_0':s18_26(+(1, n12695_26)))), ISZERO(gen_0':s18_26(+(1, n12695_26)))) ->_R^Omega(0)
c10(c12(PLUS(gen_0':s18_26(0), times(gen_0':s18_26(n12695_26), gen_0':s18_26(0))), TIMES(p(gen_0':s18_26(+(1, n12695_26))), gen_0':s18_26(0)), P(gen_0':s18_26(+(1, n12695_26)))), ISZERO(gen_0':s18_26(+(1, n12695_26)))) ->_L^Omega(0)
c10(c12(PLUS(gen_0':s18_26(0), gen_0':s18_26(*(n12695_26, 0))), TIMES(p(gen_0':s18_26(+(1, n12695_26))), gen_0':s18_26(0)), P(gen_0':s18_26(+(1, n12695_26)))), ISZERO(gen_0':s18_26(+(1, n12695_26)))) ->_R^Omega(1)
c10(c12(c7(IFPLUS(isZero(gen_0':s18_26(0)), gen_0':s18_26(0), gen_0':s18_26(0)), ISZERO(gen_0':s18_26(0))), TIMES(p(gen_0':s18_26(+(1, n12695_26))), gen_0':s18_26(0)), P(gen_0':s18_26(+(1, n12695_26)))), ISZERO(gen_0':s18_26(+(1, n12695_26)))) ->_R^Omega(0)
c10(c12(c7(IFPLUS(true, gen_0':s18_26(0), gen_0':s18_26(0)), ISZERO(gen_0':s18_26(0))), TIMES(p(gen_0':s18_26(+(1, n12695_26))), gen_0':s18_26(0)), P(gen_0':s18_26(+(1, n12695_26)))), ISZERO(gen_0':s18_26(+(1, n12695_26)))) ->_R^Omega(1)
c10(c12(c7(c8, ISZERO(gen_0':s18_26(0))), TIMES(p(gen_0':s18_26(+(1, n12695_26))), gen_0':s18_26(0)), P(gen_0':s18_26(+(1, n12695_26)))), ISZERO(gen_0':s18_26(+(1, n12695_26)))) ->_R^Omega(1)
c10(c12(c7(c8, c5), TIMES(p(gen_0':s18_26(+(1, n12695_26))), gen_0':s18_26(0)), P(gen_0':s18_26(+(1, n12695_26)))), ISZERO(gen_0':s18_26(+(1, n12695_26)))) ->_R^Omega(0)
c10(c12(c7(c8, c5), TIMES(gen_0':s18_26(n12695_26), gen_0':s18_26(0)), P(gen_0':s18_26(+(1, n12695_26)))), ISZERO(gen_0':s18_26(+(1, n12695_26)))) ->_IH
c10(c12(c7(c8, c5), *20_26, P(gen_0':s18_26(+(1, n12695_26)))), ISZERO(gen_0':s18_26(+(1, n12695_26)))) ->_R^Omega(1)
c10(c12(c7(c8, c5), *20_26, c13), ISZERO(gen_0':s18_26(+(1, n12695_26)))) ->_R^Omega(1)
c10(c12(c7(c8, c5), *20_26, c13), c6)

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

(26)
Obligation:
Innermost TRS:
Rules:
CAR(cons(z0, z1)) -> c
CDDR(nil) -> c1
CDDR(cons(z0, nil)) -> c2
CDDR(cons(z0, cons(z1, z2))) -> c3
CADR(cons(z0, cons(z1, z2))) -> c4
ISZERO(0') -> c5
ISZERO(s(z0)) -> c6
PLUS(z0, z1) -> c7(IFPLUS(isZero(z0), z0, z1), ISZERO(z0))
IFPLUS(true, z0, z1) -> c8
IFPLUS(false, z0, z1) -> c9(PLUS(p(z0), z1), P(z0))
TIMES(z0, z1) -> c10(IFTIMES(isZero(z0), z0, z1), ISZERO(z0))
IFTIMES(true, z0, z1) -> c11
IFTIMES(false, z0, z1) -> c12(PLUS(z1, times(p(z0), z1)), TIMES(p(z0), z1), P(z0))
P(s(z0)) -> c13
P(0') -> c14
SHORTER(nil, z0) -> c15
SHORTER(cons(z0, z1), 0') -> c16
SHORTER(cons(z0, z1), s(z2)) -> c17(SHORTER(z1, z2))
PROD(z0) -> c18(IF(shorter(z0, 0'), shorter(z0, s(0')), z0), SHORTER(z0, 0'))
PROD(z0) -> c19(IF(shorter(z0, 0'), shorter(z0, s(0')), z0), SHORTER(z0, s(0')))
IF(true, z0, z1) -> c20
IF(false, z0, z1) -> c21(IF2(z0, z1))
IF2(true, z0) -> c22(CAR(z0))
IF2(false, z0) -> c23(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CAR(z0))
IF2(false, z0) -> c24(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), TIMES(car(z0), cadr(z0)), CADR(z0))
IF2(false, z0) -> c25(PROD(cons(times(car(z0), cadr(z0)), cddr(z0))), CDDR(z0))
car(cons(z0, z1)) -> z0
cddr(nil) -> nil
cddr(cons(z0, nil)) -> nil
cddr(cons(z0, cons(z1, z2))) -> z2
cadr(cons(z0, cons(z1, z2))) -> z1
isZero(0') -> true
isZero(s(z0)) -> false
plus(z0, z1) -> ifplus(isZero(z0), z0, z1)
ifplus(true, z0, z1) -> z1
ifplus(false, z0, z1) -> s(plus(p(z0), z1))
times(z0, z1) -> iftimes(isZero(z0), z0, z1)
iftimes(true, z0, z1) -> 0'
iftimes(false, z0, z1) -> plus(z1, times(p(z0), z1))
p(s(z0)) -> z0
p(0') -> 0'
shorter(nil, z0) -> true
shorter(cons(z0, z1), 0') -> false
shorter(cons(z0, z1), s(z2)) -> shorter(z1, z2)
prod(z0) -> if(shorter(z0, 0'), shorter(z0, s(0')), z0)
if(true, z0, z1) -> s(0')
if(false, z0, z1) -> if2(z0, z1)
if2(true, z0) -> car(z0)
if2(false, z0) -> prod(cons(times(car(z0), cadr(z0)), cddr(z0)))

Types:
CAR :: cons:nil -> c
cons :: 0':s -> cons:nil -> cons:nil
c :: c
CDDR :: cons:nil -> c1:c2:c3
nil :: cons:nil
c1 :: c1:c2:c3
c2 :: c1:c2:c3
c3 :: c1:c2:c3
CADR :: cons:nil -> c4
c4 :: c4
ISZERO :: 0':s -> c5:c6
0' :: 0':s
c5 :: c5:c6
s :: 0':s -> 0':s
c6 :: c5:c6
PLUS :: 0':s -> 0':s -> c7
c7 :: c8:c9 -> c5:c6 -> c7
IFPLUS :: true:false -> 0':s -> 0':s -> c8:c9
isZero :: 0':s -> true:false
true :: true:false
c8 :: c8:c9
false :: true:false
c9 :: c7 -> c13:c14 -> c8:c9
p :: 0':s -> 0':s
P :: 0':s -> c13:c14
TIMES :: 0':s -> 0':s -> c10
c10 :: c11:c12 -> c5:c6 -> c10
IFTIMES :: true:false -> 0':s -> 0':s -> c11:c12
c11 :: c11:c12
c12 :: c7 -> c10 -> c13:c14 -> c11:c12
times :: 0':s -> 0':s -> 0':s
c13 :: c13:c14
c14 :: c13:c14
SHORTER :: cons:nil -> 0':s -> c15:c16:c17
c15 :: c15:c16:c17
c16 :: c15:c16:c17
c17 :: c15:c16:c17 -> c15:c16:c17
PROD :: cons:nil -> c18:c19
c18 :: c20:c21 -> c15:c16:c17 -> c18:c19
IF :: true:false -> true:false -> cons:nil -> c20:c21
shorter :: cons:nil -> 0':s -> true:false
c19 :: c20:c21 -> c15:c16:c17 -> c18:c19
c20 :: c20:c21
c21 :: c22:c23:c24:c25 -> c20:c21
IF2 :: true:false -> cons:nil -> c22:c23:c24:c25
c22 :: c -> c22:c23:c24:c25
c23 :: c18:c19 -> c10 -> c -> c22:c23:c24:c25
car :: cons:nil -> 0':s
cadr :: cons:nil -> 0':s
cddr :: cons:nil -> cons:nil
c24 :: c18:c19 -> c10 -> c4 -> c22:c23:c24:c25
c25 :: c18:c19 -> c1:c2:c3 -> c22:c23:c24:c25
plus :: 0':s -> 0':s -> 0':s
ifplus :: true:false -> 0':s -> 0':s -> 0':s
iftimes :: true:false -> 0':s -> 0':s -> 0':s
prod :: cons:nil -> 0':s
if :: true:false -> true:false -> cons:nil -> 0':s
if2 :: true:false -> cons:nil -> 0':s
hole_c1_26 :: c
hole_cons:nil2_26 :: cons:nil
hole_0':s3_26 :: 0':s
hole_c1:c2:c34_26 :: c1:c2:c3
hole_c45_26 :: c4
hole_c5:c66_26 :: c5:c6
hole_c77_26 :: c7
hole_c8:c98_26 :: c8:c9
hole_true:false9_26 :: true:false
hole_c13:c1410_26 :: c13:c14
hole_c1011_26 :: c10
hole_c11:c1212_26 :: c11:c12
hole_c15:c16:c1713_26 :: c15:c16:c17
hole_c18:c1914_26 :: c18:c19
hole_c20:c2115_26 :: c20:c21
hole_c22:c23:c24:c2516_26 :: c22:c23:c24:c25
gen_cons:nil17_26 :: Nat -> cons:nil
gen_0':s18_26 :: Nat -> 0':s
gen_c15:c16:c1719_26 :: Nat -> c15:c16:c17


Lemmas:
PLUS(gen_0':s18_26(n21_26), gen_0':s18_26(b)) -> *20_26, rt in Omega(n21_26)
SHORTER(gen_cons:nil17_26(n3405_26), gen_0':s18_26(n3405_26)) -> gen_c15:c16:c1719_26(n3405_26), rt in Omega(1 + n3405_26)
shorter(gen_cons:nil17_26(n4534_26), gen_0':s18_26(n4534_26)) -> true, rt in Omega(0)
plus(gen_0':s18_26(n5238_26), gen_0':s18_26(b)) -> gen_0':s18_26(+(n5238_26, b)), rt in Omega(0)
times(gen_0':s18_26(n8153_26), gen_0':s18_26(b)) -> gen_0':s18_26(*(n8153_26, b)), rt in Omega(0)
TIMES(gen_0':s18_26(n12695_26), gen_0':s18_26(0)) -> *20_26, rt in Omega(n12695_26)


Generator Equations:
gen_cons:nil17_26(0) <=> nil
gen_cons:nil17_26(+(x, 1)) <=> cons(0', gen_cons:nil17_26(x))
gen_0':s18_26(0) <=> 0'
gen_0':s18_26(+(x, 1)) <=> s(gen_0':s18_26(x))
gen_c15:c16:c1719_26(0) <=> c15
gen_c15:c16:c1719_26(+(x, 1)) <=> c17(gen_c15:c16:c1719_26(x))


The following defined symbols remain to be analysed:
PROD, prod