f(s(X)) → f(X)
g(cons(0, Y)) → g(Y)
g(cons(s(X), Y)) → s(X)
h(cons(X, Y)) → h(g(cons(X, Y)))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
f'(s'(X)) → f'(X)
g'(cons'(0', Y)) → g'(Y)
g'(cons'(s'(X), Y)) → s'(X)
h'(cons'(X, Y)) → h'(g'(cons'(X, Y)))
Infered types.
Rules:
f'(s'(X)) → f'(X)
g'(cons'(0', Y)) → g'(Y)
g'(cons'(s'(X), Y)) → s'(X)
h'(cons'(X, Y)) → h'(g'(cons'(X, Y)))
Types:
f' :: s':0':cons' → f'
s' :: s':0':cons' → s':0':cons'
g' :: s':0':cons' → s':0':cons'
cons' :: s':0':cons' → s':0':cons' → s':0':cons'
0' :: s':0':cons'
h' :: s':0':cons' → h'
_hole_f'1 :: f'
_hole_s':0':cons'2 :: s':0':cons'
_hole_h'3 :: h'
_gen_s':0':cons'4 :: Nat → s':0':cons'
Heuristically decided to analyse the following defined symbols:
f', g', h'
They will be analysed ascendingly in the following order:
g' < h'
Rules:
f'(s'(X)) → f'(X)
g'(cons'(0', Y)) → g'(Y)
g'(cons'(s'(X), Y)) → s'(X)
h'(cons'(X, Y)) → h'(g'(cons'(X, Y)))
Types:
f' :: s':0':cons' → f'
s' :: s':0':cons' → s':0':cons'
g' :: s':0':cons' → s':0':cons'
cons' :: s':0':cons' → s':0':cons' → s':0':cons'
0' :: s':0':cons'
h' :: s':0':cons' → h'
_hole_f'1 :: f'
_hole_s':0':cons'2 :: s':0':cons'
_hole_h'3 :: h'
_gen_s':0':cons'4 :: Nat → s':0':cons'
Generator Equations:
_gen_s':0':cons'4(0) ⇔ 0'
_gen_s':0':cons'4(+(x, 1)) ⇔ s'(_gen_s':0':cons'4(x))
The following defined symbols remain to be analysed:
f', g', h'
They will be analysed ascendingly in the following order:
g' < h'
Proved the following rewrite lemma:
f'(_gen_s':0':cons'4(+(1, _n6))) → _*5, rt ∈ Ω(n6)
Induction Base:
f'(_gen_s':0':cons'4(+(1, 0)))
Induction Step:
f'(_gen_s':0':cons'4(+(1, +(_$n7, 1)))) →RΩ(1)
f'(_gen_s':0':cons'4(+(1, _$n7))) →IH
_*5
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
f'(s'(X)) → f'(X)
g'(cons'(0', Y)) → g'(Y)
g'(cons'(s'(X), Y)) → s'(X)
h'(cons'(X, Y)) → h'(g'(cons'(X, Y)))
Types:
f' :: s':0':cons' → f'
s' :: s':0':cons' → s':0':cons'
g' :: s':0':cons' → s':0':cons'
cons' :: s':0':cons' → s':0':cons' → s':0':cons'
0' :: s':0':cons'
h' :: s':0':cons' → h'
_hole_f'1 :: f'
_hole_s':0':cons'2 :: s':0':cons'
_hole_h'3 :: h'
_gen_s':0':cons'4 :: Nat → s':0':cons'
Lemmas:
f'(_gen_s':0':cons'4(+(1, _n6))) → _*5, rt ∈ Ω(n6)
Generator Equations:
_gen_s':0':cons'4(0) ⇔ 0'
_gen_s':0':cons'4(+(x, 1)) ⇔ s'(_gen_s':0':cons'4(x))
The following defined symbols remain to be analysed:
g', h'
They will be analysed ascendingly in the following order:
g' < h'
Could not prove a rewrite lemma for the defined symbol g'.
Rules:
f'(s'(X)) → f'(X)
g'(cons'(0', Y)) → g'(Y)
g'(cons'(s'(X), Y)) → s'(X)
h'(cons'(X, Y)) → h'(g'(cons'(X, Y)))
Types:
f' :: s':0':cons' → f'
s' :: s':0':cons' → s':0':cons'
g' :: s':0':cons' → s':0':cons'
cons' :: s':0':cons' → s':0':cons' → s':0':cons'
0' :: s':0':cons'
h' :: s':0':cons' → h'
_hole_f'1 :: f'
_hole_s':0':cons'2 :: s':0':cons'
_hole_h'3 :: h'
_gen_s':0':cons'4 :: Nat → s':0':cons'
Lemmas:
f'(_gen_s':0':cons'4(+(1, _n6))) → _*5, rt ∈ Ω(n6)
Generator Equations:
_gen_s':0':cons'4(0) ⇔ 0'
_gen_s':0':cons'4(+(x, 1)) ⇔ s'(_gen_s':0':cons'4(x))
The following defined symbols remain to be analysed:
h'
Could not prove a rewrite lemma for the defined symbol h'.
Rules:
f'(s'(X)) → f'(X)
g'(cons'(0', Y)) → g'(Y)
g'(cons'(s'(X), Y)) → s'(X)
h'(cons'(X, Y)) → h'(g'(cons'(X, Y)))
Types:
f' :: s':0':cons' → f'
s' :: s':0':cons' → s':0':cons'
g' :: s':0':cons' → s':0':cons'
cons' :: s':0':cons' → s':0':cons' → s':0':cons'
0' :: s':0':cons'
h' :: s':0':cons' → h'
_hole_f'1 :: f'
_hole_s':0':cons'2 :: s':0':cons'
_hole_h'3 :: h'
_gen_s':0':cons'4 :: Nat → s':0':cons'
Lemmas:
f'(_gen_s':0':cons'4(+(1, _n6))) → _*5, rt ∈ Ω(n6)
Generator Equations:
_gen_s':0':cons'4(0) ⇔ 0'
_gen_s':0':cons'4(+(x, 1)) ⇔ s'(_gen_s':0':cons'4(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
f'(_gen_s':0':cons'4(+(1, _n6))) → _*5, rt ∈ Ω(n6)