last(nil) → 0
last(cons(x, nil)) → x
last(cons(x, cons(y, xs))) → last(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
reverse(nil) → nil
reverse(cons(x, xs)) → cons(last(cons(x, xs)), reverse(del(last(cons(x, xs)), cons(x, xs))))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
last'(nil') → 0'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, xs))) → last'(cons'(y, xs))
del'(x, nil') → nil'
del'(x, cons'(y, xs)) → if'(eq'(x, y), x, y, xs)
if'(true', x, y, xs) → xs
if'(false', x, y, xs) → cons'(y, del'(x, xs))
eq'(0', 0') → true'
eq'(0', s'(y)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
reverse'(nil') → nil'
reverse'(cons'(x, xs)) → cons'(last'(cons'(x, xs)), reverse'(del'(last'(cons'(x, xs)), cons'(x, xs))))
Infered types.
Rules:
last'(nil') → 0'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, xs))) → last'(cons'(y, xs))
del'(x, nil') → nil'
del'(x, cons'(y, xs)) → if'(eq'(x, y), x, y, xs)
if'(true', x, y, xs) → xs
if'(false', x, y, xs) → cons'(y, del'(x, xs))
eq'(0', 0') → true'
eq'(0', s'(y)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
reverse'(nil') → nil'
reverse'(cons'(x, xs)) → cons'(last'(cons'(x, xs)), reverse'(del'(last'(cons'(x, xs)), cons'(x, xs))))
Types:
last' :: nil':cons' → 0':s'
nil' :: nil':cons'
0' :: 0':s'
cons' :: 0':s' → nil':cons' → nil':cons'
del' :: 0':s' → nil':cons' → nil':cons'
if' :: true':false' → 0':s' → 0':s' → nil':cons' → nil':cons'
eq' :: 0':s' → 0':s' → true':false'
true' :: true':false'
false' :: true':false'
s' :: 0':s' → 0':s'
reverse' :: nil':cons' → nil':cons'
_hole_0':s'1 :: 0':s'
_hole_nil':cons'2 :: nil':cons'
_hole_true':false'3 :: true':false'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':cons'5 :: Nat → nil':cons'
Heuristically decided to analyse the following defined symbols:
last', del', eq', reverse'
They will be analysed ascendingly in the following order:
last' < reverse'
eq' < del'
del' < reverse'
Rules:
last'(nil') → 0'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, xs))) → last'(cons'(y, xs))
del'(x, nil') → nil'
del'(x, cons'(y, xs)) → if'(eq'(x, y), x, y, xs)
if'(true', x, y, xs) → xs
if'(false', x, y, xs) → cons'(y, del'(x, xs))
eq'(0', 0') → true'
eq'(0', s'(y)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
reverse'(nil') → nil'
reverse'(cons'(x, xs)) → cons'(last'(cons'(x, xs)), reverse'(del'(last'(cons'(x, xs)), cons'(x, xs))))
Types:
last' :: nil':cons' → 0':s'
nil' :: nil':cons'
0' :: 0':s'
cons' :: 0':s' → nil':cons' → nil':cons'
del' :: 0':s' → nil':cons' → nil':cons'
if' :: true':false' → 0':s' → 0':s' → nil':cons' → nil':cons'
eq' :: 0':s' → 0':s' → true':false'
true' :: true':false'
false' :: true':false'
s' :: 0':s' → 0':s'
reverse' :: nil':cons' → nil':cons'
_hole_0':s'1 :: 0':s'
_hole_nil':cons'2 :: nil':cons'
_hole_true':false'3 :: true':false'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':cons'5 :: Nat → nil':cons'
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_nil':cons'5(0) ⇔ nil'
_gen_nil':cons'5(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'5(x))
The following defined symbols remain to be analysed:
last', del', eq', reverse'
They will be analysed ascendingly in the following order:
last' < reverse'
eq' < del'
del' < reverse'
Proved the following rewrite lemma:
last'(_gen_nil':cons'5(+(1, _n7))) → _gen_0':s'4(0), rt ∈ Ω(1 + n7)
Induction Base:
last'(_gen_nil':cons'5(+(1, 0))) →RΩ(1)
0'
Induction Step:
last'(_gen_nil':cons'5(+(1, +(_$n8, 1)))) →RΩ(1)
last'(cons'(0', _gen_nil':cons'5(_$n8))) →IH
_gen_0':s'4(0)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
last'(nil') → 0'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, xs))) → last'(cons'(y, xs))
del'(x, nil') → nil'
del'(x, cons'(y, xs)) → if'(eq'(x, y), x, y, xs)
if'(true', x, y, xs) → xs
if'(false', x, y, xs) → cons'(y, del'(x, xs))
eq'(0', 0') → true'
eq'(0', s'(y)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
reverse'(nil') → nil'
reverse'(cons'(x, xs)) → cons'(last'(cons'(x, xs)), reverse'(del'(last'(cons'(x, xs)), cons'(x, xs))))
Types:
last' :: nil':cons' → 0':s'
nil' :: nil':cons'
0' :: 0':s'
cons' :: 0':s' → nil':cons' → nil':cons'
del' :: 0':s' → nil':cons' → nil':cons'
if' :: true':false' → 0':s' → 0':s' → nil':cons' → nil':cons'
eq' :: 0':s' → 0':s' → true':false'
true' :: true':false'
false' :: true':false'
s' :: 0':s' → 0':s'
reverse' :: nil':cons' → nil':cons'
_hole_0':s'1 :: 0':s'
_hole_nil':cons'2 :: nil':cons'
_hole_true':false'3 :: true':false'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':cons'5 :: Nat → nil':cons'
Lemmas:
last'(_gen_nil':cons'5(+(1, _n7))) → _gen_0':s'4(0), rt ∈ Ω(1 + n7)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_nil':cons'5(0) ⇔ nil'
_gen_nil':cons'5(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'5(x))
The following defined symbols remain to be analysed:
eq', del', reverse'
They will be analysed ascendingly in the following order:
eq' < del'
del' < reverse'
Proved the following rewrite lemma:
eq'(_gen_0':s'4(_n643), _gen_0':s'4(_n643)) → true', rt ∈ Ω(1 + n643)
Induction Base:
eq'(_gen_0':s'4(0), _gen_0':s'4(0)) →RΩ(1)
true'
Induction Step:
eq'(_gen_0':s'4(+(_$n644, 1)), _gen_0':s'4(+(_$n644, 1))) →RΩ(1)
eq'(_gen_0':s'4(_$n644), _gen_0':s'4(_$n644)) →IH
true'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
last'(nil') → 0'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, xs))) → last'(cons'(y, xs))
del'(x, nil') → nil'
del'(x, cons'(y, xs)) → if'(eq'(x, y), x, y, xs)
if'(true', x, y, xs) → xs
if'(false', x, y, xs) → cons'(y, del'(x, xs))
eq'(0', 0') → true'
eq'(0', s'(y)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
reverse'(nil') → nil'
reverse'(cons'(x, xs)) → cons'(last'(cons'(x, xs)), reverse'(del'(last'(cons'(x, xs)), cons'(x, xs))))
Types:
last' :: nil':cons' → 0':s'
nil' :: nil':cons'
0' :: 0':s'
cons' :: 0':s' → nil':cons' → nil':cons'
del' :: 0':s' → nil':cons' → nil':cons'
if' :: true':false' → 0':s' → 0':s' → nil':cons' → nil':cons'
eq' :: 0':s' → 0':s' → true':false'
true' :: true':false'
false' :: true':false'
s' :: 0':s' → 0':s'
reverse' :: nil':cons' → nil':cons'
_hole_0':s'1 :: 0':s'
_hole_nil':cons'2 :: nil':cons'
_hole_true':false'3 :: true':false'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':cons'5 :: Nat → nil':cons'
Lemmas:
last'(_gen_nil':cons'5(+(1, _n7))) → _gen_0':s'4(0), rt ∈ Ω(1 + n7)
eq'(_gen_0':s'4(_n643), _gen_0':s'4(_n643)) → true', rt ∈ Ω(1 + n643)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_nil':cons'5(0) ⇔ nil'
_gen_nil':cons'5(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'5(x))
The following defined symbols remain to be analysed:
del', reverse'
They will be analysed ascendingly in the following order:
del' < reverse'
Could not prove a rewrite lemma for the defined symbol del'.
Rules:
last'(nil') → 0'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, xs))) → last'(cons'(y, xs))
del'(x, nil') → nil'
del'(x, cons'(y, xs)) → if'(eq'(x, y), x, y, xs)
if'(true', x, y, xs) → xs
if'(false', x, y, xs) → cons'(y, del'(x, xs))
eq'(0', 0') → true'
eq'(0', s'(y)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
reverse'(nil') → nil'
reverse'(cons'(x, xs)) → cons'(last'(cons'(x, xs)), reverse'(del'(last'(cons'(x, xs)), cons'(x, xs))))
Types:
last' :: nil':cons' → 0':s'
nil' :: nil':cons'
0' :: 0':s'
cons' :: 0':s' → nil':cons' → nil':cons'
del' :: 0':s' → nil':cons' → nil':cons'
if' :: true':false' → 0':s' → 0':s' → nil':cons' → nil':cons'
eq' :: 0':s' → 0':s' → true':false'
true' :: true':false'
false' :: true':false'
s' :: 0':s' → 0':s'
reverse' :: nil':cons' → nil':cons'
_hole_0':s'1 :: 0':s'
_hole_nil':cons'2 :: nil':cons'
_hole_true':false'3 :: true':false'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':cons'5 :: Nat → nil':cons'
Lemmas:
last'(_gen_nil':cons'5(+(1, _n7))) → _gen_0':s'4(0), rt ∈ Ω(1 + n7)
eq'(_gen_0':s'4(_n643), _gen_0':s'4(_n643)) → true', rt ∈ Ω(1 + n643)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_nil':cons'5(0) ⇔ nil'
_gen_nil':cons'5(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'5(x))
The following defined symbols remain to be analysed:
reverse'
Proved the following rewrite lemma:
reverse'(_gen_nil':cons'5(_n1582)) → _gen_nil':cons'5(_n1582), rt ∈ Ω(1 + n1582 + n15822)
Induction Base:
reverse'(_gen_nil':cons'5(0)) →RΩ(1)
nil'
Induction Step:
reverse'(_gen_nil':cons'5(+(_$n1583, 1))) →RΩ(1)
cons'(last'(cons'(0', _gen_nil':cons'5(_$n1583))), reverse'(del'(last'(cons'(0', _gen_nil':cons'5(_$n1583))), cons'(0', _gen_nil':cons'5(_$n1583))))) →LΩ(1 + $n1583)
cons'(_gen_0':s'4(0), reverse'(del'(last'(cons'(0', _gen_nil':cons'5(_$n1583))), cons'(0', _gen_nil':cons'5(_$n1583))))) →LΩ(1 + $n1583)
cons'(_gen_0':s'4(0), reverse'(del'(_gen_0':s'4(0), cons'(0', _gen_nil':cons'5(_$n1583))))) →RΩ(1)
cons'(_gen_0':s'4(0), reverse'(if'(eq'(_gen_0':s'4(0), 0'), _gen_0':s'4(0), 0', _gen_nil':cons'5(_$n1583)))) →LΩ(1)
cons'(_gen_0':s'4(0), reverse'(if'(true', _gen_0':s'4(0), 0', _gen_nil':cons'5(_$n1583)))) →RΩ(1)
cons'(_gen_0':s'4(0), reverse'(_gen_nil':cons'5(_$n1583))) →IH
cons'(_gen_0':s'4(0), _gen_nil':cons'5(_$n1583))
We have rt ∈ Ω(n2) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n2).
Rules:
last'(nil') → 0'
last'(cons'(x, nil')) → x
last'(cons'(x, cons'(y, xs))) → last'(cons'(y, xs))
del'(x, nil') → nil'
del'(x, cons'(y, xs)) → if'(eq'(x, y), x, y, xs)
if'(true', x, y, xs) → xs
if'(false', x, y, xs) → cons'(y, del'(x, xs))
eq'(0', 0') → true'
eq'(0', s'(y)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
reverse'(nil') → nil'
reverse'(cons'(x, xs)) → cons'(last'(cons'(x, xs)), reverse'(del'(last'(cons'(x, xs)), cons'(x, xs))))
Types:
last' :: nil':cons' → 0':s'
nil' :: nil':cons'
0' :: 0':s'
cons' :: 0':s' → nil':cons' → nil':cons'
del' :: 0':s' → nil':cons' → nil':cons'
if' :: true':false' → 0':s' → 0':s' → nil':cons' → nil':cons'
eq' :: 0':s' → 0':s' → true':false'
true' :: true':false'
false' :: true':false'
s' :: 0':s' → 0':s'
reverse' :: nil':cons' → nil':cons'
_hole_0':s'1 :: 0':s'
_hole_nil':cons'2 :: nil':cons'
_hole_true':false'3 :: true':false'
_gen_0':s'4 :: Nat → 0':s'
_gen_nil':cons'5 :: Nat → nil':cons'
Lemmas:
last'(_gen_nil':cons'5(+(1, _n7))) → _gen_0':s'4(0), rt ∈ Ω(1 + n7)
eq'(_gen_0':s'4(_n643), _gen_0':s'4(_n643)) → true', rt ∈ Ω(1 + n643)
reverse'(_gen_nil':cons'5(_n1582)) → _gen_nil':cons'5(_n1582), rt ∈ Ω(1 + n1582 + n15822)
Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_nil':cons'5(0) ⇔ nil'
_gen_nil':cons'5(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'5(x))
No more defined symbols left to analyse.
The lowerbound Ω(n2) was proven with the following lemma:
reverse'(_gen_nil':cons'5(_n1582)) → _gen_nil':cons'5(_n1582), rt ∈ Ω(1 + n1582 + n15822)