isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
less_leaves(u, v) → if1(isLeaf(u), isLeaf(v), u, v)
if1(b, true, u, v) → false
if1(b, false, u, v) → if2(b, u, v)
if2(true, u, v) → true
if2(false, u, v) → less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
isLeaf'(leaf') → true'
isLeaf'(cons'(u, v)) → false'
left'(cons'(u, v)) → u
right'(cons'(u, v)) → v
concat'(leaf', y) → y
concat'(cons'(u, v), y) → cons'(u, concat'(v, y))
less_leaves'(u, v) → if1'(isLeaf'(u), isLeaf'(v), u, v)
if1'(b, true', u, v) → false'
if1'(b, false', u, v) → if2'(b, u, v)
if2'(true', u, v) → true'
if2'(false', u, v) → less_leaves'(concat'(left'(u), right'(u)), concat'(left'(v), right'(v)))
Infered types.
Rules:
isLeaf'(leaf') → true'
isLeaf'(cons'(u, v)) → false'
left'(cons'(u, v)) → u
right'(cons'(u, v)) → v
concat'(leaf', y) → y
concat'(cons'(u, v), y) → cons'(u, concat'(v, y))
less_leaves'(u, v) → if1'(isLeaf'(u), isLeaf'(v), u, v)
if1'(b, true', u, v) → false'
if1'(b, false', u, v) → if2'(b, u, v)
if2'(true', u, v) → true'
if2'(false', u, v) → less_leaves'(concat'(left'(u), right'(u)), concat'(left'(v), right'(v)))
Types:
isLeaf' :: leaf':cons' → true':false'
leaf' :: leaf':cons'
true' :: true':false'
cons' :: leaf':cons' → leaf':cons' → leaf':cons'
false' :: true':false'
left' :: leaf':cons' → leaf':cons'
right' :: leaf':cons' → leaf':cons'
concat' :: leaf':cons' → leaf':cons' → leaf':cons'
less_leaves' :: leaf':cons' → leaf':cons' → true':false'
if1' :: true':false' → true':false' → leaf':cons' → leaf':cons' → true':false'
if2' :: true':false' → leaf':cons' → leaf':cons' → true':false'
_hole_true':false'1 :: true':false'
_hole_leaf':cons'2 :: leaf':cons'
_gen_leaf':cons'3 :: Nat → leaf':cons'
Heuristically decided to analyse the following defined symbols:
concat', less_leaves'
They will be analysed ascendingly in the following order:
concat' < less_leaves'
Rules:
isLeaf'(leaf') → true'
isLeaf'(cons'(u, v)) → false'
left'(cons'(u, v)) → u
right'(cons'(u, v)) → v
concat'(leaf', y) → y
concat'(cons'(u, v), y) → cons'(u, concat'(v, y))
less_leaves'(u, v) → if1'(isLeaf'(u), isLeaf'(v), u, v)
if1'(b, true', u, v) → false'
if1'(b, false', u, v) → if2'(b, u, v)
if2'(true', u, v) → true'
if2'(false', u, v) → less_leaves'(concat'(left'(u), right'(u)), concat'(left'(v), right'(v)))
Types:
isLeaf' :: leaf':cons' → true':false'
leaf' :: leaf':cons'
true' :: true':false'
cons' :: leaf':cons' → leaf':cons' → leaf':cons'
false' :: true':false'
left' :: leaf':cons' → leaf':cons'
right' :: leaf':cons' → leaf':cons'
concat' :: leaf':cons' → leaf':cons' → leaf':cons'
less_leaves' :: leaf':cons' → leaf':cons' → true':false'
if1' :: true':false' → true':false' → leaf':cons' → leaf':cons' → true':false'
if2' :: true':false' → leaf':cons' → leaf':cons' → true':false'
_hole_true':false'1 :: true':false'
_hole_leaf':cons'2 :: leaf':cons'
_gen_leaf':cons'3 :: Nat → leaf':cons'
Generator Equations:
_gen_leaf':cons'3(0) ⇔ leaf'
_gen_leaf':cons'3(+(x, 1)) ⇔ cons'(leaf', _gen_leaf':cons'3(x))
The following defined symbols remain to be analysed:
concat', less_leaves'
They will be analysed ascendingly in the following order:
concat' < less_leaves'
Proved the following rewrite lemma:
concat'(_gen_leaf':cons'3(_n5), _gen_leaf':cons'3(b)) → _gen_leaf':cons'3(+(_n5, b)), rt ∈ Ω(1 + n5)
Induction Base:
concat'(_gen_leaf':cons'3(0), _gen_leaf':cons'3(b)) →RΩ(1)
_gen_leaf':cons'3(b)
Induction Step:
concat'(_gen_leaf':cons'3(+(_$n6, 1)), _gen_leaf':cons'3(_b146)) →RΩ(1)
cons'(leaf', concat'(_gen_leaf':cons'3(_$n6), _gen_leaf':cons'3(_b146))) →IH
cons'(leaf', _gen_leaf':cons'3(+(_$n6, _b146)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
isLeaf'(leaf') → true'
isLeaf'(cons'(u, v)) → false'
left'(cons'(u, v)) → u
right'(cons'(u, v)) → v
concat'(leaf', y) → y
concat'(cons'(u, v), y) → cons'(u, concat'(v, y))
less_leaves'(u, v) → if1'(isLeaf'(u), isLeaf'(v), u, v)
if1'(b, true', u, v) → false'
if1'(b, false', u, v) → if2'(b, u, v)
if2'(true', u, v) → true'
if2'(false', u, v) → less_leaves'(concat'(left'(u), right'(u)), concat'(left'(v), right'(v)))
Types:
isLeaf' :: leaf':cons' → true':false'
leaf' :: leaf':cons'
true' :: true':false'
cons' :: leaf':cons' → leaf':cons' → leaf':cons'
false' :: true':false'
left' :: leaf':cons' → leaf':cons'
right' :: leaf':cons' → leaf':cons'
concat' :: leaf':cons' → leaf':cons' → leaf':cons'
less_leaves' :: leaf':cons' → leaf':cons' → true':false'
if1' :: true':false' → true':false' → leaf':cons' → leaf':cons' → true':false'
if2' :: true':false' → leaf':cons' → leaf':cons' → true':false'
_hole_true':false'1 :: true':false'
_hole_leaf':cons'2 :: leaf':cons'
_gen_leaf':cons'3 :: Nat → leaf':cons'
Lemmas:
concat'(_gen_leaf':cons'3(_n5), _gen_leaf':cons'3(b)) → _gen_leaf':cons'3(+(_n5, b)), rt ∈ Ω(1 + n5)
Generator Equations:
_gen_leaf':cons'3(0) ⇔ leaf'
_gen_leaf':cons'3(+(x, 1)) ⇔ cons'(leaf', _gen_leaf':cons'3(x))
The following defined symbols remain to be analysed:
less_leaves'
Proved the following rewrite lemma:
less_leaves'(_gen_leaf':cons'3(_n861), _gen_leaf':cons'3(_n861)) → _*4, rt ∈ Ω(n861)
Induction Base:
less_leaves'(_gen_leaf':cons'3(0), _gen_leaf':cons'3(0))
Induction Step:
less_leaves'(_gen_leaf':cons'3(+(_$n862, 1)), _gen_leaf':cons'3(+(_$n862, 1))) →RΩ(1)
if1'(isLeaf'(_gen_leaf':cons'3(+(_$n862, 1))), isLeaf'(_gen_leaf':cons'3(+(_$n862, 1))), _gen_leaf':cons'3(+(_$n862, 1)), _gen_leaf':cons'3(+(_$n862, 1))) →RΩ(1)
if1'(false', isLeaf'(_gen_leaf':cons'3(+(1, _$n862))), _gen_leaf':cons'3(+(1, _$n862)), _gen_leaf':cons'3(+(1, _$n862))) →RΩ(1)
if1'(false', false', _gen_leaf':cons'3(+(1, _$n862)), _gen_leaf':cons'3(+(1, _$n862))) →RΩ(1)
if2'(false', _gen_leaf':cons'3(+(1, _$n862)), _gen_leaf':cons'3(+(1, _$n862))) →RΩ(1)
less_leaves'(concat'(left'(_gen_leaf':cons'3(+(1, _$n862))), right'(_gen_leaf':cons'3(+(1, _$n862)))), concat'(left'(_gen_leaf':cons'3(+(1, _$n862))), right'(_gen_leaf':cons'3(+(1, _$n862))))) →RΩ(1)
less_leaves'(concat'(leaf', right'(_gen_leaf':cons'3(+(1, _$n862)))), concat'(left'(_gen_leaf':cons'3(+(1, _$n862))), right'(_gen_leaf':cons'3(+(1, _$n862))))) →RΩ(1)
less_leaves'(concat'(leaf', _gen_leaf':cons'3(_$n862)), concat'(left'(_gen_leaf':cons'3(+(1, _$n862))), right'(_gen_leaf':cons'3(+(1, _$n862))))) →LΩ(1)
less_leaves'(_gen_leaf':cons'3(+(0, _$n862)), concat'(left'(_gen_leaf':cons'3(+(1, _$n862))), right'(_gen_leaf':cons'3(+(1, _$n862))))) →RΩ(1)
less_leaves'(_gen_leaf':cons'3(_$n862), concat'(leaf', right'(_gen_leaf':cons'3(+(1, _$n862))))) →RΩ(1)
less_leaves'(_gen_leaf':cons'3(_$n862), concat'(leaf', _gen_leaf':cons'3(_$n862))) →LΩ(1)
less_leaves'(_gen_leaf':cons'3(_$n862), _gen_leaf':cons'3(+(0, _$n862))) →IH
_*4
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
isLeaf'(leaf') → true'
isLeaf'(cons'(u, v)) → false'
left'(cons'(u, v)) → u
right'(cons'(u, v)) → v
concat'(leaf', y) → y
concat'(cons'(u, v), y) → cons'(u, concat'(v, y))
less_leaves'(u, v) → if1'(isLeaf'(u), isLeaf'(v), u, v)
if1'(b, true', u, v) → false'
if1'(b, false', u, v) → if2'(b, u, v)
if2'(true', u, v) → true'
if2'(false', u, v) → less_leaves'(concat'(left'(u), right'(u)), concat'(left'(v), right'(v)))
Types:
isLeaf' :: leaf':cons' → true':false'
leaf' :: leaf':cons'
true' :: true':false'
cons' :: leaf':cons' → leaf':cons' → leaf':cons'
false' :: true':false'
left' :: leaf':cons' → leaf':cons'
right' :: leaf':cons' → leaf':cons'
concat' :: leaf':cons' → leaf':cons' → leaf':cons'
less_leaves' :: leaf':cons' → leaf':cons' → true':false'
if1' :: true':false' → true':false' → leaf':cons' → leaf':cons' → true':false'
if2' :: true':false' → leaf':cons' → leaf':cons' → true':false'
_hole_true':false'1 :: true':false'
_hole_leaf':cons'2 :: leaf':cons'
_gen_leaf':cons'3 :: Nat → leaf':cons'
Lemmas:
concat'(_gen_leaf':cons'3(_n5), _gen_leaf':cons'3(b)) → _gen_leaf':cons'3(+(_n5, b)), rt ∈ Ω(1 + n5)
less_leaves'(_gen_leaf':cons'3(_n861), _gen_leaf':cons'3(_n861)) → _*4, rt ∈ Ω(n861)
Generator Equations:
_gen_leaf':cons'3(0) ⇔ leaf'
_gen_leaf':cons'3(+(x, 1)) ⇔ cons'(leaf', _gen_leaf':cons'3(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
concat'(_gen_leaf':cons'3(_n5), _gen_leaf':cons'3(b)) → _gen_leaf':cons'3(+(_n5, b)), rt ∈ Ω(1 + n5)