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), 711 ms]
(2) CpxRelTRS
(3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) typed CpxTrs
(7) OrderProof [LOWER BOUND(ID), 0 ms]
(8) typed CpxTrs
(9) RewriteLemmaProof [LOWER BOUND(ID), 338 ms]
(10) BEST
    (11) proven lower bound
        (12) LowerBoundPropagationProof [FINISHED, 0 ms]
        (13) BOUNDS(n^1, INF)
    (14) typed CpxTrs
        (15) RewriteLemmaProof [LOWER BOUND(ID), 60 ms]
        (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 25 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 23 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 56 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 0 ms]
        (24) 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:

   EVEN(0) -> c
   EVEN(s(0)) -> c1
   EVEN(s(s(z0))) -> c2(EVEN(z0))
   HALF(0) -> c3
   HALF(s(s(z0))) -> c4(HALF(z0))
   PLUS(0, z0) -> c5
   PLUS(s(z0), z1) -> c6(PLUS(z0, z1))
   TIMES(0, z0) -> c7
   TIMES(s(z0), z1) -> c8(IF_TIMES(even(s(z0)), s(z0), z1), EVEN(s(z0)))
   IF_TIMES(true, s(z0), z1) -> c9(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
   IF_TIMES(true, s(z0), z1) -> c10(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
   IF_TIMES(false, s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1))

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

   even(0) -> true
   even(s(0)) -> false
   even(s(s(z0))) -> even(z0)
   half(0) -> 0
   half(s(s(z0))) -> s(half(z0))
   plus(0, z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   times(0, z0) -> 0
   times(s(z0), z1) -> if_times(even(s(z0)), s(z0), z1)
   if_times(true, s(z0), z1) -> plus(times(half(s(z0)), z1), times(half(s(z0)), z1))
   if_times(false, s(z0), z1) -> plus(z1, times(z0, z1))

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:

   EVEN(0) -> c
   EVEN(s(0)) -> c1
   EVEN(s(s(z0))) -> c2(EVEN(z0))
   HALF(0) -> c3
   HALF(s(s(z0))) -> c4(HALF(z0))
   PLUS(0, z0) -> c5
   PLUS(s(z0), z1) -> c6(PLUS(z0, z1))
   TIMES(0, z0) -> c7
   TIMES(s(z0), z1) -> c8(IF_TIMES(even(s(z0)), s(z0), z1), EVEN(s(z0)))
   IF_TIMES(true, s(z0), z1) -> c9(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
   IF_TIMES(true, s(z0), z1) -> c10(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
   IF_TIMES(false, s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1))

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

   even(0) -> true
   even(s(0)) -> false
   even(s(s(z0))) -> even(z0)
   half(0) -> 0
   half(s(s(z0))) -> s(half(z0))
   plus(0, z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   times(0, z0) -> 0
   times(s(z0), z1) -> if_times(even(s(z0)), s(z0), z1)
   if_times(true, s(z0), z1) -> plus(times(half(s(z0)), z1), times(half(s(z0)), z1))
   if_times(false, s(z0), z1) -> plus(z1, times(z0, z1))

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:

   EVEN(0') -> c
   EVEN(s(0')) -> c1
   EVEN(s(s(z0))) -> c2(EVEN(z0))
   HALF(0') -> c3
   HALF(s(s(z0))) -> c4(HALF(z0))
   PLUS(0', z0) -> c5
   PLUS(s(z0), z1) -> c6(PLUS(z0, z1))
   TIMES(0', z0) -> c7
   TIMES(s(z0), z1) -> c8(IF_TIMES(even(s(z0)), s(z0), z1), EVEN(s(z0)))
   IF_TIMES(true, s(z0), z1) -> c9(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
   IF_TIMES(true, s(z0), z1) -> c10(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
   IF_TIMES(false, s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1))

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

   even(0') -> true
   even(s(0')) -> false
   even(s(s(z0))) -> even(z0)
   half(0') -> 0'
   half(s(s(z0))) -> s(half(z0))
   plus(0', z0) -> z0
   plus(s(z0), z1) -> s(plus(z0, z1))
   times(0', z0) -> 0'
   times(s(z0), z1) -> if_times(even(s(z0)), s(z0), z1)
   if_times(true, s(z0), z1) -> plus(times(half(s(z0)), z1), times(half(s(z0)), z1))
   if_times(false, s(z0), z1) -> plus(z1, times(z0, z1))

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

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

(6)
Obligation:
Innermost TRS:
Rules:
EVEN(0') -> c
EVEN(s(0')) -> c1
EVEN(s(s(z0))) -> c2(EVEN(z0))
HALF(0') -> c3
HALF(s(s(z0))) -> c4(HALF(z0))
PLUS(0', z0) -> c5
PLUS(s(z0), z1) -> c6(PLUS(z0, z1))
TIMES(0', z0) -> c7
TIMES(s(z0), z1) -> c8(IF_TIMES(even(s(z0)), s(z0), z1), EVEN(s(z0)))
IF_TIMES(true, s(z0), z1) -> c9(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
IF_TIMES(true, s(z0), z1) -> c10(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
IF_TIMES(false, s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
even(0') -> true
even(s(0')) -> false
even(s(s(z0))) -> even(z0)
half(0') -> 0'
half(s(s(z0))) -> s(half(z0))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> if_times(even(s(z0)), s(z0), z1)
if_times(true, s(z0), z1) -> plus(times(half(s(z0)), z1), times(half(s(z0)), z1))
if_times(false, s(z0), z1) -> plus(z1, times(z0, z1))

Types:
EVEN :: 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
HALF :: 0':s -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
PLUS :: 0':s -> 0':s -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
TIMES :: 0':s -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c9:c10:c11 -> c:c1:c2 -> c7:c8
IF_TIMES :: true:false -> 0':s -> 0':s -> c9:c10:c11
even :: 0':s -> true:false
true :: true:false
c9 :: c5:c6 -> c7:c8 -> c3:c4 -> c9:c10:c11
times :: 0':s -> 0':s -> 0':s
half :: 0':s -> 0':s
c10 :: c5:c6 -> c7:c8 -> c3:c4 -> c9:c10:c11
false :: true:false
c11 :: c5:c6 -> c7:c8 -> c9:c10:c11
plus :: 0':s -> 0':s -> 0':s
if_times :: true:false -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_12 :: c:c1:c2
hole_0':s2_12 :: 0':s
hole_c3:c43_12 :: c3:c4
hole_c5:c64_12 :: c5:c6
hole_c7:c85_12 :: c7:c8
hole_c9:c10:c116_12 :: c9:c10:c11
hole_true:false7_12 :: true:false
gen_c:c1:c28_12 :: Nat -> c:c1:c2
gen_0':s9_12 :: Nat -> 0':s
gen_c3:c410_12 :: Nat -> c3:c4
gen_c5:c611_12 :: Nat -> c5:c6

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

(7) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
EVEN, HALF, PLUS, TIMES, even, times, half, plus

They will be analysed ascendingly in the following order:
EVEN < TIMES
HALF < TIMES
PLUS < TIMES
even < TIMES
times < TIMES
half < TIMES
even < times
half < times
plus < times

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

(8)
Obligation:
Innermost TRS:
Rules:
EVEN(0') -> c
EVEN(s(0')) -> c1
EVEN(s(s(z0))) -> c2(EVEN(z0))
HALF(0') -> c3
HALF(s(s(z0))) -> c4(HALF(z0))
PLUS(0', z0) -> c5
PLUS(s(z0), z1) -> c6(PLUS(z0, z1))
TIMES(0', z0) -> c7
TIMES(s(z0), z1) -> c8(IF_TIMES(even(s(z0)), s(z0), z1), EVEN(s(z0)))
IF_TIMES(true, s(z0), z1) -> c9(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
IF_TIMES(true, s(z0), z1) -> c10(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
IF_TIMES(false, s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
even(0') -> true
even(s(0')) -> false
even(s(s(z0))) -> even(z0)
half(0') -> 0'
half(s(s(z0))) -> s(half(z0))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> if_times(even(s(z0)), s(z0), z1)
if_times(true, s(z0), z1) -> plus(times(half(s(z0)), z1), times(half(s(z0)), z1))
if_times(false, s(z0), z1) -> plus(z1, times(z0, z1))

Types:
EVEN :: 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
HALF :: 0':s -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
PLUS :: 0':s -> 0':s -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
TIMES :: 0':s -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c9:c10:c11 -> c:c1:c2 -> c7:c8
IF_TIMES :: true:false -> 0':s -> 0':s -> c9:c10:c11
even :: 0':s -> true:false
true :: true:false
c9 :: c5:c6 -> c7:c8 -> c3:c4 -> c9:c10:c11
times :: 0':s -> 0':s -> 0':s
half :: 0':s -> 0':s
c10 :: c5:c6 -> c7:c8 -> c3:c4 -> c9:c10:c11
false :: true:false
c11 :: c5:c6 -> c7:c8 -> c9:c10:c11
plus :: 0':s -> 0':s -> 0':s
if_times :: true:false -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_12 :: c:c1:c2
hole_0':s2_12 :: 0':s
hole_c3:c43_12 :: c3:c4
hole_c5:c64_12 :: c5:c6
hole_c7:c85_12 :: c7:c8
hole_c9:c10:c116_12 :: c9:c10:c11
hole_true:false7_12 :: true:false
gen_c:c1:c28_12 :: Nat -> c:c1:c2
gen_0':s9_12 :: Nat -> 0':s
gen_c3:c410_12 :: Nat -> c3:c4
gen_c5:c611_12 :: Nat -> c5:c6


Generator Equations:
gen_c:c1:c28_12(0) <=> c
gen_c:c1:c28_12(+(x, 1)) <=> c2(gen_c:c1:c28_12(x))
gen_0':s9_12(0) <=> 0'
gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x))
gen_c3:c410_12(0) <=> c3
gen_c3:c410_12(+(x, 1)) <=> c4(gen_c3:c410_12(x))
gen_c5:c611_12(0) <=> c5
gen_c5:c611_12(+(x, 1)) <=> c6(gen_c5:c611_12(x))


The following defined symbols remain to be analysed:
EVEN, HALF, PLUS, TIMES, even, times, half, plus

They will be analysed ascendingly in the following order:
EVEN < TIMES
HALF < TIMES
PLUS < TIMES
even < TIMES
times < TIMES
half < TIMES
even < times
half < times
plus < times

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

(9) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
EVEN(gen_0':s9_12(*(2, n13_12))) -> gen_c:c1:c28_12(n13_12), rt in Omega(1 + n13_12)

Induction Base:
EVEN(gen_0':s9_12(*(2, 0))) ->_R^Omega(1)
c

Induction Step:
EVEN(gen_0':s9_12(*(2, +(n13_12, 1)))) ->_R^Omega(1)
c2(EVEN(gen_0':s9_12(*(2, n13_12)))) ->_IH
c2(gen_c:c1:c28_12(c14_12))

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

(10)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
EVEN(0') -> c
EVEN(s(0')) -> c1
EVEN(s(s(z0))) -> c2(EVEN(z0))
HALF(0') -> c3
HALF(s(s(z0))) -> c4(HALF(z0))
PLUS(0', z0) -> c5
PLUS(s(z0), z1) -> c6(PLUS(z0, z1))
TIMES(0', z0) -> c7
TIMES(s(z0), z1) -> c8(IF_TIMES(even(s(z0)), s(z0), z1), EVEN(s(z0)))
IF_TIMES(true, s(z0), z1) -> c9(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
IF_TIMES(true, s(z0), z1) -> c10(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
IF_TIMES(false, s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
even(0') -> true
even(s(0')) -> false
even(s(s(z0))) -> even(z0)
half(0') -> 0'
half(s(s(z0))) -> s(half(z0))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> if_times(even(s(z0)), s(z0), z1)
if_times(true, s(z0), z1) -> plus(times(half(s(z0)), z1), times(half(s(z0)), z1))
if_times(false, s(z0), z1) -> plus(z1, times(z0, z1))

Types:
EVEN :: 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
HALF :: 0':s -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
PLUS :: 0':s -> 0':s -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
TIMES :: 0':s -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c9:c10:c11 -> c:c1:c2 -> c7:c8
IF_TIMES :: true:false -> 0':s -> 0':s -> c9:c10:c11
even :: 0':s -> true:false
true :: true:false
c9 :: c5:c6 -> c7:c8 -> c3:c4 -> c9:c10:c11
times :: 0':s -> 0':s -> 0':s
half :: 0':s -> 0':s
c10 :: c5:c6 -> c7:c8 -> c3:c4 -> c9:c10:c11
false :: true:false
c11 :: c5:c6 -> c7:c8 -> c9:c10:c11
plus :: 0':s -> 0':s -> 0':s
if_times :: true:false -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_12 :: c:c1:c2
hole_0':s2_12 :: 0':s
hole_c3:c43_12 :: c3:c4
hole_c5:c64_12 :: c5:c6
hole_c7:c85_12 :: c7:c8
hole_c9:c10:c116_12 :: c9:c10:c11
hole_true:false7_12 :: true:false
gen_c:c1:c28_12 :: Nat -> c:c1:c2
gen_0':s9_12 :: Nat -> 0':s
gen_c3:c410_12 :: Nat -> c3:c4
gen_c5:c611_12 :: Nat -> c5:c6


Generator Equations:
gen_c:c1:c28_12(0) <=> c
gen_c:c1:c28_12(+(x, 1)) <=> c2(gen_c:c1:c28_12(x))
gen_0':s9_12(0) <=> 0'
gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x))
gen_c3:c410_12(0) <=> c3
gen_c3:c410_12(+(x, 1)) <=> c4(gen_c3:c410_12(x))
gen_c5:c611_12(0) <=> c5
gen_c5:c611_12(+(x, 1)) <=> c6(gen_c5:c611_12(x))


The following defined symbols remain to be analysed:
EVEN, HALF, PLUS, TIMES, even, times, half, plus

They will be analysed ascendingly in the following order:
EVEN < TIMES
HALF < TIMES
PLUS < TIMES
even < TIMES
times < TIMES
half < TIMES
even < times
half < times
plus < times

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

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

(13)
BOUNDS(n^1, INF)

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

(14)
Obligation:
Innermost TRS:
Rules:
EVEN(0') -> c
EVEN(s(0')) -> c1
EVEN(s(s(z0))) -> c2(EVEN(z0))
HALF(0') -> c3
HALF(s(s(z0))) -> c4(HALF(z0))
PLUS(0', z0) -> c5
PLUS(s(z0), z1) -> c6(PLUS(z0, z1))
TIMES(0', z0) -> c7
TIMES(s(z0), z1) -> c8(IF_TIMES(even(s(z0)), s(z0), z1), EVEN(s(z0)))
IF_TIMES(true, s(z0), z1) -> c9(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
IF_TIMES(true, s(z0), z1) -> c10(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
IF_TIMES(false, s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
even(0') -> true
even(s(0')) -> false
even(s(s(z0))) -> even(z0)
half(0') -> 0'
half(s(s(z0))) -> s(half(z0))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> if_times(even(s(z0)), s(z0), z1)
if_times(true, s(z0), z1) -> plus(times(half(s(z0)), z1), times(half(s(z0)), z1))
if_times(false, s(z0), z1) -> plus(z1, times(z0, z1))

Types:
EVEN :: 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
HALF :: 0':s -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
PLUS :: 0':s -> 0':s -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
TIMES :: 0':s -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c9:c10:c11 -> c:c1:c2 -> c7:c8
IF_TIMES :: true:false -> 0':s -> 0':s -> c9:c10:c11
even :: 0':s -> true:false
true :: true:false
c9 :: c5:c6 -> c7:c8 -> c3:c4 -> c9:c10:c11
times :: 0':s -> 0':s -> 0':s
half :: 0':s -> 0':s
c10 :: c5:c6 -> c7:c8 -> c3:c4 -> c9:c10:c11
false :: true:false
c11 :: c5:c6 -> c7:c8 -> c9:c10:c11
plus :: 0':s -> 0':s -> 0':s
if_times :: true:false -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_12 :: c:c1:c2
hole_0':s2_12 :: 0':s
hole_c3:c43_12 :: c3:c4
hole_c5:c64_12 :: c5:c6
hole_c7:c85_12 :: c7:c8
hole_c9:c10:c116_12 :: c9:c10:c11
hole_true:false7_12 :: true:false
gen_c:c1:c28_12 :: Nat -> c:c1:c2
gen_0':s9_12 :: Nat -> 0':s
gen_c3:c410_12 :: Nat -> c3:c4
gen_c5:c611_12 :: Nat -> c5:c6


Lemmas:
EVEN(gen_0':s9_12(*(2, n13_12))) -> gen_c:c1:c28_12(n13_12), rt in Omega(1 + n13_12)


Generator Equations:
gen_c:c1:c28_12(0) <=> c
gen_c:c1:c28_12(+(x, 1)) <=> c2(gen_c:c1:c28_12(x))
gen_0':s9_12(0) <=> 0'
gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x))
gen_c3:c410_12(0) <=> c3
gen_c3:c410_12(+(x, 1)) <=> c4(gen_c3:c410_12(x))
gen_c5:c611_12(0) <=> c5
gen_c5:c611_12(+(x, 1)) <=> c6(gen_c5:c611_12(x))


The following defined symbols remain to be analysed:
HALF, PLUS, TIMES, even, times, half, plus

They will be analysed ascendingly in the following order:
HALF < TIMES
PLUS < TIMES
even < TIMES
times < TIMES
half < TIMES
even < times
half < times
plus < times

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

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
HALF(gen_0':s9_12(*(2, n453_12))) -> gen_c3:c410_12(n453_12), rt in Omega(1 + n453_12)

Induction Base:
HALF(gen_0':s9_12(*(2, 0))) ->_R^Omega(1)
c3

Induction Step:
HALF(gen_0':s9_12(*(2, +(n453_12, 1)))) ->_R^Omega(1)
c4(HALF(gen_0':s9_12(*(2, n453_12)))) ->_IH
c4(gen_c3:c410_12(c454_12))

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

(16)
Obligation:
Innermost TRS:
Rules:
EVEN(0') -> c
EVEN(s(0')) -> c1
EVEN(s(s(z0))) -> c2(EVEN(z0))
HALF(0') -> c3
HALF(s(s(z0))) -> c4(HALF(z0))
PLUS(0', z0) -> c5
PLUS(s(z0), z1) -> c6(PLUS(z0, z1))
TIMES(0', z0) -> c7
TIMES(s(z0), z1) -> c8(IF_TIMES(even(s(z0)), s(z0), z1), EVEN(s(z0)))
IF_TIMES(true, s(z0), z1) -> c9(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
IF_TIMES(true, s(z0), z1) -> c10(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
IF_TIMES(false, s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
even(0') -> true
even(s(0')) -> false
even(s(s(z0))) -> even(z0)
half(0') -> 0'
half(s(s(z0))) -> s(half(z0))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> if_times(even(s(z0)), s(z0), z1)
if_times(true, s(z0), z1) -> plus(times(half(s(z0)), z1), times(half(s(z0)), z1))
if_times(false, s(z0), z1) -> plus(z1, times(z0, z1))

Types:
EVEN :: 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
HALF :: 0':s -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
PLUS :: 0':s -> 0':s -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
TIMES :: 0':s -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c9:c10:c11 -> c:c1:c2 -> c7:c8
IF_TIMES :: true:false -> 0':s -> 0':s -> c9:c10:c11
even :: 0':s -> true:false
true :: true:false
c9 :: c5:c6 -> c7:c8 -> c3:c4 -> c9:c10:c11
times :: 0':s -> 0':s -> 0':s
half :: 0':s -> 0':s
c10 :: c5:c6 -> c7:c8 -> c3:c4 -> c9:c10:c11
false :: true:false
c11 :: c5:c6 -> c7:c8 -> c9:c10:c11
plus :: 0':s -> 0':s -> 0':s
if_times :: true:false -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_12 :: c:c1:c2
hole_0':s2_12 :: 0':s
hole_c3:c43_12 :: c3:c4
hole_c5:c64_12 :: c5:c6
hole_c7:c85_12 :: c7:c8
hole_c9:c10:c116_12 :: c9:c10:c11
hole_true:false7_12 :: true:false
gen_c:c1:c28_12 :: Nat -> c:c1:c2
gen_0':s9_12 :: Nat -> 0':s
gen_c3:c410_12 :: Nat -> c3:c4
gen_c5:c611_12 :: Nat -> c5:c6


Lemmas:
EVEN(gen_0':s9_12(*(2, n13_12))) -> gen_c:c1:c28_12(n13_12), rt in Omega(1 + n13_12)
HALF(gen_0':s9_12(*(2, n453_12))) -> gen_c3:c410_12(n453_12), rt in Omega(1 + n453_12)


Generator Equations:
gen_c:c1:c28_12(0) <=> c
gen_c:c1:c28_12(+(x, 1)) <=> c2(gen_c:c1:c28_12(x))
gen_0':s9_12(0) <=> 0'
gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x))
gen_c3:c410_12(0) <=> c3
gen_c3:c410_12(+(x, 1)) <=> c4(gen_c3:c410_12(x))
gen_c5:c611_12(0) <=> c5
gen_c5:c611_12(+(x, 1)) <=> c6(gen_c5:c611_12(x))


The following defined symbols remain to be analysed:
PLUS, TIMES, even, times, half, plus

They will be analysed ascendingly in the following order:
PLUS < TIMES
even < TIMES
times < TIMES
half < TIMES
even < times
half < times
plus < times

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
PLUS(gen_0':s9_12(n825_12), gen_0':s9_12(b)) -> gen_c5:c611_12(n825_12), rt in Omega(1 + n825_12)

Induction Base:
PLUS(gen_0':s9_12(0), gen_0':s9_12(b)) ->_R^Omega(1)
c5

Induction Step:
PLUS(gen_0':s9_12(+(n825_12, 1)), gen_0':s9_12(b)) ->_R^Omega(1)
c6(PLUS(gen_0':s9_12(n825_12), gen_0':s9_12(b))) ->_IH
c6(gen_c5:c611_12(c826_12))

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:
EVEN(0') -> c
EVEN(s(0')) -> c1
EVEN(s(s(z0))) -> c2(EVEN(z0))
HALF(0') -> c3
HALF(s(s(z0))) -> c4(HALF(z0))
PLUS(0', z0) -> c5
PLUS(s(z0), z1) -> c6(PLUS(z0, z1))
TIMES(0', z0) -> c7
TIMES(s(z0), z1) -> c8(IF_TIMES(even(s(z0)), s(z0), z1), EVEN(s(z0)))
IF_TIMES(true, s(z0), z1) -> c9(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
IF_TIMES(true, s(z0), z1) -> c10(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
IF_TIMES(false, s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
even(0') -> true
even(s(0')) -> false
even(s(s(z0))) -> even(z0)
half(0') -> 0'
half(s(s(z0))) -> s(half(z0))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> if_times(even(s(z0)), s(z0), z1)
if_times(true, s(z0), z1) -> plus(times(half(s(z0)), z1), times(half(s(z0)), z1))
if_times(false, s(z0), z1) -> plus(z1, times(z0, z1))

Types:
EVEN :: 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
HALF :: 0':s -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
PLUS :: 0':s -> 0':s -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
TIMES :: 0':s -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c9:c10:c11 -> c:c1:c2 -> c7:c8
IF_TIMES :: true:false -> 0':s -> 0':s -> c9:c10:c11
even :: 0':s -> true:false
true :: true:false
c9 :: c5:c6 -> c7:c8 -> c3:c4 -> c9:c10:c11
times :: 0':s -> 0':s -> 0':s
half :: 0':s -> 0':s
c10 :: c5:c6 -> c7:c8 -> c3:c4 -> c9:c10:c11
false :: true:false
c11 :: c5:c6 -> c7:c8 -> c9:c10:c11
plus :: 0':s -> 0':s -> 0':s
if_times :: true:false -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_12 :: c:c1:c2
hole_0':s2_12 :: 0':s
hole_c3:c43_12 :: c3:c4
hole_c5:c64_12 :: c5:c6
hole_c7:c85_12 :: c7:c8
hole_c9:c10:c116_12 :: c9:c10:c11
hole_true:false7_12 :: true:false
gen_c:c1:c28_12 :: Nat -> c:c1:c2
gen_0':s9_12 :: Nat -> 0':s
gen_c3:c410_12 :: Nat -> c3:c4
gen_c5:c611_12 :: Nat -> c5:c6


Lemmas:
EVEN(gen_0':s9_12(*(2, n13_12))) -> gen_c:c1:c28_12(n13_12), rt in Omega(1 + n13_12)
HALF(gen_0':s9_12(*(2, n453_12))) -> gen_c3:c410_12(n453_12), rt in Omega(1 + n453_12)
PLUS(gen_0':s9_12(n825_12), gen_0':s9_12(b)) -> gen_c5:c611_12(n825_12), rt in Omega(1 + n825_12)


Generator Equations:
gen_c:c1:c28_12(0) <=> c
gen_c:c1:c28_12(+(x, 1)) <=> c2(gen_c:c1:c28_12(x))
gen_0':s9_12(0) <=> 0'
gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x))
gen_c3:c410_12(0) <=> c3
gen_c3:c410_12(+(x, 1)) <=> c4(gen_c3:c410_12(x))
gen_c5:c611_12(0) <=> c5
gen_c5:c611_12(+(x, 1)) <=> c6(gen_c5:c611_12(x))


The following defined symbols remain to be analysed:
even, TIMES, times, half, plus

They will be analysed ascendingly in the following order:
even < TIMES
times < TIMES
half < TIMES
even < times
half < times
plus < times

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
even(gen_0':s9_12(*(2, n1537_12))) -> true, rt in Omega(0)

Induction Base:
even(gen_0':s9_12(*(2, 0))) ->_R^Omega(0)
true

Induction Step:
even(gen_0':s9_12(*(2, +(n1537_12, 1)))) ->_R^Omega(0)
even(gen_0':s9_12(*(2, n1537_12))) ->_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:
EVEN(0') -> c
EVEN(s(0')) -> c1
EVEN(s(s(z0))) -> c2(EVEN(z0))
HALF(0') -> c3
HALF(s(s(z0))) -> c4(HALF(z0))
PLUS(0', z0) -> c5
PLUS(s(z0), z1) -> c6(PLUS(z0, z1))
TIMES(0', z0) -> c7
TIMES(s(z0), z1) -> c8(IF_TIMES(even(s(z0)), s(z0), z1), EVEN(s(z0)))
IF_TIMES(true, s(z0), z1) -> c9(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
IF_TIMES(true, s(z0), z1) -> c10(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
IF_TIMES(false, s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
even(0') -> true
even(s(0')) -> false
even(s(s(z0))) -> even(z0)
half(0') -> 0'
half(s(s(z0))) -> s(half(z0))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> if_times(even(s(z0)), s(z0), z1)
if_times(true, s(z0), z1) -> plus(times(half(s(z0)), z1), times(half(s(z0)), z1))
if_times(false, s(z0), z1) -> plus(z1, times(z0, z1))

Types:
EVEN :: 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
HALF :: 0':s -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
PLUS :: 0':s -> 0':s -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
TIMES :: 0':s -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c9:c10:c11 -> c:c1:c2 -> c7:c8
IF_TIMES :: true:false -> 0':s -> 0':s -> c9:c10:c11
even :: 0':s -> true:false
true :: true:false
c9 :: c5:c6 -> c7:c8 -> c3:c4 -> c9:c10:c11
times :: 0':s -> 0':s -> 0':s
half :: 0':s -> 0':s
c10 :: c5:c6 -> c7:c8 -> c3:c4 -> c9:c10:c11
false :: true:false
c11 :: c5:c6 -> c7:c8 -> c9:c10:c11
plus :: 0':s -> 0':s -> 0':s
if_times :: true:false -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_12 :: c:c1:c2
hole_0':s2_12 :: 0':s
hole_c3:c43_12 :: c3:c4
hole_c5:c64_12 :: c5:c6
hole_c7:c85_12 :: c7:c8
hole_c9:c10:c116_12 :: c9:c10:c11
hole_true:false7_12 :: true:false
gen_c:c1:c28_12 :: Nat -> c:c1:c2
gen_0':s9_12 :: Nat -> 0':s
gen_c3:c410_12 :: Nat -> c3:c4
gen_c5:c611_12 :: Nat -> c5:c6


Lemmas:
EVEN(gen_0':s9_12(*(2, n13_12))) -> gen_c:c1:c28_12(n13_12), rt in Omega(1 + n13_12)
HALF(gen_0':s9_12(*(2, n453_12))) -> gen_c3:c410_12(n453_12), rt in Omega(1 + n453_12)
PLUS(gen_0':s9_12(n825_12), gen_0':s9_12(b)) -> gen_c5:c611_12(n825_12), rt in Omega(1 + n825_12)
even(gen_0':s9_12(*(2, n1537_12))) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c28_12(0) <=> c
gen_c:c1:c28_12(+(x, 1)) <=> c2(gen_c:c1:c28_12(x))
gen_0':s9_12(0) <=> 0'
gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x))
gen_c3:c410_12(0) <=> c3
gen_c3:c410_12(+(x, 1)) <=> c4(gen_c3:c410_12(x))
gen_c5:c611_12(0) <=> c5
gen_c5:c611_12(+(x, 1)) <=> c6(gen_c5:c611_12(x))


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

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

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
half(gen_0':s9_12(*(2, n1756_12))) -> gen_0':s9_12(n1756_12), rt in Omega(0)

Induction Base:
half(gen_0':s9_12(*(2, 0))) ->_R^Omega(0)
0'

Induction Step:
half(gen_0':s9_12(*(2, +(n1756_12, 1)))) ->_R^Omega(0)
s(half(gen_0':s9_12(*(2, n1756_12)))) ->_IH
s(gen_0':s9_12(c1757_12))

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:
EVEN(0') -> c
EVEN(s(0')) -> c1
EVEN(s(s(z0))) -> c2(EVEN(z0))
HALF(0') -> c3
HALF(s(s(z0))) -> c4(HALF(z0))
PLUS(0', z0) -> c5
PLUS(s(z0), z1) -> c6(PLUS(z0, z1))
TIMES(0', z0) -> c7
TIMES(s(z0), z1) -> c8(IF_TIMES(even(s(z0)), s(z0), z1), EVEN(s(z0)))
IF_TIMES(true, s(z0), z1) -> c9(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
IF_TIMES(true, s(z0), z1) -> c10(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
IF_TIMES(false, s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
even(0') -> true
even(s(0')) -> false
even(s(s(z0))) -> even(z0)
half(0') -> 0'
half(s(s(z0))) -> s(half(z0))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> if_times(even(s(z0)), s(z0), z1)
if_times(true, s(z0), z1) -> plus(times(half(s(z0)), z1), times(half(s(z0)), z1))
if_times(false, s(z0), z1) -> plus(z1, times(z0, z1))

Types:
EVEN :: 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
HALF :: 0':s -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
PLUS :: 0':s -> 0':s -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
TIMES :: 0':s -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c9:c10:c11 -> c:c1:c2 -> c7:c8
IF_TIMES :: true:false -> 0':s -> 0':s -> c9:c10:c11
even :: 0':s -> true:false
true :: true:false
c9 :: c5:c6 -> c7:c8 -> c3:c4 -> c9:c10:c11
times :: 0':s -> 0':s -> 0':s
half :: 0':s -> 0':s
c10 :: c5:c6 -> c7:c8 -> c3:c4 -> c9:c10:c11
false :: true:false
c11 :: c5:c6 -> c7:c8 -> c9:c10:c11
plus :: 0':s -> 0':s -> 0':s
if_times :: true:false -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_12 :: c:c1:c2
hole_0':s2_12 :: 0':s
hole_c3:c43_12 :: c3:c4
hole_c5:c64_12 :: c5:c6
hole_c7:c85_12 :: c7:c8
hole_c9:c10:c116_12 :: c9:c10:c11
hole_true:false7_12 :: true:false
gen_c:c1:c28_12 :: Nat -> c:c1:c2
gen_0':s9_12 :: Nat -> 0':s
gen_c3:c410_12 :: Nat -> c3:c4
gen_c5:c611_12 :: Nat -> c5:c6


Lemmas:
EVEN(gen_0':s9_12(*(2, n13_12))) -> gen_c:c1:c28_12(n13_12), rt in Omega(1 + n13_12)
HALF(gen_0':s9_12(*(2, n453_12))) -> gen_c3:c410_12(n453_12), rt in Omega(1 + n453_12)
PLUS(gen_0':s9_12(n825_12), gen_0':s9_12(b)) -> gen_c5:c611_12(n825_12), rt in Omega(1 + n825_12)
even(gen_0':s9_12(*(2, n1537_12))) -> true, rt in Omega(0)
half(gen_0':s9_12(*(2, n1756_12))) -> gen_0':s9_12(n1756_12), rt in Omega(0)


Generator Equations:
gen_c:c1:c28_12(0) <=> c
gen_c:c1:c28_12(+(x, 1)) <=> c2(gen_c:c1:c28_12(x))
gen_0':s9_12(0) <=> 0'
gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x))
gen_c3:c410_12(0) <=> c3
gen_c3:c410_12(+(x, 1)) <=> c4(gen_c3:c410_12(x))
gen_c5:c611_12(0) <=> c5
gen_c5:c611_12(+(x, 1)) <=> c6(gen_c5:c611_12(x))


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

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

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

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

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

Induction Step:
plus(gen_0':s9_12(+(n2112_12, 1)), gen_0':s9_12(b)) ->_R^Omega(0)
s(plus(gen_0':s9_12(n2112_12), gen_0':s9_12(b))) ->_IH
s(gen_0':s9_12(+(b, c2113_12)))

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:
EVEN(0') -> c
EVEN(s(0')) -> c1
EVEN(s(s(z0))) -> c2(EVEN(z0))
HALF(0') -> c3
HALF(s(s(z0))) -> c4(HALF(z0))
PLUS(0', z0) -> c5
PLUS(s(z0), z1) -> c6(PLUS(z0, z1))
TIMES(0', z0) -> c7
TIMES(s(z0), z1) -> c8(IF_TIMES(even(s(z0)), s(z0), z1), EVEN(s(z0)))
IF_TIMES(true, s(z0), z1) -> c9(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
IF_TIMES(true, s(z0), z1) -> c10(PLUS(times(half(s(z0)), z1), times(half(s(z0)), z1)), TIMES(half(s(z0)), z1), HALF(s(z0)))
IF_TIMES(false, s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
even(0') -> true
even(s(0')) -> false
even(s(s(z0))) -> even(z0)
half(0') -> 0'
half(s(s(z0))) -> s(half(z0))
plus(0', z0) -> z0
plus(s(z0), z1) -> s(plus(z0, z1))
times(0', z0) -> 0'
times(s(z0), z1) -> if_times(even(s(z0)), s(z0), z1)
if_times(true, s(z0), z1) -> plus(times(half(s(z0)), z1), times(half(s(z0)), z1))
if_times(false, s(z0), z1) -> plus(z1, times(z0, z1))

Types:
EVEN :: 0':s -> c:c1:c2
0' :: 0':s
c :: c:c1:c2
s :: 0':s -> 0':s
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
HALF :: 0':s -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
PLUS :: 0':s -> 0':s -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
TIMES :: 0':s -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c9:c10:c11 -> c:c1:c2 -> c7:c8
IF_TIMES :: true:false -> 0':s -> 0':s -> c9:c10:c11
even :: 0':s -> true:false
true :: true:false
c9 :: c5:c6 -> c7:c8 -> c3:c4 -> c9:c10:c11
times :: 0':s -> 0':s -> 0':s
half :: 0':s -> 0':s
c10 :: c5:c6 -> c7:c8 -> c3:c4 -> c9:c10:c11
false :: true:false
c11 :: c5:c6 -> c7:c8 -> c9:c10:c11
plus :: 0':s -> 0':s -> 0':s
if_times :: true:false -> 0':s -> 0':s -> 0':s
hole_c:c1:c21_12 :: c:c1:c2
hole_0':s2_12 :: 0':s
hole_c3:c43_12 :: c3:c4
hole_c5:c64_12 :: c5:c6
hole_c7:c85_12 :: c7:c8
hole_c9:c10:c116_12 :: c9:c10:c11
hole_true:false7_12 :: true:false
gen_c:c1:c28_12 :: Nat -> c:c1:c2
gen_0':s9_12 :: Nat -> 0':s
gen_c3:c410_12 :: Nat -> c3:c4
gen_c5:c611_12 :: Nat -> c5:c6


Lemmas:
EVEN(gen_0':s9_12(*(2, n13_12))) -> gen_c:c1:c28_12(n13_12), rt in Omega(1 + n13_12)
HALF(gen_0':s9_12(*(2, n453_12))) -> gen_c3:c410_12(n453_12), rt in Omega(1 + n453_12)
PLUS(gen_0':s9_12(n825_12), gen_0':s9_12(b)) -> gen_c5:c611_12(n825_12), rt in Omega(1 + n825_12)
even(gen_0':s9_12(*(2, n1537_12))) -> true, rt in Omega(0)
half(gen_0':s9_12(*(2, n1756_12))) -> gen_0':s9_12(n1756_12), rt in Omega(0)
plus(gen_0':s9_12(n2112_12), gen_0':s9_12(b)) -> gen_0':s9_12(+(n2112_12, b)), rt in Omega(0)


Generator Equations:
gen_c:c1:c28_12(0) <=> c
gen_c:c1:c28_12(+(x, 1)) <=> c2(gen_c:c1:c28_12(x))
gen_0':s9_12(0) <=> 0'
gen_0':s9_12(+(x, 1)) <=> s(gen_0':s9_12(x))
gen_c3:c410_12(0) <=> c3
gen_c3:c410_12(+(x, 1)) <=> c4(gen_c3:c410_12(x))
gen_c5:c611_12(0) <=> c5
gen_c5:c611_12(+(x, 1)) <=> c6(gen_c5:c611_12(x))


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

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