sub(0, 0) → 0
sub(s(x), 0) → s(x)
sub(0, s(x)) → 0
sub(s(x), s(y)) → sub(x, y)
zero(nil) → zero2(0, nil)
zero(cons(x, xs)) → zero2(sub(x, x), cons(x, xs))
zero2(0, nil) → nil
zero2(0, cons(x, xs)) → cons(sub(x, x), zero(xs))
zero2(s(y), nil) → zero(nil)
zero2(s(y), cons(x, xs)) → zero(cons(x, xs))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
sub'(0', 0') → 0'
sub'(s'(x), 0') → s'(x)
sub'(0', s'(x)) → 0'
sub'(s'(x), s'(y)) → sub'(x, y)
zero'(nil') → zero2'(0', nil')
zero'(cons'(x, xs)) → zero2'(sub'(x, x), cons'(x, xs))
zero2'(0', nil') → nil'
zero2'(0', cons'(x, xs)) → cons'(sub'(x, x), zero'(xs))
zero2'(s'(y), nil') → zero'(nil')
zero2'(s'(y), cons'(x, xs)) → zero'(cons'(x, xs))
Infered types.
Rules:
sub'(0', 0') → 0'
sub'(s'(x), 0') → s'(x)
sub'(0', s'(x)) → 0'
sub'(s'(x), s'(y)) → sub'(x, y)
zero'(nil') → zero2'(0', nil')
zero'(cons'(x, xs)) → zero2'(sub'(x, x), cons'(x, xs))
zero2'(0', nil') → nil'
zero2'(0', cons'(x, xs)) → cons'(sub'(x, x), zero'(xs))
zero2'(s'(y), nil') → zero'(nil')
zero2'(s'(y), cons'(x, xs)) → zero'(cons'(x, xs))
Types:
sub' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
zero' :: nil':cons' → nil':cons'
nil' :: nil':cons'
zero2' :: 0':s' → nil':cons' → nil':cons'
cons' :: 0':s' → nil':cons' → nil':cons'
_hole_0':s'1 :: 0':s'
_hole_nil':cons'2 :: nil':cons'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil':cons'4 :: Nat → nil':cons'
Heuristically decided to analyse the following defined symbols:
sub', zero'
They will be analysed ascendingly in the following order:
sub' < zero'
Rules:
sub'(0', 0') → 0'
sub'(s'(x), 0') → s'(x)
sub'(0', s'(x)) → 0'
sub'(s'(x), s'(y)) → sub'(x, y)
zero'(nil') → zero2'(0', nil')
zero'(cons'(x, xs)) → zero2'(sub'(x, x), cons'(x, xs))
zero2'(0', nil') → nil'
zero2'(0', cons'(x, xs)) → cons'(sub'(x, x), zero'(xs))
zero2'(s'(y), nil') → zero'(nil')
zero2'(s'(y), cons'(x, xs)) → zero'(cons'(x, xs))
Types:
sub' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
zero' :: nil':cons' → nil':cons'
nil' :: nil':cons'
zero2' :: 0':s' → nil':cons' → nil':cons'
cons' :: 0':s' → nil':cons' → nil':cons'
_hole_0':s'1 :: 0':s'
_hole_nil':cons'2 :: nil':cons'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil':cons'4 :: Nat → nil':cons'
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'4(x))
The following defined symbols remain to be analysed:
sub', zero'
They will be analysed ascendingly in the following order:
sub' < zero'
Proved the following rewrite lemma:
sub'(_gen_0':s'3(_n6), _gen_0':s'3(_n6)) → _gen_0':s'3(0), rt ∈ Ω(1 + n6)
Induction Base:
sub'(_gen_0':s'3(0), _gen_0':s'3(0)) →RΩ(1)
0'
Induction Step:
sub'(_gen_0':s'3(+(_$n7, 1)), _gen_0':s'3(+(_$n7, 1))) →RΩ(1)
sub'(_gen_0':s'3(_$n7), _gen_0':s'3(_$n7)) →IH
_gen_0':s'3(0)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
sub'(0', 0') → 0'
sub'(s'(x), 0') → s'(x)
sub'(0', s'(x)) → 0'
sub'(s'(x), s'(y)) → sub'(x, y)
zero'(nil') → zero2'(0', nil')
zero'(cons'(x, xs)) → zero2'(sub'(x, x), cons'(x, xs))
zero2'(0', nil') → nil'
zero2'(0', cons'(x, xs)) → cons'(sub'(x, x), zero'(xs))
zero2'(s'(y), nil') → zero'(nil')
zero2'(s'(y), cons'(x, xs)) → zero'(cons'(x, xs))
Types:
sub' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
zero' :: nil':cons' → nil':cons'
nil' :: nil':cons'
zero2' :: 0':s' → nil':cons' → nil':cons'
cons' :: 0':s' → nil':cons' → nil':cons'
_hole_0':s'1 :: 0':s'
_hole_nil':cons'2 :: nil':cons'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil':cons'4 :: Nat → nil':cons'
Lemmas:
sub'(_gen_0':s'3(_n6), _gen_0':s'3(_n6)) → _gen_0':s'3(0), rt ∈ Ω(1 + n6)
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'4(x))
The following defined symbols remain to be analysed:
zero'
Proved the following rewrite lemma:
zero'(_gen_nil':cons'4(_n1060)) → _gen_nil':cons'4(_n1060), rt ∈ Ω(1 + n1060)
Induction Base:
zero'(_gen_nil':cons'4(0)) →RΩ(1)
zero2'(0', nil') →RΩ(1)
nil'
Induction Step:
zero'(_gen_nil':cons'4(+(_$n1061, 1))) →RΩ(1)
zero2'(sub'(0', 0'), cons'(0', _gen_nil':cons'4(_$n1061))) →LΩ(1)
zero2'(_gen_0':s'3(0), cons'(0', _gen_nil':cons'4(_$n1061))) →RΩ(1)
cons'(sub'(0', 0'), zero'(_gen_nil':cons'4(_$n1061))) →LΩ(1)
cons'(_gen_0':s'3(0), zero'(_gen_nil':cons'4(_$n1061))) →IH
cons'(_gen_0':s'3(0), _gen_nil':cons'4(_$n1061))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
sub'(0', 0') → 0'
sub'(s'(x), 0') → s'(x)
sub'(0', s'(x)) → 0'
sub'(s'(x), s'(y)) → sub'(x, y)
zero'(nil') → zero2'(0', nil')
zero'(cons'(x, xs)) → zero2'(sub'(x, x), cons'(x, xs))
zero2'(0', nil') → nil'
zero2'(0', cons'(x, xs)) → cons'(sub'(x, x), zero'(xs))
zero2'(s'(y), nil') → zero'(nil')
zero2'(s'(y), cons'(x, xs)) → zero'(cons'(x, xs))
Types:
sub' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
zero' :: nil':cons' → nil':cons'
nil' :: nil':cons'
zero2' :: 0':s' → nil':cons' → nil':cons'
cons' :: 0':s' → nil':cons' → nil':cons'
_hole_0':s'1 :: 0':s'
_hole_nil':cons'2 :: nil':cons'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil':cons'4 :: Nat → nil':cons'
Lemmas:
sub'(_gen_0':s'3(_n6), _gen_0':s'3(_n6)) → _gen_0':s'3(0), rt ∈ Ω(1 + n6)
zero'(_gen_nil':cons'4(_n1060)) → _gen_nil':cons'4(_n1060), rt ∈ Ω(1 + n1060)
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(0', _gen_nil':cons'4(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
sub'(_gen_0':s'3(_n6), _gen_0':s'3(_n6)) → _gen_0':s'3(0), rt ∈ Ω(1 + n6)