Runtime Complexity TRS:
The TRS R consists of the following rules:

-(x, 0) → x
-(s(x), s(y)) → -(x, y)
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
if(true, x, y) → x
if(false, x, y) → y
odd(0) → false
odd(s(0)) → true
odd(s(s(x))) → odd(x)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
if(true, x, y) → true
if(false, x, y) → false
pow(x, y) → f(x, y, s(0))
f(x, 0, z) → z
f(x, s(y), z) → if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:

-'(x, 0') → x
-'(s'(x), s'(y)) → -'(x, y)
*'(x, 0') → 0'
*'(x, s'(y)) → +'(*'(x, y), x)
if'(true', x, y) → x
if'(false', x, y) → y
odd'(0') → false'
odd'(s'(0')) → true'
odd'(s'(s'(x))) → odd'(x)
half'(0') → 0'
half'(s'(0')) → 0'
half'(s'(s'(x))) → s'(half'(x))
if'(true', x, y) → true'
if'(false', x, y) → false'
pow'(x, y) → f'(x, y, s'(0'))
f'(x, 0', z) → z
f'(x, s'(y), z) → if'(odd'(s'(y)), f'(x, y, *'(x, z)), f'(*'(x, x), half'(s'(y)), z))

Rewrite Strategy: INNERMOST

Sliced the following arguments:
*'/0
+'/1

Runtime Complexity TRS:
The TRS R consists of the following rules:

-'(x, 0') → x
-'(s'(x), s'(y)) → -'(x, y)
*'(0') → 0'
*'(s'(y)) → +'(*'(y))
if'(true', x, y) → x
if'(false', x, y) → y
odd'(0') → false'
odd'(s'(0')) → true'
odd'(s'(s'(x))) → odd'(x)
half'(0') → 0'
half'(s'(0')) → 0'
half'(s'(s'(x))) → s'(half'(x))
if'(true', x, y) → true'
if'(false', x, y) → false'
pow'(x, y) → f'(x, y, s'(0'))
f'(x, 0', z) → z
f'(x, s'(y), z) → if'(odd'(s'(y)), f'(x, y, *'(z)), f'(*'(x), half'(s'(y)), z))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
-'(x, 0') → x
-'(s'(x), s'(y)) → -'(x, y)
*'(0') → 0'
*'(s'(y)) → +'(*'(y))
if'(true', x, y) → x
if'(false', x, y) → y
odd'(0') → false'
odd'(s'(0')) → true'
odd'(s'(s'(x))) → odd'(x)
half'(0') → 0'
half'(s'(0')) → 0'
half'(s'(s'(x))) → s'(half'(x))
if'(true', x, y) → true'
if'(false', x, y) → false'
pow'(x, y) → f'(x, y, s'(0'))
f'(x, 0', z) → z
f'(x, s'(y), z) → if'(odd'(s'(y)), f'(x, y, *'(z)), f'(*'(x), half'(s'(y)), z))

Types:
-' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
0' :: 0':s':+':true':false'
s' :: 0':s':+':true':false' → 0':s':+':true':false'
*' :: 0':s':+':true':false' → 0':s':+':true':false'
+' :: 0':s':+':true':false' → 0':s':+':true':false'
if' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
true' :: 0':s':+':true':false'
false' :: 0':s':+':true':false'
odd' :: 0':s':+':true':false' → 0':s':+':true':false'
half' :: 0':s':+':true':false' → 0':s':+':true':false'
pow' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
f' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
_hole_0':s':+':true':false'1 :: 0':s':+':true':false'
_gen_0':s':+':true':false'2 :: Nat → 0':s':+':true':false'

Heuristically decided to analyse the following defined symbols:
-', *', odd', half', f'

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

Rules:
-'(x, 0') → x
-'(s'(x), s'(y)) → -'(x, y)
*'(0') → 0'
*'(s'(y)) → +'(*'(y))
if'(true', x, y) → x
if'(false', x, y) → y
odd'(0') → false'
odd'(s'(0')) → true'
odd'(s'(s'(x))) → odd'(x)
half'(0') → 0'
half'(s'(0')) → 0'
half'(s'(s'(x))) → s'(half'(x))
if'(true', x, y) → true'
if'(false', x, y) → false'
pow'(x, y) → f'(x, y, s'(0'))
f'(x, 0', z) → z
f'(x, s'(y), z) → if'(odd'(s'(y)), f'(x, y, *'(z)), f'(*'(x), half'(s'(y)), z))

Types:
-' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
0' :: 0':s':+':true':false'
s' :: 0':s':+':true':false' → 0':s':+':true':false'
*' :: 0':s':+':true':false' → 0':s':+':true':false'
+' :: 0':s':+':true':false' → 0':s':+':true':false'
if' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
true' :: 0':s':+':true':false'
false' :: 0':s':+':true':false'
odd' :: 0':s':+':true':false' → 0':s':+':true':false'
half' :: 0':s':+':true':false' → 0':s':+':true':false'
pow' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
f' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
_hole_0':s':+':true':false'1 :: 0':s':+':true':false'
_gen_0':s':+':true':false'2 :: Nat → 0':s':+':true':false'

Generator Equations:
_gen_0':s':+':true':false'2(0) ⇔ 0'
_gen_0':s':+':true':false'2(+(x, 1)) ⇔ s'(_gen_0':s':+':true':false'2(x))

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

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

Proved the following rewrite lemma:
-'(_gen_0':s':+':true':false'2(_n4), _gen_0':s':+':true':false'2(_n4)) → _gen_0':s':+':true':false'2(0), rt ∈ Ω(1 + n4)

Induction Base:
-'(_gen_0':s':+':true':false'2(0), _gen_0':s':+':true':false'2(0)) →RΩ(1)
_gen_0':s':+':true':false'2(0)

Induction Step:
-'(_gen_0':s':+':true':false'2(+(_\$n5, 1)), _gen_0':s':+':true':false'2(+(_\$n5, 1))) →RΩ(1)
-'(_gen_0':s':+':true':false'2(_\$n5), _gen_0':s':+':true':false'2(_\$n5)) →IH
_gen_0':s':+':true':false'2(0)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

Rules:
-'(x, 0') → x
-'(s'(x), s'(y)) → -'(x, y)
*'(0') → 0'
*'(s'(y)) → +'(*'(y))
if'(true', x, y) → x
if'(false', x, y) → y
odd'(0') → false'
odd'(s'(0')) → true'
odd'(s'(s'(x))) → odd'(x)
half'(0') → 0'
half'(s'(0')) → 0'
half'(s'(s'(x))) → s'(half'(x))
if'(true', x, y) → true'
if'(false', x, y) → false'
pow'(x, y) → f'(x, y, s'(0'))
f'(x, 0', z) → z
f'(x, s'(y), z) → if'(odd'(s'(y)), f'(x, y, *'(z)), f'(*'(x), half'(s'(y)), z))

Types:
-' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
0' :: 0':s':+':true':false'
s' :: 0':s':+':true':false' → 0':s':+':true':false'
*' :: 0':s':+':true':false' → 0':s':+':true':false'
+' :: 0':s':+':true':false' → 0':s':+':true':false'
if' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
true' :: 0':s':+':true':false'
false' :: 0':s':+':true':false'
odd' :: 0':s':+':true':false' → 0':s':+':true':false'
half' :: 0':s':+':true':false' → 0':s':+':true':false'
pow' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
f' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
_hole_0':s':+':true':false'1 :: 0':s':+':true':false'
_gen_0':s':+':true':false'2 :: Nat → 0':s':+':true':false'

Lemmas:
-'(_gen_0':s':+':true':false'2(_n4), _gen_0':s':+':true':false'2(_n4)) → _gen_0':s':+':true':false'2(0), rt ∈ Ω(1 + n4)

Generator Equations:
_gen_0':s':+':true':false'2(0) ⇔ 0'
_gen_0':s':+':true':false'2(+(x, 1)) ⇔ s'(_gen_0':s':+':true':false'2(x))

The following defined symbols remain to be analysed:
*', odd', half', f'

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

Proved the following rewrite lemma:
*'(_gen_0':s':+':true':false'2(+(1, _n870))) → _*3, rt ∈ Ω(n870)

Induction Base:
*'(_gen_0':s':+':true':false'2(+(1, 0)))

Induction Step:
*'(_gen_0':s':+':true':false'2(+(1, +(_\$n871, 1)))) →RΩ(1)
+'(*'(_gen_0':s':+':true':false'2(+(1, _\$n871)))) →IH
+'(_*3)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

Rules:
-'(x, 0') → x
-'(s'(x), s'(y)) → -'(x, y)
*'(0') → 0'
*'(s'(y)) → +'(*'(y))
if'(true', x, y) → x
if'(false', x, y) → y
odd'(0') → false'
odd'(s'(0')) → true'
odd'(s'(s'(x))) → odd'(x)
half'(0') → 0'
half'(s'(0')) → 0'
half'(s'(s'(x))) → s'(half'(x))
if'(true', x, y) → true'
if'(false', x, y) → false'
pow'(x, y) → f'(x, y, s'(0'))
f'(x, 0', z) → z
f'(x, s'(y), z) → if'(odd'(s'(y)), f'(x, y, *'(z)), f'(*'(x), half'(s'(y)), z))

Types:
-' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
0' :: 0':s':+':true':false'
s' :: 0':s':+':true':false' → 0':s':+':true':false'
*' :: 0':s':+':true':false' → 0':s':+':true':false'
+' :: 0':s':+':true':false' → 0':s':+':true':false'
if' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
true' :: 0':s':+':true':false'
false' :: 0':s':+':true':false'
odd' :: 0':s':+':true':false' → 0':s':+':true':false'
half' :: 0':s':+':true':false' → 0':s':+':true':false'
pow' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
f' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
_hole_0':s':+':true':false'1 :: 0':s':+':true':false'
_gen_0':s':+':true':false'2 :: Nat → 0':s':+':true':false'

Lemmas:
-'(_gen_0':s':+':true':false'2(_n4), _gen_0':s':+':true':false'2(_n4)) → _gen_0':s':+':true':false'2(0), rt ∈ Ω(1 + n4)
*'(_gen_0':s':+':true':false'2(+(1, _n870))) → _*3, rt ∈ Ω(n870)

Generator Equations:
_gen_0':s':+':true':false'2(0) ⇔ 0'
_gen_0':s':+':true':false'2(+(x, 1)) ⇔ s'(_gen_0':s':+':true':false'2(x))

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

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

Proved the following rewrite lemma:
odd'(_gen_0':s':+':true':false'2(*(2, _n1929))) → false', rt ∈ Ω(1 + n1929)

Induction Base:
odd'(_gen_0':s':+':true':false'2(*(2, 0))) →RΩ(1)
false'

Induction Step:
odd'(_gen_0':s':+':true':false'2(*(2, +(_\$n1930, 1)))) →RΩ(1)
odd'(_gen_0':s':+':true':false'2(*(2, _\$n1930))) →IH
false'

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

