length(nil) → 0
length(cons(x, l)) → s(length(l))
lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
head(cons(x, l)) → x
head(nil) → undefined
tail(nil) → nil
tail(cons(x, l)) → l
reverse(l) → rev(0, l, nil, l)
rev(x, l, accu, orig) → if(lt(x, length(orig)), x, l, accu, orig)
if(true, x, l, accu, orig) → rev(s(x), tail(l), cons(head(l), accu), orig)
if(false, x, l, accu, orig) → accu
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
length'(nil') → 0'
length'(cons'(x, l)) → s'(length'(l))
lt'(x, 0') → false'
lt'(0', s'(y)) → true'
lt'(s'(x), s'(y)) → lt'(x, y)
head'(cons'(x, l)) → x
head'(nil') → undefined'
tail'(nil') → nil'
tail'(cons'(x, l)) → l
reverse'(l) → rev'(0', l, nil', l)
rev'(x, l, accu, orig) → if'(lt'(x, length'(orig)), x, l, accu, orig)
if'(true', x, l, accu, orig) → rev'(s'(x), tail'(l), cons'(head'(l), accu), orig)
if'(false', x, l, accu, orig) → accu
Infered types.
Rules:
length'(nil') → 0'
length'(cons'(x, l)) → s'(length'(l))
lt'(x, 0') → false'
lt'(0', s'(y)) → true'
lt'(s'(x), s'(y)) → lt'(x, y)
head'(cons'(x, l)) → x
head'(nil') → undefined'
tail'(nil') → nil'
tail'(cons'(x, l)) → l
reverse'(l) → rev'(0', l, nil', l)
rev'(x, l, accu, orig) → if'(lt'(x, length'(orig)), x, l, accu, orig)
if'(true', x, l, accu, orig) → rev'(s'(x), tail'(l), cons'(head'(l), accu), orig)
if'(false', x, l, accu, orig) → accu
Types:
length' :: nil':cons' → 0':s'
nil' :: nil':cons'
0' :: 0':s'
cons' :: undefined' → nil':cons' → nil':cons'
s' :: 0':s' → 0':s'
lt' :: 0':s' → 0':s' → false':true'
false' :: false':true'
true' :: false':true'
head' :: nil':cons' → undefined'
undefined' :: undefined'
tail' :: nil':cons' → nil':cons'
reverse' :: nil':cons' → nil':cons'
rev' :: 0':s' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
if' :: false':true' → 0':s' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
_hole_0':s'1 :: 0':s'
_hole_nil':cons'2 :: nil':cons'
_hole_undefined'3 :: undefined'
_hole_false':true'4 :: false':true'
_gen_0':s'5 :: Nat → 0':s'
_gen_nil':cons'6 :: Nat → nil':cons'
Heuristically decided to analyse the following defined symbols:
length', lt', rev'
They will be analysed ascendingly in the following order:
length' < rev'
lt' < rev'
Rules:
length'(nil') → 0'
length'(cons'(x, l)) → s'(length'(l))
lt'(x, 0') → false'
lt'(0', s'(y)) → true'
lt'(s'(x), s'(y)) → lt'(x, y)
head'(cons'(x, l)) → x
head'(nil') → undefined'
tail'(nil') → nil'
tail'(cons'(x, l)) → l
reverse'(l) → rev'(0', l, nil', l)
rev'(x, l, accu, orig) → if'(lt'(x, length'(orig)), x, l, accu, orig)
if'(true', x, l, accu, orig) → rev'(s'(x), tail'(l), cons'(head'(l), accu), orig)
if'(false', x, l, accu, orig) → accu
Types:
length' :: nil':cons' → 0':s'
nil' :: nil':cons'
0' :: 0':s'
cons' :: undefined' → nil':cons' → nil':cons'
s' :: 0':s' → 0':s'
lt' :: 0':s' → 0':s' → false':true'
false' :: false':true'
true' :: false':true'
head' :: nil':cons' → undefined'
undefined' :: undefined'
tail' :: nil':cons' → nil':cons'
reverse' :: nil':cons' → nil':cons'
rev' :: 0':s' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
if' :: false':true' → 0':s' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
_hole_0':s'1 :: 0':s'
_hole_nil':cons'2 :: nil':cons'
_hole_undefined'3 :: undefined'
_hole_false':true'4 :: false':true'
_gen_0':s'5 :: Nat → 0':s'
_gen_nil':cons'6 :: Nat → nil':cons'
Generator Equations:
_gen_0':s'5(0) ⇔ 0'
_gen_0':s'5(+(x, 1)) ⇔ s'(_gen_0':s'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(undefined', _gen_nil':cons'6(x))
The following defined symbols remain to be analysed:
length', lt', rev'
They will be analysed ascendingly in the following order:
length' < rev'
lt' < rev'
Proved the following rewrite lemma:
length'(_gen_nil':cons'6(_n8)) → _gen_0':s'5(_n8), rt ∈ Ω(1 + n8)
Induction Base:
length'(_gen_nil':cons'6(0)) →RΩ(1)
0'
Induction Step:
length'(_gen_nil':cons'6(+(_$n9, 1))) →RΩ(1)
s'(length'(_gen_nil':cons'6(_$n9))) →IH
s'(_gen_0':s'5(_$n9))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
length'(nil') → 0'
length'(cons'(x, l)) → s'(length'(l))
lt'(x, 0') → false'
lt'(0', s'(y)) → true'
lt'(s'(x), s'(y)) → lt'(x, y)
head'(cons'(x, l)) → x
head'(nil') → undefined'
tail'(nil') → nil'
tail'(cons'(x, l)) → l
reverse'(l) → rev'(0', l, nil', l)
rev'(x, l, accu, orig) → if'(lt'(x, length'(orig)), x, l, accu, orig)
if'(true', x, l, accu, orig) → rev'(s'(x), tail'(l), cons'(head'(l), accu), orig)
if'(false', x, l, accu, orig) → accu
Types:
length' :: nil':cons' → 0':s'
nil' :: nil':cons'
0' :: 0':s'
cons' :: undefined' → nil':cons' → nil':cons'
s' :: 0':s' → 0':s'
lt' :: 0':s' → 0':s' → false':true'
false' :: false':true'
true' :: false':true'
head' :: nil':cons' → undefined'
undefined' :: undefined'
tail' :: nil':cons' → nil':cons'
reverse' :: nil':cons' → nil':cons'
rev' :: 0':s' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
if' :: false':true' → 0':s' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
_hole_0':s'1 :: 0':s'
_hole_nil':cons'2 :: nil':cons'
_hole_undefined'3 :: undefined'
_hole_false':true'4 :: false':true'
_gen_0':s'5 :: Nat → 0':s'
_gen_nil':cons'6 :: Nat → nil':cons'
Lemmas:
length'(_gen_nil':cons'6(_n8)) → _gen_0':s'5(_n8), rt ∈ Ω(1 + n8)
Generator Equations:
_gen_0':s'5(0) ⇔ 0'
_gen_0':s'5(+(x, 1)) ⇔ s'(_gen_0':s'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(undefined', _gen_nil':cons'6(x))
The following defined symbols remain to be analysed:
lt', rev'
They will be analysed ascendingly in the following order:
lt' < rev'
Proved the following rewrite lemma:
lt'(_gen_0':s'5(_n520), _gen_0':s'5(_n520)) → false', rt ∈ Ω(1 + n520)
Induction Base:
lt'(_gen_0':s'5(0), _gen_0':s'5(0)) →RΩ(1)
false'
Induction Step:
lt'(_gen_0':s'5(+(_$n521, 1)), _gen_0':s'5(+(_$n521, 1))) →RΩ(1)
lt'(_gen_0':s'5(_$n521), _gen_0':s'5(_$n521)) →IH
false'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
length'(nil') → 0'
length'(cons'(x, l)) → s'(length'(l))
lt'(x, 0') → false'
lt'(0', s'(y)) → true'
lt'(s'(x), s'(y)) → lt'(x, y)
head'(cons'(x, l)) → x
head'(nil') → undefined'
tail'(nil') → nil'
tail'(cons'(x, l)) → l
reverse'(l) → rev'(0', l, nil', l)
rev'(x, l, accu, orig) → if'(lt'(x, length'(orig)), x, l, accu, orig)
if'(true', x, l, accu, orig) → rev'(s'(x), tail'(l), cons'(head'(l), accu), orig)
if'(false', x, l, accu, orig) → accu
Types:
length' :: nil':cons' → 0':s'
nil' :: nil':cons'
0' :: 0':s'
cons' :: undefined' → nil':cons' → nil':cons'
s' :: 0':s' → 0':s'
lt' :: 0':s' → 0':s' → false':true'
false' :: false':true'
true' :: false':true'
head' :: nil':cons' → undefined'
undefined' :: undefined'
tail' :: nil':cons' → nil':cons'
reverse' :: nil':cons' → nil':cons'
rev' :: 0':s' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
if' :: false':true' → 0':s' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
_hole_0':s'1 :: 0':s'
_hole_nil':cons'2 :: nil':cons'
_hole_undefined'3 :: undefined'
_hole_false':true'4 :: false':true'
_gen_0':s'5 :: Nat → 0':s'
_gen_nil':cons'6 :: Nat → nil':cons'
Lemmas:
length'(_gen_nil':cons'6(_n8)) → _gen_0':s'5(_n8), rt ∈ Ω(1 + n8)
lt'(_gen_0':s'5(_n520), _gen_0':s'5(_n520)) → false', rt ∈ Ω(1 + n520)
Generator Equations:
_gen_0':s'5(0) ⇔ 0'
_gen_0':s'5(+(x, 1)) ⇔ s'(_gen_0':s'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(undefined', _gen_nil':cons'6(x))
The following defined symbols remain to be analysed:
rev'
Could not prove a rewrite lemma for the defined symbol rev'.
Rules:
length'(nil') → 0'
length'(cons'(x, l)) → s'(length'(l))
lt'(x, 0') → false'
lt'(0', s'(y)) → true'
lt'(s'(x), s'(y)) → lt'(x, y)
head'(cons'(x, l)) → x
head'(nil') → undefined'
tail'(nil') → nil'
tail'(cons'(x, l)) → l
reverse'(l) → rev'(0', l, nil', l)
rev'(x, l, accu, orig) → if'(lt'(x, length'(orig)), x, l, accu, orig)
if'(true', x, l, accu, orig) → rev'(s'(x), tail'(l), cons'(head'(l), accu), orig)
if'(false', x, l, accu, orig) → accu
Types:
length' :: nil':cons' → 0':s'
nil' :: nil':cons'
0' :: 0':s'
cons' :: undefined' → nil':cons' → nil':cons'
s' :: 0':s' → 0':s'
lt' :: 0':s' → 0':s' → false':true'
false' :: false':true'
true' :: false':true'
head' :: nil':cons' → undefined'
undefined' :: undefined'
tail' :: nil':cons' → nil':cons'
reverse' :: nil':cons' → nil':cons'
rev' :: 0':s' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
if' :: false':true' → 0':s' → nil':cons' → nil':cons' → nil':cons' → nil':cons'
_hole_0':s'1 :: 0':s'
_hole_nil':cons'2 :: nil':cons'
_hole_undefined'3 :: undefined'
_hole_false':true'4 :: false':true'
_gen_0':s'5 :: Nat → 0':s'
_gen_nil':cons'6 :: Nat → nil':cons'
Lemmas:
length'(_gen_nil':cons'6(_n8)) → _gen_0':s'5(_n8), rt ∈ Ω(1 + n8)
lt'(_gen_0':s'5(_n520), _gen_0':s'5(_n520)) → false', rt ∈ Ω(1 + n520)
Generator Equations:
_gen_0':s'5(0) ⇔ 0'
_gen_0':s'5(+(x, 1)) ⇔ s'(_gen_0':s'5(x))
_gen_nil':cons'6(0) ⇔ nil'
_gen_nil':cons'6(+(x, 1)) ⇔ cons'(undefined', _gen_nil':cons'6(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
length'(_gen_nil':cons'6(_n8)) → _gen_0':s'5(_n8), rt ∈ Ω(1 + n8)