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, l1)
ifappend(l1, l2, nil) → l2
ifappend(l1, l2, cons(x, l)) → cons(x, append(l, 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, l1)
ifappend'(l1, l2, nil') → l2
ifappend'(l1, l2, cons'(x, l)) → cons'(x, append'(l, l2))
Sliced the following arguments:
ifappend'/0
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'(l2, l1)
ifappend'(l2, nil') → l2
ifappend'(l2, cons'(x, l)) → cons'(x, append'(l, 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'(l2, l1)
ifappend'(l2, nil') → l2
ifappend'(l2, cons'(x, l)) → cons'(x, append'(l, 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' → 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', ifappend'
They will be analysed ascendingly in the following order:
append' = ifappend'
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'(l2, l1)
ifappend'(l2, nil') → l2
ifappend'(l2, cons'(x, l)) → cons'(x, append'(l, 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' → 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:
ifappend', append'
They will be analysed ascendingly in the following order:
append' = ifappend'
Proved the following rewrite lemma:
ifappend'(_gen_nil':cons'4(a), _gen_nil':cons'4(_n6)) → _gen_nil':cons'4(+(_n6, a)), rt ∈ Ω(1 + n6)
Induction Base:
ifappend'(_gen_nil':cons'4(a), _gen_nil':cons'4(0)) →RΩ(1)
_gen_nil':cons'4(a)
Induction Step:
ifappend'(_gen_nil':cons'4(_a153), _gen_nil':cons'4(+(_$n7, 1))) →RΩ(1)
cons'(_hole_hd'3, append'(_gen_nil':cons'4(_$n7), _gen_nil':cons'4(_a153))) →RΩ(1)
cons'(_hole_hd'3, ifappend'(_gen_nil':cons'4(_a153), _gen_nil':cons'4(_$n7))) →IH
cons'(_hole_hd'3, _gen_nil':cons'4(+(_$n7, _a153)))
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'(l2, l1)
ifappend'(l2, nil') → l2
ifappend'(l2, cons'(x, l)) → cons'(x, append'(l, 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' → 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:
ifappend'(_gen_nil':cons'4(a), _gen_nil':cons'4(_n6)) → _gen_nil':cons'4(+(_n6, a)), 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))
The following defined symbols remain to be analysed:
append'
They will be analysed ascendingly in the following order:
append' = ifappend'
Could not prove a rewrite lemma for the defined symbol 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'(l2, l1)
ifappend'(l2, nil') → l2
ifappend'(l2, cons'(x, l)) → cons'(x, append'(l, 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' → 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:
ifappend'(_gen_nil':cons'4(a), _gen_nil':cons'4(_n6)) → _gen_nil':cons'4(+(_n6, a)), 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:
ifappend'(_gen_nil':cons'4(a), _gen_nil':cons'4(_n6)) → _gen_nil':cons'4(+(_n6, a)), rt ∈ Ω(1 + n6)