WORST_CASE(?,O(n^2))
* Step 1: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
+(x,0()) -> x
+(x,s(y)) -> s(+(x,y))
double(0()) -> 0()
double(s(x)) -> s(s(double(x)))
sqr(0()) -> 0()
sqr(s(x)) -> +(sqr(x),s(double(x)))
sqr(s(x)) -> s(+(sqr(x),double(x)))
- Signature:
{+/2,double/1,sqr/1} / {0/0,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {+,double,sqr} and constructors {0,s}
+ 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(+) = {1,2},
uargs(s) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(+) = [1] x1 + [1] x2 + [5]
p(0) = [0]
p(double) = [2]
p(s) = [1] x1 + [8]
p(sqr) = [1] x1 + [0]
Following rules are strictly oriented:
+(x,0()) = [1] x + [5]
> [1] x + [0]
= x
double(0()) = [2]
> [0]
= 0()
Following rules are (at-least) weakly oriented:
+(x,s(y)) = [1] x + [1] y + [13]
>= [1] x + [1] y + [13]
= s(+(x,y))
double(s(x)) = [2]
>= [18]
= s(s(double(x)))
sqr(0()) = [0]
>= [0]
= 0()
sqr(s(x)) = [1] x + [8]
>= [1] x + [15]
= +(sqr(x),s(double(x)))
sqr(s(x)) = [1] x + [8]
>= [1] x + [15]
= s(+(sqr(x),double(x)))
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
+(x,s(y)) -> s(+(x,y))
double(s(x)) -> s(s(double(x)))
sqr(0()) -> 0()
sqr(s(x)) -> +(sqr(x),s(double(x)))
sqr(s(x)) -> s(+(sqr(x),double(x)))
- Weak TRS:
+(x,0()) -> x
double(0()) -> 0()
- Signature:
{+/2,double/1,sqr/1} / {0/0,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {+,double,sqr} and constructors {0,s}
+ 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(+) = {1,2},
uargs(s) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(+) = [1] x1 + [1] x2 + [0]
p(0) = [0]
p(double) = [14]
p(s) = [1] x1 + [1]
p(sqr) = [1]
Following rules are strictly oriented:
sqr(0()) = [1]
> [0]
= 0()
Following rules are (at-least) weakly oriented:
+(x,0()) = [1] x + [0]
>= [1] x + [0]
= x
+(x,s(y)) = [1] x + [1] y + [1]
>= [1] x + [1] y + [1]
= s(+(x,y))
double(0()) = [14]
>= [0]
= 0()
double(s(x)) = [14]
>= [16]
= s(s(double(x)))
sqr(s(x)) = [1]
>= [16]
= +(sqr(x),s(double(x)))
sqr(s(x)) = [1]
>= [16]
= s(+(sqr(x),double(x)))
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
+(x,s(y)) -> s(+(x,y))
double(s(x)) -> s(s(double(x)))
sqr(s(x)) -> +(sqr(x),s(double(x)))
sqr(s(x)) -> s(+(sqr(x),double(x)))
- Weak TRS:
+(x,0()) -> x
double(0()) -> 0()
sqr(0()) -> 0()
- Signature:
{+/2,double/1,sqr/1} / {0/0,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {+,double,sqr} and constructors {0,s}
+ 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(+) = {1,2},
uargs(s) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(+) = [1] x1 + [1] x2 + [0]
p(0) = [0]
p(double) = [12]
p(s) = [1] x1 + [2]
p(sqr) = [8] x1 + [13]
Following rules are strictly oriented:
sqr(s(x)) = [8] x + [29]
> [8] x + [27]
= +(sqr(x),s(double(x)))
sqr(s(x)) = [8] x + [29]
> [8] x + [27]
= s(+(sqr(x),double(x)))
Following rules are (at-least) weakly oriented:
+(x,0()) = [1] x + [0]
>= [1] x + [0]
= x
+(x,s(y)) = [1] x + [1] y + [2]
>= [1] x + [1] y + [2]
= s(+(x,y))
double(0()) = [12]
>= [0]
= 0()
double(s(x)) = [12]
>= [16]
= s(s(double(x)))
sqr(0()) = [13]
>= [0]
= 0()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: Ara WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
+(x,s(y)) -> s(+(x,y))
double(s(x)) -> s(s(double(x)))
- Weak TRS:
+(x,0()) -> x
double(0()) -> 0()
sqr(0()) -> 0()
sqr(s(x)) -> +(sqr(x),s(double(x)))
sqr(s(x)) -> s(+(sqr(x),double(x)))
- Signature:
{+/2,double/1,sqr/1} / {0/0,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {+,double,sqr} and constructors {0,s}
+ Applied Processor:
Ara {heuristics_ = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 15, araFindStrictRules = Just 1}
+ Details:
Signatures used:
----------------
+ :: [A(0, 0) x A(2, 0)] -(0)-> A(0, 0)
0 :: [] -(0)-> A(2, 0)
0 :: [] -(0)-> A(14, 0)
0 :: [] -(0)-> A(0, 15)
0 :: [] -(0)-> A(4, 7)
0 :: [] -(0)-> A(6, 7)
double :: [A(14, 0)] -(9)-> A(2, 0)
s :: [A(2, 0)] -(2)-> A(2, 0)
s :: [A(14, 0)] -(14)-> A(14, 0)
s :: [A(15, 15)] -(15)-> A(0, 15)
s :: [A(0, 0)] -(0)-> A(0, 0)
sqr :: [A(0, 15)] -(1)-> A(0, 0)
Cost-free Signatures used:
--------------------------
+ :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
0 :: [] -(0)-> A_cf(0, 0)
double :: [A_cf(0, 0)] -(0)-> A_cf(0, 0)
s :: [A_cf(0, 0)] -(0)-> A_cf(0, 0)
sqr :: [A_cf(0, 0)] -(0)-> A_cf(0, 0)
Base Constructor Signatures used:
---------------------------------
0_A :: [] -(0)-> A(1, 0)
0_A :: [] -(0)-> A(0, 1)
s_A :: [A(1, 0)] -(1)-> A(1, 0)
s_A :: [A(1, 1)] -(1)-> A(0, 1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
+(x,s(y)) -> s(+(x,y))
2. Weak:
double(s(x)) -> s(s(double(x)))
* Step 5: Ara WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
double(s(x)) -> s(s(double(x)))
- Weak TRS:
+(x,0()) -> x
+(x,s(y)) -> s(+(x,y))
double(0()) -> 0()
sqr(0()) -> 0()
sqr(s(x)) -> +(sqr(x),s(double(x)))
sqr(s(x)) -> s(+(sqr(x),double(x)))
- Signature:
{+/2,double/1,sqr/1} / {0/0,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {+,double,sqr} and constructors {0,s}
+ Applied Processor:
Ara {heuristics_ = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 15, araFindStrictRules = Just 1}
+ Details:
Signatures used:
----------------
+ :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0)
0 :: [] -(0)-> A(0, 0)
0 :: [] -(0)-> A(10, 0)
0 :: [] -(0)-> A(1, 14)
0 :: [] -(0)-> A(7, 6)
double :: [A(10, 0)] -(0)-> A(0, 0)
s :: [A(10, 0)] -(10)-> A(10, 0)
s :: [A(0, 0)] -(0)-> A(0, 0)
s :: [A(15, 14)] -(1)-> A(1, 14)
sqr :: [A(1, 14)] -(8)-> A(0, 0)
Cost-free Signatures used:
--------------------------
+ :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
0 :: [] -(0)-> A_cf(0, 0)
0 :: [] -(0)-> A_cf(4, 0)
0 :: [] -(0)-> A_cf(2, 2)
double :: [A_cf(0, 0)] -(0)-> A_cf(0, 0)
double :: [A_cf(0, 0)] -(4)-> A_cf(0, 0)
s :: [A_cf(0, 0)] -(0)-> A_cf(0, 0)
s :: [A_cf(4, 0)] -(4)-> A_cf(4, 0)
sqr :: [A_cf(4, 0)] -(1)-> A_cf(0, 0)
sqr :: [A_cf(0, 0)] -(0)-> A_cf(0, 0)
Base Constructor Signatures used:
---------------------------------
0_A :: [] -(0)-> A(1, 0)
0_A :: [] -(0)-> A(0, 1)
s_A :: [A(1, 0)] -(1)-> A(1, 0)
s_A :: [A(1, 1)] -(0)-> A(0, 1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
double(s(x)) -> s(s(double(x)))
2. Weak:
* Step 6: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
+(x,0()) -> x
+(x,s(y)) -> s(+(x,y))
double(0()) -> 0()
double(s(x)) -> s(s(double(x)))
sqr(0()) -> 0()
sqr(s(x)) -> +(sqr(x),s(double(x)))
sqr(s(x)) -> s(+(sqr(x),double(x)))
- Signature:
{+/2,double/1,sqr/1} / {0/0,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {+,double,sqr} and constructors {0,s}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^2))