* Step 1: Sum WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
goal(xs,ys) -> merge(xs,ys)
merge(Cons(x,xs),Nil()) -> Cons(x,xs)
merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
merge(Nil(),ys) -> ys
- Weak TRS:
<=(0(),y) -> True()
<=(S(x),0()) -> False()
<=(S(x),S(y)) -> <=(x,y)
merge[Ite](False(),xs',Cons(x,xs)) -> Cons(x,merge(xs',xs))
merge[Ite](True(),Cons(x,xs),ys) -> Cons(x,merge(xs,ys))
- Signature:
{<=/2,goal/2,merge/2,merge[Ite]/3} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {<=,goal,merge,merge[Ite]} and constructors {0,Cons,False
,Nil,S,True}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* Step 2: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
goal(xs,ys) -> merge(xs,ys)
merge(Cons(x,xs),Nil()) -> Cons(x,xs)
merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
merge(Nil(),ys) -> ys
- Weak TRS:
<=(0(),y) -> True()
<=(S(x),0()) -> False()
<=(S(x),S(y)) -> <=(x,y)
merge[Ite](False(),xs',Cons(x,xs)) -> Cons(x,merge(xs',xs))
merge[Ite](True(),Cons(x,xs),ys) -> Cons(x,merge(xs,ys))
- Signature:
{<=/2,goal/2,merge/2,merge[Ite]/3} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {<=,goal,merge,merge[Ite]} and constructors {0,Cons,False
,Nil,S,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(merge[Ite]) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(<=) = [3]
p(Cons) = [1] x2 + [0]
p(False) = [3]
p(Nil) = [3]
p(S) = [1]
p(True) = [3]
p(goal) = [4] x1 + [4] x2 + [0]
p(merge) = [4] x1 + [4] x2 + [3]
p(merge[Ite]) = [1] x1 + [4] x2 + [4] x3 + [0]
Following rules are strictly oriented:
merge(Cons(x,xs),Nil()) = [4] xs + [15]
> [1] xs + [0]
= Cons(x,xs)
merge(Nil(),ys) = [4] ys + [15]
> [1] ys + [0]
= ys
Following rules are (at-least) weakly oriented:
<=(0(),y) = [3]
>= [3]
= True()
<=(S(x),0()) = [3]
>= [3]
= False()
<=(S(x),S(y)) = [3]
>= [3]
= <=(x,y)
goal(xs,ys) = [4] xs + [4] ys + [0]
>= [4] xs + [4] ys + [3]
= merge(xs,ys)
merge(Cons(x',xs'),Cons(x,xs)) = [4] xs + [4] xs' + [3]
>= [4] xs + [4] xs' + [3]
= merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
merge[Ite](False(),xs',Cons(x,xs)) = [4] xs + [4] xs' + [3]
>= [4] xs + [4] xs' + [3]
= Cons(x,merge(xs',xs))
merge[Ite](True(),Cons(x,xs),ys) = [4] xs + [4] ys + [3]
>= [4] xs + [4] ys + [3]
= Cons(x,merge(xs,ys))
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:
goal(xs,ys) -> merge(xs,ys)
merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
- Weak TRS:
<=(0(),y) -> True()
<=(S(x),0()) -> False()
<=(S(x),S(y)) -> <=(x,y)
merge(Cons(x,xs),Nil()) -> Cons(x,xs)
merge(Nil(),ys) -> ys
merge[Ite](False(),xs',Cons(x,xs)) -> Cons(x,merge(xs',xs))
merge[Ite](True(),Cons(x,xs),ys) -> Cons(x,merge(xs,ys))
- Signature:
{<=/2,goal/2,merge/2,merge[Ite]/3} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {<=,goal,merge,merge[Ite]} and constructors {0,Cons,False
,Nil,S,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(merge[Ite]) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(<=) = [3]
p(Cons) = [1] x2 + [0]
p(False) = [0]
p(Nil) = [2]
p(S) = [0]
p(True) = [0]
p(goal) = [4] x1 + [6] x2 + [1]
p(merge) = [4] x1 + [4] x2 + [0]
p(merge[Ite]) = [1] x1 + [4] x2 + [4] x3 + [0]
Following rules are strictly oriented:
goal(xs,ys) = [4] xs + [6] ys + [1]
> [4] xs + [4] ys + [0]
= merge(xs,ys)
Following rules are (at-least) weakly oriented:
<=(0(),y) = [3]
>= [0]
= True()
<=(S(x),0()) = [3]
>= [0]
= False()
<=(S(x),S(y)) = [3]
>= [3]
= <=(x,y)
merge(Cons(x,xs),Nil()) = [4] xs + [8]
>= [1] xs + [0]
= Cons(x,xs)
merge(Cons(x',xs'),Cons(x,xs)) = [4] xs + [4] xs' + [0]
>= [4] xs + [4] xs' + [3]
= merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
merge(Nil(),ys) = [4] ys + [8]
>= [1] ys + [0]
= ys
merge[Ite](False(),xs',Cons(x,xs)) = [4] xs + [4] xs' + [0]
>= [4] xs + [4] xs' + [0]
= Cons(x,merge(xs',xs))
merge[Ite](True(),Cons(x,xs),ys) = [4] xs + [4] ys + [0]
>= [4] xs + [4] ys + [0]
= Cons(x,merge(xs,ys))
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:
merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
- Weak TRS:
<=(0(),y) -> True()
<=(S(x),0()) -> False()
<=(S(x),S(y)) -> <=(x,y)
goal(xs,ys) -> merge(xs,ys)
merge(Cons(x,xs),Nil()) -> Cons(x,xs)
merge(Nil(),ys) -> ys
merge[Ite](False(),xs',Cons(x,xs)) -> Cons(x,merge(xs',xs))
merge[Ite](True(),Cons(x,xs),ys) -> Cons(x,merge(xs,ys))
- Signature:
{<=/2,goal/2,merge/2,merge[Ite]/3} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {<=,goal,merge,merge[Ite]} and constructors {0,Cons,False
,Nil,S,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(merge[Ite]) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [1]
p(<=) = [4]
p(Cons) = [1] x2 + [1]
p(False) = [2]
p(Nil) = [0]
p(S) = [1] x1 + [2]
p(True) = [4]
p(goal) = [6] x1 + [4] x2 + [5]
p(merge) = [4] x1 + [4] x2 + [5]
p(merge[Ite]) = [1] x1 + [4] x2 + [4] x3 + [0]
Following rules are strictly oriented:
merge(Cons(x',xs'),Cons(x,xs)) = [4] xs + [4] xs' + [13]
> [4] xs + [4] xs' + [12]
= merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
Following rules are (at-least) weakly oriented:
<=(0(),y) = [4]
>= [4]
= True()
<=(S(x),0()) = [4]
>= [2]
= False()
<=(S(x),S(y)) = [4]
>= [4]
= <=(x,y)
goal(xs,ys) = [6] xs + [4] ys + [5]
>= [4] xs + [4] ys + [5]
= merge(xs,ys)
merge(Cons(x,xs),Nil()) = [4] xs + [9]
>= [1] xs + [1]
= Cons(x,xs)
merge(Nil(),ys) = [4] ys + [5]
>= [1] ys + [0]
= ys
merge[Ite](False(),xs',Cons(x,xs)) = [4] xs + [4] xs' + [6]
>= [4] xs + [4] xs' + [6]
= Cons(x,merge(xs',xs))
merge[Ite](True(),Cons(x,xs),ys) = [4] xs + [4] ys + [8]
>= [4] xs + [4] ys + [6]
= Cons(x,merge(xs,ys))
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:
<=(0(),y) -> True()
<=(S(x),0()) -> False()
<=(S(x),S(y)) -> <=(x,y)
goal(xs,ys) -> merge(xs,ys)
merge(Cons(x,xs),Nil()) -> Cons(x,xs)
merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
merge(Nil(),ys) -> ys
merge[Ite](False(),xs',Cons(x,xs)) -> Cons(x,merge(xs',xs))
merge[Ite](True(),Cons(x,xs),ys) -> Cons(x,merge(xs,ys))
- Signature:
{<=/2,goal/2,merge/2,merge[Ite]/3} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {<=,goal,merge,merge[Ite]} and constructors {0,Cons,False
,Nil,S,True}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^1))