Rules:
-'(x, 0') → x
-'(s'(x), s'(y)) → -'(x, y)
*'(0') → 0'
*'(s'(y)) → +'(*'(y))
if'(true', x, y) → x
if'(false', x, y) → y
odd'(0') → false'
odd'(s'(0')) → true'
odd'(s'(s'(x))) → odd'(x)
half'(0') → 0'
half'(s'(0')) → 0'
half'(s'(s'(x))) → s'(half'(x))
if'(true', x, y) → true'
if'(false', x, y) → false'
pow'(x, y) → f'(x, y, s'(0'))
f'(x, 0', z) → z
f'(x, s'(y), z) → if'(odd'(s'(y)), f'(x, y, *'(z)), f'(*'(x), half'(s'(y)), z))

Types:
-' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
0' :: 0':s':+':true':false'
s' :: 0':s':+':true':false' → 0':s':+':true':false'
*' :: 0':s':+':true':false' → 0':s':+':true':false'
+' :: 0':s':+':true':false' → 0':s':+':true':false'
if' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
true' :: 0':s':+':true':false'
false' :: 0':s':+':true':false'
odd' :: 0':s':+':true':false' → 0':s':+':true':false'
half' :: 0':s':+':true':false' → 0':s':+':true':false'
pow' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
f' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
_hole_0':s':+':true':false'1 :: 0':s':+':true':false'
_gen_0':s':+':true':false'2 :: Nat → 0':s':+':true':false'

Lemmas:
-'(_gen_0':s':+':true':false'2(_n4), _gen_0':s':+':true':false'2(_n4)) → _gen_0':s':+':true':false'2(0), rt ∈ Ω(1 + n4)
*'(_gen_0':s':+':true':false'2(+(1, _n870))) → _*3, rt ∈ Ω(n870)
odd'(_gen_0':s':+':true':false'2(*(2, _n1929))) → false', rt ∈ Ω(1 + n1929)

Generator Equations:
_gen_0':s':+':true':false'2(0) ⇔ 0'
_gen_0':s':+':true':false'2(+(x, 1)) ⇔ s'(_gen_0':s':+':true':false'2(x))

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

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

Proved the following rewrite lemma:
half'(_gen_0':s':+':true':false'2(*(2, _n2547))) → _gen_0':s':+':true':false'2(_n2547), rt ∈ Ω(1 + n2547)

Induction Base:
half'(_gen_0':s':+':true':false'2(*(2, 0))) →RΩ(1)
0'

Induction Step:
half'(_gen_0':s':+':true':false'2(*(2, +(_\$n2548, 1)))) →RΩ(1)
s'(half'(_gen_0':s':+':true':false'2(*(2, _\$n2548)))) →IH
s'(_gen_0':s':+':true':false'2(_\$n2548))

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

