WORST_CASE(Omega(n^1),?)
proof of /export/starexec/sandbox/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), 600 ms]
(2) CpxRelTRS
(3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) SlicingProof [LOWER BOUND(ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 10 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 327 ms]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 2150 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 93 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 79 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 39 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 57 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 489 ms]
        (28) BOUNDS(1, INF)


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

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

   -'(z0, 0) -> c
   -'(s(z0), s(z1)) -> c1(-'(z0, z1))
   *'(z0, 0) -> c2
   *'(z0, s(z1)) -> c3(*'(z0, z1))
   IF(true, z0, z1) -> c4
   IF(false, z0, z1) -> c5
   IF(true, z0, z1) -> c6
   IF(false, z0, z1) -> c7
   ODD(0) -> c8
   ODD(s(0)) -> c9
   ODD(s(s(z0))) -> c10(ODD(z0))
   HALF(0) -> c11
   HALF(s(0)) -> c12
   HALF(s(s(z0))) -> c13(HALF(z0))
   POW(z0, z1) -> c14(F(z0, z1, s(0)))
   F(z0, 0, z1) -> c15
   F(z0, s(z1), z2) -> c16(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), ODD(s(z1)))
   F(z0, s(z1), z2) -> c17(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), F(z0, z1, *(z0, z2)), *'(z0, z2))
   F(z0, s(z1), z2) -> c18(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), F(*(z0, z0), half(s(z1)), z2), *'(z0, z0))
   F(z0, s(z1), z2) -> c19(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), F(*(z0, z0), half(s(z1)), z2), HALF(s(z1)))

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

   -(z0, 0) -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   *(z0, 0) -> 0
   *(z0, s(z1)) -> +(*(z0, z1), z0)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   if(true, z0, z1) -> true
   if(false, z0, z1) -> false
   odd(0) -> false
   odd(s(0)) -> true
   odd(s(s(z0))) -> odd(z0)
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   pow(z0, z1) -> f(z0, z1, s(0))
   f(z0, 0, z1) -> z1
   f(z0, s(z1), z2) -> if(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2))

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:

   -'(z0, 0) -> c
   -'(s(z0), s(z1)) -> c1(-'(z0, z1))
   *'(z0, 0) -> c2
   *'(z0, s(z1)) -> c3(*'(z0, z1))
   IF(true, z0, z1) -> c4
   IF(false, z0, z1) -> c5
   IF(true, z0, z1) -> c6
   IF(false, z0, z1) -> c7
   ODD(0) -> c8
   ODD(s(0)) -> c9
   ODD(s(s(z0))) -> c10(ODD(z0))
   HALF(0) -> c11
   HALF(s(0)) -> c12
   HALF(s(s(z0))) -> c13(HALF(z0))
   POW(z0, z1) -> c14(F(z0, z1, s(0)))
   F(z0, 0, z1) -> c15
   F(z0, s(z1), z2) -> c16(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), ODD(s(z1)))
   F(z0, s(z1), z2) -> c17(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), F(z0, z1, *(z0, z2)), *'(z0, z2))
   F(z0, s(z1), z2) -> c18(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), F(*(z0, z0), half(s(z1)), z2), *'(z0, z0))
   F(z0, s(z1), z2) -> c19(IF(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2)), F(*(z0, z0), half(s(z1)), z2), HALF(s(z1)))

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

   -(z0, 0) -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   *(z0, 0) -> 0
   *(z0, s(z1)) -> +(*(z0, z1), z0)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   if(true, z0, z1) -> true
   if(false, z0, z1) -> false
   odd(0) -> false
   odd(s(0)) -> true
   odd(s(s(z0))) -> odd(z0)
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(z0))) -> s(half(z0))
   pow(z0, z1) -> f(z0, z1, s(0))
   f(z0, 0, z1) -> z1
   f(z0, s(z1), z2) -> if(odd(s(z1)), f(z0, z1, *(z0, z2)), f(*(z0, z0), half(s(z1)), z2))

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:

   -'(z0, 0') -> c
   -'(s(z0), s(z1)) -> c1(-'(z0, z1))
   *'(z0, 0') -> c2
   *'(z0, s(z1)) -> c3(*'(z0, z1))
   IF(true, z0, z1) -> c4
   IF(false, z0, z1) -> c5
   IF(true, z0, z1) -> c6
   IF(false, z0, z1) -> c7
   ODD(0') -> c8
   ODD(s(0')) -> c9
   ODD(s(s(z0))) -> c10(ODD(z0))
   HALF(0') -> c11
   HALF(s(0')) -> c12
   HALF(s(s(z0))) -> c13(HALF(z0))
   POW(z0, z1) -> c14(F(z0, z1, s(0')))
   F(z0, 0', z1) -> c15
   F(z0, s(z1), z2) -> c16(IF(odd(s(z1)), f(z0, z1, *'(z0, z2)), f(*'(z0, z0), half(s(z1)), z2)), ODD(s(z1)))
   F(z0, s(z1), z2) -> c17(IF(odd(s(z1)), f(z0, z1, *'(z0, z2)), f(*'(z0, z0), half(s(z1)), z2)), F(z0, z1, *'(z0, z2)), *'(z0, z2))
   F(z0, s(z1), z2) -> c18(IF(odd(s(z1)), f(z0, z1, *'(z0, z2)), f(*'(z0, z0), half(s(z1)), z2)), F(*'(z0, z0), half(s(z1)), z2), *'(z0, z0))
   F(z0, s(z1), z2) -> c19(IF(odd(s(z1)), f(z0, z1, *'(z0, z2)), f(*'(z0, z0), half(s(z1)), z2)), F(*'(z0, z0), half(s(z1)), z2), HALF(s(z1)))

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

   -(z0, 0') -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   *'(z0, 0') -> 0'
   *'(z0, s(z1)) -> +'(*'(z0, z1), z0)
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   if(true, z0, z1) -> true
   if(false, z0, z1) -> false
   odd(0') -> false
   odd(s(0')) -> true
   odd(s(s(z0))) -> odd(z0)
   half(0') -> 0'
   half(s(0')) -> 0'
   half(s(s(z0))) -> s(half(z0))
   pow(z0, z1) -> f(z0, z1, s(0'))
   f(z0, 0', z1) -> z1
   f(z0, s(z1), z2) -> if(odd(s(z1)), f(z0, z1, *'(z0, z2)), f(*'(z0, z0), half(s(z1)), z2))

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

(5) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
*'/0
+'/1

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

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


The TRS R consists of the following rules:

   -'(z0, 0') -> c
   -'(s(z0), s(z1)) -> c1(-'(z0, z1))
   *'(0') -> c2
   *'(s(z1)) -> c3(*'(z1))
   IF(true, z0, z1) -> c4
   IF(false, z0, z1) -> c5
   IF(true, z0, z1) -> c6
   IF(false, z0, z1) -> c7
   ODD(0') -> c8
   ODD(s(0')) -> c9
   ODD(s(s(z0))) -> c10(ODD(z0))
   HALF(0') -> c11
   HALF(s(0')) -> c12
   HALF(s(s(z0))) -> c13(HALF(z0))
   POW(z0, z1) -> c14(F(z0, z1, s(0')))
   F(z0, 0', z1) -> c15
   F(z0, s(z1), z2) -> c16(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), ODD(s(z1)))
   F(z0, s(z1), z2) -> c17(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(z0, z1, *'(z2)), *'(z2))
   F(z0, s(z1), z2) -> c18(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(*'(z0), half(s(z1)), z2), *'(z0))
   F(z0, s(z1), z2) -> c19(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(*'(z0), half(s(z1)), z2), HALF(s(z1)))

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

   -(z0, 0') -> z0
   -(s(z0), s(z1)) -> -(z0, z1)
   *'(0') -> 0'
   *'(s(z1)) -> +'(*'(z1))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   if(true, z0, z1) -> true
   if(false, z0, z1) -> false
   odd(0') -> false
   odd(s(0')) -> true
   odd(s(s(z0))) -> odd(z0)
   half(0') -> 0'
   half(s(0')) -> 0'
   half(s(s(z0))) -> s(half(z0))
   pow(z0, z1) -> f(z0, z1, s(0'))
   f(z0, 0', z1) -> z1
   f(z0, s(z1), z2) -> if(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
-'(z0, 0') -> c
-'(s(z0), s(z1)) -> c1(-'(z0, z1))
*'(0') -> c2
*'(s(z1)) -> c3(*'(z1))
IF(true, z0, z1) -> c4
IF(false, z0, z1) -> c5
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
ODD(0') -> c8
ODD(s(0')) -> c9
ODD(s(s(z0))) -> c10(ODD(z0))
HALF(0') -> c11
HALF(s(0')) -> c12
HALF(s(s(z0))) -> c13(HALF(z0))
POW(z0, z1) -> c14(F(z0, z1, s(0')))
F(z0, 0', z1) -> c15
F(z0, s(z1), z2) -> c16(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), ODD(s(z1)))
F(z0, s(z1), z2) -> c17(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(z0, z1, *'(z2)), *'(z2))
F(z0, s(z1), z2) -> c18(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(*'(z0), half(s(z1)), z2), *'(z0))
F(z0, s(z1), z2) -> c19(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(*'(z0), half(s(z1)), z2), HALF(s(z1)))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
*'(0') -> 0'
*'(s(z1)) -> +'(*'(z1))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
if(true, z0, z1) -> true
if(false, z0, z1) -> false
odd(0') -> false
odd(s(0')) -> true
odd(s(s(z0))) -> odd(z0)
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
pow(z0, z1) -> f(z0, z1, s(0'))
f(z0, 0', z1) -> z1
f(z0, s(z1), z2) -> if(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2))

Types:
-' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c:c1
0' :: 0':s:c2:c3:true:false:+'
c :: c:c1
s :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c1 :: c:c1 -> c:c1
*' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c2 :: 0':s:c2:c3:true:false:+'
c3 :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
IF :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c4:c5:c6:c7
true :: 0':s:c2:c3:true:false:+'
c4 :: c4:c5:c6:c7
false :: 0':s:c2:c3:true:false:+'
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
ODD :: 0':s:c2:c3:true:false:+' -> c8:c9:c10
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
HALF :: 0':s:c2:c3:true:false:+' -> c11:c12:c13
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
POW :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c14
c14 :: c15:c16:c17:c18:c19 -> c14
F :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c15 :: c15:c16:c17:c18:c19
c16 :: c4:c5:c6:c7 -> c8:c9:c10 -> c15:c16:c17:c18:c19
odd :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
f :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
half :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c17 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c18 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c19 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> c11:c12:c13 -> c15:c16:c17:c18:c19
- :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
+' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
if :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
pow :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
hole_c:c11_20 :: c:c1
hole_0':s:c2:c3:true:false:+'2_20 :: 0':s:c2:c3:true:false:+'
hole_c4:c5:c6:c73_20 :: c4:c5:c6:c7
hole_c8:c9:c104_20 :: c8:c9:c10
hole_c11:c12:c135_20 :: c11:c12:c13
hole_c146_20 :: c14
hole_c15:c16:c17:c18:c197_20 :: c15:c16:c17:c18:c19
gen_c:c18_20 :: Nat -> c:c1
gen_0':s:c2:c3:true:false:+'9_20 :: Nat -> 0':s:c2:c3:true:false:+'
gen_c8:c9:c1010_20 :: Nat -> c8:c9:c10
gen_c11:c12:c1311_20 :: Nat -> c11:c12:c13
gen_c15:c16:c17:c18:c1912_20 :: Nat -> c15:c16:c17:c18:c19

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
-', *', ODD, HALF, F, odd, f, half, -

They will be analysed ascendingly in the following order:
*' < F
*' < f
ODD < F
HALF < F
odd < F
f < F
half < F
odd < f
half < f

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

(10)
Obligation:
Innermost TRS:
Rules:
-'(z0, 0') -> c
-'(s(z0), s(z1)) -> c1(-'(z0, z1))
*'(0') -> c2
*'(s(z1)) -> c3(*'(z1))
IF(true, z0, z1) -> c4
IF(false, z0, z1) -> c5
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
ODD(0') -> c8
ODD(s(0')) -> c9
ODD(s(s(z0))) -> c10(ODD(z0))
HALF(0') -> c11
HALF(s(0')) -> c12
HALF(s(s(z0))) -> c13(HALF(z0))
POW(z0, z1) -> c14(F(z0, z1, s(0')))
F(z0, 0', z1) -> c15
F(z0, s(z1), z2) -> c16(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), ODD(s(z1)))
F(z0, s(z1), z2) -> c17(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(z0, z1, *'(z2)), *'(z2))
F(z0, s(z1), z2) -> c18(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(*'(z0), half(s(z1)), z2), *'(z0))
F(z0, s(z1), z2) -> c19(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(*'(z0), half(s(z1)), z2), HALF(s(z1)))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
*'(0') -> 0'
*'(s(z1)) -> +'(*'(z1))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
if(true, z0, z1) -> true
if(false, z0, z1) -> false
odd(0') -> false
odd(s(0')) -> true
odd(s(s(z0))) -> odd(z0)
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
pow(z0, z1) -> f(z0, z1, s(0'))
f(z0, 0', z1) -> z1
f(z0, s(z1), z2) -> if(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2))

Types:
-' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c:c1
0' :: 0':s:c2:c3:true:false:+'
c :: c:c1
s :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c1 :: c:c1 -> c:c1
*' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c2 :: 0':s:c2:c3:true:false:+'
c3 :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
IF :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c4:c5:c6:c7
true :: 0':s:c2:c3:true:false:+'
c4 :: c4:c5:c6:c7
false :: 0':s:c2:c3:true:false:+'
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
ODD :: 0':s:c2:c3:true:false:+' -> c8:c9:c10
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
HALF :: 0':s:c2:c3:true:false:+' -> c11:c12:c13
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
POW :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c14
c14 :: c15:c16:c17:c18:c19 -> c14
F :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c15 :: c15:c16:c17:c18:c19
c16 :: c4:c5:c6:c7 -> c8:c9:c10 -> c15:c16:c17:c18:c19
odd :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
f :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
half :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c17 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c18 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c19 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> c11:c12:c13 -> c15:c16:c17:c18:c19
- :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
+' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
if :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
pow :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
hole_c:c11_20 :: c:c1
hole_0':s:c2:c3:true:false:+'2_20 :: 0':s:c2:c3:true:false:+'
hole_c4:c5:c6:c73_20 :: c4:c5:c6:c7
hole_c8:c9:c104_20 :: c8:c9:c10
hole_c11:c12:c135_20 :: c11:c12:c13
hole_c146_20 :: c14
hole_c15:c16:c17:c18:c197_20 :: c15:c16:c17:c18:c19
gen_c:c18_20 :: Nat -> c:c1
gen_0':s:c2:c3:true:false:+'9_20 :: Nat -> 0':s:c2:c3:true:false:+'
gen_c8:c9:c1010_20 :: Nat -> c8:c9:c10
gen_c11:c12:c1311_20 :: Nat -> c11:c12:c13
gen_c15:c16:c17:c18:c1912_20 :: Nat -> c15:c16:c17:c18:c19


Generator Equations:
gen_c:c18_20(0) <=> c
gen_c:c18_20(+(x, 1)) <=> c1(gen_c:c18_20(x))
gen_0':s:c2:c3:true:false:+'9_20(0) <=> 0'
gen_0':s:c2:c3:true:false:+'9_20(+(x, 1)) <=> s(gen_0':s:c2:c3:true:false:+'9_20(x))
gen_c8:c9:c1010_20(0) <=> c8
gen_c8:c9:c1010_20(+(x, 1)) <=> c10(gen_c8:c9:c1010_20(x))
gen_c11:c12:c1311_20(0) <=> c11
gen_c11:c12:c1311_20(+(x, 1)) <=> c13(gen_c11:c12:c1311_20(x))
gen_c15:c16:c17:c18:c1912_20(0) <=> c15
gen_c15:c16:c17:c18:c1912_20(+(x, 1)) <=> c17(c4, gen_c15:c16:c17:c18:c1912_20(x), 0')


The following defined symbols remain to be analysed:
-', *', ODD, HALF, F, odd, f, half, -

They will be analysed ascendingly in the following order:
*' < F
*' < f
ODD < F
HALF < F
odd < F
f < F
half < F
odd < f
half < f

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
-'(gen_0':s:c2:c3:true:false:+'9_20(n14_20), gen_0':s:c2:c3:true:false:+'9_20(n14_20)) -> gen_c:c18_20(n14_20), rt in Omega(1 + n14_20)

Induction Base:
-'(gen_0':s:c2:c3:true:false:+'9_20(0), gen_0':s:c2:c3:true:false:+'9_20(0)) ->_R^Omega(1)
c

Induction Step:
-'(gen_0':s:c2:c3:true:false:+'9_20(+(n14_20, 1)), gen_0':s:c2:c3:true:false:+'9_20(+(n14_20, 1))) ->_R^Omega(1)
c1(-'(gen_0':s:c2:c3:true:false:+'9_20(n14_20), gen_0':s:c2:c3:true:false:+'9_20(n14_20))) ->_IH
c1(gen_c:c18_20(c15_20))

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:
-'(z0, 0') -> c
-'(s(z0), s(z1)) -> c1(-'(z0, z1))
*'(0') -> c2
*'(s(z1)) -> c3(*'(z1))
IF(true, z0, z1) -> c4
IF(false, z0, z1) -> c5
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
ODD(0') -> c8
ODD(s(0')) -> c9
ODD(s(s(z0))) -> c10(ODD(z0))
HALF(0') -> c11
HALF(s(0')) -> c12
HALF(s(s(z0))) -> c13(HALF(z0))
POW(z0, z1) -> c14(F(z0, z1, s(0')))
F(z0, 0', z1) -> c15
F(z0, s(z1), z2) -> c16(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), ODD(s(z1)))
F(z0, s(z1), z2) -> c17(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(z0, z1, *'(z2)), *'(z2))
F(z0, s(z1), z2) -> c18(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(*'(z0), half(s(z1)), z2), *'(z0))
F(z0, s(z1), z2) -> c19(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(*'(z0), half(s(z1)), z2), HALF(s(z1)))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
*'(0') -> 0'
*'(s(z1)) -> +'(*'(z1))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
if(true, z0, z1) -> true
if(false, z0, z1) -> false
odd(0') -> false
odd(s(0')) -> true
odd(s(s(z0))) -> odd(z0)
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
pow(z0, z1) -> f(z0, z1, s(0'))
f(z0, 0', z1) -> z1
f(z0, s(z1), z2) -> if(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2))

Types:
-' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c:c1
0' :: 0':s:c2:c3:true:false:+'
c :: c:c1
s :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c1 :: c:c1 -> c:c1
*' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c2 :: 0':s:c2:c3:true:false:+'
c3 :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
IF :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c4:c5:c6:c7
true :: 0':s:c2:c3:true:false:+'
c4 :: c4:c5:c6:c7
false :: 0':s:c2:c3:true:false:+'
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
ODD :: 0':s:c2:c3:true:false:+' -> c8:c9:c10
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
HALF :: 0':s:c2:c3:true:false:+' -> c11:c12:c13
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
POW :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c14
c14 :: c15:c16:c17:c18:c19 -> c14
F :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c15 :: c15:c16:c17:c18:c19
c16 :: c4:c5:c6:c7 -> c8:c9:c10 -> c15:c16:c17:c18:c19
odd :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
f :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
half :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c17 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c18 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c19 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> c11:c12:c13 -> c15:c16:c17:c18:c19
- :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
+' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
if :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
pow :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
hole_c:c11_20 :: c:c1
hole_0':s:c2:c3:true:false:+'2_20 :: 0':s:c2:c3:true:false:+'
hole_c4:c5:c6:c73_20 :: c4:c5:c6:c7
hole_c8:c9:c104_20 :: c8:c9:c10
hole_c11:c12:c135_20 :: c11:c12:c13
hole_c146_20 :: c14
hole_c15:c16:c17:c18:c197_20 :: c15:c16:c17:c18:c19
gen_c:c18_20 :: Nat -> c:c1
gen_0':s:c2:c3:true:false:+'9_20 :: Nat -> 0':s:c2:c3:true:false:+'
gen_c8:c9:c1010_20 :: Nat -> c8:c9:c10
gen_c11:c12:c1311_20 :: Nat -> c11:c12:c13
gen_c15:c16:c17:c18:c1912_20 :: Nat -> c15:c16:c17:c18:c19


Generator Equations:
gen_c:c18_20(0) <=> c
gen_c:c18_20(+(x, 1)) <=> c1(gen_c:c18_20(x))
gen_0':s:c2:c3:true:false:+'9_20(0) <=> 0'
gen_0':s:c2:c3:true:false:+'9_20(+(x, 1)) <=> s(gen_0':s:c2:c3:true:false:+'9_20(x))
gen_c8:c9:c1010_20(0) <=> c8
gen_c8:c9:c1010_20(+(x, 1)) <=> c10(gen_c8:c9:c1010_20(x))
gen_c11:c12:c1311_20(0) <=> c11
gen_c11:c12:c1311_20(+(x, 1)) <=> c13(gen_c11:c12:c1311_20(x))
gen_c15:c16:c17:c18:c1912_20(0) <=> c15
gen_c15:c16:c17:c18:c1912_20(+(x, 1)) <=> c17(c4, gen_c15:c16:c17:c18:c1912_20(x), 0')


The following defined symbols remain to be analysed:
-', *', ODD, HALF, F, odd, f, half, -

They will be analysed ascendingly in the following order:
*' < F
*' < f
ODD < F
HALF < F
odd < F
f < F
half < F
odd < f
half < f

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
-'(z0, 0') -> c
-'(s(z0), s(z1)) -> c1(-'(z0, z1))
*'(0') -> c2
*'(s(z1)) -> c3(*'(z1))
IF(true, z0, z1) -> c4
IF(false, z0, z1) -> c5
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
ODD(0') -> c8
ODD(s(0')) -> c9
ODD(s(s(z0))) -> c10(ODD(z0))
HALF(0') -> c11
HALF(s(0')) -> c12
HALF(s(s(z0))) -> c13(HALF(z0))
POW(z0, z1) -> c14(F(z0, z1, s(0')))
F(z0, 0', z1) -> c15
F(z0, s(z1), z2) -> c16(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), ODD(s(z1)))
F(z0, s(z1), z2) -> c17(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(z0, z1, *'(z2)), *'(z2))
F(z0, s(z1), z2) -> c18(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(*'(z0), half(s(z1)), z2), *'(z0))
F(z0, s(z1), z2) -> c19(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(*'(z0), half(s(z1)), z2), HALF(s(z1)))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
*'(0') -> 0'
*'(s(z1)) -> +'(*'(z1))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
if(true, z0, z1) -> true
if(false, z0, z1) -> false
odd(0') -> false
odd(s(0')) -> true
odd(s(s(z0))) -> odd(z0)
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
pow(z0, z1) -> f(z0, z1, s(0'))
f(z0, 0', z1) -> z1
f(z0, s(z1), z2) -> if(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2))

Types:
-' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c:c1
0' :: 0':s:c2:c3:true:false:+'
c :: c:c1
s :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c1 :: c:c1 -> c:c1
*' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c2 :: 0':s:c2:c3:true:false:+'
c3 :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
IF :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c4:c5:c6:c7
true :: 0':s:c2:c3:true:false:+'
c4 :: c4:c5:c6:c7
false :: 0':s:c2:c3:true:false:+'
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
ODD :: 0':s:c2:c3:true:false:+' -> c8:c9:c10
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
HALF :: 0':s:c2:c3:true:false:+' -> c11:c12:c13
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
POW :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c14
c14 :: c15:c16:c17:c18:c19 -> c14
F :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c15 :: c15:c16:c17:c18:c19
c16 :: c4:c5:c6:c7 -> c8:c9:c10 -> c15:c16:c17:c18:c19
odd :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
f :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
half :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c17 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c18 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c19 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> c11:c12:c13 -> c15:c16:c17:c18:c19
- :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
+' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
if :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
pow :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
hole_c:c11_20 :: c:c1
hole_0':s:c2:c3:true:false:+'2_20 :: 0':s:c2:c3:true:false:+'
hole_c4:c5:c6:c73_20 :: c4:c5:c6:c7
hole_c8:c9:c104_20 :: c8:c9:c10
hole_c11:c12:c135_20 :: c11:c12:c13
hole_c146_20 :: c14
hole_c15:c16:c17:c18:c197_20 :: c15:c16:c17:c18:c19
gen_c:c18_20 :: Nat -> c:c1
gen_0':s:c2:c3:true:false:+'9_20 :: Nat -> 0':s:c2:c3:true:false:+'
gen_c8:c9:c1010_20 :: Nat -> c8:c9:c10
gen_c11:c12:c1311_20 :: Nat -> c11:c12:c13
gen_c15:c16:c17:c18:c1912_20 :: Nat -> c15:c16:c17:c18:c19


Lemmas:
-'(gen_0':s:c2:c3:true:false:+'9_20(n14_20), gen_0':s:c2:c3:true:false:+'9_20(n14_20)) -> gen_c:c18_20(n14_20), rt in Omega(1 + n14_20)


Generator Equations:
gen_c:c18_20(0) <=> c
gen_c:c18_20(+(x, 1)) <=> c1(gen_c:c18_20(x))
gen_0':s:c2:c3:true:false:+'9_20(0) <=> 0'
gen_0':s:c2:c3:true:false:+'9_20(+(x, 1)) <=> s(gen_0':s:c2:c3:true:false:+'9_20(x))
gen_c8:c9:c1010_20(0) <=> c8
gen_c8:c9:c1010_20(+(x, 1)) <=> c10(gen_c8:c9:c1010_20(x))
gen_c11:c12:c1311_20(0) <=> c11
gen_c11:c12:c1311_20(+(x, 1)) <=> c13(gen_c11:c12:c1311_20(x))
gen_c15:c16:c17:c18:c1912_20(0) <=> c15
gen_c15:c16:c17:c18:c1912_20(+(x, 1)) <=> c17(c4, gen_c15:c16:c17:c18:c1912_20(x), 0')


The following defined symbols remain to be analysed:
*', ODD, HALF, F, odd, f, half, -

They will be analysed ascendingly in the following order:
*' < F
*' < f
ODD < F
HALF < F
odd < F
f < F
half < F
odd < f
half < f

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
*'(gen_0':s:c2:c3:true:false:+'9_20(+(1, n618_20))) -> *13_20, rt in Omega(n618_20)

Induction Base:
*'(gen_0':s:c2:c3:true:false:+'9_20(+(1, 0)))

Induction Step:
*'(gen_0':s:c2:c3:true:false:+'9_20(+(1, +(n618_20, 1)))) ->_R^Omega(1)
c3(*'(gen_0':s:c2:c3:true:false:+'9_20(+(1, n618_20)))) ->_IH
c3(*13_20)

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:
-'(z0, 0') -> c
-'(s(z0), s(z1)) -> c1(-'(z0, z1))
*'(0') -> c2
*'(s(z1)) -> c3(*'(z1))
IF(true, z0, z1) -> c4
IF(false, z0, z1) -> c5
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
ODD(0') -> c8
ODD(s(0')) -> c9
ODD(s(s(z0))) -> c10(ODD(z0))
HALF(0') -> c11
HALF(s(0')) -> c12
HALF(s(s(z0))) -> c13(HALF(z0))
POW(z0, z1) -> c14(F(z0, z1, s(0')))
F(z0, 0', z1) -> c15
F(z0, s(z1), z2) -> c16(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), ODD(s(z1)))
F(z0, s(z1), z2) -> c17(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(z0, z1, *'(z2)), *'(z2))
F(z0, s(z1), z2) -> c18(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(*'(z0), half(s(z1)), z2), *'(z0))
F(z0, s(z1), z2) -> c19(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(*'(z0), half(s(z1)), z2), HALF(s(z1)))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
*'(0') -> 0'
*'(s(z1)) -> +'(*'(z1))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
if(true, z0, z1) -> true
if(false, z0, z1) -> false
odd(0') -> false
odd(s(0')) -> true
odd(s(s(z0))) -> odd(z0)
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
pow(z0, z1) -> f(z0, z1, s(0'))
f(z0, 0', z1) -> z1
f(z0, s(z1), z2) -> if(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2))

Types:
-' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c:c1
0' :: 0':s:c2:c3:true:false:+'
c :: c:c1
s :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c1 :: c:c1 -> c:c1
*' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c2 :: 0':s:c2:c3:true:false:+'
c3 :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
IF :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c4:c5:c6:c7
true :: 0':s:c2:c3:true:false:+'
c4 :: c4:c5:c6:c7
false :: 0':s:c2:c3:true:false:+'
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
ODD :: 0':s:c2:c3:true:false:+' -> c8:c9:c10
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
HALF :: 0':s:c2:c3:true:false:+' -> c11:c12:c13
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
POW :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c14
c14 :: c15:c16:c17:c18:c19 -> c14
F :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c15 :: c15:c16:c17:c18:c19
c16 :: c4:c5:c6:c7 -> c8:c9:c10 -> c15:c16:c17:c18:c19
odd :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
f :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
half :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c17 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c18 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c19 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> c11:c12:c13 -> c15:c16:c17:c18:c19
- :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
+' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
if :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
pow :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
hole_c:c11_20 :: c:c1
hole_0':s:c2:c3:true:false:+'2_20 :: 0':s:c2:c3:true:false:+'
hole_c4:c5:c6:c73_20 :: c4:c5:c6:c7
hole_c8:c9:c104_20 :: c8:c9:c10
hole_c11:c12:c135_20 :: c11:c12:c13
hole_c146_20 :: c14
hole_c15:c16:c17:c18:c197_20 :: c15:c16:c17:c18:c19
gen_c:c18_20 :: Nat -> c:c1
gen_0':s:c2:c3:true:false:+'9_20 :: Nat -> 0':s:c2:c3:true:false:+'
gen_c8:c9:c1010_20 :: Nat -> c8:c9:c10
gen_c11:c12:c1311_20 :: Nat -> c11:c12:c13
gen_c15:c16:c17:c18:c1912_20 :: Nat -> c15:c16:c17:c18:c19


Lemmas:
-'(gen_0':s:c2:c3:true:false:+'9_20(n14_20), gen_0':s:c2:c3:true:false:+'9_20(n14_20)) -> gen_c:c18_20(n14_20), rt in Omega(1 + n14_20)
*'(gen_0':s:c2:c3:true:false:+'9_20(+(1, n618_20))) -> *13_20, rt in Omega(n618_20)


Generator Equations:
gen_c:c18_20(0) <=> c
gen_c:c18_20(+(x, 1)) <=> c1(gen_c:c18_20(x))
gen_0':s:c2:c3:true:false:+'9_20(0) <=> 0'
gen_0':s:c2:c3:true:false:+'9_20(+(x, 1)) <=> s(gen_0':s:c2:c3:true:false:+'9_20(x))
gen_c8:c9:c1010_20(0) <=> c8
gen_c8:c9:c1010_20(+(x, 1)) <=> c10(gen_c8:c9:c1010_20(x))
gen_c11:c12:c1311_20(0) <=> c11
gen_c11:c12:c1311_20(+(x, 1)) <=> c13(gen_c11:c12:c1311_20(x))
gen_c15:c16:c17:c18:c1912_20(0) <=> c15
gen_c15:c16:c17:c18:c1912_20(+(x, 1)) <=> c17(c4, gen_c15:c16:c17:c18:c1912_20(x), 0')


The following defined symbols remain to be analysed:
ODD, HALF, F, odd, f, half, -

They will be analysed ascendingly in the following order:
ODD < F
HALF < F
odd < F
f < F
half < F
odd < f
half < f

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ODD(gen_0':s:c2:c3:true:false:+'9_20(*(2, n1610_20))) -> gen_c8:c9:c1010_20(n1610_20), rt in Omega(1 + n1610_20)

Induction Base:
ODD(gen_0':s:c2:c3:true:false:+'9_20(*(2, 0))) ->_R^Omega(1)
c8

Induction Step:
ODD(gen_0':s:c2:c3:true:false:+'9_20(*(2, +(n1610_20, 1)))) ->_R^Omega(1)
c10(ODD(gen_0':s:c2:c3:true:false:+'9_20(*(2, n1610_20)))) ->_IH
c10(gen_c8:c9:c1010_20(c1611_20))

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

(20)
Obligation:
Innermost TRS:
Rules:
-'(z0, 0') -> c
-'(s(z0), s(z1)) -> c1(-'(z0, z1))
*'(0') -> c2
*'(s(z1)) -> c3(*'(z1))
IF(true, z0, z1) -> c4
IF(false, z0, z1) -> c5
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
ODD(0') -> c8
ODD(s(0')) -> c9
ODD(s(s(z0))) -> c10(ODD(z0))
HALF(0') -> c11
HALF(s(0')) -> c12
HALF(s(s(z0))) -> c13(HALF(z0))
POW(z0, z1) -> c14(F(z0, z1, s(0')))
F(z0, 0', z1) -> c15
F(z0, s(z1), z2) -> c16(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), ODD(s(z1)))
F(z0, s(z1), z2) -> c17(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(z0, z1, *'(z2)), *'(z2))
F(z0, s(z1), z2) -> c18(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(*'(z0), half(s(z1)), z2), *'(z0))
F(z0, s(z1), z2) -> c19(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(*'(z0), half(s(z1)), z2), HALF(s(z1)))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
*'(0') -> 0'
*'(s(z1)) -> +'(*'(z1))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
if(true, z0, z1) -> true
if(false, z0, z1) -> false
odd(0') -> false
odd(s(0')) -> true
odd(s(s(z0))) -> odd(z0)
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
pow(z0, z1) -> f(z0, z1, s(0'))
f(z0, 0', z1) -> z1
f(z0, s(z1), z2) -> if(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2))

Types:
-' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c:c1
0' :: 0':s:c2:c3:true:false:+'
c :: c:c1
s :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c1 :: c:c1 -> c:c1
*' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c2 :: 0':s:c2:c3:true:false:+'
c3 :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
IF :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c4:c5:c6:c7
true :: 0':s:c2:c3:true:false:+'
c4 :: c4:c5:c6:c7
false :: 0':s:c2:c3:true:false:+'
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
ODD :: 0':s:c2:c3:true:false:+' -> c8:c9:c10
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
HALF :: 0':s:c2:c3:true:false:+' -> c11:c12:c13
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
POW :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c14
c14 :: c15:c16:c17:c18:c19 -> c14
F :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c15 :: c15:c16:c17:c18:c19
c16 :: c4:c5:c6:c7 -> c8:c9:c10 -> c15:c16:c17:c18:c19
odd :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
f :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
half :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c17 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c18 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c19 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> c11:c12:c13 -> c15:c16:c17:c18:c19
- :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
+' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
if :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
pow :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
hole_c:c11_20 :: c:c1
hole_0':s:c2:c3:true:false:+'2_20 :: 0':s:c2:c3:true:false:+'
hole_c4:c5:c6:c73_20 :: c4:c5:c6:c7
hole_c8:c9:c104_20 :: c8:c9:c10
hole_c11:c12:c135_20 :: c11:c12:c13
hole_c146_20 :: c14
hole_c15:c16:c17:c18:c197_20 :: c15:c16:c17:c18:c19
gen_c:c18_20 :: Nat -> c:c1
gen_0':s:c2:c3:true:false:+'9_20 :: Nat -> 0':s:c2:c3:true:false:+'
gen_c8:c9:c1010_20 :: Nat -> c8:c9:c10
gen_c11:c12:c1311_20 :: Nat -> c11:c12:c13
gen_c15:c16:c17:c18:c1912_20 :: Nat -> c15:c16:c17:c18:c19


Lemmas:
-'(gen_0':s:c2:c3:true:false:+'9_20(n14_20), gen_0':s:c2:c3:true:false:+'9_20(n14_20)) -> gen_c:c18_20(n14_20), rt in Omega(1 + n14_20)
*'(gen_0':s:c2:c3:true:false:+'9_20(+(1, n618_20))) -> *13_20, rt in Omega(n618_20)
ODD(gen_0':s:c2:c3:true:false:+'9_20(*(2, n1610_20))) -> gen_c8:c9:c1010_20(n1610_20), rt in Omega(1 + n1610_20)


Generator Equations:
gen_c:c18_20(0) <=> c
gen_c:c18_20(+(x, 1)) <=> c1(gen_c:c18_20(x))
gen_0':s:c2:c3:true:false:+'9_20(0) <=> 0'
gen_0':s:c2:c3:true:false:+'9_20(+(x, 1)) <=> s(gen_0':s:c2:c3:true:false:+'9_20(x))
gen_c8:c9:c1010_20(0) <=> c8
gen_c8:c9:c1010_20(+(x, 1)) <=> c10(gen_c8:c9:c1010_20(x))
gen_c11:c12:c1311_20(0) <=> c11
gen_c11:c12:c1311_20(+(x, 1)) <=> c13(gen_c11:c12:c1311_20(x))
gen_c15:c16:c17:c18:c1912_20(0) <=> c15
gen_c15:c16:c17:c18:c1912_20(+(x, 1)) <=> c17(c4, gen_c15:c16:c17:c18:c1912_20(x), 0')


The following defined symbols remain to be analysed:
HALF, F, odd, f, half, -

They will be analysed ascendingly in the following order:
HALF < F
odd < F
f < F
half < F
odd < f
half < f

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
HALF(gen_0':s:c2:c3:true:false:+'9_20(*(2, n2313_20))) -> gen_c11:c12:c1311_20(n2313_20), rt in Omega(1 + n2313_20)

Induction Base:
HALF(gen_0':s:c2:c3:true:false:+'9_20(*(2, 0))) ->_R^Omega(1)
c11

Induction Step:
HALF(gen_0':s:c2:c3:true:false:+'9_20(*(2, +(n2313_20, 1)))) ->_R^Omega(1)
c13(HALF(gen_0':s:c2:c3:true:false:+'9_20(*(2, n2313_20)))) ->_IH
c13(gen_c11:c12:c1311_20(c2314_20))

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

(22)
Obligation:
Innermost TRS:
Rules:
-'(z0, 0') -> c
-'(s(z0), s(z1)) -> c1(-'(z0, z1))
*'(0') -> c2
*'(s(z1)) -> c3(*'(z1))
IF(true, z0, z1) -> c4
IF(false, z0, z1) -> c5
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
ODD(0') -> c8
ODD(s(0')) -> c9
ODD(s(s(z0))) -> c10(ODD(z0))
HALF(0') -> c11
HALF(s(0')) -> c12
HALF(s(s(z0))) -> c13(HALF(z0))
POW(z0, z1) -> c14(F(z0, z1, s(0')))
F(z0, 0', z1) -> c15
F(z0, s(z1), z2) -> c16(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), ODD(s(z1)))
F(z0, s(z1), z2) -> c17(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(z0, z1, *'(z2)), *'(z2))
F(z0, s(z1), z2) -> c18(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(*'(z0), half(s(z1)), z2), *'(z0))
F(z0, s(z1), z2) -> c19(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(*'(z0), half(s(z1)), z2), HALF(s(z1)))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
*'(0') -> 0'
*'(s(z1)) -> +'(*'(z1))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
if(true, z0, z1) -> true
if(false, z0, z1) -> false
odd(0') -> false
odd(s(0')) -> true
odd(s(s(z0))) -> odd(z0)
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
pow(z0, z1) -> f(z0, z1, s(0'))
f(z0, 0', z1) -> z1
f(z0, s(z1), z2) -> if(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2))

Types:
-' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c:c1
0' :: 0':s:c2:c3:true:false:+'
c :: c:c1
s :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c1 :: c:c1 -> c:c1
*' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c2 :: 0':s:c2:c3:true:false:+'
c3 :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
IF :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c4:c5:c6:c7
true :: 0':s:c2:c3:true:false:+'
c4 :: c4:c5:c6:c7
false :: 0':s:c2:c3:true:false:+'
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
ODD :: 0':s:c2:c3:true:false:+' -> c8:c9:c10
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
HALF :: 0':s:c2:c3:true:false:+' -> c11:c12:c13
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
POW :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c14
c14 :: c15:c16:c17:c18:c19 -> c14
F :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c15 :: c15:c16:c17:c18:c19
c16 :: c4:c5:c6:c7 -> c8:c9:c10 -> c15:c16:c17:c18:c19
odd :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
f :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
half :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c17 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c18 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c19 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> c11:c12:c13 -> c15:c16:c17:c18:c19
- :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
+' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
if :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
pow :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
hole_c:c11_20 :: c:c1
hole_0':s:c2:c3:true:false:+'2_20 :: 0':s:c2:c3:true:false:+'
hole_c4:c5:c6:c73_20 :: c4:c5:c6:c7
hole_c8:c9:c104_20 :: c8:c9:c10
hole_c11:c12:c135_20 :: c11:c12:c13
hole_c146_20 :: c14
hole_c15:c16:c17:c18:c197_20 :: c15:c16:c17:c18:c19
gen_c:c18_20 :: Nat -> c:c1
gen_0':s:c2:c3:true:false:+'9_20 :: Nat -> 0':s:c2:c3:true:false:+'
gen_c8:c9:c1010_20 :: Nat -> c8:c9:c10
gen_c11:c12:c1311_20 :: Nat -> c11:c12:c13
gen_c15:c16:c17:c18:c1912_20 :: Nat -> c15:c16:c17:c18:c19


Lemmas:
-'(gen_0':s:c2:c3:true:false:+'9_20(n14_20), gen_0':s:c2:c3:true:false:+'9_20(n14_20)) -> gen_c:c18_20(n14_20), rt in Omega(1 + n14_20)
*'(gen_0':s:c2:c3:true:false:+'9_20(+(1, n618_20))) -> *13_20, rt in Omega(n618_20)
ODD(gen_0':s:c2:c3:true:false:+'9_20(*(2, n1610_20))) -> gen_c8:c9:c1010_20(n1610_20), rt in Omega(1 + n1610_20)
HALF(gen_0':s:c2:c3:true:false:+'9_20(*(2, n2313_20))) -> gen_c11:c12:c1311_20(n2313_20), rt in Omega(1 + n2313_20)


Generator Equations:
gen_c:c18_20(0) <=> c
gen_c:c18_20(+(x, 1)) <=> c1(gen_c:c18_20(x))
gen_0':s:c2:c3:true:false:+'9_20(0) <=> 0'
gen_0':s:c2:c3:true:false:+'9_20(+(x, 1)) <=> s(gen_0':s:c2:c3:true:false:+'9_20(x))
gen_c8:c9:c1010_20(0) <=> c8
gen_c8:c9:c1010_20(+(x, 1)) <=> c10(gen_c8:c9:c1010_20(x))
gen_c11:c12:c1311_20(0) <=> c11
gen_c11:c12:c1311_20(+(x, 1)) <=> c13(gen_c11:c12:c1311_20(x))
gen_c15:c16:c17:c18:c1912_20(0) <=> c15
gen_c15:c16:c17:c18:c1912_20(+(x, 1)) <=> c17(c4, gen_c15:c16:c17:c18:c1912_20(x), 0')


The following defined symbols remain to be analysed:
odd, F, f, half, -

They will be analysed ascendingly in the following order:
odd < F
f < F
half < F
odd < f
half < f

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
odd(gen_0':s:c2:c3:true:false:+'9_20(*(2, n3054_20))) -> false, rt in Omega(0)

Induction Base:
odd(gen_0':s:c2:c3:true:false:+'9_20(*(2, 0))) ->_R^Omega(0)
false

Induction Step:
odd(gen_0':s:c2:c3:true:false:+'9_20(*(2, +(n3054_20, 1)))) ->_R^Omega(0)
odd(gen_0':s:c2:c3:true:false:+'9_20(*(2, n3054_20))) ->_IH
false

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:
-'(z0, 0') -> c
-'(s(z0), s(z1)) -> c1(-'(z0, z1))
*'(0') -> c2
*'(s(z1)) -> c3(*'(z1))
IF(true, z0, z1) -> c4
IF(false, z0, z1) -> c5
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
ODD(0') -> c8
ODD(s(0')) -> c9
ODD(s(s(z0))) -> c10(ODD(z0))
HALF(0') -> c11
HALF(s(0')) -> c12
HALF(s(s(z0))) -> c13(HALF(z0))
POW(z0, z1) -> c14(F(z0, z1, s(0')))
F(z0, 0', z1) -> c15
F(z0, s(z1), z2) -> c16(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), ODD(s(z1)))
F(z0, s(z1), z2) -> c17(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(z0, z1, *'(z2)), *'(z2))
F(z0, s(z1), z2) -> c18(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(*'(z0), half(s(z1)), z2), *'(z0))
F(z0, s(z1), z2) -> c19(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(*'(z0), half(s(z1)), z2), HALF(s(z1)))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
*'(0') -> 0'
*'(s(z1)) -> +'(*'(z1))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
if(true, z0, z1) -> true
if(false, z0, z1) -> false
odd(0') -> false
odd(s(0')) -> true
odd(s(s(z0))) -> odd(z0)
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
pow(z0, z1) -> f(z0, z1, s(0'))
f(z0, 0', z1) -> z1
f(z0, s(z1), z2) -> if(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2))

Types:
-' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c:c1
0' :: 0':s:c2:c3:true:false:+'
c :: c:c1
s :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c1 :: c:c1 -> c:c1
*' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c2 :: 0':s:c2:c3:true:false:+'
c3 :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
IF :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c4:c5:c6:c7
true :: 0':s:c2:c3:true:false:+'
c4 :: c4:c5:c6:c7
false :: 0':s:c2:c3:true:false:+'
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
ODD :: 0':s:c2:c3:true:false:+' -> c8:c9:c10
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
HALF :: 0':s:c2:c3:true:false:+' -> c11:c12:c13
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
POW :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c14
c14 :: c15:c16:c17:c18:c19 -> c14
F :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c15 :: c15:c16:c17:c18:c19
c16 :: c4:c5:c6:c7 -> c8:c9:c10 -> c15:c16:c17:c18:c19
odd :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
f :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
half :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c17 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c18 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c19 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> c11:c12:c13 -> c15:c16:c17:c18:c19
- :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
+' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
if :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
pow :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
hole_c:c11_20 :: c:c1
hole_0':s:c2:c3:true:false:+'2_20 :: 0':s:c2:c3:true:false:+'
hole_c4:c5:c6:c73_20 :: c4:c5:c6:c7
hole_c8:c9:c104_20 :: c8:c9:c10
hole_c11:c12:c135_20 :: c11:c12:c13
hole_c146_20 :: c14
hole_c15:c16:c17:c18:c197_20 :: c15:c16:c17:c18:c19
gen_c:c18_20 :: Nat -> c:c1
gen_0':s:c2:c3:true:false:+'9_20 :: Nat -> 0':s:c2:c3:true:false:+'
gen_c8:c9:c1010_20 :: Nat -> c8:c9:c10
gen_c11:c12:c1311_20 :: Nat -> c11:c12:c13
gen_c15:c16:c17:c18:c1912_20 :: Nat -> c15:c16:c17:c18:c19


Lemmas:
-'(gen_0':s:c2:c3:true:false:+'9_20(n14_20), gen_0':s:c2:c3:true:false:+'9_20(n14_20)) -> gen_c:c18_20(n14_20), rt in Omega(1 + n14_20)
*'(gen_0':s:c2:c3:true:false:+'9_20(+(1, n618_20))) -> *13_20, rt in Omega(n618_20)
ODD(gen_0':s:c2:c3:true:false:+'9_20(*(2, n1610_20))) -> gen_c8:c9:c1010_20(n1610_20), rt in Omega(1 + n1610_20)
HALF(gen_0':s:c2:c3:true:false:+'9_20(*(2, n2313_20))) -> gen_c11:c12:c1311_20(n2313_20), rt in Omega(1 + n2313_20)
odd(gen_0':s:c2:c3:true:false:+'9_20(*(2, n3054_20))) -> false, rt in Omega(0)


Generator Equations:
gen_c:c18_20(0) <=> c
gen_c:c18_20(+(x, 1)) <=> c1(gen_c:c18_20(x))
gen_0':s:c2:c3:true:false:+'9_20(0) <=> 0'
gen_0':s:c2:c3:true:false:+'9_20(+(x, 1)) <=> s(gen_0':s:c2:c3:true:false:+'9_20(x))
gen_c8:c9:c1010_20(0) <=> c8
gen_c8:c9:c1010_20(+(x, 1)) <=> c10(gen_c8:c9:c1010_20(x))
gen_c11:c12:c1311_20(0) <=> c11
gen_c11:c12:c1311_20(+(x, 1)) <=> c13(gen_c11:c12:c1311_20(x))
gen_c15:c16:c17:c18:c1912_20(0) <=> c15
gen_c15:c16:c17:c18:c1912_20(+(x, 1)) <=> c17(c4, gen_c15:c16:c17:c18:c1912_20(x), 0')


The following defined symbols remain to be analysed:
half, F, f, -

They will be analysed ascendingly in the following order:
f < F
half < F
half < f

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
half(gen_0':s:c2:c3:true:false:+'9_20(*(2, n3387_20))) -> gen_0':s:c2:c3:true:false:+'9_20(n3387_20), rt in Omega(0)

Induction Base:
half(gen_0':s:c2:c3:true:false:+'9_20(*(2, 0))) ->_R^Omega(0)
0'

Induction Step:
half(gen_0':s:c2:c3:true:false:+'9_20(*(2, +(n3387_20, 1)))) ->_R^Omega(0)
s(half(gen_0':s:c2:c3:true:false:+'9_20(*(2, n3387_20)))) ->_IH
s(gen_0':s:c2:c3:true:false:+'9_20(c3388_20))

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

(26)
Obligation:
Innermost TRS:
Rules:
-'(z0, 0') -> c
-'(s(z0), s(z1)) -> c1(-'(z0, z1))
*'(0') -> c2
*'(s(z1)) -> c3(*'(z1))
IF(true, z0, z1) -> c4
IF(false, z0, z1) -> c5
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
ODD(0') -> c8
ODD(s(0')) -> c9
ODD(s(s(z0))) -> c10(ODD(z0))
HALF(0') -> c11
HALF(s(0')) -> c12
HALF(s(s(z0))) -> c13(HALF(z0))
POW(z0, z1) -> c14(F(z0, z1, s(0')))
F(z0, 0', z1) -> c15
F(z0, s(z1), z2) -> c16(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), ODD(s(z1)))
F(z0, s(z1), z2) -> c17(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(z0, z1, *'(z2)), *'(z2))
F(z0, s(z1), z2) -> c18(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(*'(z0), half(s(z1)), z2), *'(z0))
F(z0, s(z1), z2) -> c19(IF(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2)), F(*'(z0), half(s(z1)), z2), HALF(s(z1)))
-(z0, 0') -> z0
-(s(z0), s(z1)) -> -(z0, z1)
*'(0') -> 0'
*'(s(z1)) -> +'(*'(z1))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
if(true, z0, z1) -> true
if(false, z0, z1) -> false
odd(0') -> false
odd(s(0')) -> true
odd(s(s(z0))) -> odd(z0)
half(0') -> 0'
half(s(0')) -> 0'
half(s(s(z0))) -> s(half(z0))
pow(z0, z1) -> f(z0, z1, s(0'))
f(z0, 0', z1) -> z1
f(z0, s(z1), z2) -> if(odd(s(z1)), f(z0, z1, *'(z2)), f(*'(z0), half(s(z1)), z2))

Types:
-' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c:c1
0' :: 0':s:c2:c3:true:false:+'
c :: c:c1
s :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c1 :: c:c1 -> c:c1
*' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c2 :: 0':s:c2:c3:true:false:+'
c3 :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
IF :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c4:c5:c6:c7
true :: 0':s:c2:c3:true:false:+'
c4 :: c4:c5:c6:c7
false :: 0':s:c2:c3:true:false:+'
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
ODD :: 0':s:c2:c3:true:false:+' -> c8:c9:c10
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
HALF :: 0':s:c2:c3:true:false:+' -> c11:c12:c13
c11 :: c11:c12:c13
c12 :: c11:c12:c13
c13 :: c11:c12:c13 -> c11:c12:c13
POW :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c14
c14 :: c15:c16:c17:c18:c19 -> c14
F :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c15 :: c15:c16:c17:c18:c19
c16 :: c4:c5:c6:c7 -> c8:c9:c10 -> c15:c16:c17:c18:c19
odd :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
f :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
half :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
c17 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c18 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> 0':s:c2:c3:true:false:+' -> c15:c16:c17:c18:c19
c19 :: c4:c5:c6:c7 -> c15:c16:c17:c18:c19 -> c11:c12:c13 -> c15:c16:c17:c18:c19
- :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
+' :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
if :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
pow :: 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+' -> 0':s:c2:c3:true:false:+'
hole_c:c11_20 :: c:c1
hole_0':s:c2:c3:true:false:+'2_20 :: 0':s:c2:c3:true:false:+'
hole_c4:c5:c6:c73_20 :: c4:c5:c6:c7
hole_c8:c9:c104_20 :: c8:c9:c10
hole_c11:c12:c135_20 :: c11:c12:c13
hole_c146_20 :: c14
hole_c15:c16:c17:c18:c197_20 :: c15:c16:c17:c18:c19
gen_c:c18_20 :: Nat -> c:c1
gen_0':s:c2:c3:true:false:+'9_20 :: Nat -> 0':s:c2:c3:true:false:+'
gen_c8:c9:c1010_20 :: Nat -> c8:c9:c10
gen_c11:c12:c1311_20 :: Nat -> c11:c12:c13
gen_c15:c16:c17:c18:c1912_20 :: Nat -> c15:c16:c17:c18:c19


Lemmas:
-'(gen_0':s:c2:c3:true:false:+'9_20(n14_20), gen_0':s:c2:c3:true:false:+'9_20(n14_20)) -> gen_c:c18_20(n14_20), rt in Omega(1 + n14_20)
*'(gen_0':s:c2:c3:true:false:+'9_20(+(1, n618_20))) -> *13_20, rt in Omega(n618_20)
ODD(gen_0':s:c2:c3:true:false:+'9_20(*(2, n1610_20))) -> gen_c8:c9:c1010_20(n1610_20), rt in Omega(1 + n1610_20)
HALF(gen_0':s:c2:c3:true:false:+'9_20(*(2, n2313_20))) -> gen_c11:c12:c1311_20(n2313_20), rt in Omega(1 + n2313_20)
odd(gen_0':s:c2:c3:true:false:+'9_20(*(2, n3054_20))) -> false, rt in Omega(0)
half(gen_0':s:c2:c3:true:false:+'9_20(*(2, n3387_20))) -> gen_0':s:c2:c3:true:false:+'9_20(n3387_20), rt in Omega(0)


Generator Equations:
gen_c:c18_20(0) <=> c
gen_c:c18_20(+(x, 1)) <=> c1(gen_c:c18_20(x))
gen_0':s:c2:c3:true:false:+'9_20(0) <=> 0'
gen_0':s:c2:c3:true:false:+'9_20(+(x, 1)) <=> s(gen_0':s:c2:c3:true:false:+'9_20(x))
gen_c8:c9:c1010_20(0) <=> c8
gen_c8:c9:c1010_20(+(x, 1)) <=> c10(gen_c8:c9:c1010_20(x))
gen_c11:c12:c1311_20(0) <=> c11
gen_c11:c12:c1311_20(+(x, 1)) <=> c13(gen_c11:c12:c1311_20(x))
gen_c15:c16:c17:c18:c1912_20(0) <=> c15
gen_c15:c16:c17:c18:c1912_20(+(x, 1)) <=> c17(c4, gen_c15:c16:c17:c18:c1912_20(x), 0')


The following defined symbols remain to be analysed:
f, F, -

They will be analysed ascendingly in the following order:
f < F

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
-(gen_0':s:c2:c3:true:false:+'9_20(n15588_20), gen_0':s:c2:c3:true:false:+'9_20(n15588_20)) -> gen_0':s:c2:c3:true:false:+'9_20(0), rt in Omega(0)

Induction Base:
-(gen_0':s:c2:c3:true:false:+'9_20(0), gen_0':s:c2:c3:true:false:+'9_20(0)) ->_R^Omega(0)
gen_0':s:c2:c3:true:false:+'9_20(0)

Induction Step:
-(gen_0':s:c2:c3:true:false:+'9_20(+(n15588_20, 1)), gen_0':s:c2:c3:true:false:+'9_20(+(n15588_20, 1))) ->_R^Omega(0)
-(gen_0':s:c2:c3:true:false:+'9_20(n15588_20), gen_0':s:c2:c3:true:false:+'9_20(n15588_20)) ->_IH
gen_0':s:c2:c3:true:false:+'9_20(0)

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

(28)
BOUNDS(1, INF)