WORST_CASE(?,O(n^2))
* Step 1: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
app(Nil(),ys) -> ys
goal(xs) -> naiverev(xs)
naiverev(Cons(x,xs)) -> app(naiverev(xs),Cons(x,Nil()))
naiverev(Nil()) -> Nil()
notEmpty(Cons(x,xs)) -> True()
notEmpty(Nil()) -> False()
- Signature:
{app/2,goal/1,naiverev/1,notEmpty/1} / {Cons/2,False/0,Nil/0,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,goal,naiverev,notEmpty} and constructors {Cons,False
,Nil,True}
+ 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(app) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(Cons) = [1] x2 + [0]
p(False) = [0]
p(Nil) = [1]
p(True) = [0]
p(app) = [1] x1 + [2] x2 + [0]
p(goal) = [8]
p(naiverev) = [3]
p(notEmpty) = [1]
Following rules are strictly oriented:
app(Nil(),ys) = [2] ys + [1]
> [1] ys + [0]
= ys
goal(xs) = [8]
> [3]
= naiverev(xs)
naiverev(Nil()) = [3]
> [1]
= Nil()
notEmpty(Cons(x,xs)) = [1]
> [0]
= True()
notEmpty(Nil()) = [1]
> [0]
= False()
Following rules are (at-least) weakly oriented:
app(Cons(x,xs),ys) = [1] xs + [2] ys + [0]
>= [1] xs + [2] ys + [0]
= Cons(x,app(xs,ys))
naiverev(Cons(x,xs)) = [3]
>= [5]
= app(naiverev(xs),Cons(x,Nil()))
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:
app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
naiverev(Cons(x,xs)) -> app(naiverev(xs),Cons(x,Nil()))
- Weak TRS:
app(Nil(),ys) -> ys
goal(xs) -> naiverev(xs)
naiverev(Nil()) -> Nil()
notEmpty(Cons(x,xs)) -> True()
notEmpty(Nil()) -> False()
- Signature:
{app/2,goal/1,naiverev/1,notEmpty/1} / {Cons/2,False/0,Nil/0,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,goal,naiverev,notEmpty} and constructors {Cons,False
,Nil,True}
+ 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(app) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(Cons) = [1] x1 + [1] x2 + [4]
p(False) = [2]
p(Nil) = [0]
p(True) = [12]
p(app) = [1] x1 + [1] x2 + [0]
p(goal) = [4] x1 + [11]
p(naiverev) = [4] x1 + [10]
p(notEmpty) = [12]
Following rules are strictly oriented:
naiverev(Cons(x,xs)) = [4] x + [4] xs + [26]
> [1] x + [4] xs + [14]
= app(naiverev(xs),Cons(x,Nil()))
Following rules are (at-least) weakly oriented:
app(Cons(x,xs),ys) = [1] x + [1] xs + [1] ys + [4]
>= [1] x + [1] xs + [1] ys + [4]
= Cons(x,app(xs,ys))
app(Nil(),ys) = [1] ys + [0]
>= [1] ys + [0]
= ys
goal(xs) = [4] xs + [11]
>= [4] xs + [10]
= naiverev(xs)
naiverev(Nil()) = [10]
>= [0]
= Nil()
notEmpty(Cons(x,xs)) = [12]
>= [12]
= True()
notEmpty(Nil()) = [12]
>= [2]
= False()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: Ara WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
- Weak TRS:
app(Nil(),ys) -> ys
goal(xs) -> naiverev(xs)
naiverev(Cons(x,xs)) -> app(naiverev(xs),Cons(x,Nil()))
naiverev(Nil()) -> Nil()
notEmpty(Cons(x,xs)) -> True()
notEmpty(Nil()) -> False()
- Signature:
{app/2,goal/1,naiverev/1,notEmpty/1} / {Cons/2,False/0,Nil/0,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,goal,naiverev,notEmpty} and constructors {Cons,False
,Nil,True}
+ Applied Processor:
Ara {heuristics_ = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 15, araFindStrictRules = Just 1}
+ Details:
Signatures used:
----------------
Cons :: [A(0, 0) x A(1, 0)] -(1)-> A(1, 0)
Cons :: [A(5, 5) x A(5, 5)] -(5)-> A(0, 5)
Cons :: [A(8, 8) x A(8, 8)] -(8)-> A(0, 8)
Cons :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0)
False :: [] -(0)-> A(14, 14)
Nil :: [] -(0)-> A(1, 0)
Nil :: [] -(0)-> A(0, 5)
Nil :: [] -(0)-> A(0, 8)
Nil :: [] -(0)-> A(7, 13)
Nil :: [] -(0)-> A(7, 7)
True :: [] -(0)-> A(14, 14)
app :: [A(1, 0) x A(0, 0)] -(4)-> A(0, 0)
goal :: [A(14, 11)] -(15)-> A(0, 0)
naiverev :: [A(0, 5)] -(1)-> A(0, 0)
notEmpty :: [A(0, 8)] -(15)-> A(0, 0)
Cost-free Signatures used:
--------------------------
Cons :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
Cons :: [A_cf(0, 0) x A_cf(5, 0)] -(5)-> A_cf(5, 0)
Cons :: [A_cf(0, 0) x A_cf(2, 0)] -(2)-> A_cf(2, 0)
Nil :: [] -(0)-> A_cf(0, 0)
Nil :: [] -(0)-> A_cf(5, 0)
Nil :: [] -(0)-> A_cf(2, 0)
Nil :: [] -(0)-> A_cf(11, 11)
Nil :: [] -(0)-> A_cf(3, 2)
app :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0)
app :: [A_cf(2, 0) x A_cf(2, 0)] -(0)-> A_cf(2, 0)
naiverev :: [A_cf(5, 0)] -(1)-> A_cf(2, 0)
Base Constructor Signatures used:
---------------------------------
Cons_A :: [A(0, 0) x A(1, 0)] -(1)-> A(1, 0)
Cons_A :: [A(1, 1) x A(1, 1)] -(1)-> A(0, 1)
False_A :: [] -(0)-> A(1, 0)
False_A :: [] -(0)-> A(0, 1)
Nil_A :: [] -(0)-> A(1, 0)
Nil_A :: [] -(0)-> A(0, 1)
True_A :: [] -(0)-> A(1, 0)
True_A :: [] -(0)-> A(0, 1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
2. Weak:
* Step 4: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
app(Nil(),ys) -> ys
goal(xs) -> naiverev(xs)
naiverev(Cons(x,xs)) -> app(naiverev(xs),Cons(x,Nil()))
naiverev(Nil()) -> Nil()
notEmpty(Cons(x,xs)) -> True()
notEmpty(Nil()) -> False()
- Signature:
{app/2,goal/1,naiverev/1,notEmpty/1} / {Cons/2,False/0,Nil/0,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,goal,naiverev,notEmpty} 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^2))