+(0, y) → y
+(s(x), y) → s(+(x, y))
++(nil, ys) → ys
++(:(x, xs), ys) → :(x, ++(xs, ys))
sum(:(x, nil)) → :(x, nil)
sum(:(x, :(y, xs))) → sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) → sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(-(x, y), s(y)))
length(nil) → 0
length(:(x, xs)) → s(length(xs))
hd(:(x, xs)) → x
avg(xs) → quot(hd(sum(xs)), length(xs))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
+'(0', y) → y
+'(s'(x), y) → s'(+'(x, y))
++'(nil', ys) → ys
++'(:'(x, xs), ys) → :'(x, ++'(xs, ys))
sum'(:'(x, nil')) → :'(x, nil')
sum'(:'(x, :'(y, xs))) → sum'(:'(+'(x, y), xs))
sum'(++'(xs, :'(x, :'(y, ys)))) → sum'(++'(xs, sum'(:'(x, :'(y, ys)))))
-'(x, 0') → x
-'(0', s'(y)) → 0'
-'(s'(x), s'(y)) → -'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(-'(x, y), s'(y)))
length'(nil') → 0'
length'(:'(x, xs)) → s'(length'(xs))
hd'(:'(x, xs)) → x
avg'(xs) → quot'(hd'(sum'(xs)), length'(xs))
Infered types.
Rules:
+'(0', y) → y
+'(s'(x), y) → s'(+'(x, y))
++'(nil', ys) → ys
++'(:'(x, xs), ys) → :'(x, ++'(xs, ys))
sum'(:'(x, nil')) → :'(x, nil')
sum'(:'(x, :'(y, xs))) → sum'(:'(+'(x, y), xs))
sum'(++'(xs, :'(x, :'(y, ys)))) → sum'(++'(xs, sum'(:'(x, :'(y, ys)))))
-'(x, 0') → x
-'(0', s'(y)) → 0'
-'(s'(x), s'(y)) → -'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(-'(x, y), s'(y)))
length'(nil') → 0'
length'(:'(x, xs)) → s'(length'(xs))
hd'(:'(x, xs)) → x
avg'(xs) → quot'(hd'(sum'(xs)), length'(xs))
Types:
+' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
++' :: nil'::' → nil'::' → nil'::'
nil' :: nil'::'
:' :: 0':s' → nil'::' → nil'::'
sum' :: nil'::' → nil'::'
-' :: 0':s' → 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
length' :: nil'::' → 0':s'
hd' :: nil'::' → 0':s'
avg' :: nil'::' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_nil'::'2 :: nil'::'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil'::'4 :: Nat → nil'::'
Heuristically decided to analyse the following defined symbols:
+', ++', sum', -', quot', length'
They will be analysed ascendingly in the following order:
+' < sum'
++' < sum'
-' < quot'
Rules:
+'(0', y) → y
+'(s'(x), y) → s'(+'(x, y))
++'(nil', ys) → ys
++'(:'(x, xs), ys) → :'(x, ++'(xs, ys))
sum'(:'(x, nil')) → :'(x, nil')
sum'(:'(x, :'(y, xs))) → sum'(:'(+'(x, y), xs))
sum'(++'(xs, :'(x, :'(y, ys)))) → sum'(++'(xs, sum'(:'(x, :'(y, ys)))))
-'(x, 0') → x
-'(0', s'(y)) → 0'
-'(s'(x), s'(y)) → -'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(-'(x, y), s'(y)))
length'(nil') → 0'
length'(:'(x, xs)) → s'(length'(xs))
hd'(:'(x, xs)) → x
avg'(xs) → quot'(hd'(sum'(xs)), length'(xs))
Types:
+' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
++' :: nil'::' → nil'::' → nil'::'
nil' :: nil'::'
:' :: 0':s' → nil'::' → nil'::'
sum' :: nil'::' → nil'::'
-' :: 0':s' → 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
length' :: nil'::' → 0':s'
hd' :: nil'::' → 0':s'
avg' :: nil'::' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_nil'::'2 :: nil'::'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil'::'4 :: Nat → nil'::'
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil'::'4(0) ⇔ nil'
_gen_nil'::'4(+(x, 1)) ⇔ :'(0', _gen_nil'::'4(x))
The following defined symbols remain to be analysed:
+', ++', sum', -', quot', length'
They will be analysed ascendingly in the following order:
+' < sum'
++' < sum'
-' < quot'
Proved the following rewrite lemma:
+'(_gen_0':s'3(_n6), _gen_0':s'3(b)) → _gen_0':s'3(+(_n6, b)), rt ∈ Ω(1 + n6)
Induction Base:
+'(_gen_0':s'3(0), _gen_0':s'3(b)) →RΩ(1)
_gen_0':s'3(b)
Induction Step:
+'(_gen_0':s'3(+(_$n7, 1)), _gen_0':s'3(_b175)) →RΩ(1)
s'(+'(_gen_0':s'3(_$n7), _gen_0':s'3(_b175))) →IH
s'(_gen_0':s'3(+(_$n7, _b175)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
+'(0', y) → y
+'(s'(x), y) → s'(+'(x, y))
++'(nil', ys) → ys
++'(:'(x, xs), ys) → :'(x, ++'(xs, ys))
sum'(:'(x, nil')) → :'(x, nil')
sum'(:'(x, :'(y, xs))) → sum'(:'(+'(x, y), xs))
sum'(++'(xs, :'(x, :'(y, ys)))) → sum'(++'(xs, sum'(:'(x, :'(y, ys)))))
-'(x, 0') → x
-'(0', s'(y)) → 0'
-'(s'(x), s'(y)) → -'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(-'(x, y), s'(y)))
length'(nil') → 0'
length'(:'(x, xs)) → s'(length'(xs))
hd'(:'(x, xs)) → x
avg'(xs) → quot'(hd'(sum'(xs)), length'(xs))
Types:
+' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
++' :: nil'::' → nil'::' → nil'::'
nil' :: nil'::'
:' :: 0':s' → nil'::' → nil'::'
sum' :: nil'::' → nil'::'
-' :: 0':s' → 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
length' :: nil'::' → 0':s'
hd' :: nil'::' → 0':s'
avg' :: nil'::' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_nil'::'2 :: nil'::'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil'::'4 :: Nat → nil'::'
Lemmas:
+'(_gen_0':s'3(_n6), _gen_0':s'3(b)) → _gen_0':s'3(+(_n6, b)), 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'::'4(0) ⇔ nil'
_gen_nil'::'4(+(x, 1)) ⇔ :'(0', _gen_nil'::'4(x))
The following defined symbols remain to be analysed:
++', sum', -', quot', length'
They will be analysed ascendingly in the following order:
++' < sum'
-' < quot'
Proved the following rewrite lemma:
++'(_gen_nil'::'4(_n1085), _gen_nil'::'4(b)) → _gen_nil'::'4(+(_n1085, b)), rt ∈ Ω(1 + n1085)
Induction Base:
++'(_gen_nil'::'4(0), _gen_nil'::'4(b)) →RΩ(1)
_gen_nil'::'4(b)
Induction Step:
++'(_gen_nil'::'4(+(_$n1086, 1)), _gen_nil'::'4(_b1316)) →RΩ(1)
:'(0', ++'(_gen_nil'::'4(_$n1086), _gen_nil'::'4(_b1316))) →IH
:'(0', _gen_nil'::'4(+(_$n1086, _b1316)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
+'(0', y) → y
+'(s'(x), y) → s'(+'(x, y))
++'(nil', ys) → ys
++'(:'(x, xs), ys) → :'(x, ++'(xs, ys))
sum'(:'(x, nil')) → :'(x, nil')
sum'(:'(x, :'(y, xs))) → sum'(:'(+'(x, y), xs))
sum'(++'(xs, :'(x, :'(y, ys)))) → sum'(++'(xs, sum'(:'(x, :'(y, ys)))))
-'(x, 0') → x
-'(0', s'(y)) → 0'
-'(s'(x), s'(y)) → -'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(-'(x, y), s'(y)))
length'(nil') → 0'
length'(:'(x, xs)) → s'(length'(xs))
hd'(:'(x, xs)) → x
avg'(xs) → quot'(hd'(sum'(xs)), length'(xs))
Types:
+' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
++' :: nil'::' → nil'::' → nil'::'
nil' :: nil'::'
:' :: 0':s' → nil'::' → nil'::'
sum' :: nil'::' → nil'::'
-' :: 0':s' → 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
length' :: nil'::' → 0':s'
hd' :: nil'::' → 0':s'
avg' :: nil'::' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_nil'::'2 :: nil'::'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil'::'4 :: Nat → nil'::'
Lemmas:
+'(_gen_0':s'3(_n6), _gen_0':s'3(b)) → _gen_0':s'3(+(_n6, b)), rt ∈ Ω(1 + n6)
++'(_gen_nil'::'4(_n1085), _gen_nil'::'4(b)) → _gen_nil'::'4(+(_n1085, b)), rt ∈ Ω(1 + n1085)
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil'::'4(0) ⇔ nil'
_gen_nil'::'4(+(x, 1)) ⇔ :'(0', _gen_nil'::'4(x))
The following defined symbols remain to be analysed:
sum', -', quot', length'
They will be analysed ascendingly in the following order:
-' < quot'
Proved the following rewrite lemma:
sum'(_gen_nil'::'4(+(1, _n2295))) → _gen_nil'::'4(1), rt ∈ Ω(1 + n2295)
Induction Base:
sum'(_gen_nil'::'4(+(1, 0))) →RΩ(1)
:'(0', nil')
Induction Step:
sum'(_gen_nil'::'4(+(1, +(_$n2296, 1)))) →RΩ(1)
sum'(:'(+'(0', 0'), _gen_nil'::'4(_$n2296))) →LΩ(1)
sum'(:'(_gen_0':s'3(+(0, 0)), _gen_nil'::'4(_$n2296))) →IH
_gen_nil'::'4(1)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
+'(0', y) → y
+'(s'(x), y) → s'(+'(x, y))
++'(nil', ys) → ys
++'(:'(x, xs), ys) → :'(x, ++'(xs, ys))
sum'(:'(x, nil')) → :'(x, nil')
sum'(:'(x, :'(y, xs))) → sum'(:'(+'(x, y), xs))
sum'(++'(xs, :'(x, :'(y, ys)))) → sum'(++'(xs, sum'(:'(x, :'(y, ys)))))
-'(x, 0') → x
-'(0', s'(y)) → 0'
-'(s'(x), s'(y)) → -'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(-'(x, y), s'(y)))
length'(nil') → 0'
length'(:'(x, xs)) → s'(length'(xs))
hd'(:'(x, xs)) → x
avg'(xs) → quot'(hd'(sum'(xs)), length'(xs))
Types:
+' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
++' :: nil'::' → nil'::' → nil'::'
nil' :: nil'::'
:' :: 0':s' → nil'::' → nil'::'
sum' :: nil'::' → nil'::'
-' :: 0':s' → 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
length' :: nil'::' → 0':s'
hd' :: nil'::' → 0':s'
avg' :: nil'::' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_nil'::'2 :: nil'::'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil'::'4 :: Nat → nil'::'
Lemmas:
+'(_gen_0':s'3(_n6), _gen_0':s'3(b)) → _gen_0':s'3(+(_n6, b)), rt ∈ Ω(1 + n6)
++'(_gen_nil'::'4(_n1085), _gen_nil'::'4(b)) → _gen_nil'::'4(+(_n1085, b)), rt ∈ Ω(1 + n1085)
sum'(_gen_nil'::'4(+(1, _n2295))) → _gen_nil'::'4(1), rt ∈ Ω(1 + n2295)
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil'::'4(0) ⇔ nil'
_gen_nil'::'4(+(x, 1)) ⇔ :'(0', _gen_nil'::'4(x))
The following defined symbols remain to be analysed:
-', quot', length'
They will be analysed ascendingly in the following order:
-' < quot'
Proved the following rewrite lemma:
-'(_gen_0':s'3(_n4030), _gen_0':s'3(_n4030)) → _gen_0':s'3(0), rt ∈ Ω(1 + n4030)
Induction Base:
-'(_gen_0':s'3(0), _gen_0':s'3(0)) →RΩ(1)
_gen_0':s'3(0)
Induction Step:
-'(_gen_0':s'3(+(_$n4031, 1)), _gen_0':s'3(+(_$n4031, 1))) →RΩ(1)
-'(_gen_0':s'3(_$n4031), _gen_0':s'3(_$n4031)) →IH
_gen_0':s'3(0)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
+'(0', y) → y
+'(s'(x), y) → s'(+'(x, y))
++'(nil', ys) → ys
++'(:'(x, xs), ys) → :'(x, ++'(xs, ys))
sum'(:'(x, nil')) → :'(x, nil')
sum'(:'(x, :'(y, xs))) → sum'(:'(+'(x, y), xs))
sum'(++'(xs, :'(x, :'(y, ys)))) → sum'(++'(xs, sum'(:'(x, :'(y, ys)))))
-'(x, 0') → x
-'(0', s'(y)) → 0'
-'(s'(x), s'(y)) → -'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(-'(x, y), s'(y)))
length'(nil') → 0'
length'(:'(x, xs)) → s'(length'(xs))
hd'(:'(x, xs)) → x
avg'(xs) → quot'(hd'(sum'(xs)), length'(xs))
Types:
+' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
++' :: nil'::' → nil'::' → nil'::'
nil' :: nil'::'
:' :: 0':s' → nil'::' → nil'::'
sum' :: nil'::' → nil'::'
-' :: 0':s' → 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
length' :: nil'::' → 0':s'
hd' :: nil'::' → 0':s'
avg' :: nil'::' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_nil'::'2 :: nil'::'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil'::'4 :: Nat → nil'::'
Lemmas:
+'(_gen_0':s'3(_n6), _gen_0':s'3(b)) → _gen_0':s'3(+(_n6, b)), rt ∈ Ω(1 + n6)
++'(_gen_nil'::'4(_n1085), _gen_nil'::'4(b)) → _gen_nil'::'4(+(_n1085, b)), rt ∈ Ω(1 + n1085)
sum'(_gen_nil'::'4(+(1, _n2295))) → _gen_nil'::'4(1), rt ∈ Ω(1 + n2295)
-'(_gen_0':s'3(_n4030), _gen_0':s'3(_n4030)) → _gen_0':s'3(0), rt ∈ Ω(1 + n4030)
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil'::'4(0) ⇔ nil'
_gen_nil'::'4(+(x, 1)) ⇔ :'(0', _gen_nil'::'4(x))
The following defined symbols remain to be analysed:
quot', length'
Could not prove a rewrite lemma for the defined symbol quot'.
Rules:
+'(0', y) → y
+'(s'(x), y) → s'(+'(x, y))
++'(nil', ys) → ys
++'(:'(x, xs), ys) → :'(x, ++'(xs, ys))
sum'(:'(x, nil')) → :'(x, nil')
sum'(:'(x, :'(y, xs))) → sum'(:'(+'(x, y), xs))
sum'(++'(xs, :'(x, :'(y, ys)))) → sum'(++'(xs, sum'(:'(x, :'(y, ys)))))
-'(x, 0') → x
-'(0', s'(y)) → 0'
-'(s'(x), s'(y)) → -'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(-'(x, y), s'(y)))
length'(nil') → 0'
length'(:'(x, xs)) → s'(length'(xs))
hd'(:'(x, xs)) → x
avg'(xs) → quot'(hd'(sum'(xs)), length'(xs))
Types:
+' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
++' :: nil'::' → nil'::' → nil'::'
nil' :: nil'::'
:' :: 0':s' → nil'::' → nil'::'
sum' :: nil'::' → nil'::'
-' :: 0':s' → 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
length' :: nil'::' → 0':s'
hd' :: nil'::' → 0':s'
avg' :: nil'::' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_nil'::'2 :: nil'::'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil'::'4 :: Nat → nil'::'
Lemmas:
+'(_gen_0':s'3(_n6), _gen_0':s'3(b)) → _gen_0':s'3(+(_n6, b)), rt ∈ Ω(1 + n6)
++'(_gen_nil'::'4(_n1085), _gen_nil'::'4(b)) → _gen_nil'::'4(+(_n1085, b)), rt ∈ Ω(1 + n1085)
sum'(_gen_nil'::'4(+(1, _n2295))) → _gen_nil'::'4(1), rt ∈ Ω(1 + n2295)
-'(_gen_0':s'3(_n4030), _gen_0':s'3(_n4030)) → _gen_0':s'3(0), rt ∈ Ω(1 + n4030)
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil'::'4(0) ⇔ nil'
_gen_nil'::'4(+(x, 1)) ⇔ :'(0', _gen_nil'::'4(x))
The following defined symbols remain to be analysed:
length'
Proved the following rewrite lemma:
length'(_gen_nil'::'4(_n5532)) → _gen_0':s'3(_n5532), rt ∈ Ω(1 + n5532)
Induction Base:
length'(_gen_nil'::'4(0)) →RΩ(1)
0'
Induction Step:
length'(_gen_nil'::'4(+(_$n5533, 1))) →RΩ(1)
s'(length'(_gen_nil'::'4(_$n5533))) →IH
s'(_gen_0':s'3(_$n5533))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
+'(0', y) → y
+'(s'(x), y) → s'(+'(x, y))
++'(nil', ys) → ys
++'(:'(x, xs), ys) → :'(x, ++'(xs, ys))
sum'(:'(x, nil')) → :'(x, nil')
sum'(:'(x, :'(y, xs))) → sum'(:'(+'(x, y), xs))
sum'(++'(xs, :'(x, :'(y, ys)))) → sum'(++'(xs, sum'(:'(x, :'(y, ys)))))
-'(x, 0') → x
-'(0', s'(y)) → 0'
-'(s'(x), s'(y)) → -'(x, y)
quot'(0', s'(y)) → 0'
quot'(s'(x), s'(y)) → s'(quot'(-'(x, y), s'(y)))
length'(nil') → 0'
length'(:'(x, xs)) → s'(length'(xs))
hd'(:'(x, xs)) → x
avg'(xs) → quot'(hd'(sum'(xs)), length'(xs))
Types:
+' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
++' :: nil'::' → nil'::' → nil'::'
nil' :: nil'::'
:' :: 0':s' → nil'::' → nil'::'
sum' :: nil'::' → nil'::'
-' :: 0':s' → 0':s' → 0':s'
quot' :: 0':s' → 0':s' → 0':s'
length' :: nil'::' → 0':s'
hd' :: nil'::' → 0':s'
avg' :: nil'::' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_nil'::'2 :: nil'::'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil'::'4 :: Nat → nil'::'
Lemmas:
+'(_gen_0':s'3(_n6), _gen_0':s'3(b)) → _gen_0':s'3(+(_n6, b)), rt ∈ Ω(1 + n6)
++'(_gen_nil'::'4(_n1085), _gen_nil'::'4(b)) → _gen_nil'::'4(+(_n1085, b)), rt ∈ Ω(1 + n1085)
sum'(_gen_nil'::'4(+(1, _n2295))) → _gen_nil'::'4(1), rt ∈ Ω(1 + n2295)
-'(_gen_0':s'3(_n4030), _gen_0':s'3(_n4030)) → _gen_0':s'3(0), rt ∈ Ω(1 + n4030)
length'(_gen_nil'::'4(_n5532)) → _gen_0':s'3(_n5532), rt ∈ Ω(1 + n5532)
Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil'::'4(0) ⇔ nil'
_gen_nil'::'4(+(x, 1)) ⇔ :'(0', _gen_nil'::'4(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
+'(_gen_0':s'3(_n6), _gen_0':s'3(b)) → _gen_0':s'3(+(_n6, b)), rt ∈ Ω(1 + n6)