f(nil) → nil
f(.(nil, y)) → .(nil, f(y))
f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(nil) → nil
g(.(x, nil)) → .(g(x), nil)
g(.(x, .(y, z))) → g(.(.(x, y), z))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
f'(nil') → nil'
f'(.'(nil', y)) → .'(nil', f'(y))
f'(.'(.'(x, y), z)) → f'(.'(x, .'(y, z)))
g'(nil') → nil'
g'(.'(x, nil')) → .'(g'(x), nil')
g'(.'(x, .'(y, z))) → g'(.'(.'(x, y), z))
Infered types.
Rules:
f'(nil') → nil'
f'(.'(nil', y)) → .'(nil', f'(y))
f'(.'(.'(x, y), z)) → f'(.'(x, .'(y, z)))
g'(nil') → nil'
g'(.'(x, nil')) → .'(g'(x), nil')
g'(.'(x, .'(y, z))) → g'(.'(.'(x, y), z))
Types:
f' :: nil':.' → nil':.'
nil' :: nil':.'
.' :: nil':.' → nil':.' → nil':.'
g' :: nil':.' → nil':.'
_hole_nil':.'1 :: nil':.'
_gen_nil':.'2 :: Nat → nil':.'
Heuristically decided to analyse the following defined symbols:
f', g'
Rules:
f'(nil') → nil'
f'(.'(nil', y)) → .'(nil', f'(y))
f'(.'(.'(x, y), z)) → f'(.'(x, .'(y, z)))
g'(nil') → nil'
g'(.'(x, nil')) → .'(g'(x), nil')
g'(.'(x, .'(y, z))) → g'(.'(.'(x, y), z))
Types:
f' :: nil':.' → nil':.'
nil' :: nil':.'
.' :: nil':.' → nil':.' → nil':.'
g' :: nil':.' → nil':.'
_hole_nil':.'1 :: nil':.'
_gen_nil':.'2 :: Nat → nil':.'
Generator Equations:
_gen_nil':.'2(0) ⇔ nil'
_gen_nil':.'2(+(x, 1)) ⇔ .'(nil', _gen_nil':.'2(x))
The following defined symbols remain to be analysed:
f', g'
Proved the following rewrite lemma:
f'(_gen_nil':.'2(_n4)) → _gen_nil':.'2(_n4), rt ∈ Ω(1 + n4)
Induction Base:
f'(_gen_nil':.'2(0)) →RΩ(1)
nil'
Induction Step:
f'(_gen_nil':.'2(+(_$n5, 1))) →RΩ(1)
.'(nil', f'(_gen_nil':.'2(_$n5))) →IH
.'(nil', _gen_nil':.'2(_$n5))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
f'(nil') → nil'
f'(.'(nil', y)) → .'(nil', f'(y))
f'(.'(.'(x, y), z)) → f'(.'(x, .'(y, z)))
g'(nil') → nil'
g'(.'(x, nil')) → .'(g'(x), nil')
g'(.'(x, .'(y, z))) → g'(.'(.'(x, y), z))
Types:
f' :: nil':.' → nil':.'
nil' :: nil':.'
.' :: nil':.' → nil':.' → nil':.'
g' :: nil':.' → nil':.'
_hole_nil':.'1 :: nil':.'
_gen_nil':.'2 :: Nat → nil':.'
Lemmas:
f'(_gen_nil':.'2(_n4)) → _gen_nil':.'2(_n4), rt ∈ Ω(1 + n4)
Generator Equations:
_gen_nil':.'2(0) ⇔ nil'
_gen_nil':.'2(+(x, 1)) ⇔ .'(nil', _gen_nil':.'2(x))
The following defined symbols remain to be analysed:
g'
Could not prove a rewrite lemma for the defined symbol g'.
The following conjecture could not be proven:
g'(_gen_nil':.'2(+(2, _n334))) →? _*3
Rules:
f'(nil') → nil'
f'(.'(nil', y)) → .'(nil', f'(y))
f'(.'(.'(x, y), z)) → f'(.'(x, .'(y, z)))
g'(nil') → nil'
g'(.'(x, nil')) → .'(g'(x), nil')
g'(.'(x, .'(y, z))) → g'(.'(.'(x, y), z))
Types:
f' :: nil':.' → nil':.'
nil' :: nil':.'
.' :: nil':.' → nil':.' → nil':.'
g' :: nil':.' → nil':.'
_hole_nil':.'1 :: nil':.'
_gen_nil':.'2 :: Nat → nil':.'
Lemmas:
f'(_gen_nil':.'2(_n4)) → _gen_nil':.'2(_n4), rt ∈ Ω(1 + n4)
Generator Equations:
_gen_nil':.'2(0) ⇔ nil'
_gen_nil':.'2(+(x, 1)) ⇔ .'(nil', _gen_nil':.'2(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
f'(_gen_nil':.'2(_n4)) → _gen_nil':.'2(_n4), rt ∈ Ω(1 + n4)