append(@l1, @l2) → append#1(@l1, @l2)
append#1(::(@x, @xs), @l2) → ::(@x, append(@xs, @l2))
append#1(nil, @l2) → @l2
subtrees(@t) → subtrees#1(@t)
subtrees#1(leaf) → nil
subtrees#1(node(@x, @t1, @t2)) → subtrees#2(subtrees(@t1), @t1, @t2, @x)
subtrees#2(@l1, @t1, @t2, @x) → subtrees#3(subtrees(@t2), @l1, @t1, @t2, @x)
subtrees#3(@l2, @l1, @t1, @t2, @x) → ::(node(@x, @t1, @t2), append(@l1, @l2))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
append'(@l1, @l2) → append#1'(@l1, @l2)
append#1'(::'(@x, @xs), @l2) → ::'(@x, append'(@xs, @l2))
append#1'(nil', @l2) → @l2
subtrees'(@t) → subtrees#1'(@t)
subtrees#1'(leaf') → nil'
subtrees#1'(node'(@x, @t1, @t2)) → subtrees#2'(subtrees'(@t1), @t1, @t2, @x)
subtrees#2'(@l1, @t1, @t2, @x) → subtrees#3'(subtrees'(@t2), @l1, @t1, @t2, @x)
subtrees#3'(@l2, @l1, @t1, @t2, @x) → ::'(node'(@x, @t1, @t2), append'(@l1, @l2))
Sliced the following arguments:
::'/0
node'/0
subtrees#2'/1
subtrees#2'/3
subtrees#3'/2
subtrees#3'/3
subtrees#3'/4
Runtime Complexity TRS:
The TRS R consists of the following rules:
append'(@l1, @l2) → append#1'(@l1, @l2)
append#1'(::'(@xs), @l2) → ::'(append'(@xs, @l2))
append#1'(nil', @l2) → @l2
subtrees'(@t) → subtrees#1'(@t)
subtrees#1'(leaf') → nil'
subtrees#1'(node'(@t1, @t2)) → subtrees#2'(subtrees'(@t1), @t2)
subtrees#2'(@l1, @t2) → subtrees#3'(subtrees'(@t2), @l1)
subtrees#3'(@l2, @l1) → ::'(append'(@l1, @l2))
Infered types.
Rules:
append'(@l1, @l2) → append#1'(@l1, @l2)
append#1'(::'(@xs), @l2) → ::'(append'(@xs, @l2))
append#1'(nil', @l2) → @l2
subtrees'(@t) → subtrees#1'(@t)
subtrees#1'(leaf') → nil'
subtrees#1'(node'(@t1, @t2)) → subtrees#2'(subtrees'(@t1), @t2)
subtrees#2'(@l1, @t2) → subtrees#3'(subtrees'(@t2), @l1)
subtrees#3'(@l2, @l1) → ::'(append'(@l1, @l2))
Types:
append' :: ::':nil' → ::':nil' → ::':nil'
append#1' :: ::':nil' → ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil'
nil' :: ::':nil'
subtrees' :: leaf':node' → ::':nil'
subtrees#1' :: leaf':node' → ::':nil'
leaf' :: leaf':node'
node' :: leaf':node' → leaf':node' → leaf':node'
subtrees#2' :: ::':nil' → leaf':node' → ::':nil'
subtrees#3' :: ::':nil' → ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_hole_leaf':node'2 :: leaf':node'
_gen_::':nil'3 :: Nat → ::':nil'
_gen_leaf':node'4 :: Nat → leaf':node'
Heuristically decided to analyse the following defined symbols:
append', append#1', subtrees', subtrees#1'
They will be analysed ascendingly in the following order:
append' = append#1'
subtrees' = subtrees#1'
Rules:
append'(@l1, @l2) → append#1'(@l1, @l2)
append#1'(::'(@xs), @l2) → ::'(append'(@xs, @l2))
append#1'(nil', @l2) → @l2
subtrees'(@t) → subtrees#1'(@t)
subtrees#1'(leaf') → nil'
subtrees#1'(node'(@t1, @t2)) → subtrees#2'(subtrees'(@t1), @t2)
subtrees#2'(@l1, @t2) → subtrees#3'(subtrees'(@t2), @l1)
subtrees#3'(@l2, @l1) → ::'(append'(@l1, @l2))
Types:
append' :: ::':nil' → ::':nil' → ::':nil'
append#1' :: ::':nil' → ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil'
nil' :: ::':nil'
subtrees' :: leaf':node' → ::':nil'
subtrees#1' :: leaf':node' → ::':nil'
leaf' :: leaf':node'
node' :: leaf':node' → leaf':node' → leaf':node'
subtrees#2' :: ::':nil' → leaf':node' → ::':nil'
subtrees#3' :: ::':nil' → ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_hole_leaf':node'2 :: leaf':node'
_gen_::':nil'3 :: Nat → ::':nil'
_gen_leaf':node'4 :: Nat → leaf':node'
Generator Equations:
_gen_::':nil'3(0) ⇔ nil'
_gen_::':nil'3(+(x, 1)) ⇔ ::'(_gen_::':nil'3(x))
_gen_leaf':node'4(0) ⇔ leaf'
_gen_leaf':node'4(+(x, 1)) ⇔ node'(leaf', _gen_leaf':node'4(x))
The following defined symbols remain to be analysed:
subtrees#1', append', append#1', subtrees'
They will be analysed ascendingly in the following order:
append' = append#1'
subtrees' = subtrees#1'
Proved the following rewrite lemma:
subtrees#1'(_gen_leaf':node'4(_n6)) → _gen_::':nil'3(_n6), rt ∈ Ω(1 + n6)
Induction Base:
subtrees#1'(_gen_leaf':node'4(0)) →RΩ(1)
nil'
Induction Step:
subtrees#1'(_gen_leaf':node'4(+(_$n7, 1))) →RΩ(1)
subtrees#2'(subtrees'(leaf'), _gen_leaf':node'4(_$n7)) →RΩ(1)
subtrees#2'(subtrees#1'(leaf'), _gen_leaf':node'4(_$n7)) →RΩ(1)
subtrees#2'(nil', _gen_leaf':node'4(_$n7)) →RΩ(1)
subtrees#3'(subtrees'(_gen_leaf':node'4(_$n7)), nil') →RΩ(1)
subtrees#3'(subtrees#1'(_gen_leaf':node'4(_$n7)), nil') →IH
subtrees#3'(_gen_::':nil'3(_$n7), nil') →RΩ(1)
::'(append'(nil', _gen_::':nil'3(_$n7))) →RΩ(1)
::'(append#1'(nil', _gen_::':nil'3(_$n7))) →RΩ(1)
::'(_gen_::':nil'3(_$n7))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
append'(@l1, @l2) → append#1'(@l1, @l2)
append#1'(::'(@xs), @l2) → ::'(append'(@xs, @l2))
append#1'(nil', @l2) → @l2
subtrees'(@t) → subtrees#1'(@t)
subtrees#1'(leaf') → nil'
subtrees#1'(node'(@t1, @t2)) → subtrees#2'(subtrees'(@t1), @t2)
subtrees#2'(@l1, @t2) → subtrees#3'(subtrees'(@t2), @l1)
subtrees#3'(@l2, @l1) → ::'(append'(@l1, @l2))
Types:
append' :: ::':nil' → ::':nil' → ::':nil'
append#1' :: ::':nil' → ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil'
nil' :: ::':nil'
subtrees' :: leaf':node' → ::':nil'
subtrees#1' :: leaf':node' → ::':nil'
leaf' :: leaf':node'
node' :: leaf':node' → leaf':node' → leaf':node'
subtrees#2' :: ::':nil' → leaf':node' → ::':nil'
subtrees#3' :: ::':nil' → ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_hole_leaf':node'2 :: leaf':node'
_gen_::':nil'3 :: Nat → ::':nil'
_gen_leaf':node'4 :: Nat → leaf':node'
Lemmas:
subtrees#1'(_gen_leaf':node'4(_n6)) → _gen_::':nil'3(_n6), rt ∈ Ω(1 + n6)
Generator Equations:
_gen_::':nil'3(0) ⇔ nil'
_gen_::':nil'3(+(x, 1)) ⇔ ::'(_gen_::':nil'3(x))
_gen_leaf':node'4(0) ⇔ leaf'
_gen_leaf':node'4(+(x, 1)) ⇔ node'(leaf', _gen_leaf':node'4(x))
The following defined symbols remain to be analysed:
subtrees', append', append#1'
They will be analysed ascendingly in the following order:
append' = append#1'
subtrees' = subtrees#1'
Could not prove a rewrite lemma for the defined symbol subtrees'.
Rules:
append'(@l1, @l2) → append#1'(@l1, @l2)
append#1'(::'(@xs), @l2) → ::'(append'(@xs, @l2))
append#1'(nil', @l2) → @l2
subtrees'(@t) → subtrees#1'(@t)
subtrees#1'(leaf') → nil'
subtrees#1'(node'(@t1, @t2)) → subtrees#2'(subtrees'(@t1), @t2)
subtrees#2'(@l1, @t2) → subtrees#3'(subtrees'(@t2), @l1)
subtrees#3'(@l2, @l1) → ::'(append'(@l1, @l2))
Types:
append' :: ::':nil' → ::':nil' → ::':nil'
append#1' :: ::':nil' → ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil'
nil' :: ::':nil'
subtrees' :: leaf':node' → ::':nil'
subtrees#1' :: leaf':node' → ::':nil'
leaf' :: leaf':node'
node' :: leaf':node' → leaf':node' → leaf':node'
subtrees#2' :: ::':nil' → leaf':node' → ::':nil'
subtrees#3' :: ::':nil' → ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_hole_leaf':node'2 :: leaf':node'
_gen_::':nil'3 :: Nat → ::':nil'
_gen_leaf':node'4 :: Nat → leaf':node'
Lemmas:
subtrees#1'(_gen_leaf':node'4(_n6)) → _gen_::':nil'3(_n6), rt ∈ Ω(1 + n6)
Generator Equations:
_gen_::':nil'3(0) ⇔ nil'
_gen_::':nil'3(+(x, 1)) ⇔ ::'(_gen_::':nil'3(x))
_gen_leaf':node'4(0) ⇔ leaf'
_gen_leaf':node'4(+(x, 1)) ⇔ node'(leaf', _gen_leaf':node'4(x))
The following defined symbols remain to be analysed:
append#1', append'
They will be analysed ascendingly in the following order:
append' = append#1'
Proved the following rewrite lemma:
append#1'(_gen_::':nil'3(_n805), _gen_::':nil'3(b)) → _gen_::':nil'3(+(_n805, b)), rt ∈ Ω(1 + n805)
Induction Base:
append#1'(_gen_::':nil'3(0), _gen_::':nil'3(b)) →RΩ(1)
_gen_::':nil'3(b)
Induction Step:
append#1'(_gen_::':nil'3(+(_$n806, 1)), _gen_::':nil'3(_b978)) →RΩ(1)
::'(append'(_gen_::':nil'3(_$n806), _gen_::':nil'3(_b978))) →RΩ(1)
::'(append#1'(_gen_::':nil'3(_$n806), _gen_::':nil'3(_b978))) →IH
::'(_gen_::':nil'3(+(_$n806, _b978)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
append'(@l1, @l2) → append#1'(@l1, @l2)
append#1'(::'(@xs), @l2) → ::'(append'(@xs, @l2))
append#1'(nil', @l2) → @l2
subtrees'(@t) → subtrees#1'(@t)
subtrees#1'(leaf') → nil'
subtrees#1'(node'(@t1, @t2)) → subtrees#2'(subtrees'(@t1), @t2)
subtrees#2'(@l1, @t2) → subtrees#3'(subtrees'(@t2), @l1)
subtrees#3'(@l2, @l1) → ::'(append'(@l1, @l2))
Types:
append' :: ::':nil' → ::':nil' → ::':nil'
append#1' :: ::':nil' → ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil'
nil' :: ::':nil'
subtrees' :: leaf':node' → ::':nil'
subtrees#1' :: leaf':node' → ::':nil'
leaf' :: leaf':node'
node' :: leaf':node' → leaf':node' → leaf':node'
subtrees#2' :: ::':nil' → leaf':node' → ::':nil'
subtrees#3' :: ::':nil' → ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_hole_leaf':node'2 :: leaf':node'
_gen_::':nil'3 :: Nat → ::':nil'
_gen_leaf':node'4 :: Nat → leaf':node'
Lemmas:
subtrees#1'(_gen_leaf':node'4(_n6)) → _gen_::':nil'3(_n6), rt ∈ Ω(1 + n6)
append#1'(_gen_::':nil'3(_n805), _gen_::':nil'3(b)) → _gen_::':nil'3(+(_n805, b)), rt ∈ Ω(1 + n805)
Generator Equations:
_gen_::':nil'3(0) ⇔ nil'
_gen_::':nil'3(+(x, 1)) ⇔ ::'(_gen_::':nil'3(x))
_gen_leaf':node'4(0) ⇔ leaf'
_gen_leaf':node'4(+(x, 1)) ⇔ node'(leaf', _gen_leaf':node'4(x))
The following defined symbols remain to be analysed:
append'
They will be analysed ascendingly in the following order:
append' = append#1'
Could not prove a rewrite lemma for the defined symbol append'.
Rules:
append'(@l1, @l2) → append#1'(@l1, @l2)
append#1'(::'(@xs), @l2) → ::'(append'(@xs, @l2))
append#1'(nil', @l2) → @l2
subtrees'(@t) → subtrees#1'(@t)
subtrees#1'(leaf') → nil'
subtrees#1'(node'(@t1, @t2)) → subtrees#2'(subtrees'(@t1), @t2)
subtrees#2'(@l1, @t2) → subtrees#3'(subtrees'(@t2), @l1)
subtrees#3'(@l2, @l1) → ::'(append'(@l1, @l2))
Types:
append' :: ::':nil' → ::':nil' → ::':nil'
append#1' :: ::':nil' → ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil'
nil' :: ::':nil'
subtrees' :: leaf':node' → ::':nil'
subtrees#1' :: leaf':node' → ::':nil'
leaf' :: leaf':node'
node' :: leaf':node' → leaf':node' → leaf':node'
subtrees#2' :: ::':nil' → leaf':node' → ::':nil'
subtrees#3' :: ::':nil' → ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_hole_leaf':node'2 :: leaf':node'
_gen_::':nil'3 :: Nat → ::':nil'
_gen_leaf':node'4 :: Nat → leaf':node'
Lemmas:
subtrees#1'(_gen_leaf':node'4(_n6)) → _gen_::':nil'3(_n6), rt ∈ Ω(1 + n6)
append#1'(_gen_::':nil'3(_n805), _gen_::':nil'3(b)) → _gen_::':nil'3(+(_n805, b)), rt ∈ Ω(1 + n805)
Generator Equations:
_gen_::':nil'3(0) ⇔ nil'
_gen_::':nil'3(+(x, 1)) ⇔ ::'(_gen_::':nil'3(x))
_gen_leaf':node'4(0) ⇔ leaf'
_gen_leaf':node'4(+(x, 1)) ⇔ node'(leaf', _gen_leaf':node'4(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
subtrees#1'(_gen_leaf':node'4(_n6)) → _gen_::':nil'3(_n6), rt ∈ Ω(1 + n6)