```* Step 1: DependencyPairs WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
append(l1,l2) -> ifappend(l1,l2,l1)
hd(cons(x,l)) -> x
ifappend(l1,l2,cons(x,l)) -> cons(x,append(l,l2))
ifappend(l1,l2,nil()) -> l2
is_empty(cons(x,l)) -> false()
is_empty(nil()) -> true()
tl(cons(x,l)) -> l
- Signature:
{append/2,hd/1,ifappend/3,is_empty/1,tl/1} / {cons/2,false/0,nil/0,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append,hd,ifappend,is_empty,tl} and constructors {cons
,false,nil,true}
+ Applied Processor:
DependencyPairs {dpKind_ = WIDP}
+ Details:
We add the following weak innermost dependency pairs:

Strict DPs
append#(l1,l2) -> c_1(ifappend#(l1,l2,l1))
hd#(cons(x,l)) -> c_2()
ifappend#(l1,l2,cons(x,l)) -> c_3(append#(l,l2))
ifappend#(l1,l2,nil()) -> c_4()
is_empty#(cons(x,l)) -> c_5()
is_empty#(nil()) -> c_6()
tl#(cons(x,l)) -> c_7()
Weak DPs

and mark the set of starting terms.
* Step 2: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
append#(l1,l2) -> c_1(ifappend#(l1,l2,l1))
hd#(cons(x,l)) -> c_2()
ifappend#(l1,l2,cons(x,l)) -> c_3(append#(l,l2))
ifappend#(l1,l2,nil()) -> c_4()
is_empty#(cons(x,l)) -> c_5()
is_empty#(nil()) -> c_6()
tl#(cons(x,l)) -> c_7()
- Strict TRS:
append(l1,l2) -> ifappend(l1,l2,l1)
hd(cons(x,l)) -> x
ifappend(l1,l2,cons(x,l)) -> cons(x,append(l,l2))
ifappend(l1,l2,nil()) -> l2
is_empty(cons(x,l)) -> false()
is_empty(nil()) -> true()
tl(cons(x,l)) -> l
- Signature:
{append/2,hd/1,ifappend/3,is_empty/1,tl/1,append#/2,hd#/1,ifappend#/3,is_empty#/1,tl#/1} / {cons/2,false/0
,nil/0,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/0,c_7/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,hd#,ifappend#,is_empty#
,tl#} and constructors {cons,false,nil,true}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
append#(l1,l2) -> c_1(ifappend#(l1,l2,l1))
hd#(cons(x,l)) -> c_2()
ifappend#(l1,l2,cons(x,l)) -> c_3(append#(l,l2))
ifappend#(l1,l2,nil()) -> c_4()
is_empty#(cons(x,l)) -> c_5()
is_empty#(nil()) -> c_6()
tl#(cons(x,l)) -> c_7()
* Step 3: PredecessorEstimation WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
append#(l1,l2) -> c_1(ifappend#(l1,l2,l1))
hd#(cons(x,l)) -> c_2()
ifappend#(l1,l2,cons(x,l)) -> c_3(append#(l,l2))
ifappend#(l1,l2,nil()) -> c_4()
is_empty#(cons(x,l)) -> c_5()
is_empty#(nil()) -> c_6()
tl#(cons(x,l)) -> c_7()
- Signature:
{append/2,hd/1,ifappend/3,is_empty/1,tl/1,append#/2,hd#/1,ifappend#/3,is_empty#/1,tl#/1} / {cons/2,false/0
,nil/0,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/0,c_7/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,hd#,ifappend#,is_empty#
,tl#} and constructors {cons,false,nil,true}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{2,4,5,6,7}
by application of
Pre({2,4,5,6,7}) = {1}.
Here rules are labelled as follows:
1: append#(l1,l2) -> c_1(ifappend#(l1,l2,l1))
2: hd#(cons(x,l)) -> c_2()
3: ifappend#(l1,l2,cons(x,l)) -> c_3(append#(l,l2))
4: ifappend#(l1,l2,nil()) -> c_4()
5: is_empty#(cons(x,l)) -> c_5()
6: is_empty#(nil()) -> c_6()
7: tl#(cons(x,l)) -> c_7()
* Step 4: RemoveWeakSuffixes WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
append#(l1,l2) -> c_1(ifappend#(l1,l2,l1))
ifappend#(l1,l2,cons(x,l)) -> c_3(append#(l,l2))
- Weak DPs:
hd#(cons(x,l)) -> c_2()
ifappend#(l1,l2,nil()) -> c_4()
is_empty#(cons(x,l)) -> c_5()
is_empty#(nil()) -> c_6()
tl#(cons(x,l)) -> c_7()
- Signature:
{append/2,hd/1,ifappend/3,is_empty/1,tl/1,append#/2,hd#/1,ifappend#/3,is_empty#/1,tl#/1} / {cons/2,false/0
,nil/0,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/0,c_7/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,hd#,ifappend#,is_empty#
,tl#} and constructors {cons,false,nil,true}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:append#(l1,l2) -> c_1(ifappend#(l1,l2,l1))
-->_1 ifappend#(l1,l2,cons(x,l)) -> c_3(append#(l,l2)):2
-->_1 ifappend#(l1,l2,nil()) -> c_4():4

2:S:ifappend#(l1,l2,cons(x,l)) -> c_3(append#(l,l2))
-->_1 append#(l1,l2) -> c_1(ifappend#(l1,l2,l1)):1

3:W:hd#(cons(x,l)) -> c_2()

4:W:ifappend#(l1,l2,nil()) -> c_4()

5:W:is_empty#(cons(x,l)) -> c_5()

6:W:is_empty#(nil()) -> c_6()

7:W:tl#(cons(x,l)) -> c_7()

The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
7: tl#(cons(x,l)) -> c_7()
6: is_empty#(nil()) -> c_6()
5: is_empty#(cons(x,l)) -> c_5()
3: hd#(cons(x,l)) -> c_2()
4: ifappend#(l1,l2,nil()) -> c_4()
* Step 5: PredecessorEstimationCP WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
append#(l1,l2) -> c_1(ifappend#(l1,l2,l1))
ifappend#(l1,l2,cons(x,l)) -> c_3(append#(l,l2))
- Signature:
{append/2,hd/1,ifappend/3,is_empty/1,tl/1,append#/2,hd#/1,ifappend#/3,is_empty#/1,tl#/1} / {cons/2,false/0
,nil/0,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/0,c_7/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,hd#,ifappend#,is_empty#
,tl#} and constructors {cons,false,nil,true}
+ Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}}
+ Details:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
2: ifappend#(l1,l2,cons(x,l)) -> c_3(append#(l,l2))

Consider the set of all dependency pairs
1: append#(l1,l2) -> c_1(ifappend#(l1,l2,l1))
2: ifappend#(l1,l2,cons(x,l)) -> c_3(append#(l,l2))
Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1))
SPACE(?,?)on application of the dependency pairs
{2}
These cover all (indirect) predecessors of dependency pairs
{1,2}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
** Step 5.a:1: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
append#(l1,l2) -> c_1(ifappend#(l1,l2,l1))
ifappend#(l1,l2,cons(x,l)) -> c_3(append#(l,l2))
- Signature:
{append/2,hd/1,ifappend/3,is_empty/1,tl/1,append#/2,hd#/1,ifappend#/3,is_empty#/1,tl#/1} / {cons/2,false/0
,nil/0,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/0,c_7/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,hd#,ifappend#,is_empty#
,tl#} and constructors {cons,false,nil,true}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_1) = {1},
uargs(c_3) = {1}

Following symbols are considered usable:
{append#,hd#,ifappend#,is_empty#,tl#}
TcT has computed the following interpretation:
p(append) = [1]
p(cons) = [1] x2 + [2]
p(false) = [1]
p(hd) = [0]
p(ifappend) = [1] x1 + [2] x2 + [4] x3 + [8]
p(is_empty) = [1]
p(nil) = [2]
p(tl) = [0]
p(true) = [2]
p(append#) = [15] x1 + [4] x2 + [0]
p(hd#) = [1]
p(ifappend#) = [4] x2 + [15] x3 + [0]
p(is_empty#) = [1]
p(tl#) = [1] x1 + [2]
p(c_1) = [1] x1 + [0]
p(c_2) = [2]
p(c_3) = [1] x1 + [12]
p(c_4) = [0]
p(c_5) = [1]
p(c_6) = [1]
p(c_7) = [1]

Following rules are strictly oriented:
ifappend#(l1,l2,cons(x,l)) = [15] l + [4] l2 + [30]
> [15] l + [4] l2 + [12]
= c_3(append#(l,l2))

Following rules are (at-least) weakly oriented:
append#(l1,l2) =  [15] l1 + [4] l2 + [0]
>= [15] l1 + [4] l2 + [0]
=  c_1(ifappend#(l1,l2,l1))

** Step 5.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
append#(l1,l2) -> c_1(ifappend#(l1,l2,l1))
- Weak DPs:
ifappend#(l1,l2,cons(x,l)) -> c_3(append#(l,l2))
- Signature:
{append/2,hd/1,ifappend/3,is_empty/1,tl/1,append#/2,hd#/1,ifappend#/3,is_empty#/1,tl#/1} / {cons/2,false/0
,nil/0,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/0,c_7/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,hd#,ifappend#,is_empty#
,tl#} and constructors {cons,false,nil,true}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()

** Step 5.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
append#(l1,l2) -> c_1(ifappend#(l1,l2,l1))
ifappend#(l1,l2,cons(x,l)) -> c_3(append#(l,l2))
- Signature:
{append/2,hd/1,ifappend/3,is_empty/1,tl/1,append#/2,hd#/1,ifappend#/3,is_empty#/1,tl#/1} / {cons/2,false/0
,nil/0,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/0,c_7/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,hd#,ifappend#,is_empty#
,tl#} and constructors {cons,false,nil,true}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:W:append#(l1,l2) -> c_1(ifappend#(l1,l2,l1))
-->_1 ifappend#(l1,l2,cons(x,l)) -> c_3(append#(l,l2)):2

2:W:ifappend#(l1,l2,cons(x,l)) -> c_3(append#(l,l2))
-->_1 append#(l1,l2) -> c_1(ifappend#(l1,l2,l1)):1

The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: append#(l1,l2) -> c_1(ifappend#(l1,l2,l1))
2: ifappend#(l1,l2,cons(x,l)) -> c_3(append#(l,l2))
** Step 5.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:

- Signature:
{append/2,hd/1,ifappend/3,is_empty/1,tl/1,append#/2,hd#/1,ifappend#/3,is_empty#/1,tl#/1} / {cons/2,false/0
,nil/0,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/0,c_7/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append#,hd#,ifappend#,is_empty#
,tl#} and constructors {cons,false,nil,true}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^1))
```