rev(nil) → nil
rev(++(x, y)) → ++(rev1(x, y), rev2(x, y))
rev1(x, nil) → x
rev1(x, ++(y, z)) → rev1(y, z)
rev2(x, nil) → nil
rev2(x, ++(y, z)) → rev(++(x, rev(rev2(y, z))))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
rev'(nil') → nil'
rev'(++'(x, y)) → ++'(rev1'(x, y), rev2'(x, y))
rev1'(x, nil') → x
rev1'(x, ++'(y, z)) → rev1'(y, z)
rev2'(x, nil') → nil'
rev2'(x, ++'(y, z)) → rev'(++'(x, rev'(rev2'(y, z))))
Infered types.
Rules:
rev'(nil') → nil'
rev'(++'(x, y)) → ++'(rev1'(x, y), rev2'(x, y))
rev1'(x, nil') → x
rev1'(x, ++'(y, z)) → rev1'(y, z)
rev2'(x, nil') → nil'
rev2'(x, ++'(y, z)) → rev'(++'(x, rev'(rev2'(y, z))))
Types:
rev' :: nil':++' → nil':++'
nil' :: nil':++'
++' :: rev1' → nil':++' → nil':++'
rev1' :: rev1' → nil':++' → rev1'
rev2' :: rev1' → nil':++' → nil':++'
_hole_nil':++'1 :: nil':++'
_hole_rev1'2 :: rev1'
_gen_nil':++'3 :: Nat → nil':++'
Heuristically decided to analyse the following defined symbols:
rev', rev1', rev2'
They will be analysed ascendingly in the following order:
rev1' < rev'
rev' = rev2'
Rules:
rev'(nil') → nil'
rev'(++'(x, y)) → ++'(rev1'(x, y), rev2'(x, y))
rev1'(x, nil') → x
rev1'(x, ++'(y, z)) → rev1'(y, z)
rev2'(x, nil') → nil'
rev2'(x, ++'(y, z)) → rev'(++'(x, rev'(rev2'(y, z))))
Types:
rev' :: nil':++' → nil':++'
nil' :: nil':++'
++' :: rev1' → nil':++' → nil':++'
rev1' :: rev1' → nil':++' → rev1'
rev2' :: rev1' → nil':++' → nil':++'
_hole_nil':++'1 :: nil':++'
_hole_rev1'2 :: rev1'
_gen_nil':++'3 :: Nat → nil':++'
Generator Equations:
_gen_nil':++'3(0) ⇔ nil'
_gen_nil':++'3(+(x, 1)) ⇔ ++'(_hole_rev1'2, _gen_nil':++'3(x))
The following defined symbols remain to be analysed:
rev1', rev', rev2'
They will be analysed ascendingly in the following order:
rev1' < rev'
rev' = rev2'
Proved the following rewrite lemma:
rev1'(_hole_rev1'2, _gen_nil':++'3(_n5)) → _hole_rev1'2, rt ∈ Ω(1 + n5)
Induction Base:
rev1'(_hole_rev1'2, _gen_nil':++'3(0)) →RΩ(1)
_hole_rev1'2
Induction Step:
rev1'(_hole_rev1'2, _gen_nil':++'3(+(_$n6, 1))) →RΩ(1)
rev1'(_hole_rev1'2, _gen_nil':++'3(_$n6)) →IH
_hole_rev1'2
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
rev'(nil') → nil'
rev'(++'(x, y)) → ++'(rev1'(x, y), rev2'(x, y))
rev1'(x, nil') → x
rev1'(x, ++'(y, z)) → rev1'(y, z)
rev2'(x, nil') → nil'
rev2'(x, ++'(y, z)) → rev'(++'(x, rev'(rev2'(y, z))))
Types:
rev' :: nil':++' → nil':++'
nil' :: nil':++'
++' :: rev1' → nil':++' → nil':++'
rev1' :: rev1' → nil':++' → rev1'
rev2' :: rev1' → nil':++' → nil':++'
_hole_nil':++'1 :: nil':++'
_hole_rev1'2 :: rev1'
_gen_nil':++'3 :: Nat → nil':++'
Lemmas:
rev1'(_hole_rev1'2, _gen_nil':++'3(_n5)) → _hole_rev1'2, rt ∈ Ω(1 + n5)
Generator Equations:
_gen_nil':++'3(0) ⇔ nil'
_gen_nil':++'3(+(x, 1)) ⇔ ++'(_hole_rev1'2, _gen_nil':++'3(x))
The following defined symbols remain to be analysed:
rev2', rev'
They will be analysed ascendingly in the following order:
rev' = rev2'
Proved the following rewrite lemma:
rev2'(_hole_rev1'2, _gen_nil':++'3(_n243)) → _*4, rt ∈ Ω(n243)
Induction Base:
rev2'(_hole_rev1'2, _gen_nil':++'3(0))
Induction Step:
rev2'(_hole_rev1'2, _gen_nil':++'3(+(_$n244, 1))) →RΩ(1)
rev'(++'(_hole_rev1'2, rev'(rev2'(_hole_rev1'2, _gen_nil':++'3(_$n244))))) →IH
rev'(++'(_hole_rev1'2, rev'(_*4)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
rev'(nil') → nil'
rev'(++'(x, y)) → ++'(rev1'(x, y), rev2'(x, y))
rev1'(x, nil') → x
rev1'(x, ++'(y, z)) → rev1'(y, z)
rev2'(x, nil') → nil'
rev2'(x, ++'(y, z)) → rev'(++'(x, rev'(rev2'(y, z))))
Types:
rev' :: nil':++' → nil':++'
nil' :: nil':++'
++' :: rev1' → nil':++' → nil':++'
rev1' :: rev1' → nil':++' → rev1'
rev2' :: rev1' → nil':++' → nil':++'
_hole_nil':++'1 :: nil':++'
_hole_rev1'2 :: rev1'
_gen_nil':++'3 :: Nat → nil':++'
Lemmas:
rev1'(_hole_rev1'2, _gen_nil':++'3(_n5)) → _hole_rev1'2, rt ∈ Ω(1 + n5)
rev2'(_hole_rev1'2, _gen_nil':++'3(_n243)) → _*4, rt ∈ Ω(n243)
Generator Equations:
_gen_nil':++'3(0) ⇔ nil'
_gen_nil':++'3(+(x, 1)) ⇔ ++'(_hole_rev1'2, _gen_nil':++'3(x))
The following defined symbols remain to be analysed:
rev'
They will be analysed ascendingly in the following order:
rev' = rev2'
Could not prove a rewrite lemma for the defined symbol rev'.
The following conjecture could not be proven:
rev'(_gen_nil':++'3(_n5559)) →? _gen_nil':++'3(_n5559)
Rules:
rev'(nil') → nil'
rev'(++'(x, y)) → ++'(rev1'(x, y), rev2'(x, y))
rev1'(x, nil') → x
rev1'(x, ++'(y, z)) → rev1'(y, z)
rev2'(x, nil') → nil'
rev2'(x, ++'(y, z)) → rev'(++'(x, rev'(rev2'(y, z))))
Types:
rev' :: nil':++' → nil':++'
nil' :: nil':++'
++' :: rev1' → nil':++' → nil':++'
rev1' :: rev1' → nil':++' → rev1'
rev2' :: rev1' → nil':++' → nil':++'
_hole_nil':++'1 :: nil':++'
_hole_rev1'2 :: rev1'
_gen_nil':++'3 :: Nat → nil':++'
Lemmas:
rev1'(_hole_rev1'2, _gen_nil':++'3(_n5)) → _hole_rev1'2, rt ∈ Ω(1 + n5)
rev2'(_hole_rev1'2, _gen_nil':++'3(_n243)) → _*4, rt ∈ Ω(n243)
Generator Equations:
_gen_nil':++'3(0) ⇔ nil'
_gen_nil':++'3(+(x, 1)) ⇔ ++'(_hole_rev1'2, _gen_nil':++'3(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
rev1'(_hole_rev1'2, _gen_nil':++'3(_n5)) → _hole_rev1'2, rt ∈ Ω(1 + n5)