f_0(x) → a
f_1(x) → g_1(x, x)
g_1(s(x), y) → b(f_0(y), g_1(x, y))
f_2(x) → g_2(x, x)
g_2(s(x), y) → b(f_1(y), g_2(x, y))
f_3(x) → g_3(x, x)
g_3(s(x), y) → b(f_2(y), g_3(x, y))
f_4(x) → g_4(x, x)
g_4(s(x), y) → b(f_3(y), g_4(x, y))
f_5(x) → g_5(x, x)
g_5(s(x), y) → b(f_4(y), g_5(x, y))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
f_0'(x) → a'
f_1'(x) → g_1'(x, x)
g_1'(s'(x), y) → b'(f_0'(y), g_1'(x, y))
f_2'(x) → g_2'(x, x)
g_2'(s'(x), y) → b'(f_1'(y), g_2'(x, y))
f_3'(x) → g_3'(x, x)
g_3'(s'(x), y) → b'(f_2'(y), g_3'(x, y))
f_4'(x) → g_4'(x, x)
g_4'(s'(x), y) → b'(f_3'(y), g_4'(x, y))
f_5'(x) → g_5'(x, x)
g_5'(s'(x), y) → b'(f_4'(y), g_5'(x, y))
Sliced the following arguments:
f_0'/0
g_1'/1
Runtime Complexity TRS:
The TRS R consists of the following rules:
f_0' → a'
f_1'(x) → g_1'(x)
g_1'(s'(x)) → b'(f_0', g_1'(x))
f_2'(x) → g_2'(x, x)
g_2'(s'(x), y) → b'(f_1'(y), g_2'(x, y))
f_3'(x) → g_3'(x, x)
g_3'(s'(x), y) → b'(f_2'(y), g_3'(x, y))
f_4'(x) → g_4'(x, x)
g_4'(s'(x), y) → b'(f_3'(y), g_4'(x, y))
f_5'(x) → g_5'(x, x)
g_5'(s'(x), y) → b'(f_4'(y), g_5'(x, y))
Infered types.
Rules:
f_0' → a'
f_1'(x) → g_1'(x)
g_1'(s'(x)) → b'(f_0', g_1'(x))
f_2'(x) → g_2'(x, x)
g_2'(s'(x), y) → b'(f_1'(y), g_2'(x, y))
f_3'(x) → g_3'(x, x)
g_3'(s'(x), y) → b'(f_2'(y), g_3'(x, y))
f_4'(x) → g_4'(x, x)
g_4'(s'(x), y) → b'(f_3'(y), g_4'(x, y))
f_5'(x) → g_5'(x, x)
g_5'(s'(x), y) → b'(f_4'(y), g_5'(x, y))
Types:
f_0' :: a':b'
a' :: a':b'
f_1' :: s' → a':b'
g_1' :: s' → a':b'
s' :: s' → s'
b' :: a':b' → a':b' → a':b'
f_2' :: s' → a':b'
g_2' :: s' → s' → a':b'
f_3' :: s' → a':b'
g_3' :: s' → s' → a':b'
f_4' :: s' → a':b'
g_4' :: s' → s' → a':b'
f_5' :: s' → a':b'
g_5' :: s' → s' → a':b'
_hole_a':b'1 :: a':b'
_hole_s'2 :: s'
_gen_a':b'3 :: Nat → a':b'
_gen_s'4 :: Nat → s'
Heuristically decided to analyse the following defined symbols:
g_1', g_2', g_3', g_4', g_5'
Rules:
f_0' → a'
f_1'(x) → g_1'(x)
g_1'(s'(x)) → b'(f_0', g_1'(x))
f_2'(x) → g_2'(x, x)
g_2'(s'(x), y) → b'(f_1'(y), g_2'(x, y))
f_3'(x) → g_3'(x, x)
g_3'(s'(x), y) → b'(f_2'(y), g_3'(x, y))
f_4'(x) → g_4'(x, x)
g_4'(s'(x), y) → b'(f_3'(y), g_4'(x, y))
f_5'(x) → g_5'(x, x)
g_5'(s'(x), y) → b'(f_4'(y), g_5'(x, y))
Types:
f_0' :: a':b'
a' :: a':b'
f_1' :: s' → a':b'
g_1' :: s' → a':b'
s' :: s' → s'
b' :: a':b' → a':b' → a':b'
f_2' :: s' → a':b'
g_2' :: s' → s' → a':b'
f_3' :: s' → a':b'
g_3' :: s' → s' → a':b'
f_4' :: s' → a':b'
g_4' :: s' → s' → a':b'
f_5' :: s' → a':b'
g_5' :: s' → s' → a':b'
_hole_a':b'1 :: a':b'
_hole_s'2 :: s'
_gen_a':b'3 :: Nat → a':b'
_gen_s'4 :: Nat → s'
Generator Equations:
_gen_a':b'3(0) ⇔ a'
_gen_a':b'3(+(x, 1)) ⇔ b'(a', _gen_a':b'3(x))
_gen_s'4(0) ⇔ _hole_s'2
_gen_s'4(+(x, 1)) ⇔ s'(_gen_s'4(x))
The following defined symbols remain to be analysed:
g_1', g_2', g_3', g_4', g_5'
Proved the following rewrite lemma:
g_1'(_gen_s'4(+(1, _n6))) → _*5, rt ∈ Ω(n6)
Induction Base:
g_1'(_gen_s'4(+(1, 0)))
Induction Step:
g_1'(_gen_s'4(+(1, +(_$n7, 1)))) →RΩ(1)
b'(f_0', g_1'(_gen_s'4(+(1, _$n7)))) →RΩ(1)
b'(a', g_1'(_gen_s'4(+(1, _$n7)))) →IH
b'(a', _*5)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
f_0' → a'
f_1'(x) → g_1'(x)
g_1'(s'(x)) → b'(f_0', g_1'(x))
f_2'(x) → g_2'(x, x)
g_2'(s'(x), y) → b'(f_1'(y), g_2'(x, y))
f_3'(x) → g_3'(x, x)
g_3'(s'(x), y) → b'(f_2'(y), g_3'(x, y))
f_4'(x) → g_4'(x, x)
g_4'(s'(x), y) → b'(f_3'(y), g_4'(x, y))
f_5'(x) → g_5'(x, x)
g_5'(s'(x), y) → b'(f_4'(y), g_5'(x, y))
Types:
f_0' :: a':b'
a' :: a':b'
f_1' :: s' → a':b'
g_1' :: s' → a':b'
s' :: s' → s'
b' :: a':b' → a':b' → a':b'
f_2' :: s' → a':b'
g_2' :: s' → s' → a':b'
f_3' :: s' → a':b'
g_3' :: s' → s' → a':b'
f_4' :: s' → a':b'
g_4' :: s' → s' → a':b'
f_5' :: s' → a':b'
g_5' :: s' → s' → a':b'
_hole_a':b'1 :: a':b'
_hole_s'2 :: s'
_gen_a':b'3 :: Nat → a':b'
_gen_s'4 :: Nat → s'
Lemmas:
g_1'(_gen_s'4(+(1, _n6))) → _*5, rt ∈ Ω(n6)
Generator Equations:
_gen_a':b'3(0) ⇔ a'
_gen_a':b'3(+(x, 1)) ⇔ b'(a', _gen_a':b'3(x))
_gen_s'4(0) ⇔ _hole_s'2
_gen_s'4(+(x, 1)) ⇔ s'(_gen_s'4(x))
The following defined symbols remain to be analysed:
g_2', g_3', g_4', g_5'
Could not prove a rewrite lemma for the defined symbol g_2'.
Rules:
f_0' → a'
f_1'(x) → g_1'(x)
g_1'(s'(x)) → b'(f_0', g_1'(x))
f_2'(x) → g_2'(x, x)
g_2'(s'(x), y) → b'(f_1'(y), g_2'(x, y))
f_3'(x) → g_3'(x, x)
g_3'(s'(x), y) → b'(f_2'(y), g_3'(x, y))
f_4'(x) → g_4'(x, x)
g_4'(s'(x), y) → b'(f_3'(y), g_4'(x, y))
f_5'(x) → g_5'(x, x)
g_5'(s'(x), y) → b'(f_4'(y), g_5'(x, y))
Types:
f_0' :: a':b'
a' :: a':b'
f_1' :: s' → a':b'
g_1' :: s' → a':b'
s' :: s' → s'
b' :: a':b' → a':b' → a':b'
f_2' :: s' → a':b'
g_2' :: s' → s' → a':b'
f_3' :: s' → a':b'
g_3' :: s' → s' → a':b'
f_4' :: s' → a':b'
g_4' :: s' → s' → a':b'
f_5' :: s' → a':b'
g_5' :: s' → s' → a':b'
_hole_a':b'1 :: a':b'
_hole_s'2 :: s'
_gen_a':b'3 :: Nat → a':b'
_gen_s'4 :: Nat → s'
Lemmas:
g_1'(_gen_s'4(+(1, _n6))) → _*5, rt ∈ Ω(n6)
Generator Equations:
_gen_a':b'3(0) ⇔ a'
_gen_a':b'3(+(x, 1)) ⇔ b'(a', _gen_a':b'3(x))
_gen_s'4(0) ⇔ _hole_s'2
_gen_s'4(+(x, 1)) ⇔ s'(_gen_s'4(x))
The following defined symbols remain to be analysed:
g_3', g_4', g_5'
Could not prove a rewrite lemma for the defined symbol g_3'.
Rules:
f_0' → a'
f_1'(x) → g_1'(x)
g_1'(s'(x)) → b'(f_0', g_1'(x))
f_2'(x) → g_2'(x, x)
g_2'(s'(x), y) → b'(f_1'(y), g_2'(x, y))
f_3'(x) → g_3'(x, x)
g_3'(s'(x), y) → b'(f_2'(y), g_3'(x, y))
f_4'(x) → g_4'(x, x)
g_4'(s'(x), y) → b'(f_3'(y), g_4'(x, y))
f_5'(x) → g_5'(x, x)
g_5'(s'(x), y) → b'(f_4'(y), g_5'(x, y))
Types:
f_0' :: a':b'
a' :: a':b'
f_1' :: s' → a':b'
g_1' :: s' → a':b'
s' :: s' → s'
b' :: a':b' → a':b' → a':b'
f_2' :: s' → a':b'
g_2' :: s' → s' → a':b'
f_3' :: s' → a':b'
g_3' :: s' → s' → a':b'
f_4' :: s' → a':b'
g_4' :: s' → s' → a':b'
f_5' :: s' → a':b'
g_5' :: s' → s' → a':b'
_hole_a':b'1 :: a':b'
_hole_s'2 :: s'
_gen_a':b'3 :: Nat → a':b'
_gen_s'4 :: Nat → s'
Lemmas:
g_1'(_gen_s'4(+(1, _n6))) → _*5, rt ∈ Ω(n6)
Generator Equations:
_gen_a':b'3(0) ⇔ a'
_gen_a':b'3(+(x, 1)) ⇔ b'(a', _gen_a':b'3(x))
_gen_s'4(0) ⇔ _hole_s'2
_gen_s'4(+(x, 1)) ⇔ s'(_gen_s'4(x))
The following defined symbols remain to be analysed:
g_4', g_5'
Could not prove a rewrite lemma for the defined symbol g_4'.
Rules:
f_0' → a'
f_1'(x) → g_1'(x)
g_1'(s'(x)) → b'(f_0', g_1'(x))
f_2'(x) → g_2'(x, x)
g_2'(s'(x), y) → b'(f_1'(y), g_2'(x, y))
f_3'(x) → g_3'(x, x)
g_3'(s'(x), y) → b'(f_2'(y), g_3'(x, y))
f_4'(x) → g_4'(x, x)
g_4'(s'(x), y) → b'(f_3'(y), g_4'(x, y))
f_5'(x) → g_5'(x, x)
g_5'(s'(x), y) → b'(f_4'(y), g_5'(x, y))
Types:
f_0' :: a':b'
a' :: a':b'
f_1' :: s' → a':b'
g_1' :: s' → a':b'
s' :: s' → s'
b' :: a':b' → a':b' → a':b'
f_2' :: s' → a':b'
g_2' :: s' → s' → a':b'
f_3' :: s' → a':b'
g_3' :: s' → s' → a':b'
f_4' :: s' → a':b'
g_4' :: s' → s' → a':b'
f_5' :: s' → a':b'
g_5' :: s' → s' → a':b'
_hole_a':b'1 :: a':b'
_hole_s'2 :: s'
_gen_a':b'3 :: Nat → a':b'
_gen_s'4 :: Nat → s'
Lemmas:
g_1'(_gen_s'4(+(1, _n6))) → _*5, rt ∈ Ω(n6)
Generator Equations:
_gen_a':b'3(0) ⇔ a'
_gen_a':b'3(+(x, 1)) ⇔ b'(a', _gen_a':b'3(x))
_gen_s'4(0) ⇔ _hole_s'2
_gen_s'4(+(x, 1)) ⇔ s'(_gen_s'4(x))
The following defined symbols remain to be analysed:
g_5'
Could not prove a rewrite lemma for the defined symbol g_5'.
Rules:
f_0' → a'
f_1'(x) → g_1'(x)
g_1'(s'(x)) → b'(f_0', g_1'(x))
f_2'(x) → g_2'(x, x)
g_2'(s'(x), y) → b'(f_1'(y), g_2'(x, y))
f_3'(x) → g_3'(x, x)
g_3'(s'(x), y) → b'(f_2'(y), g_3'(x, y))
f_4'(x) → g_4'(x, x)
g_4'(s'(x), y) → b'(f_3'(y), g_4'(x, y))
f_5'(x) → g_5'(x, x)
g_5'(s'(x), y) → b'(f_4'(y), g_5'(x, y))
Types:
f_0' :: a':b'
a' :: a':b'
f_1' :: s' → a':b'
g_1' :: s' → a':b'
s' :: s' → s'
b' :: a':b' → a':b' → a':b'
f_2' :: s' → a':b'
g_2' :: s' → s' → a':b'
f_3' :: s' → a':b'
g_3' :: s' → s' → a':b'
f_4' :: s' → a':b'
g_4' :: s' → s' → a':b'
f_5' :: s' → a':b'
g_5' :: s' → s' → a':b'
_hole_a':b'1 :: a':b'
_hole_s'2 :: s'
_gen_a':b'3 :: Nat → a':b'
_gen_s'4 :: Nat → s'
Lemmas:
g_1'(_gen_s'4(+(1, _n6))) → _*5, rt ∈ Ω(n6)
Generator Equations:
_gen_a':b'3(0) ⇔ a'
_gen_a':b'3(+(x, 1)) ⇔ b'(a', _gen_a':b'3(x))
_gen_s'4(0) ⇔ _hole_s'2
_gen_s'4(+(x, 1)) ⇔ s'(_gen_s'4(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
g_1'(_gen_s'4(+(1, _n6))) → _*5, rt ∈ Ω(n6)