g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
f(s(x), y) → f(half(s(x)), double(y))
f(s(0), y) → y
id(x) → f(x, s(0))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
g'(x, 0') → 0'
g'(d', s'(x)) → s'(s'(g'(d', x)))
g'(h', s'(0')) → 0'
g'(h', s'(s'(x))) → s'(g'(h', x))
double'(x) → g'(d', x)
half'(x) → g'(h', x)
f'(s'(x), y) → f'(half'(s'(x)), double'(y))
f'(s'(0'), y) → y
id'(x) → f'(x, s'(0'))
Infered types.
Rules:
g'(x, 0') → 0'
g'(d', s'(x)) → s'(s'(g'(d', x)))
g'(h', s'(0')) → 0'
g'(h', s'(s'(x))) → s'(g'(h', x))
double'(x) → g'(d', x)
half'(x) → g'(h', x)
f'(s'(x), y) → f'(half'(s'(x)), double'(y))
f'(s'(0'), y) → y
id'(x) → f'(x, s'(0'))
Types:
g' :: d':h' → 0':s' → 0':s'
0' :: 0':s'
d' :: d':h'
s' :: 0':s' → 0':s'
h' :: d':h'
double' :: 0':s' → 0':s'
half' :: 0':s' → 0':s'
f' :: 0':s' → 0':s' → 0':s'
id' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_d':h'2 :: d':h'
_gen_0':s'3 :: Nat → 0':s'
Heuristically decided to analyse the following defined symbols:
g', f'
Rules:
g'(x, 0') → 0'
g'(d', s'(x)) → s'(s'(g'(d', x)))
g'(h', s'(0')) → 0'
g'(h', s'(s'(x))) → s'(g'(h', x))
double'(x) → g'(d', x)
half'(x) → g'(h', x)
f'(s'(x), y) → f'(half'(s'(x)), double'(y))
f'(s'(0'), y) → y
id'(x) → f'(x, s'(0'))
Types:
g' :: d':h' → 0':s' → 0':s'
0' :: 0':s'
d' :: d':h'
s' :: 0':s' → 0':s'
h' :: d':h'
double' :: 0':s' → 0':s'
half' :: 0':s' → 0':s'
f' :: 0':s' → 0':s' → 0':s'
id' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_d':h'2 :: d':h'
_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:
g', f'
Proved the following rewrite lemma:
g'(h', _gen_0':s'3(*(2, _n5))) → _gen_0':s'3(_n5), rt ∈ Ω(1 + n5)
Induction Base:
g'(h', _gen_0':s'3(*(2, 0))) →RΩ(1)
0'
Induction Step:
g'(h', _gen_0':s'3(*(2, +(_$n6, 1)))) →RΩ(1)
s'(g'(h', _gen_0':s'3(*(2, _$n6)))) →IH
s'(_gen_0':s'3(_$n6))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
g'(x, 0') → 0'
g'(d', s'(x)) → s'(s'(g'(d', x)))
g'(h', s'(0')) → 0'
g'(h', s'(s'(x))) → s'(g'(h', x))
double'(x) → g'(d', x)
half'(x) → g'(h', x)
f'(s'(x), y) → f'(half'(s'(x)), double'(y))
f'(s'(0'), y) → y
id'(x) → f'(x, s'(0'))
Types:
g' :: d':h' → 0':s' → 0':s'
0' :: 0':s'
d' :: d':h'
s' :: 0':s' → 0':s'
h' :: d':h'
double' :: 0':s' → 0':s'
half' :: 0':s' → 0':s'
f' :: 0':s' → 0':s' → 0':s'
id' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_d':h'2 :: d':h'
_gen_0':s'3 :: Nat → 0':s'
Lemmas:
g'(h', _gen_0':s'3(*(2, _n5))) → _gen_0':s'3(_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:
f'
Could not prove a rewrite lemma for the defined symbol f'.
Rules:
g'(x, 0') → 0'
g'(d', s'(x)) → s'(s'(g'(d', x)))
g'(h', s'(0')) → 0'
g'(h', s'(s'(x))) → s'(g'(h', x))
double'(x) → g'(d', x)
half'(x) → g'(h', x)
f'(s'(x), y) → f'(half'(s'(x)), double'(y))
f'(s'(0'), y) → y
id'(x) → f'(x, s'(0'))
Types:
g' :: d':h' → 0':s' → 0':s'
0' :: 0':s'
d' :: d':h'
s' :: 0':s' → 0':s'
h' :: d':h'
double' :: 0':s' → 0':s'
half' :: 0':s' → 0':s'
f' :: 0':s' → 0':s' → 0':s'
id' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_d':h'2 :: d':h'
_gen_0':s'3 :: Nat → 0':s'
Lemmas:
g'(h', _gen_0':s'3(*(2, _n5))) → _gen_0':s'3(_n5), rt ∈ Ω(1 + n5)
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:
g'(h', _gen_0':s'3(*(2, _n5))) → _gen_0':s'3(_n5), rt ∈ Ω(1 + n5)