WORST_CASE(?,O(n^1))
* Step 1: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
add#2(x2,Nil()) -> x2
add#2(Cons(x6,x4),Cons(Zero(),x2)) -> Cons(x6,add#2(x4,x2))
add#2(Cons(One(),x4),Cons(One(),x2)) -> Cons(Zero(),inc#1(add#2(x4,x2)))
add#2(Cons(Zero(),x4),Cons(One(),x2)) -> Cons(One(),add#2(x4,x2))
add#2(Nil(),Cons(x4,x2)) -> Cons(x4,x2)
inc#1(Cons(One(),x8)) -> Cons(Zero(),inc#1(x8))
inc#1(Cons(Zero(),x8)) -> Cons(One(),x8)
inc#1(Nil()) -> Cons(One(),Nil())
main(x2,x1) -> add#2(x2,x1)
- Signature:
{add#2/2,inc#1/1,main/2} / {Cons/2,Nil/0,One/0,Zero/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {add#2,inc#1,main} and constructors {Cons,Nil,One,Zero}
+ 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(Cons) = {2},
uargs(inc#1) = {1}
Following symbols are considered usable:
{add#2,inc#1,main}
TcT has computed the following interpretation:
p(Cons) = x2
p(Nil) = 0
p(One) = 0
p(Zero) = 0
p(add#2) = 4 + 4*x1 + x2
p(inc#1) = x1
p(main) = 4 + 4*x1 + x2
Following rules are strictly oriented:
add#2(x2,Nil()) = 4 + 4*x2
> x2
= x2
add#2(Nil(),Cons(x4,x2)) = 4 + x2
> x2
= Cons(x4,x2)
Following rules are (at-least) weakly oriented:
add#2(Cons(x6,x4),Cons(Zero(),x2)) = 4 + x2 + 4*x4
>= 4 + x2 + 4*x4
= Cons(x6,add#2(x4,x2))
add#2(Cons(One(),x4),Cons(One(),x2)) = 4 + x2 + 4*x4
>= 4 + x2 + 4*x4
= Cons(Zero(),inc#1(add#2(x4,x2)))
add#2(Cons(Zero(),x4),Cons(One(),x2)) = 4 + x2 + 4*x4
>= 4 + x2 + 4*x4
= Cons(One(),add#2(x4,x2))
inc#1(Cons(One(),x8)) = x8
>= x8
= Cons(Zero(),inc#1(x8))
inc#1(Cons(Zero(),x8)) = x8
>= x8
= Cons(One(),x8)
inc#1(Nil()) = 0
>= 0
= Cons(One(),Nil())
main(x2,x1) = 4 + x1 + 4*x2
>= 4 + x1 + 4*x2
= add#2(x2,x1)
* Step 2: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
add#2(Cons(x6,x4),Cons(Zero(),x2)) -> Cons(x6,add#2(x4,x2))
add#2(Cons(One(),x4),Cons(One(),x2)) -> Cons(Zero(),inc#1(add#2(x4,x2)))
add#2(Cons(Zero(),x4),Cons(One(),x2)) -> Cons(One(),add#2(x4,x2))
inc#1(Cons(One(),x8)) -> Cons(Zero(),inc#1(x8))
inc#1(Cons(Zero(),x8)) -> Cons(One(),x8)
inc#1(Nil()) -> Cons(One(),Nil())
main(x2,x1) -> add#2(x2,x1)
- Weak TRS:
add#2(x2,Nil()) -> x2
add#2(Nil(),Cons(x4,x2)) -> Cons(x4,x2)
- Signature:
{add#2/2,inc#1/1,main/2} / {Cons/2,Nil/0,One/0,Zero/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {add#2,inc#1,main} and constructors {Cons,Nil,One,Zero}
+ 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(Cons) = {2},
uargs(inc#1) = {1}
Following symbols are considered usable:
{add#2,inc#1,main}
TcT has computed the following interpretation:
p(Cons) = [1] x2 + [4]
p(Nil) = [0]
p(One) = [1]
p(Zero) = [0]
p(add#2) = [3] x1 + [1] x2 + [0]
p(inc#1) = [1] x1 + [4]
p(main) = [3] x1 + [1] x2 + [2]
Following rules are strictly oriented:
add#2(Cons(x6,x4),Cons(Zero(),x2)) = [1] x2 + [3] x4 + [16]
> [1] x2 + [3] x4 + [4]
= Cons(x6,add#2(x4,x2))
add#2(Cons(One(),x4),Cons(One(),x2)) = [1] x2 + [3] x4 + [16]
> [1] x2 + [3] x4 + [8]
= Cons(Zero(),inc#1(add#2(x4,x2)))
add#2(Cons(Zero(),x4),Cons(One(),x2)) = [1] x2 + [3] x4 + [16]
> [1] x2 + [3] x4 + [4]
= Cons(One(),add#2(x4,x2))
inc#1(Cons(Zero(),x8)) = [1] x8 + [8]
> [1] x8 + [4]
= Cons(One(),x8)
main(x2,x1) = [1] x1 + [3] x2 + [2]
> [1] x1 + [3] x2 + [0]
= add#2(x2,x1)
Following rules are (at-least) weakly oriented:
add#2(x2,Nil()) = [3] x2 + [0]
>= [1] x2 + [0]
= x2
add#2(Nil(),Cons(x4,x2)) = [1] x2 + [4]
>= [1] x2 + [4]
= Cons(x4,x2)
inc#1(Cons(One(),x8)) = [1] x8 + [8]
>= [1] x8 + [8]
= Cons(Zero(),inc#1(x8))
inc#1(Nil()) = [4]
>= [4]
= Cons(One(),Nil())
* Step 3: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
inc#1(Cons(One(),x8)) -> Cons(Zero(),inc#1(x8))
inc#1(Nil()) -> Cons(One(),Nil())
- Weak TRS:
add#2(x2,Nil()) -> x2
add#2(Cons(x6,x4),Cons(Zero(),x2)) -> Cons(x6,add#2(x4,x2))
add#2(Cons(One(),x4),Cons(One(),x2)) -> Cons(Zero(),inc#1(add#2(x4,x2)))
add#2(Cons(Zero(),x4),Cons(One(),x2)) -> Cons(One(),add#2(x4,x2))
add#2(Nil(),Cons(x4,x2)) -> Cons(x4,x2)
inc#1(Cons(Zero(),x8)) -> Cons(One(),x8)
main(x2,x1) -> add#2(x2,x1)
- Signature:
{add#2/2,inc#1/1,main/2} / {Cons/2,Nil/0,One/0,Zero/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {add#2,inc#1,main} and constructors {Cons,Nil,One,Zero}
+ 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(Cons) = {2},
uargs(inc#1) = {1}
Following symbols are considered usable:
{add#2,inc#1,main}
TcT has computed the following interpretation:
p(Cons) = x1 + x2
p(Nil) = 2
p(One) = 2
p(Zero) = 1
p(add#2) = 4 + 4*x1 + x2
p(inc#1) = 4 + x1
p(main) = 6 + 4*x1 + x2
Following rules are strictly oriented:
inc#1(Cons(One(),x8)) = 6 + x8
> 5 + x8
= Cons(Zero(),inc#1(x8))
inc#1(Nil()) = 6
> 4
= Cons(One(),Nil())
Following rules are (at-least) weakly oriented:
add#2(x2,Nil()) = 6 + 4*x2
>= x2
= x2
add#2(Cons(x6,x4),Cons(Zero(),x2)) = 5 + x2 + 4*x4 + 4*x6
>= 4 + x2 + 4*x4 + x6
= Cons(x6,add#2(x4,x2))
add#2(Cons(One(),x4),Cons(One(),x2)) = 14 + x2 + 4*x4
>= 9 + x2 + 4*x4
= Cons(Zero(),inc#1(add#2(x4,x2)))
add#2(Cons(Zero(),x4),Cons(One(),x2)) = 10 + x2 + 4*x4
>= 6 + x2 + 4*x4
= Cons(One(),add#2(x4,x2))
add#2(Nil(),Cons(x4,x2)) = 12 + x2 + x4
>= x2 + x4
= Cons(x4,x2)
inc#1(Cons(Zero(),x8)) = 5 + x8
>= 2 + x8
= Cons(One(),x8)
main(x2,x1) = 6 + x1 + 4*x2
>= 4 + x1 + 4*x2
= add#2(x2,x1)
* Step 4: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
add#2(x2,Nil()) -> x2
add#2(Cons(x6,x4),Cons(Zero(),x2)) -> Cons(x6,add#2(x4,x2))
add#2(Cons(One(),x4),Cons(One(),x2)) -> Cons(Zero(),inc#1(add#2(x4,x2)))
add#2(Cons(Zero(),x4),Cons(One(),x2)) -> Cons(One(),add#2(x4,x2))
add#2(Nil(),Cons(x4,x2)) -> Cons(x4,x2)
inc#1(Cons(One(),x8)) -> Cons(Zero(),inc#1(x8))
inc#1(Cons(Zero(),x8)) -> Cons(One(),x8)
inc#1(Nil()) -> Cons(One(),Nil())
main(x2,x1) -> add#2(x2,x1)
- Signature:
{add#2/2,inc#1/1,main/2} / {Cons/2,Nil/0,One/0,Zero/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {add#2,inc#1,main} and constructors {Cons,Nil,One,Zero}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^1))