tower(x) → f(a, x, s(0))
f(a, 0, y) → y
f(a, s(x), y) → f(b, y, s(x))
f(b, y, x) → f(a, half(x), exp(y))
exp(0) → s(0)
exp(s(x)) → double(exp(x))
double(0) → 0
double(s(x)) → s(s(double(x)))
half(0) → double(0)
half(s(0)) → half(0)
half(s(s(x))) → s(half(x))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
tower'(x) → f'(a', x, s'(0'))
f'(a', 0', y) → y
f'(a', s'(x), y) → f'(b', y, s'(x))
f'(b', y, x) → f'(a', half'(x), exp'(y))
exp'(0') → s'(0')
exp'(s'(x)) → double'(exp'(x))
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
half'(0') → double'(0')
half'(s'(0')) → half'(0')
half'(s'(s'(x))) → s'(half'(x))
Infered types.
Rules:
tower'(x) → f'(a', x, s'(0'))
f'(a', 0', y) → y
f'(a', s'(x), y) → f'(b', y, s'(x))
f'(b', y, x) → f'(a', half'(x), exp'(y))
exp'(0') → s'(0')
exp'(s'(x)) → double'(exp'(x))
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
half'(0') → double'(0')
half'(s'(0')) → half'(0')
half'(s'(s'(x))) → s'(half'(x))
Types:
tower' :: 0':s' → 0':s'
f' :: a':b' → 0':s' → 0':s' → 0':s'
a' :: a':b'
s' :: 0':s' → 0':s'
0' :: 0':s'
b' :: a':b'
half' :: 0':s' → 0':s'
exp' :: 0':s' → 0':s'
double' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_a':b'2 :: a':b'
_gen_0':s'3 :: Nat → 0':s'
Heuristically decided to analyse the following defined symbols:
f', half', exp', double'
They will be analysed ascendingly in the following order:
half' < f'
exp' < f'
double' < half'
double' < exp'
Rules:
tower'(x) → f'(a', x, s'(0'))
f'(a', 0', y) → y
f'(a', s'(x), y) → f'(b', y, s'(x))
f'(b', y, x) → f'(a', half'(x), exp'(y))
exp'(0') → s'(0')
exp'(s'(x)) → double'(exp'(x))
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
half'(0') → double'(0')
half'(s'(0')) → half'(0')
half'(s'(s'(x))) → s'(half'(x))
Types:
tower' :: 0':s' → 0':s'
f' :: a':b' → 0':s' → 0':s' → 0':s'
a' :: a':b'
s' :: 0':s' → 0':s'
0' :: 0':s'
b' :: a':b'
half' :: 0':s' → 0':s'
exp' :: 0':s' → 0':s'
double' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_a':b'2 :: a':b'
_gen_0':s'3 :: Nat → 0':s'
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
The following defined symbols remain to be analysed:
double', f', half', exp'
They will be analysed ascendingly in the following order:
half' < f'
exp' < f'
double' < half'
double' < exp'
Proved the following rewrite lemma:
double'(_gen_0':s'3(_n5)) → _gen_0':s'3(*(2, _n5)), rt ∈ Ω(1 + n5)
Induction Base:
double'(_gen_0':s'3(0)) →RΩ(1)
0'
Induction Step:
double'(_gen_0':s'3(+(_$n6, 1))) →RΩ(1)
s'(s'(double'(_gen_0':s'3(_$n6)))) →IH
s'(s'(_gen_0':s'3(*(2, _$n6))))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
tower'(x) → f'(a', x, s'(0'))
f'(a', 0', y) → y
f'(a', s'(x), y) → f'(b', y, s'(x))
f'(b', y, x) → f'(a', half'(x), exp'(y))
exp'(0') → s'(0')
exp'(s'(x)) → double'(exp'(x))
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
half'(0') → double'(0')
half'(s'(0')) → half'(0')
half'(s'(s'(x))) → s'(half'(x))
Types:
tower' :: 0':s' → 0':s'
f' :: a':b' → 0':s' → 0':s' → 0':s'
a' :: a':b'
s' :: 0':s' → 0':s'
0' :: 0':s'
b' :: a':b'
half' :: 0':s' → 0':s'
exp' :: 0':s' → 0':s'
double' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_a':b'2 :: a':b'
_gen_0':s'3 :: Nat → 0':s'
Lemmas:
double'(_gen_0':s'3(_n5)) → _gen_0':s'3(*(2, _n5)), rt ∈ Ω(1 + n5)
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
The following defined symbols remain to be analysed:
half', f', exp'
They will be analysed ascendingly in the following order:
half' < f'
exp' < f'
Proved the following rewrite lemma:
half'(_gen_0':s'3(*(2, _n351))) → _gen_0':s'3(_n351), rt ∈ Ω(1 + n351)
Induction Base:
half'(_gen_0':s'3(*(2, 0))) →RΩ(1)
double'(0') →LΩ(1)
_gen_0':s'3(*(2, 0))
Induction Step:
half'(_gen_0':s'3(*(2, +(_$n352, 1)))) →RΩ(1)
s'(half'(_gen_0':s'3(*(2, _$n352)))) →IH
s'(_gen_0':s'3(_$n352))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
tower'(x) → f'(a', x, s'(0'))
f'(a', 0', y) → y
f'(a', s'(x), y) → f'(b', y, s'(x))
f'(b', y, x) → f'(a', half'(x), exp'(y))
exp'(0') → s'(0')
exp'(s'(x)) → double'(exp'(x))
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
half'(0') → double'(0')
half'(s'(0')) → half'(0')
half'(s'(s'(x))) → s'(half'(x))
Types:
tower' :: 0':s' → 0':s'
f' :: a':b' → 0':s' → 0':s' → 0':s'
a' :: a':b'
s' :: 0':s' → 0':s'
0' :: 0':s'
b' :: a':b'
half' :: 0':s' → 0':s'
exp' :: 0':s' → 0':s'
double' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_a':b'2 :: a':b'
_gen_0':s'3 :: Nat → 0':s'
Lemmas:
double'(_gen_0':s'3(_n5)) → _gen_0':s'3(*(2, _n5)), rt ∈ Ω(1 + n5)
half'(_gen_0':s'3(*(2, _n351))) → _gen_0':s'3(_n351), rt ∈ Ω(1 + n351)
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
The following defined symbols remain to be analysed:
exp', f'
They will be analysed ascendingly in the following order:
exp' < f'
Proved the following rewrite lemma:
exp'(_gen_0':s'3(+(1, _n984))) → _*4, rt ∈ Ω(n984)
Induction Base:
exp'(_gen_0':s'3(+(1, 0)))
Induction Step:
exp'(_gen_0':s'3(+(1, +(_$n985, 1)))) →RΩ(1)
double'(exp'(_gen_0':s'3(+(1, _$n985)))) →IH
double'(_*4)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
tower'(x) → f'(a', x, s'(0'))
f'(a', 0', y) → y
f'(a', s'(x), y) → f'(b', y, s'(x))
f'(b', y, x) → f'(a', half'(x), exp'(y))
exp'(0') → s'(0')
exp'(s'(x)) → double'(exp'(x))
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
half'(0') → double'(0')
half'(s'(0')) → half'(0')
half'(s'(s'(x))) → s'(half'(x))
Types:
tower' :: 0':s' → 0':s'
f' :: a':b' → 0':s' → 0':s' → 0':s'
a' :: a':b'
s' :: 0':s' → 0':s'
0' :: 0':s'
b' :: a':b'
half' :: 0':s' → 0':s'
exp' :: 0':s' → 0':s'
double' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_a':b'2 :: a':b'
_gen_0':s'3 :: Nat → 0':s'
Lemmas:
double'(_gen_0':s'3(_n5)) → _gen_0':s'3(*(2, _n5)), rt ∈ Ω(1 + n5)
half'(_gen_0':s'3(*(2, _n351))) → _gen_0':s'3(_n351), rt ∈ Ω(1 + n351)
exp'(_gen_0':s'3(+(1, _n984))) → _*4, rt ∈ Ω(n984)
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
The following defined symbols remain to be analysed:
f'
Could not prove a rewrite lemma for the defined symbol f'.
Rules:
tower'(x) → f'(a', x, s'(0'))
f'(a', 0', y) → y
f'(a', s'(x), y) → f'(b', y, s'(x))
f'(b', y, x) → f'(a', half'(x), exp'(y))
exp'(0') → s'(0')
exp'(s'(x)) → double'(exp'(x))
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
half'(0') → double'(0')
half'(s'(0')) → half'(0')
half'(s'(s'(x))) → s'(half'(x))
Types:
tower' :: 0':s' → 0':s'
f' :: a':b' → 0':s' → 0':s' → 0':s'
a' :: a':b'
s' :: 0':s' → 0':s'
0' :: 0':s'
b' :: a':b'
half' :: 0':s' → 0':s'
exp' :: 0':s' → 0':s'
double' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_a':b'2 :: a':b'
_gen_0':s'3 :: Nat → 0':s'
Lemmas:
double'(_gen_0':s'3(_n5)) → _gen_0':s'3(*(2, _n5)), rt ∈ Ω(1 + n5)
half'(_gen_0':s'3(*(2, _n351))) → _gen_0':s'3(_n351), rt ∈ Ω(1 + n351)
exp'(_gen_0':s'3(+(1, _n984))) → _*4, rt ∈ Ω(n984)
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
double'(_gen_0':s'3(_n5)) → _gen_0':s'3(*(2, _n5)), rt ∈ Ω(1 + n5)