WORST_CASE(?,O(n^1))
* Step 1: WeightGap 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:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
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:
all
TcT has computed the following interpretation:
p(Cons) = [1] x1 + [1] x2 + [1]
p(Nil) = [6]
p(One) = [0]
p(Zero) = [4]
p(add#2) = [1] x1 + [4] x2 + [0]
p(inc#1) = [1] x1 + [0]
p(main) = [1] x1 + [4] x2 + [2]
Following rules are strictly oriented:
add#2(x2,Nil()) = [1] x2 + [24]
> [1] x2 + [0]
= x2
add#2(Cons(x6,x4),Cons(Zero(),x2)) = [4] x2 + [1] x4 + [1] x6 + [21]
> [4] x2 + [1] x4 + [1] x6 + [1]
= Cons(x6,add#2(x4,x2))
add#2(Cons(Zero(),x4),Cons(One(),x2)) = [4] x2 + [1] x4 + [9]
> [4] x2 + [1] x4 + [1]
= Cons(One(),add#2(x4,x2))
add#2(Nil(),Cons(x4,x2)) = [4] x2 + [4] x4 + [10]
> [1] x2 + [1] x4 + [1]
= Cons(x4,x2)
inc#1(Cons(Zero(),x8)) = [1] x8 + [5]
> [1] x8 + [1]
= Cons(One(),x8)
main(x2,x1) = [4] x1 + [1] x2 + [2]
> [4] x1 + [1] x2 + [0]
= add#2(x2,x1)
Following rules are (at-least) weakly oriented:
add#2(Cons(One(),x4),Cons(One(),x2)) = [4] x2 + [1] x4 + [5]
>= [4] x2 + [1] x4 + [5]
= Cons(Zero(),inc#1(add#2(x4,x2)))
inc#1(Cons(One(),x8)) = [1] x8 + [1]
>= [1] x8 + [5]
= Cons(Zero(),inc#1(x8))
inc#1(Nil()) = [6]
>= [7]
= Cons(One(),Nil())
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
add#2(Cons(One(),x4),Cons(One(),x2)) -> Cons(Zero(),inc#1(add#2(x4,x2)))
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(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:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
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:
all
TcT has computed the following interpretation:
p(Cons) = [1] x1 + [1] x2 + [0]
p(Nil) = [0]
p(One) = [0]
p(Zero) = [2]
p(add#2) = [2] x1 + [2] x2 + [4]
p(inc#1) = [1] x1 + [1]
p(main) = [2] x1 + [4] x2 + [4]
Following rules are strictly oriented:
inc#1(Nil()) = [1]
> [0]
= Cons(One(),Nil())
Following rules are (at-least) weakly oriented:
add#2(x2,Nil()) = [2] x2 + [4]
>= [1] x2 + [0]
= x2
add#2(Cons(x6,x4),Cons(Zero(),x2)) = [2] x2 + [2] x4 + [2] x6 + [8]
>= [2] x2 + [2] x4 + [1] x6 + [4]
= Cons(x6,add#2(x4,x2))
add#2(Cons(One(),x4),Cons(One(),x2)) = [2] x2 + [2] x4 + [4]
>= [2] x2 + [2] x4 + [7]
= Cons(Zero(),inc#1(add#2(x4,x2)))
add#2(Cons(Zero(),x4),Cons(One(),x2)) = [2] x2 + [2] x4 + [8]
>= [2] x2 + [2] x4 + [4]
= Cons(One(),add#2(x4,x2))
add#2(Nil(),Cons(x4,x2)) = [2] x2 + [2] x4 + [4]
>= [1] x2 + [1] x4 + [0]
= Cons(x4,x2)
inc#1(Cons(One(),x8)) = [1] x8 + [1]
>= [1] x8 + [3]
= Cons(Zero(),inc#1(x8))
inc#1(Cons(Zero(),x8)) = [1] x8 + [3]
>= [1] x8 + [0]
= Cons(One(),x8)
main(x2,x1) = [4] x1 + [2] x2 + [4]
>= [2] x1 + [2] x2 + [4]
= add#2(x2,x1)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
add#2(Cons(One(),x4),Cons(One(),x2)) -> Cons(Zero(),inc#1(add#2(x4,x2)))
inc#1(Cons(One(),x8)) -> Cons(Zero(),inc#1(x8))
- Weak TRS:
add#2(x2,Nil()) -> x2
add#2(Cons(x6,x4),Cons(Zero(),x2)) -> Cons(x6,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)
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:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
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:
all
TcT has computed the following interpretation:
p(Cons) = [1] x2 + [2]
p(Nil) = [0]
p(One) = [0]
p(Zero) = [0]
p(add#2) = [4] x1 + [1] x2 + [0]
p(inc#1) = [1] x1 + [2]
p(main) = [4] x1 + [1] x2 + [0]
Following rules are strictly oriented:
add#2(Cons(One(),x4),Cons(One(),x2)) = [1] x2 + [4] x4 + [10]
> [1] x2 + [4] x4 + [4]
= Cons(Zero(),inc#1(add#2(x4,x2)))
Following rules are (at-least) weakly oriented:
add#2(x2,Nil()) = [4] x2 + [0]
>= [1] x2 + [0]
= x2
add#2(Cons(x6,x4),Cons(Zero(),x2)) = [1] x2 + [4] x4 + [10]
>= [1] x2 + [4] x4 + [2]
= Cons(x6,add#2(x4,x2))
add#2(Cons(Zero(),x4),Cons(One(),x2)) = [1] x2 + [4] x4 + [10]
>= [1] x2 + [4] x4 + [2]
= Cons(One(),add#2(x4,x2))
add#2(Nil(),Cons(x4,x2)) = [1] x2 + [2]
>= [1] x2 + [2]
= Cons(x4,x2)
inc#1(Cons(One(),x8)) = [1] x8 + [4]
>= [1] x8 + [4]
= Cons(Zero(),inc#1(x8))
inc#1(Cons(Zero(),x8)) = [1] x8 + [4]
>= [1] x8 + [2]
= Cons(One(),x8)
inc#1(Nil()) = [2]
>= [2]
= Cons(One(),Nil())
main(x2,x1) = [1] x1 + [4] x2 + [0]
>= [1] x1 + [4] x2 + [0]
= add#2(x2,x1)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
inc#1(Cons(One(),x8)) -> Cons(Zero(),inc#1(x8))
- 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)
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:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
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:
all
TcT has computed the following interpretation:
p(Cons) = [1] x1 + [1] x2 + [0]
p(Nil) = [0]
p(One) = [1]
p(Zero) = [0]
p(add#2) = [6] x1 + [1] x2 + [0]
p(inc#1) = [1] x1 + [4]
p(main) = [7] x1 + [5] x2 + [0]
Following rules are strictly oriented:
inc#1(Cons(One(),x8)) = [1] x8 + [5]
> [1] x8 + [4]
= Cons(Zero(),inc#1(x8))
Following rules are (at-least) weakly oriented:
add#2(x2,Nil()) = [6] x2 + [0]
>= [1] x2 + [0]
= x2
add#2(Cons(x6,x4),Cons(Zero(),x2)) = [1] x2 + [6] x4 + [6] x6 + [0]
>= [1] x2 + [6] x4 + [1] x6 + [0]
= Cons(x6,add#2(x4,x2))
add#2(Cons(One(),x4),Cons(One(),x2)) = [1] x2 + [6] x4 + [7]
>= [1] x2 + [6] x4 + [4]
= Cons(Zero(),inc#1(add#2(x4,x2)))
add#2(Cons(Zero(),x4),Cons(One(),x2)) = [1] x2 + [6] x4 + [1]
>= [1] x2 + [6] x4 + [1]
= Cons(One(),add#2(x4,x2))
add#2(Nil(),Cons(x4,x2)) = [1] x2 + [1] x4 + [0]
>= [1] x2 + [1] x4 + [0]
= Cons(x4,x2)
inc#1(Cons(Zero(),x8)) = [1] x8 + [4]
>= [1] x8 + [1]
= Cons(One(),x8)
inc#1(Nil()) = [4]
>= [1]
= Cons(One(),Nil())
main(x2,x1) = [5] x1 + [7] x2 + [0]
>= [1] x1 + [6] x2 + [0]
= add#2(x2,x1)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: 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))