is_empty(nil) → true
is_empty(cons(x, l)) → false
hd(cons(x, l)) → x
tl(cons(x, l)) → l
append(l1, l2) → ifappend(l1, l2, is_empty(l1))
ifappend(l1, l2, true) → l2
ifappend(l1, l2, false) → cons(hd(l1), append(tl(l1), l2))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
is_empty'(nil') → true'
is_empty'(cons'(x, l)) → false'
hd'(cons'(x, l)) → x
tl'(cons'(x, l)) → l
append'(l1, l2) → ifappend'(l1, l2, is_empty'(l1))
ifappend'(l1, l2, true') → l2
ifappend'(l1, l2, false') → cons'(hd'(l1), append'(tl'(l1), l2))
Infered types.
Rules:
is_empty'(nil') → true'
is_empty'(cons'(x, l)) → false'
hd'(cons'(x, l)) → x
tl'(cons'(x, l)) → l
append'(l1, l2) → ifappend'(l1, l2, is_empty'(l1))
ifappend'(l1, l2, true') → l2
ifappend'(l1, l2, false') → cons'(hd'(l1), append'(tl'(l1), l2))
Types:
is_empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: hd' → nil':cons' → nil':cons'
false' :: true':false'
hd' :: nil':cons' → hd'
tl' :: nil':cons' → nil':cons'
append' :: nil':cons' → nil':cons' → nil':cons'
ifappend' :: nil':cons' → nil':cons' → true':false' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_hd'3 :: hd'
_gen_nil':cons'4 :: Nat → nil':cons'
Heuristically decided to analyse the following defined symbols:
append'
Rules:
is_empty'(nil') → true'
is_empty'(cons'(x, l)) → false'
hd'(cons'(x, l)) → x
tl'(cons'(x, l)) → l
append'(l1, l2) → ifappend'(l1, l2, is_empty'(l1))
ifappend'(l1, l2, true') → l2
ifappend'(l1, l2, false') → cons'(hd'(l1), append'(tl'(l1), l2))
Types:
is_empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: hd' → nil':cons' → nil':cons'
false' :: true':false'
hd' :: nil':cons' → hd'
tl' :: nil':cons' → nil':cons'
append' :: nil':cons' → nil':cons' → nil':cons'
ifappend' :: nil':cons' → nil':cons' → true':false' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_hd'3 :: hd'
_gen_nil':cons'4 :: Nat → nil':cons'
Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(_hole_hd'3, _gen_nil':cons'4(x))
The following defined symbols remain to be analysed:
append'
Proved the following rewrite lemma:
append'(_gen_nil':cons'4(_n6), _gen_nil':cons'4(b)) → _gen_nil':cons'4(+(_n6, b)), rt ∈ Ω(1 + n6)
Induction Base:
append'(_gen_nil':cons'4(0), _gen_nil':cons'4(b)) →RΩ(1)
ifappend'(_gen_nil':cons'4(0), _gen_nil':cons'4(b), is_empty'(_gen_nil':cons'4(0))) →RΩ(1)
ifappend'(_gen_nil':cons'4(0), _gen_nil':cons'4(b), true') →RΩ(1)
_gen_nil':cons'4(b)
Induction Step:
append'(_gen_nil':cons'4(+(_$n7, 1)), _gen_nil':cons'4(_b304)) →RΩ(1)
ifappend'(_gen_nil':cons'4(+(_$n7, 1)), _gen_nil':cons'4(_b304), is_empty'(_gen_nil':cons'4(+(_$n7, 1)))) →RΩ(1)
ifappend'(_gen_nil':cons'4(+(1, _$n7)), _gen_nil':cons'4(_b304), false') →RΩ(1)
cons'(hd'(_gen_nil':cons'4(+(1, _$n7))), append'(tl'(_gen_nil':cons'4(+(1, _$n7))), _gen_nil':cons'4(_b304))) →RΩ(1)
cons'(_hole_hd'3, append'(tl'(_gen_nil':cons'4(+(1, _$n7))), _gen_nil':cons'4(_b304))) →RΩ(1)
cons'(_hole_hd'3, append'(_gen_nil':cons'4(_$n7), _gen_nil':cons'4(_b304))) →IH
cons'(_hole_hd'3, _gen_nil':cons'4(+(_$n7, _b304)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
is_empty'(nil') → true'
is_empty'(cons'(x, l)) → false'
hd'(cons'(x, l)) → x
tl'(cons'(x, l)) → l
append'(l1, l2) → ifappend'(l1, l2, is_empty'(l1))
ifappend'(l1, l2, true') → l2
ifappend'(l1, l2, false') → cons'(hd'(l1), append'(tl'(l1), l2))
Types:
is_empty' :: nil':cons' → true':false'
nil' :: nil':cons'
true' :: true':false'
cons' :: hd' → nil':cons' → nil':cons'
false' :: true':false'
hd' :: nil':cons' → hd'
tl' :: nil':cons' → nil':cons'
append' :: nil':cons' → nil':cons' → nil':cons'
ifappend' :: nil':cons' → nil':cons' → true':false' → nil':cons'
_hole_true':false'1 :: true':false'
_hole_nil':cons'2 :: nil':cons'
_hole_hd'3 :: hd'
_gen_nil':cons'4 :: Nat → nil':cons'
Lemmas:
append'(_gen_nil':cons'4(_n6), _gen_nil':cons'4(b)) → _gen_nil':cons'4(+(_n6, b)), rt ∈ Ω(1 + n6)
Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(_hole_hd'3, _gen_nil':cons'4(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
append'(_gen_nil':cons'4(_n6), _gen_nil':cons'4(b)) → _gen_nil':cons'4(+(_n6, b)), rt ∈ Ω(1 + n6)