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