WORST_CASE(?,O(n^1))
* Step 1: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
append(l1,l2) -> append#1(l1,l2)
append#1(cons(x,xs),l2) -> cons(x,append(xs,l2))
append#1(nil(),l2) -> l2
appendAll(l) -> appendAll#1(l)
appendAll#1(cons(l1,ls)) -> append(l1,appendAll(ls))
appendAll#1(nil()) -> nil()
appendAll2(l) -> appendAll2#1(l)
appendAll2#1(cons(l1,ls)) -> append(appendAll(l1),appendAll2(ls))
appendAll2#1(nil()) -> nil()
appendAll3(l) -> appendAll3#1(l)
appendAll3#1(cons(l1,ls)) -> append(appendAll2(l1),appendAll3(ls))
appendAll3#1(nil()) -> nil()
- Signature:
{append/2,append#1/2,appendAll/1,appendAll#1/1,appendAll2/1,appendAll2#1/1,appendAll3/1
,appendAll3#1/1} / {cons/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append,append#1,appendAll,appendAll#1,appendAll2
,appendAll2#1,appendAll3,appendAll3#1} and constructors {cons,nil}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(append) = {1,2},
uargs(cons) = {2}
Following symbols are considered usable:
{append,append#1,appendAll,appendAll#1,appendAll2,appendAll2#1,appendAll3,appendAll3#1}
TcT has computed the following interpretation:
p(append) = [1] x1 + [1] x2 + [0]
p(append#1) = [1] x1 + [1] x2 + [0]
p(appendAll) = [2] x1 + [3]
p(appendAll#1) = [2] x1 + [0]
p(appendAll2) = [2] x1 + [1]
p(appendAll2#1) = [2] x1 + [1]
p(appendAll3) = [4] x1 + [1]
p(appendAll3#1) = [4] x1 + [1]
p(cons) = [1] x1 + [1] x2 + [2]
p(nil) = [0]
Following rules are strictly oriented:
appendAll(l) = [2] l + [3]
> [2] l + [0]
= appendAll#1(l)
appendAll#1(cons(l1,ls)) = [2] l1 + [2] ls + [4]
> [1] l1 + [2] ls + [3]
= append(l1,appendAll(ls))
appendAll2#1(cons(l1,ls)) = [2] l1 + [2] ls + [5]
> [2] l1 + [2] ls + [4]
= append(appendAll(l1),appendAll2(ls))
appendAll2#1(nil()) = [1]
> [0]
= nil()
appendAll3#1(cons(l1,ls)) = [4] l1 + [4] ls + [9]
> [2] l1 + [4] ls + [2]
= append(appendAll2(l1),appendAll3(ls))
appendAll3#1(nil()) = [1]
> [0]
= nil()
Following rules are (at-least) weakly oriented:
append(l1,l2) = [1] l1 + [1] l2 + [0]
>= [1] l1 + [1] l2 + [0]
= append#1(l1,l2)
append#1(cons(x,xs),l2) = [1] l2 + [1] x + [1] xs + [2]
>= [1] l2 + [1] x + [1] xs + [2]
= cons(x,append(xs,l2))
append#1(nil(),l2) = [1] l2 + [0]
>= [1] l2 + [0]
= l2
appendAll#1(nil()) = [0]
>= [0]
= nil()
appendAll2(l) = [2] l + [1]
>= [2] l + [1]
= appendAll2#1(l)
appendAll3(l) = [4] l + [1]
>= [4] l + [1]
= appendAll3#1(l)
* Step 2: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
append(l1,l2) -> append#1(l1,l2)
append#1(cons(x,xs),l2) -> cons(x,append(xs,l2))
append#1(nil(),l2) -> l2
appendAll#1(nil()) -> nil()
appendAll2(l) -> appendAll2#1(l)
appendAll3(l) -> appendAll3#1(l)
- Weak TRS:
appendAll(l) -> appendAll#1(l)
appendAll#1(cons(l1,ls)) -> append(l1,appendAll(ls))
appendAll2#1(cons(l1,ls)) -> append(appendAll(l1),appendAll2(ls))
appendAll2#1(nil()) -> nil()
appendAll3#1(cons(l1,ls)) -> append(appendAll2(l1),appendAll3(ls))
appendAll3#1(nil()) -> nil()
- Signature:
{append/2,append#1/2,appendAll/1,appendAll#1/1,appendAll2/1,appendAll2#1/1,appendAll3/1
,appendAll3#1/1} / {cons/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append,append#1,appendAll,appendAll#1,appendAll2
,appendAll2#1,appendAll3,appendAll3#1} and constructors {cons,nil}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(append) = {1,2},
uargs(cons) = {2}
Following symbols are considered usable:
{append,append#1,appendAll,appendAll#1,appendAll2,appendAll2#1,appendAll3,appendAll3#1}
TcT has computed the following interpretation:
p(append) = [1] x1 + [1] x2 + [0]
p(append#1) = [1] x1 + [1] x2 + [0]
p(appendAll) = [1] x1 + [0]
p(appendAll#1) = [1] x1 + [0]
p(appendAll2) = [1] x1 + [8]
p(appendAll2#1) = [1] x1 + [0]
p(appendAll3) = [1] x1 + [4]
p(appendAll3#1) = [1] x1 + [4]
p(cons) = [1] x1 + [1] x2 + [9]
p(nil) = [0]
Following rules are strictly oriented:
appendAll2(l) = [1] l + [8]
> [1] l + [0]
= appendAll2#1(l)
Following rules are (at-least) weakly oriented:
append(l1,l2) = [1] l1 + [1] l2 + [0]
>= [1] l1 + [1] l2 + [0]
= append#1(l1,l2)
append#1(cons(x,xs),l2) = [1] l2 + [1] x + [1] xs + [9]
>= [1] l2 + [1] x + [1] xs + [9]
= cons(x,append(xs,l2))
append#1(nil(),l2) = [1] l2 + [0]
>= [1] l2 + [0]
= l2
appendAll(l) = [1] l + [0]
>= [1] l + [0]
= appendAll#1(l)
appendAll#1(cons(l1,ls)) = [1] l1 + [1] ls + [9]
>= [1] l1 + [1] ls + [0]
= append(l1,appendAll(ls))
appendAll#1(nil()) = [0]
>= [0]
= nil()
appendAll2#1(cons(l1,ls)) = [1] l1 + [1] ls + [9]
>= [1] l1 + [1] ls + [8]
= append(appendAll(l1),appendAll2(ls))
appendAll2#1(nil()) = [0]
>= [0]
= nil()
appendAll3(l) = [1] l + [4]
>= [1] l + [4]
= appendAll3#1(l)
appendAll3#1(cons(l1,ls)) = [1] l1 + [1] ls + [13]
>= [1] l1 + [1] ls + [12]
= append(appendAll2(l1),appendAll3(ls))
appendAll3#1(nil()) = [4]
>= [0]
= nil()
* Step 3: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
append(l1,l2) -> append#1(l1,l2)
append#1(cons(x,xs),l2) -> cons(x,append(xs,l2))
append#1(nil(),l2) -> l2
appendAll#1(nil()) -> nil()
appendAll3(l) -> appendAll3#1(l)
- Weak TRS:
appendAll(l) -> appendAll#1(l)
appendAll#1(cons(l1,ls)) -> append(l1,appendAll(ls))
appendAll2(l) -> appendAll2#1(l)
appendAll2#1(cons(l1,ls)) -> append(appendAll(l1),appendAll2(ls))
appendAll2#1(nil()) -> nil()
appendAll3#1(cons(l1,ls)) -> append(appendAll2(l1),appendAll3(ls))
appendAll3#1(nil()) -> nil()
- Signature:
{append/2,append#1/2,appendAll/1,appendAll#1/1,appendAll2/1,appendAll2#1/1,appendAll3/1
,appendAll3#1/1} / {cons/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append,append#1,appendAll,appendAll#1,appendAll2
,appendAll2#1,appendAll3,appendAll3#1} and constructors {cons,nil}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(append) = {1,2},
uargs(cons) = {2}
Following symbols are considered usable:
{append,append#1,appendAll,appendAll#1,appendAll2,appendAll2#1,appendAll3,appendAll3#1}
TcT has computed the following interpretation:
p(append) = [1] x1 + [1] x2 + [12]
p(append#1) = [1] x1 + [1] x2 + [12]
p(appendAll) = [2] x1 + [0]
p(appendAll#1) = [2] x1 + [0]
p(appendAll2) = [2] x1 + [0]
p(appendAll2#1) = [2] x1 + [0]
p(appendAll3) = [2] x1 + [0]
p(appendAll3#1) = [2] x1 + [0]
p(cons) = [1] x1 + [1] x2 + [6]
p(nil) = [0]
Following rules are strictly oriented:
append#1(nil(),l2) = [1] l2 + [12]
> [1] l2 + [0]
= l2
Following rules are (at-least) weakly oriented:
append(l1,l2) = [1] l1 + [1] l2 + [12]
>= [1] l1 + [1] l2 + [12]
= append#1(l1,l2)
append#1(cons(x,xs),l2) = [1] l2 + [1] x + [1] xs + [18]
>= [1] l2 + [1] x + [1] xs + [18]
= cons(x,append(xs,l2))
appendAll(l) = [2] l + [0]
>= [2] l + [0]
= appendAll#1(l)
appendAll#1(cons(l1,ls)) = [2] l1 + [2] ls + [12]
>= [1] l1 + [2] ls + [12]
= append(l1,appendAll(ls))
appendAll#1(nil()) = [0]
>= [0]
= nil()
appendAll2(l) = [2] l + [0]
>= [2] l + [0]
= appendAll2#1(l)
appendAll2#1(cons(l1,ls)) = [2] l1 + [2] ls + [12]
>= [2] l1 + [2] ls + [12]
= append(appendAll(l1),appendAll2(ls))
appendAll2#1(nil()) = [0]
>= [0]
= nil()
appendAll3(l) = [2] l + [0]
>= [2] l + [0]
= appendAll3#1(l)
appendAll3#1(cons(l1,ls)) = [2] l1 + [2] ls + [12]
>= [2] l1 + [2] ls + [12]
= append(appendAll2(l1),appendAll3(ls))
appendAll3#1(nil()) = [0]
>= [0]
= nil()
* Step 4: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
append(l1,l2) -> append#1(l1,l2)
append#1(cons(x,xs),l2) -> cons(x,append(xs,l2))
appendAll#1(nil()) -> nil()
appendAll3(l) -> appendAll3#1(l)
- Weak TRS:
append#1(nil(),l2) -> l2
appendAll(l) -> appendAll#1(l)
appendAll#1(cons(l1,ls)) -> append(l1,appendAll(ls))
appendAll2(l) -> appendAll2#1(l)
appendAll2#1(cons(l1,ls)) -> append(appendAll(l1),appendAll2(ls))
appendAll2#1(nil()) -> nil()
appendAll3#1(cons(l1,ls)) -> append(appendAll2(l1),appendAll3(ls))
appendAll3#1(nil()) -> nil()
- Signature:
{append/2,append#1/2,appendAll/1,appendAll#1/1,appendAll2/1,appendAll2#1/1,appendAll3/1
,appendAll3#1/1} / {cons/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append,append#1,appendAll,appendAll#1,appendAll2
,appendAll2#1,appendAll3,appendAll3#1} and constructors {cons,nil}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(append) = {1,2},
uargs(cons) = {2}
Following symbols are considered usable:
{append,append#1,appendAll,appendAll#1,appendAll2,appendAll2#1,appendAll3,appendAll3#1}
TcT has computed the following interpretation:
p(append) = [2] x1 + [1] x2 + [0]
p(append#1) = [2] x1 + [1] x2 + [0]
p(appendAll) = [2] x1 + [0]
p(appendAll#1) = [2] x1 + [0]
p(appendAll2) = [4] x1 + [0]
p(appendAll2#1) = [4] x1 + [0]
p(appendAll3) = [8] x1 + [9]
p(appendAll3#1) = [8] x1 + [9]
p(cons) = [1] x1 + [1] x2 + [0]
p(nil) = [1]
Following rules are strictly oriented:
appendAll#1(nil()) = [2]
> [1]
= nil()
Following rules are (at-least) weakly oriented:
append(l1,l2) = [2] l1 + [1] l2 + [0]
>= [2] l1 + [1] l2 + [0]
= append#1(l1,l2)
append#1(cons(x,xs),l2) = [1] l2 + [2] x + [2] xs + [0]
>= [1] l2 + [1] x + [2] xs + [0]
= cons(x,append(xs,l2))
append#1(nil(),l2) = [1] l2 + [2]
>= [1] l2 + [0]
= l2
appendAll(l) = [2] l + [0]
>= [2] l + [0]
= appendAll#1(l)
appendAll#1(cons(l1,ls)) = [2] l1 + [2] ls + [0]
>= [2] l1 + [2] ls + [0]
= append(l1,appendAll(ls))
appendAll2(l) = [4] l + [0]
>= [4] l + [0]
= appendAll2#1(l)
appendAll2#1(cons(l1,ls)) = [4] l1 + [4] ls + [0]
>= [4] l1 + [4] ls + [0]
= append(appendAll(l1),appendAll2(ls))
appendAll2#1(nil()) = [4]
>= [1]
= nil()
appendAll3(l) = [8] l + [9]
>= [8] l + [9]
= appendAll3#1(l)
appendAll3#1(cons(l1,ls)) = [8] l1 + [8] ls + [9]
>= [8] l1 + [8] ls + [9]
= append(appendAll2(l1),appendAll3(ls))
appendAll3#1(nil()) = [17]
>= [1]
= nil()
* Step 5: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
append(l1,l2) -> append#1(l1,l2)
append#1(cons(x,xs),l2) -> cons(x,append(xs,l2))
appendAll3(l) -> appendAll3#1(l)
- Weak TRS:
append#1(nil(),l2) -> l2
appendAll(l) -> appendAll#1(l)
appendAll#1(cons(l1,ls)) -> append(l1,appendAll(ls))
appendAll#1(nil()) -> nil()
appendAll2(l) -> appendAll2#1(l)
appendAll2#1(cons(l1,ls)) -> append(appendAll(l1),appendAll2(ls))
appendAll2#1(nil()) -> nil()
appendAll3#1(cons(l1,ls)) -> append(appendAll2(l1),appendAll3(ls))
appendAll3#1(nil()) -> nil()
- Signature:
{append/2,append#1/2,appendAll/1,appendAll#1/1,appendAll2/1,appendAll2#1/1,appendAll3/1
,appendAll3#1/1} / {cons/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append,append#1,appendAll,appendAll#1,appendAll2
,appendAll2#1,appendAll3,appendAll3#1} and constructors {cons,nil}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(append) = {1,2},
uargs(cons) = {2}
Following symbols are considered usable:
{append,append#1,appendAll,appendAll#1,appendAll2,appendAll2#1,appendAll3,appendAll3#1}
TcT has computed the following interpretation:
p(append) = [1] x1 + [1] x2 + [1]
p(append#1) = [1] x1 + [1] x2 + [1]
p(appendAll) = [1] x1 + [0]
p(appendAll#1) = [1] x1 + [0]
p(appendAll2) = [2] x1 + [9]
p(appendAll2#1) = [2] x1 + [6]
p(appendAll3) = [8] x1 + [6]
p(appendAll3#1) = [8] x1 + [0]
p(cons) = [1] x1 + [1] x2 + [2]
p(nil) = [1]
Following rules are strictly oriented:
appendAll3(l) = [8] l + [6]
> [8] l + [0]
= appendAll3#1(l)
Following rules are (at-least) weakly oriented:
append(l1,l2) = [1] l1 + [1] l2 + [1]
>= [1] l1 + [1] l2 + [1]
= append#1(l1,l2)
append#1(cons(x,xs),l2) = [1] l2 + [1] x + [1] xs + [3]
>= [1] l2 + [1] x + [1] xs + [3]
= cons(x,append(xs,l2))
append#1(nil(),l2) = [1] l2 + [2]
>= [1] l2 + [0]
= l2
appendAll(l) = [1] l + [0]
>= [1] l + [0]
= appendAll#1(l)
appendAll#1(cons(l1,ls)) = [1] l1 + [1] ls + [2]
>= [1] l1 + [1] ls + [1]
= append(l1,appendAll(ls))
appendAll#1(nil()) = [1]
>= [1]
= nil()
appendAll2(l) = [2] l + [9]
>= [2] l + [6]
= appendAll2#1(l)
appendAll2#1(cons(l1,ls)) = [2] l1 + [2] ls + [10]
>= [1] l1 + [2] ls + [10]
= append(appendAll(l1),appendAll2(ls))
appendAll2#1(nil()) = [8]
>= [1]
= nil()
appendAll3#1(cons(l1,ls)) = [8] l1 + [8] ls + [16]
>= [2] l1 + [8] ls + [16]
= append(appendAll2(l1),appendAll3(ls))
appendAll3#1(nil()) = [8]
>= [1]
= nil()
* Step 6: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
append(l1,l2) -> append#1(l1,l2)
append#1(cons(x,xs),l2) -> cons(x,append(xs,l2))
- Weak TRS:
append#1(nil(),l2) -> l2
appendAll(l) -> appendAll#1(l)
appendAll#1(cons(l1,ls)) -> append(l1,appendAll(ls))
appendAll#1(nil()) -> nil()
appendAll2(l) -> appendAll2#1(l)
appendAll2#1(cons(l1,ls)) -> append(appendAll(l1),appendAll2(ls))
appendAll2#1(nil()) -> nil()
appendAll3(l) -> appendAll3#1(l)
appendAll3#1(cons(l1,ls)) -> append(appendAll2(l1),appendAll3(ls))
appendAll3#1(nil()) -> nil()
- Signature:
{append/2,append#1/2,appendAll/1,appendAll#1/1,appendAll2/1,appendAll2#1/1,appendAll3/1
,appendAll3#1/1} / {cons/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append,append#1,appendAll,appendAll#1,appendAll2
,appendAll2#1,appendAll3,appendAll3#1} and constructors {cons,nil}
+ Applied Processor:
NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(linear):
The following argument positions are considered usable:
uargs(append) = {1,2},
uargs(cons) = {2}
Following symbols are considered usable:
{append,append#1,appendAll,appendAll#1,appendAll2,appendAll2#1,appendAll3,appendAll3#1}
TcT has computed the following interpretation:
p(append) = 2*x1 + x2
p(append#1) = 2*x1 + x2
p(appendAll) = 3*x1
p(appendAll#1) = 3*x1
p(appendAll2) = 1 + 7*x1
p(appendAll2#1) = 1 + 7*x1
p(appendAll3) = 5 + 14*x1
p(appendAll3#1) = 4 + 14*x1
p(cons) = 1 + x1 + x2
p(nil) = 0
Following rules are strictly oriented:
append#1(cons(x,xs),l2) = 2 + l2 + 2*x + 2*xs
> 1 + l2 + x + 2*xs
= cons(x,append(xs,l2))
Following rules are (at-least) weakly oriented:
append(l1,l2) = 2*l1 + l2
>= 2*l1 + l2
= append#1(l1,l2)
append#1(nil(),l2) = l2
>= l2
= l2
appendAll(l) = 3*l
>= 3*l
= appendAll#1(l)
appendAll#1(cons(l1,ls)) = 3 + 3*l1 + 3*ls
>= 2*l1 + 3*ls
= append(l1,appendAll(ls))
appendAll#1(nil()) = 0
>= 0
= nil()
appendAll2(l) = 1 + 7*l
>= 1 + 7*l
= appendAll2#1(l)
appendAll2#1(cons(l1,ls)) = 8 + 7*l1 + 7*ls
>= 1 + 6*l1 + 7*ls
= append(appendAll(l1),appendAll2(ls))
appendAll2#1(nil()) = 1
>= 0
= nil()
appendAll3(l) = 5 + 14*l
>= 4 + 14*l
= appendAll3#1(l)
appendAll3#1(cons(l1,ls)) = 18 + 14*l1 + 14*ls
>= 7 + 14*l1 + 14*ls
= append(appendAll2(l1),appendAll3(ls))
appendAll3#1(nil()) = 4
>= 0
= nil()
* Step 7: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
append(l1,l2) -> append#1(l1,l2)
- Weak TRS:
append#1(cons(x,xs),l2) -> cons(x,append(xs,l2))
append#1(nil(),l2) -> l2
appendAll(l) -> appendAll#1(l)
appendAll#1(cons(l1,ls)) -> append(l1,appendAll(ls))
appendAll#1(nil()) -> nil()
appendAll2(l) -> appendAll2#1(l)
appendAll2#1(cons(l1,ls)) -> append(appendAll(l1),appendAll2(ls))
appendAll2#1(nil()) -> nil()
appendAll3(l) -> appendAll3#1(l)
appendAll3#1(cons(l1,ls)) -> append(appendAll2(l1),appendAll3(ls))
appendAll3#1(nil()) -> nil()
- Signature:
{append/2,append#1/2,appendAll/1,appendAll#1/1,appendAll2/1,appendAll2#1/1,appendAll3/1
,appendAll3#1/1} / {cons/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append,append#1,appendAll,appendAll#1,appendAll2
,appendAll2#1,appendAll3,appendAll3#1} and constructors {cons,nil}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(append) = {1,2},
uargs(cons) = {2}
Following symbols are considered usable:
{append,append#1,appendAll,appendAll#1,appendAll2,appendAll2#1,appendAll3,appendAll3#1}
TcT has computed the following interpretation:
p(append) = [2] x1 + [1] x2 + [4]
p(append#1) = [2] x1 + [1] x2 + [3]
p(appendAll) = [2] x1 + [2]
p(appendAll#1) = [2] x1 + [2]
p(appendAll2) = [4] x1 + [0]
p(appendAll2#1) = [4] x1 + [0]
p(appendAll3) = [11] x1 + [2]
p(appendAll3#1) = [11] x1 + [1]
p(cons) = [1] x1 + [1] x2 + [2]
p(nil) = [0]
Following rules are strictly oriented:
append(l1,l2) = [2] l1 + [1] l2 + [4]
> [2] l1 + [1] l2 + [3]
= append#1(l1,l2)
Following rules are (at-least) weakly oriented:
append#1(cons(x,xs),l2) = [1] l2 + [2] x + [2] xs + [7]
>= [1] l2 + [1] x + [2] xs + [6]
= cons(x,append(xs,l2))
append#1(nil(),l2) = [1] l2 + [3]
>= [1] l2 + [0]
= l2
appendAll(l) = [2] l + [2]
>= [2] l + [2]
= appendAll#1(l)
appendAll#1(cons(l1,ls)) = [2] l1 + [2] ls + [6]
>= [2] l1 + [2] ls + [6]
= append(l1,appendAll(ls))
appendAll#1(nil()) = [2]
>= [0]
= nil()
appendAll2(l) = [4] l + [0]
>= [4] l + [0]
= appendAll2#1(l)
appendAll2#1(cons(l1,ls)) = [4] l1 + [4] ls + [8]
>= [4] l1 + [4] ls + [8]
= append(appendAll(l1),appendAll2(ls))
appendAll2#1(nil()) = [0]
>= [0]
= nil()
appendAll3(l) = [11] l + [2]
>= [11] l + [1]
= appendAll3#1(l)
appendAll3#1(cons(l1,ls)) = [11] l1 + [11] ls + [23]
>= [8] l1 + [11] ls + [6]
= append(appendAll2(l1),appendAll3(ls))
appendAll3#1(nil()) = [1]
>= [0]
= nil()
* Step 8: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
append(l1,l2) -> append#1(l1,l2)
append#1(cons(x,xs),l2) -> cons(x,append(xs,l2))
append#1(nil(),l2) -> l2
appendAll(l) -> appendAll#1(l)
appendAll#1(cons(l1,ls)) -> append(l1,appendAll(ls))
appendAll#1(nil()) -> nil()
appendAll2(l) -> appendAll2#1(l)
appendAll2#1(cons(l1,ls)) -> append(appendAll(l1),appendAll2(ls))
appendAll2#1(nil()) -> nil()
appendAll3(l) -> appendAll3#1(l)
appendAll3#1(cons(l1,ls)) -> append(appendAll2(l1),appendAll3(ls))
appendAll3#1(nil()) -> nil()
- Signature:
{append/2,append#1/2,appendAll/1,appendAll#1/1,appendAll2/1,appendAll2#1/1,appendAll3/1
,appendAll3#1/1} / {cons/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {append,append#1,appendAll,appendAll#1,appendAll2
,appendAll2#1,appendAll3,appendAll3#1} and constructors {cons,nil}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^1))