Rules:
-'(x, 0') → x
-'(s'(x), s'(y)) → -'(x, y)
*'(0') → 0'
*'(s'(y)) → +'(*'(y))
if'(true', x, y) → x
if'(false', x, y) → y
odd'(0') → false'
odd'(s'(0')) → true'
odd'(s'(s'(x))) → odd'(x)
half'(0') → 0'
half'(s'(0')) → 0'
half'(s'(s'(x))) → s'(half'(x))
if'(true', x, y) → true'
if'(false', x, y) → false'
pow'(x, y) → f'(x, y, s'(0'))
f'(x, 0', z) → z
f'(x, s'(y), z) → if'(odd'(s'(y)), f'(x, y, *'(z)), f'(*'(x), half'(s'(y)), z))

Types:
-' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
0' :: 0':s':+':true':false'
s' :: 0':s':+':true':false' → 0':s':+':true':false'
*' :: 0':s':+':true':false' → 0':s':+':true':false'
+' :: 0':s':+':true':false' → 0':s':+':true':false'
if' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
true' :: 0':s':+':true':false'
false' :: 0':s':+':true':false'
odd' :: 0':s':+':true':false' → 0':s':+':true':false'
half' :: 0':s':+':true':false' → 0':s':+':true':false'
pow' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
f' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
_hole_0':s':+':true':false'1 :: 0':s':+':true':false'
_gen_0':s':+':true':false'2 :: Nat → 0':s':+':true':false'

Lemmas:
-'(_gen_0':s':+':true':false'2(_n4), _gen_0':s':+':true':false'2(_n4)) → _gen_0':s':+':true':false'2(0), rt ∈ Ω(1 + n4)
*'(_gen_0':s':+':true':false'2(+(1, _n870))) → _*3, rt ∈ Ω(n870)
odd'(_gen_0':s':+':true':false'2(*(2, _n1929))) → false', rt ∈ Ω(1 + n1929)
half'(_gen_0':s':+':true':false'2(*(2, _n2547))) → _gen_0':s':+':true':false'2(_n2547), rt ∈ Ω(1 + n2547)

Generator Equations:
_gen_0':s':+':true':false'2(0) ⇔ 0'
_gen_0':s':+':true':false'2(+(x, 1)) ⇔ s'(_gen_0':s':+':true':false'2(x))

The following defined symbols remain to be analysed:
f'

Could not prove a rewrite lemma for the defined symbol f'.

Rules:
-'(x, 0') → x
-'(s'(x), s'(y)) → -'(x, y)
*'(0') → 0'
*'(s'(y)) → +'(*'(y))
if'(true', x, y) → x
if'(false', x, y) → y
odd'(0') → false'
odd'(s'(0')) → true'
odd'(s'(s'(x))) → odd'(x)
half'(0') → 0'
half'(s'(0')) → 0'
half'(s'(s'(x))) → s'(half'(x))
if'(true', x, y) → true'
if'(false', x, y) → false'
pow'(x, y) → f'(x, y, s'(0'))
f'(x, 0', z) → z
f'(x, s'(y), z) → if'(odd'(s'(y)), f'(x, y, *'(z)), f'(*'(x), half'(s'(y)), z))

Types:
-' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
0' :: 0':s':+':true':false'
s' :: 0':s':+':true':false' → 0':s':+':true':false'
*' :: 0':s':+':true':false' → 0':s':+':true':false'
+' :: 0':s':+':true':false' → 0':s':+':true':false'
if' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
true' :: 0':s':+':true':false'
false' :: 0':s':+':true':false'
odd' :: 0':s':+':true':false' → 0':s':+':true':false'
half' :: 0':s':+':true':false' → 0':s':+':true':false'
pow' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
f' :: 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false' → 0':s':+':true':false'
_hole_0':s':+':true':false'1 :: 0':s':+':true':false'
_gen_0':s':+':true':false'2 :: Nat → 0':s':+':true':false'

Lemmas:
-'(_gen_0':s':+':true':false'2(_n4), _gen_0':s':+':true':false'2(_n4)) → _gen_0':s':+':true':false'2(0), rt ∈ Ω(1 + n4)
*'(_gen_0':s':+':true':false'2(+(1, _n870))) → _*3, rt ∈ Ω(n870)
odd'(_gen_0':s':+':true':false'2(*(2, _n1929))) → false', rt ∈ Ω(1 + n1929)
half'(_gen_0':s':+':true':false'2(*(2, _n2547))) → _gen_0':s':+':true':false'2(_n2547), rt ∈ Ω(1 + n2547)

Generator Equations:
_gen_0':s':+':true':false'2(0) ⇔ 0'
_gen_0':s':+':true':false'2(+(x, 1)) ⇔ s'(_gen_0':s':+':true':false'2(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
-'(_gen_0':s':+':true':false'2(_n4), _gen_0':s':+':true':false'2(_n4)) → _gen_0':s':+':true':false'2(0), rt ∈ Ω(1 + n4)