double(0) → 0
double(s(x)) → s(s(double(x)))
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)
first(nil) → 0
first(cons(x, xs)) → x
doublelist(nil) → nil
doublelist(cons(x, xs)) → cons(double(x), doublelist(del(first(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:
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
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)
first'(nil') → 0'
first'(cons'(x, xs)) → x
doublelist'(nil') → nil'
doublelist'(cons'(x, xs)) → cons'(double'(x), doublelist'(del'(first'(cons'(x, xs)), cons'(x, xs))))
Infered types.
Rules:
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
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)
first'(nil') → 0'
first'(cons'(x, xs)) → x
doublelist'(nil') → nil'
doublelist'(cons'(x, xs)) → cons'(double'(x), doublelist'(del'(first'(cons'(x, xs)), cons'(x, xs))))
Types:
double' :: 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
del' :: 0':s' → nil':cons' → nil':cons'
nil' :: nil':cons'
cons' :: 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'
first' :: nil':cons' → 0':s'
doublelist' :: 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:
double', del', eq', doublelist'
They will be analysed ascendingly in the following order:
double' < doublelist'
eq' < del'
del' < doublelist'
Rules:
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
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)
first'(nil') → 0'
first'(cons'(x, xs)) → x
doublelist'(nil') → nil'
doublelist'(cons'(x, xs)) → cons'(double'(x), doublelist'(del'(first'(cons'(x, xs)), cons'(x, xs))))
Types:
double' :: 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
del' :: 0':s' → nil':cons' → nil':cons'
nil' :: nil':cons'
cons' :: 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'
first' :: nil':cons' → 0':s'
doublelist' :: 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:
double', del', eq', doublelist'
They will be analysed ascendingly in the following order:
double' < doublelist'
eq' < del'
del' < doublelist'
Proved the following rewrite lemma:
double'(_gen_0':s'4(_n7)) → _gen_0':s'4(*(2, _n7)), rt ∈ Ω(1 + n7)
Induction Base:
double'(_gen_0':s'4(0)) →RΩ(1)
0'
Induction Step:
double'(_gen_0':s'4(+(_$n8, 1))) →RΩ(1)
s'(s'(double'(_gen_0':s'4(_$n8)))) →IH
s'(s'(_gen_0':s'4(*(2, _$n8))))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
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)
first'(nil') → 0'
first'(cons'(x, xs)) → x
doublelist'(nil') → nil'
doublelist'(cons'(x, xs)) → cons'(double'(x), doublelist'(del'(first'(cons'(x, xs)), cons'(x, xs))))
Types:
double' :: 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
del' :: 0':s' → nil':cons' → nil':cons'
nil' :: nil':cons'
cons' :: 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'
first' :: nil':cons' → 0':s'
doublelist' :: 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:
double'(_gen_0':s'4(_n7)) → _gen_0':s'4(*(2, _n7)), 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', doublelist'
They will be analysed ascendingly in the following order:
eq' < del'
del' < doublelist'
Proved the following rewrite lemma:
eq'(_gen_0':s'4(_n525), _gen_0':s'4(_n525)) → true', rt ∈ Ω(1 + n525)
Induction Base:
eq'(_gen_0':s'4(0), _gen_0':s'4(0)) →RΩ(1)
true'
Induction Step:
eq'(_gen_0':s'4(+(_$n526, 1)), _gen_0':s'4(+(_$n526, 1))) →RΩ(1)
eq'(_gen_0':s'4(_$n526), _gen_0':s'4(_$n526)) →IH
true'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
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)
first'(nil') → 0'
first'(cons'(x, xs)) → x
doublelist'(nil') → nil'
doublelist'(cons'(x, xs)) → cons'(double'(x), doublelist'(del'(first'(cons'(x, xs)), cons'(x, xs))))
Types:
double' :: 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
del' :: 0':s' → nil':cons' → nil':cons'
nil' :: nil':cons'
cons' :: 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'
first' :: nil':cons' → 0':s'
doublelist' :: 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:
double'(_gen_0':s'4(_n7)) → _gen_0':s'4(*(2, _n7)), rt ∈ Ω(1 + n7)
eq'(_gen_0':s'4(_n525), _gen_0':s'4(_n525)) → true', rt ∈ Ω(1 + n525)
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', doublelist'
They will be analysed ascendingly in the following order:
del' < doublelist'
Could not prove a rewrite lemma for the defined symbol del'.
Rules:
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
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)
first'(nil') → 0'
first'(cons'(x, xs)) → x
doublelist'(nil') → nil'
doublelist'(cons'(x, xs)) → cons'(double'(x), doublelist'(del'(first'(cons'(x, xs)), cons'(x, xs))))
Types:
double' :: 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
del' :: 0':s' → nil':cons' → nil':cons'
nil' :: nil':cons'
cons' :: 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'
first' :: nil':cons' → 0':s'
doublelist' :: 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:
double'(_gen_0':s'4(_n7)) → _gen_0':s'4(*(2, _n7)), rt ∈ Ω(1 + n7)
eq'(_gen_0':s'4(_n525), _gen_0':s'4(_n525)) → true', rt ∈ Ω(1 + n525)
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:
doublelist'
Proved the following rewrite lemma:
doublelist'(_gen_nil':cons'5(_n1455)) → _gen_nil':cons'5(_n1455), rt ∈ Ω(1 + n1455)
Induction Base:
doublelist'(_gen_nil':cons'5(0)) →RΩ(1)
nil'
Induction Step:
doublelist'(_gen_nil':cons'5(+(_$n1456, 1))) →RΩ(1)
cons'(double'(0'), doublelist'(del'(first'(cons'(0', _gen_nil':cons'5(_$n1456))), cons'(0', _gen_nil':cons'5(_$n1456))))) →LΩ(1)
cons'(_gen_0':s'4(*(2, 0)), doublelist'(del'(first'(cons'(0', _gen_nil':cons'5(_$n1456))), cons'(0', _gen_nil':cons'5(_$n1456))))) →RΩ(1)
cons'(_gen_0':s'4(0), doublelist'(del'(0', cons'(0', _gen_nil':cons'5(_$n1456))))) →RΩ(1)
cons'(_gen_0':s'4(0), doublelist'(if'(eq'(0', 0'), 0', 0', _gen_nil':cons'5(_$n1456)))) →LΩ(1)
cons'(_gen_0':s'4(0), doublelist'(if'(true', 0', 0', _gen_nil':cons'5(_$n1456)))) →RΩ(1)
cons'(_gen_0':s'4(0), doublelist'(_gen_nil':cons'5(_$n1456))) →IH
cons'(_gen_0':s'4(0), _gen_nil':cons'5(_$n1456))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
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)
first'(nil') → 0'
first'(cons'(x, xs)) → x
doublelist'(nil') → nil'
doublelist'(cons'(x, xs)) → cons'(double'(x), doublelist'(del'(first'(cons'(x, xs)), cons'(x, xs))))
Types:
double' :: 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
del' :: 0':s' → nil':cons' → nil':cons'
nil' :: nil':cons'
cons' :: 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'
first' :: nil':cons' → 0':s'
doublelist' :: 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:
double'(_gen_0':s'4(_n7)) → _gen_0':s'4(*(2, _n7)), rt ∈ Ω(1 + n7)
eq'(_gen_0':s'4(_n525), _gen_0':s'4(_n525)) → true', rt ∈ Ω(1 + n525)
doublelist'(_gen_nil':cons'5(_n1455)) → _gen_nil':cons'5(_n1455), rt ∈ Ω(1 + n1455)
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 Ω(n) was proven with the following lemma:
double'(_gen_0':s'4(_n7)) → _gen_0':s'4(*(2, _n7)), rt ∈ Ω(1 + n7)