norm(nil) → 0
norm(g(x, y)) → s(norm(x))
f(x, nil) → g(nil, x)
f(x, g(y, z)) → g(f(x, y), z)
rem(nil, y) → nil
rem(g(x, y), 0) → g(x, y)
rem(g(x, y), s(z)) → rem(x, z)
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
norm'(nil') → 0'
norm'(g'(x, y)) → s'(norm'(x))
f'(x, nil') → g'(nil', x)
f'(x, g'(y, z)) → g'(f'(x, y), z)
rem'(nil', y) → nil'
rem'(g'(x, y), 0') → g'(x, y)
rem'(g'(x, y), s'(z)) → rem'(x, z)
Sliced the following arguments:
g'/1
f'/0
Runtime Complexity TRS:
The TRS R consists of the following rules:
norm'(nil') → 0'
norm'(g'(x)) → s'(norm'(x))
f'(nil') → g'(nil')
f'(g'(y)) → g'(f'(y))
rem'(nil', y) → nil'
rem'(g'(x), 0') → g'(x)
rem'(g'(x), s'(z)) → rem'(x, z)
Infered types.
Rules:
norm'(nil') → 0'
norm'(g'(x)) → s'(norm'(x))
f'(nil') → g'(nil')
f'(g'(y)) → g'(f'(y))
rem'(nil', y) → nil'
rem'(g'(x), 0') → g'(x)
rem'(g'(x), s'(z)) → rem'(x, z)
Types:
norm' :: nil':g' → 0':s'
nil' :: nil':g'
0' :: 0':s'
g' :: nil':g' → nil':g'
s' :: 0':s' → 0':s'
f' :: nil':g' → nil':g'
rem' :: nil':g' → 0':s' → nil':g'
_hole_0':s'1 :: 0':s'
_hole_nil':g'2 :: nil':g'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil':g'4 :: Nat → nil':g'
Heuristically decided to analyse the following defined symbols:
norm', f', rem'
Rules:
norm'(nil') → 0'
norm'(g'(x)) → s'(norm'(x))
f'(nil') → g'(nil')
f'(g'(y)) → g'(f'(y))
rem'(nil', y) → nil'
rem'(g'(x), 0') → g'(x)
rem'(g'(x), s'(z)) → rem'(x, z)
Types:
norm' :: nil':g' → 0':s'
nil' :: nil':g'
0' :: 0':s'
g' :: nil':g' → nil':g'
s' :: 0':s' → 0':s'
f' :: nil':g' → nil':g'
rem' :: nil':g' → 0':s' → nil':g'
_hole_0':s'1 :: 0':s'
_hole_nil':g'2 :: nil':g'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil':g'4 :: Nat → nil':g'
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil':g'4(0) ⇔ nil'
_gen_nil':g'4(+(x, 1)) ⇔ g'(_gen_nil':g'4(x))
The following defined symbols remain to be analysed:
norm', f', rem'
Proved the following rewrite lemma:
norm'(_gen_nil':g'4(_n6)) → _gen_0':s'3(_n6), rt ∈ Ω(1 + n6)
Induction Base:
norm'(_gen_nil':g'4(0)) →RΩ(1)
0'
Induction Step:
norm'(_gen_nil':g'4(+(_$n7, 1))) →RΩ(1)
s'(norm'(_gen_nil':g'4(_$n7))) →IH
s'(_gen_0':s'3(_$n7))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
norm'(nil') → 0'
norm'(g'(x)) → s'(norm'(x))
f'(nil') → g'(nil')
f'(g'(y)) → g'(f'(y))
rem'(nil', y) → nil'
rem'(g'(x), 0') → g'(x)
rem'(g'(x), s'(z)) → rem'(x, z)
Types:
norm' :: nil':g' → 0':s'
nil' :: nil':g'
0' :: 0':s'
g' :: nil':g' → nil':g'
s' :: 0':s' → 0':s'
f' :: nil':g' → nil':g'
rem' :: nil':g' → 0':s' → nil':g'
_hole_0':s'1 :: 0':s'
_hole_nil':g'2 :: nil':g'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil':g'4 :: Nat → nil':g'
Lemmas:
norm'(_gen_nil':g'4(_n6)) → _gen_0':s'3(_n6), rt ∈ Ω(1 + n6)
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil':g'4(0) ⇔ nil'
_gen_nil':g'4(+(x, 1)) ⇔ g'(_gen_nil':g'4(x))
The following defined symbols remain to be analysed:
f', rem'
Proved the following rewrite lemma:
f'(_gen_nil':g'4(_n228)) → _gen_nil':g'4(+(1, _n228)), rt ∈ Ω(1 + n228)
Induction Base:
f'(_gen_nil':g'4(0)) →RΩ(1)
g'(nil')
Induction Step:
f'(_gen_nil':g'4(+(_$n229, 1))) →RΩ(1)
g'(f'(_gen_nil':g'4(_$n229))) →IH
g'(_gen_nil':g'4(+(1, _$n229)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
norm'(nil') → 0'
norm'(g'(x)) → s'(norm'(x))
f'(nil') → g'(nil')
f'(g'(y)) → g'(f'(y))
rem'(nil', y) → nil'
rem'(g'(x), 0') → g'(x)
rem'(g'(x), s'(z)) → rem'(x, z)
Types:
norm' :: nil':g' → 0':s'
nil' :: nil':g'
0' :: 0':s'
g' :: nil':g' → nil':g'
s' :: 0':s' → 0':s'
f' :: nil':g' → nil':g'
rem' :: nil':g' → 0':s' → nil':g'
_hole_0':s'1 :: 0':s'
_hole_nil':g'2 :: nil':g'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil':g'4 :: Nat → nil':g'
Lemmas:
norm'(_gen_nil':g'4(_n6)) → _gen_0':s'3(_n6), rt ∈ Ω(1 + n6)
f'(_gen_nil':g'4(_n228)) → _gen_nil':g'4(+(1, _n228)), rt ∈ Ω(1 + n228)
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil':g'4(0) ⇔ nil'
_gen_nil':g'4(+(x, 1)) ⇔ g'(_gen_nil':g'4(x))
The following defined symbols remain to be analysed:
rem'
Proved the following rewrite lemma:
rem'(_gen_nil':g'4(_n525), _gen_0':s'3(_n525)) → _gen_nil':g'4(0), rt ∈ Ω(1 + n525)
Induction Base:
rem'(_gen_nil':g'4(0), _gen_0':s'3(0)) →RΩ(1)
nil'
Induction Step:
rem'(_gen_nil':g'4(+(_$n526, 1)), _gen_0':s'3(+(_$n526, 1))) →RΩ(1)
rem'(_gen_nil':g'4(_$n526), _gen_0':s'3(_$n526)) →IH
_gen_nil':g'4(0)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
norm'(nil') → 0'
norm'(g'(x)) → s'(norm'(x))
f'(nil') → g'(nil')
f'(g'(y)) → g'(f'(y))
rem'(nil', y) → nil'
rem'(g'(x), 0') → g'(x)
rem'(g'(x), s'(z)) → rem'(x, z)
Types:
norm' :: nil':g' → 0':s'
nil' :: nil':g'
0' :: 0':s'
g' :: nil':g' → nil':g'
s' :: 0':s' → 0':s'
f' :: nil':g' → nil':g'
rem' :: nil':g' → 0':s' → nil':g'
_hole_0':s'1 :: 0':s'
_hole_nil':g'2 :: nil':g'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil':g'4 :: Nat → nil':g'
Lemmas:
norm'(_gen_nil':g'4(_n6)) → _gen_0':s'3(_n6), rt ∈ Ω(1 + n6)
f'(_gen_nil':g'4(_n228)) → _gen_nil':g'4(+(1, _n228)), rt ∈ Ω(1 + n228)
rem'(_gen_nil':g'4(_n525), _gen_0':s'3(_n525)) → _gen_nil':g'4(0), rt ∈ Ω(1 + n525)
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil':g'4(0) ⇔ nil'
_gen_nil':g'4(+(x, 1)) ⇔ g'(_gen_nil':g'4(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
norm'(_gen_nil':g'4(_n6)) → _gen_0':s'3(_n6), rt ∈ Ω(1 + n6)