isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0)
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
isEmpty'(empty') → true'
isEmpty'(node'(l, r)) → false'
left'(empty') → empty'
left'(node'(l, r)) → l
right'(empty') → empty'
right'(node'(l, r)) → r
inc'(0') → s'(0')
inc'(s'(x)) → s'(inc'(x))
count'(n, x) → if'(isEmpty'(n), isEmpty'(left'(n)), right'(n), node'(left'(left'(n)), node'(right'(left'(n)), right'(n))), x, inc'(x))
if'(true', b, n, m, x, y) → x
if'(false', false', n, m, x, y) → count'(m, x)
if'(false', true', n, m, x, y) → count'(n, y)
nrOfNodes'(n) → count'(n, 0')
Infered types.
Rules:
isEmpty'(empty') → true'
isEmpty'(node'(l, r)) → false'
left'(empty') → empty'
left'(node'(l, r)) → l
right'(empty') → empty'
right'(node'(l, r)) → r
inc'(0') → s'(0')
inc'(s'(x)) → s'(inc'(x))
count'(n, x) → if'(isEmpty'(n), isEmpty'(left'(n)), right'(n), node'(left'(left'(n)), node'(right'(left'(n)), right'(n))), x, inc'(x))
if'(true', b, n, m, x, y) → x
if'(false', false', n, m, x, y) → count'(m, x)
if'(false', true', n, m, x, y) → count'(n, y)
nrOfNodes'(n) → count'(n, 0')
Types:
isEmpty' :: empty':node' → true':false'
empty' :: empty':node'
true' :: true':false'
node' :: empty':node' → empty':node' → empty':node'
false' :: true':false'
left' :: empty':node' → empty':node'
right' :: empty':node' → empty':node'
inc' :: 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
count' :: empty':node' → 0':s' → 0':s'
if' :: true':false' → true':false' → empty':node' → empty':node' → 0':s' → 0':s' → 0':s'
nrOfNodes' :: empty':node' → 0':s'
_hole_true':false'1 :: true':false'
_hole_empty':node'2 :: empty':node'
_hole_0':s'3 :: 0':s'
_gen_empty':node'4 :: Nat → empty':node'
_gen_0':s'5 :: Nat → 0':s'
Heuristically decided to analyse the following defined symbols:
inc', count'
They will be analysed ascendingly in the following order:
inc' < count'
Rules:
isEmpty'(empty') → true'
isEmpty'(node'(l, r)) → false'
left'(empty') → empty'
left'(node'(l, r)) → l
right'(empty') → empty'
right'(node'(l, r)) → r
inc'(0') → s'(0')
inc'(s'(x)) → s'(inc'(x))
count'(n, x) → if'(isEmpty'(n), isEmpty'(left'(n)), right'(n), node'(left'(left'(n)), node'(right'(left'(n)), right'(n))), x, inc'(x))
if'(true', b, n, m, x, y) → x
if'(false', false', n, m, x, y) → count'(m, x)
if'(false', true', n, m, x, y) → count'(n, y)
nrOfNodes'(n) → count'(n, 0')
Types:
isEmpty' :: empty':node' → true':false'
empty' :: empty':node'
true' :: true':false'
node' :: empty':node' → empty':node' → empty':node'
false' :: true':false'
left' :: empty':node' → empty':node'
right' :: empty':node' → empty':node'
inc' :: 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
count' :: empty':node' → 0':s' → 0':s'
if' :: true':false' → true':false' → empty':node' → empty':node' → 0':s' → 0':s' → 0':s'
nrOfNodes' :: empty':node' → 0':s'
_hole_true':false'1 :: true':false'
_hole_empty':node'2 :: empty':node'
_hole_0':s'3 :: 0':s'
_gen_empty':node'4 :: Nat → empty':node'
_gen_0':s'5 :: Nat → 0':s'
Generator Equations:
_gen_empty':node'4(0) ⇔ empty'
_gen_empty':node'4(+(x, 1)) ⇔ node'(empty', _gen_empty':node'4(x))
_gen_0':s'5(0) ⇔ 0'
_gen_0':s'5(+(x, 1)) ⇔ s'(_gen_0':s'5(x))
The following defined symbols remain to be analysed:
inc', count'
They will be analysed ascendingly in the following order:
inc' < count'
Proved the following rewrite lemma:
inc'(_gen_0':s'5(_n7)) → _gen_0':s'5(+(1, _n7)), rt ∈ Ω(1 + n7)
Induction Base:
inc'(_gen_0':s'5(0)) →RΩ(1)
s'(0')
Induction Step:
inc'(_gen_0':s'5(+(_$n8, 1))) →RΩ(1)
s'(inc'(_gen_0':s'5(_$n8))) →IH
s'(_gen_0':s'5(+(1, _$n8)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
isEmpty'(empty') → true'
isEmpty'(node'(l, r)) → false'
left'(empty') → empty'
left'(node'(l, r)) → l
right'(empty') → empty'
right'(node'(l, r)) → r
inc'(0') → s'(0')
inc'(s'(x)) → s'(inc'(x))
count'(n, x) → if'(isEmpty'(n), isEmpty'(left'(n)), right'(n), node'(left'(left'(n)), node'(right'(left'(n)), right'(n))), x, inc'(x))
if'(true', b, n, m, x, y) → x
if'(false', false', n, m, x, y) → count'(m, x)
if'(false', true', n, m, x, y) → count'(n, y)
nrOfNodes'(n) → count'(n, 0')
Types:
isEmpty' :: empty':node' → true':false'
empty' :: empty':node'
true' :: true':false'
node' :: empty':node' → empty':node' → empty':node'
false' :: true':false'
left' :: empty':node' → empty':node'
right' :: empty':node' → empty':node'
inc' :: 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
count' :: empty':node' → 0':s' → 0':s'
if' :: true':false' → true':false' → empty':node' → empty':node' → 0':s' → 0':s' → 0':s'
nrOfNodes' :: empty':node' → 0':s'
_hole_true':false'1 :: true':false'
_hole_empty':node'2 :: empty':node'
_hole_0':s'3 :: 0':s'
_gen_empty':node'4 :: Nat → empty':node'
_gen_0':s'5 :: Nat → 0':s'
Lemmas:
inc'(_gen_0':s'5(_n7)) → _gen_0':s'5(+(1, _n7)), rt ∈ Ω(1 + n7)
Generator Equations:
_gen_empty':node'4(0) ⇔ empty'
_gen_empty':node'4(+(x, 1)) ⇔ node'(empty', _gen_empty':node'4(x))
_gen_0':s'5(0) ⇔ 0'
_gen_0':s'5(+(x, 1)) ⇔ s'(_gen_0':s'5(x))
The following defined symbols remain to be analysed:
count'
Could not prove a rewrite lemma for the defined symbol count'.
The following conjecture could not be proven:
count'(_gen_empty':node'4(_n620), _gen_0':s'5(b)) →? _gen_0':s'5(+(_n620, b))
Rules:
isEmpty'(empty') → true'
isEmpty'(node'(l, r)) → false'
left'(empty') → empty'
left'(node'(l, r)) → l
right'(empty') → empty'
right'(node'(l, r)) → r
inc'(0') → s'(0')
inc'(s'(x)) → s'(inc'(x))
count'(n, x) → if'(isEmpty'(n), isEmpty'(left'(n)), right'(n), node'(left'(left'(n)), node'(right'(left'(n)), right'(n))), x, inc'(x))
if'(true', b, n, m, x, y) → x
if'(false', false', n, m, x, y) → count'(m, x)
if'(false', true', n, m, x, y) → count'(n, y)
nrOfNodes'(n) → count'(n, 0')
Types:
isEmpty' :: empty':node' → true':false'
empty' :: empty':node'
true' :: true':false'
node' :: empty':node' → empty':node' → empty':node'
false' :: true':false'
left' :: empty':node' → empty':node'
right' :: empty':node' → empty':node'
inc' :: 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
count' :: empty':node' → 0':s' → 0':s'
if' :: true':false' → true':false' → empty':node' → empty':node' → 0':s' → 0':s' → 0':s'
nrOfNodes' :: empty':node' → 0':s'
_hole_true':false'1 :: true':false'
_hole_empty':node'2 :: empty':node'
_hole_0':s'3 :: 0':s'
_gen_empty':node'4 :: Nat → empty':node'
_gen_0':s'5 :: Nat → 0':s'
Lemmas:
inc'(_gen_0':s'5(_n7)) → _gen_0':s'5(+(1, _n7)), rt ∈ Ω(1 + n7)
Generator Equations:
_gen_empty':node'4(0) ⇔ empty'
_gen_empty':node'4(+(x, 1)) ⇔ node'(empty', _gen_empty':node'4(x))
_gen_0':s'5(0) ⇔ 0'
_gen_0':s'5(+(x, 1)) ⇔ s'(_gen_0':s'5(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
inc'(_gen_0':s'5(_n7)) → _gen_0':s'5(+(1, _n7)), rt ∈ Ω(1 + n7)