* Step 1: Sum WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
nub(@l) -> nub#1(@l)
nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) -> nil()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0
,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove
,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* Step 2: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
nub(@l) -> nub#1(@l)
nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) -> nil()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0
,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove
,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ 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(#and) = {1,2},
uargs(::) = {2},
uargs(and) = {1,2},
uargs(nub) = {1},
uargs(remove#2) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(#0) = [0]
p(#and) = [1] x1 + [1] x2 + [0]
p(#eq) = [0]
p(#equal) = [0]
p(#false) = [0]
p(#neg) = [1] x1 + [0]
p(#pos) = [1] x1 + [0]
p(#s) = [1] x1 + [0]
p(#true) = [0]
p(::) = [1] x2 + [5]
p(and) = [1] x1 + [1] x2 + [0]
p(eq) = [4]
p(eq#1) = [0]
p(eq#2) = [0]
p(eq#3) = [0]
p(nil) = [0]
p(nub) = [1] x1 + [0]
p(nub#1) = [1] x1 + [0]
p(remove) = [0]
p(remove#1) = [0]
p(remove#2) = [1] x1 + [0]
Following rules are strictly oriented:
eq(@l1,@l2) = [4]
> [0]
= eq#1(@l1,@l2)
Following rules are (at-least) weakly oriented:
#and(#false(),#false()) = [0]
>= [0]
= #false()
#and(#false(),#true()) = [0]
>= [0]
= #false()
#and(#true(),#false()) = [0]
>= [0]
= #false()
#and(#true(),#true()) = [0]
>= [0]
= #true()
#eq(#0(),#0()) = [0]
>= [0]
= #true()
#eq(#0(),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#s(@y)) = [0]
>= [0]
= #false()
#eq(#neg(@x),#0()) = [0]
>= [0]
= #false()
#eq(#neg(@x),#neg(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#0()) = [0]
>= [0]
= #false()
#eq(#pos(@x),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#pos(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#s(@x),#0()) = [0]
>= [0]
= #false()
#eq(#s(@x),#s(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0]
>= [0]
= #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) = [0]
>= [0]
= #false()
#eq(nil(),::(@y_1,@y_2)) = [0]
>= [0]
= #false()
#eq(nil(),nil()) = [0]
>= [0]
= #true()
#equal(@x,@y) = [0]
>= [0]
= #eq(@x,@y)
and(@x,@y) = [1] @x + [1] @y + [0]
>= [1] @x + [1] @y + [0]
= #and(@x,@y)
eq#1(::(@x,@xs),@l2) = [0]
>= [0]
= eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) = [0]
>= [0]
= eq#2(@l2)
eq#2(::(@y,@ys)) = [0]
>= [0]
= #false()
eq#2(nil()) = [0]
>= [0]
= #true()
eq#3(::(@y,@ys),@x,@xs) = [0]
>= [4]
= and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) = [0]
>= [0]
= #false()
nub(@l) = [1] @l + [0]
>= [1] @l + [0]
= nub#1(@l)
nub#1(::(@x,@xs)) = [1] @xs + [5]
>= [5]
= ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) = [0]
>= [0]
= nil()
remove(@x,@l) = [0]
>= [0]
= remove#1(@l,@x)
remove#1(::(@y,@ys),@x) = [0]
>= [4]
= remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) = [0]
>= [0]
= nil()
remove#2(#false(),@x,@y,@ys) = [0]
>= [5]
= ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) = [0]
>= [0]
= remove(@x,@ys)
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:
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
nub(@l) -> nub#1(@l)
nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) -> nil()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
eq(@l1,@l2) -> eq#1(@l1,@l2)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0
,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove
,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ 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(#and) = {1,2},
uargs(::) = {2},
uargs(and) = {1,2},
uargs(nub) = {1},
uargs(remove#2) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(#0) = [0]
p(#and) = [1] x1 + [1] x2 + [0]
p(#eq) = [0]
p(#equal) = [0]
p(#false) = [0]
p(#neg) = [1] x1 + [0]
p(#pos) = [0]
p(#s) = [1] x1 + [0]
p(#true) = [0]
p(::) = [1] x2 + [7]
p(and) = [1] x1 + [1] x2 + [0]
p(eq) = [0]
p(eq#1) = [0]
p(eq#2) = [0]
p(eq#3) = [0]
p(nil) = [0]
p(nub) = [1] x1 + [0]
p(nub#1) = [1] x1 + [2]
p(remove) = [0]
p(remove#1) = [0]
p(remove#2) = [1] x1 + [0]
Following rules are strictly oriented:
nub#1(::(@x,@xs)) = [1] @xs + [9]
> [7]
= ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) = [2]
> [0]
= nil()
Following rules are (at-least) weakly oriented:
#and(#false(),#false()) = [0]
>= [0]
= #false()
#and(#false(),#true()) = [0]
>= [0]
= #false()
#and(#true(),#false()) = [0]
>= [0]
= #false()
#and(#true(),#true()) = [0]
>= [0]
= #true()
#eq(#0(),#0()) = [0]
>= [0]
= #true()
#eq(#0(),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#s(@y)) = [0]
>= [0]
= #false()
#eq(#neg(@x),#0()) = [0]
>= [0]
= #false()
#eq(#neg(@x),#neg(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#0()) = [0]
>= [0]
= #false()
#eq(#pos(@x),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#pos(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#s(@x),#0()) = [0]
>= [0]
= #false()
#eq(#s(@x),#s(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0]
>= [0]
= #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) = [0]
>= [0]
= #false()
#eq(nil(),::(@y_1,@y_2)) = [0]
>= [0]
= #false()
#eq(nil(),nil()) = [0]
>= [0]
= #true()
#equal(@x,@y) = [0]
>= [0]
= #eq(@x,@y)
and(@x,@y) = [1] @x + [1] @y + [0]
>= [1] @x + [1] @y + [0]
= #and(@x,@y)
eq(@l1,@l2) = [0]
>= [0]
= eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) = [0]
>= [0]
= eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) = [0]
>= [0]
= eq#2(@l2)
eq#2(::(@y,@ys)) = [0]
>= [0]
= #false()
eq#2(nil()) = [0]
>= [0]
= #true()
eq#3(::(@y,@ys),@x,@xs) = [0]
>= [0]
= and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) = [0]
>= [0]
= #false()
nub(@l) = [1] @l + [0]
>= [1] @l + [2]
= nub#1(@l)
remove(@x,@l) = [0]
>= [0]
= remove#1(@l,@x)
remove#1(::(@y,@ys),@x) = [0]
>= [0]
= remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) = [0]
>= [0]
= nil()
remove#2(#false(),@x,@y,@ys) = [0]
>= [7]
= ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) = [0]
>= [0]
= remove(@x,@ys)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
nub(@l) -> nub#1(@l)
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
eq(@l1,@l2) -> eq#1(@l1,@l2)
nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) -> nil()
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0
,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove
,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ 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(#and) = {1,2},
uargs(::) = {2},
uargs(and) = {1,2},
uargs(nub) = {1},
uargs(remove#2) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(#0) = [0]
p(#and) = [1] x1 + [1] x2 + [0]
p(#eq) = [0]
p(#equal) = [0]
p(#false) = [0]
p(#neg) = [0]
p(#pos) = [1] x1 + [0]
p(#s) = [1] x1 + [0]
p(#true) = [0]
p(::) = [1] x2 + [0]
p(and) = [1] x1 + [1] x2 + [0]
p(eq) = [3]
p(eq#1) = [3]
p(eq#2) = [0]
p(eq#3) = [0]
p(nil) = [5]
p(nub) = [1] x1 + [5]
p(nub#1) = [5]
p(remove) = [0]
p(remove#1) = [0]
p(remove#2) = [1] x1 + [5]
Following rules are strictly oriented:
eq#1(::(@x,@xs),@l2) = [3]
> [0]
= eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) = [3]
> [0]
= eq#2(@l2)
remove#2(#false(),@x,@y,@ys) = [5]
> [0]
= ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) = [5]
> [0]
= remove(@x,@ys)
Following rules are (at-least) weakly oriented:
#and(#false(),#false()) = [0]
>= [0]
= #false()
#and(#false(),#true()) = [0]
>= [0]
= #false()
#and(#true(),#false()) = [0]
>= [0]
= #false()
#and(#true(),#true()) = [0]
>= [0]
= #true()
#eq(#0(),#0()) = [0]
>= [0]
= #true()
#eq(#0(),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#s(@y)) = [0]
>= [0]
= #false()
#eq(#neg(@x),#0()) = [0]
>= [0]
= #false()
#eq(#neg(@x),#neg(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#0()) = [0]
>= [0]
= #false()
#eq(#pos(@x),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#pos(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#s(@x),#0()) = [0]
>= [0]
= #false()
#eq(#s(@x),#s(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0]
>= [0]
= #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) = [0]
>= [0]
= #false()
#eq(nil(),::(@y_1,@y_2)) = [0]
>= [0]
= #false()
#eq(nil(),nil()) = [0]
>= [0]
= #true()
#equal(@x,@y) = [0]
>= [0]
= #eq(@x,@y)
and(@x,@y) = [1] @x + [1] @y + [0]
>= [1] @x + [1] @y + [0]
= #and(@x,@y)
eq(@l1,@l2) = [3]
>= [3]
= eq#1(@l1,@l2)
eq#2(::(@y,@ys)) = [0]
>= [0]
= #false()
eq#2(nil()) = [0]
>= [0]
= #true()
eq#3(::(@y,@ys),@x,@xs) = [0]
>= [3]
= and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) = [0]
>= [0]
= #false()
nub(@l) = [1] @l + [5]
>= [5]
= nub#1(@l)
nub#1(::(@x,@xs)) = [5]
>= [5]
= ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) = [5]
>= [5]
= nil()
remove(@x,@l) = [0]
>= [0]
= remove#1(@l,@x)
remove#1(::(@y,@ys),@x) = [0]
>= [8]
= remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) = [0]
>= [5]
= nil()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
nub(@l) -> nub#1(@l)
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0
,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove
,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ 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(#and) = {1,2},
uargs(::) = {2},
uargs(and) = {1,2},
uargs(nub) = {1},
uargs(remove#2) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(#0) = [0]
p(#and) = [1] x1 + [1] x2 + [0]
p(#eq) = [0]
p(#equal) = [1]
p(#false) = [0]
p(#neg) = [1] x1 + [0]
p(#pos) = [1] x1 + [0]
p(#s) = [0]
p(#true) = [0]
p(::) = [1] x2 + [0]
p(and) = [1] x1 + [1] x2 + [0]
p(eq) = [0]
p(eq#1) = [0]
p(eq#2) = [0]
p(eq#3) = [0]
p(nil) = [0]
p(nub) = [1] x1 + [0]
p(nub#1) = [0]
p(remove) = [0]
p(remove#1) = [0]
p(remove#2) = [1] x1 + [0]
Following rules are strictly oriented:
#equal(@x,@y) = [1]
> [0]
= #eq(@x,@y)
Following rules are (at-least) weakly oriented:
#and(#false(),#false()) = [0]
>= [0]
= #false()
#and(#false(),#true()) = [0]
>= [0]
= #false()
#and(#true(),#false()) = [0]
>= [0]
= #false()
#and(#true(),#true()) = [0]
>= [0]
= #true()
#eq(#0(),#0()) = [0]
>= [0]
= #true()
#eq(#0(),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#s(@y)) = [0]
>= [0]
= #false()
#eq(#neg(@x),#0()) = [0]
>= [0]
= #false()
#eq(#neg(@x),#neg(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#0()) = [0]
>= [0]
= #false()
#eq(#pos(@x),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#pos(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#s(@x),#0()) = [0]
>= [0]
= #false()
#eq(#s(@x),#s(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0]
>= [0]
= #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) = [0]
>= [0]
= #false()
#eq(nil(),::(@y_1,@y_2)) = [0]
>= [0]
= #false()
#eq(nil(),nil()) = [0]
>= [0]
= #true()
and(@x,@y) = [1] @x + [1] @y + [0]
>= [1] @x + [1] @y + [0]
= #and(@x,@y)
eq(@l1,@l2) = [0]
>= [0]
= eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) = [0]
>= [0]
= eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) = [0]
>= [0]
= eq#2(@l2)
eq#2(::(@y,@ys)) = [0]
>= [0]
= #false()
eq#2(nil()) = [0]
>= [0]
= #true()
eq#3(::(@y,@ys),@x,@xs) = [0]
>= [1]
= and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) = [0]
>= [0]
= #false()
nub(@l) = [1] @l + [0]
>= [0]
= nub#1(@l)
nub#1(::(@x,@xs)) = [0]
>= [0]
= ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) = [0]
>= [0]
= nil()
remove(@x,@l) = [0]
>= [0]
= remove#1(@l,@x)
remove#1(::(@y,@ys),@x) = [0]
>= [0]
= remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) = [0]
>= [0]
= nil()
remove#2(#false(),@x,@y,@ys) = [0]
>= [0]
= ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) = [0]
>= [0]
= remove(@x,@ys)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 6: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
and(@x,@y) -> #and(@x,@y)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
nub(@l) -> nub#1(@l)
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0
,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove
,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ 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(#and) = {1,2},
uargs(::) = {2},
uargs(and) = {1,2},
uargs(nub) = {1},
uargs(remove#2) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(#0) = [0]
p(#and) = [1] x1 + [1] x2 + [0]
p(#eq) = [0]
p(#equal) = [0]
p(#false) = [0]
p(#neg) = [0]
p(#pos) = [1] x1 + [0]
p(#s) = [1] x1 + [0]
p(#true) = [0]
p(::) = [1] x2 + [0]
p(and) = [1] x1 + [1] x2 + [0]
p(eq) = [0]
p(eq#1) = [0]
p(eq#2) = [0]
p(eq#3) = [0]
p(nil) = [0]
p(nub) = [1] x1 + [0]
p(nub#1) = [0]
p(remove) = [0]
p(remove#1) = [5]
p(remove#2) = [1] x1 + [0]
Following rules are strictly oriented:
remove#1(::(@y,@ys),@x) = [5]
> [0]
= remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) = [5]
> [0]
= nil()
Following rules are (at-least) weakly oriented:
#and(#false(),#false()) = [0]
>= [0]
= #false()
#and(#false(),#true()) = [0]
>= [0]
= #false()
#and(#true(),#false()) = [0]
>= [0]
= #false()
#and(#true(),#true()) = [0]
>= [0]
= #true()
#eq(#0(),#0()) = [0]
>= [0]
= #true()
#eq(#0(),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#s(@y)) = [0]
>= [0]
= #false()
#eq(#neg(@x),#0()) = [0]
>= [0]
= #false()
#eq(#neg(@x),#neg(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#0()) = [0]
>= [0]
= #false()
#eq(#pos(@x),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#pos(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#s(@x),#0()) = [0]
>= [0]
= #false()
#eq(#s(@x),#s(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0]
>= [0]
= #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) = [0]
>= [0]
= #false()
#eq(nil(),::(@y_1,@y_2)) = [0]
>= [0]
= #false()
#eq(nil(),nil()) = [0]
>= [0]
= #true()
#equal(@x,@y) = [0]
>= [0]
= #eq(@x,@y)
and(@x,@y) = [1] @x + [1] @y + [0]
>= [1] @x + [1] @y + [0]
= #and(@x,@y)
eq(@l1,@l2) = [0]
>= [0]
= eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) = [0]
>= [0]
= eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) = [0]
>= [0]
= eq#2(@l2)
eq#2(::(@y,@ys)) = [0]
>= [0]
= #false()
eq#2(nil()) = [0]
>= [0]
= #true()
eq#3(::(@y,@ys),@x,@xs) = [0]
>= [0]
= and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) = [0]
>= [0]
= #false()
nub(@l) = [1] @l + [0]
>= [0]
= nub#1(@l)
nub#1(::(@x,@xs)) = [0]
>= [0]
= ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) = [0]
>= [0]
= nil()
remove(@x,@l) = [0]
>= [5]
= remove#1(@l,@x)
remove#2(#false(),@x,@y,@ys) = [0]
>= [0]
= ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) = [0]
>= [0]
= remove(@x,@ys)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 7: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
and(@x,@y) -> #and(@x,@y)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
nub(@l) -> nub#1(@l)
remove(@x,@l) -> remove#1(@l,@x)
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) -> nil()
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0
,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove
,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ 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(#and) = {1,2},
uargs(::) = {2},
uargs(and) = {1,2},
uargs(nub) = {1},
uargs(remove#2) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(#0) = [0]
p(#and) = [1] x1 + [1] x2 + [0]
p(#eq) = [0]
p(#equal) = [0]
p(#false) = [0]
p(#neg) = [1] x1 + [0]
p(#pos) = [0]
p(#s) = [1] x1 + [0]
p(#true) = [0]
p(::) = [1] x2 + [0]
p(and) = [1] x1 + [1] x2 + [0]
p(eq) = [1]
p(eq#1) = [1]
p(eq#2) = [1]
p(eq#3) = [1]
p(nil) = [6]
p(nub) = [1] x1 + [0]
p(nub#1) = [1] x1 + [0]
p(remove) = [0]
p(remove#1) = [6]
p(remove#2) = [1] x1 + [5]
Following rules are strictly oriented:
eq#2(::(@y,@ys)) = [1]
> [0]
= #false()
eq#2(nil()) = [1]
> [0]
= #true()
eq#3(nil(),@x,@xs) = [1]
> [0]
= #false()
Following rules are (at-least) weakly oriented:
#and(#false(),#false()) = [0]
>= [0]
= #false()
#and(#false(),#true()) = [0]
>= [0]
= #false()
#and(#true(),#false()) = [0]
>= [0]
= #false()
#and(#true(),#true()) = [0]
>= [0]
= #true()
#eq(#0(),#0()) = [0]
>= [0]
= #true()
#eq(#0(),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#s(@y)) = [0]
>= [0]
= #false()
#eq(#neg(@x),#0()) = [0]
>= [0]
= #false()
#eq(#neg(@x),#neg(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#0()) = [0]
>= [0]
= #false()
#eq(#pos(@x),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#pos(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#s(@x),#0()) = [0]
>= [0]
= #false()
#eq(#s(@x),#s(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0]
>= [0]
= #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) = [0]
>= [0]
= #false()
#eq(nil(),::(@y_1,@y_2)) = [0]
>= [0]
= #false()
#eq(nil(),nil()) = [0]
>= [0]
= #true()
#equal(@x,@y) = [0]
>= [0]
= #eq(@x,@y)
and(@x,@y) = [1] @x + [1] @y + [0]
>= [1] @x + [1] @y + [0]
= #and(@x,@y)
eq(@l1,@l2) = [1]
>= [1]
= eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) = [1]
>= [1]
= eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) = [1]
>= [1]
= eq#2(@l2)
eq#3(::(@y,@ys),@x,@xs) = [1]
>= [1]
= and(#equal(@x,@y),eq(@xs,@ys))
nub(@l) = [1] @l + [0]
>= [1] @l + [0]
= nub#1(@l)
nub#1(::(@x,@xs)) = [1] @xs + [0]
>= [0]
= ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) = [6]
>= [6]
= nil()
remove(@x,@l) = [0]
>= [6]
= remove#1(@l,@x)
remove#1(::(@y,@ys),@x) = [6]
>= [6]
= remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) = [6]
>= [6]
= nil()
remove#2(#false(),@x,@y,@ys) = [5]
>= [0]
= ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) = [5]
>= [0]
= remove(@x,@ys)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 8: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
and(@x,@y) -> #and(@x,@y)
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
nub(@l) -> nub#1(@l)
remove(@x,@l) -> remove#1(@l,@x)
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(nil(),@x,@xs) -> #false()
nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) -> nil()
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0
,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove
,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ 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(#and) = {1,2},
uargs(::) = {2},
uargs(and) = {1,2},
uargs(nub) = {1},
uargs(remove#2) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(#0) = [0]
p(#and) = [1] x1 + [1] x2 + [0]
p(#eq) = [0]
p(#equal) = [0]
p(#false) = [0]
p(#neg) = [0]
p(#pos) = [0]
p(#s) = [1] x1 + [0]
p(#true) = [0]
p(::) = [1] x2 + [0]
p(and) = [1] x1 + [1] x2 + [1]
p(eq) = [1]
p(eq#1) = [0]
p(eq#2) = [0]
p(eq#3) = [0]
p(nil) = [1]
p(nub) = [1] x1 + [0]
p(nub#1) = [1]
p(remove) = [1]
p(remove#1) = [2]
p(remove#2) = [1] x1 + [1]
Following rules are strictly oriented:
and(@x,@y) = [1] @x + [1] @y + [1]
> [1] @x + [1] @y + [0]
= #and(@x,@y)
Following rules are (at-least) weakly oriented:
#and(#false(),#false()) = [0]
>= [0]
= #false()
#and(#false(),#true()) = [0]
>= [0]
= #false()
#and(#true(),#false()) = [0]
>= [0]
= #false()
#and(#true(),#true()) = [0]
>= [0]
= #true()
#eq(#0(),#0()) = [0]
>= [0]
= #true()
#eq(#0(),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#s(@y)) = [0]
>= [0]
= #false()
#eq(#neg(@x),#0()) = [0]
>= [0]
= #false()
#eq(#neg(@x),#neg(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#0()) = [0]
>= [0]
= #false()
#eq(#pos(@x),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#pos(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#s(@x),#0()) = [0]
>= [0]
= #false()
#eq(#s(@x),#s(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0]
>= [0]
= #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) = [0]
>= [0]
= #false()
#eq(nil(),::(@y_1,@y_2)) = [0]
>= [0]
= #false()
#eq(nil(),nil()) = [0]
>= [0]
= #true()
#equal(@x,@y) = [0]
>= [0]
= #eq(@x,@y)
eq(@l1,@l2) = [1]
>= [0]
= eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) = [0]
>= [0]
= eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) = [0]
>= [0]
= eq#2(@l2)
eq#2(::(@y,@ys)) = [0]
>= [0]
= #false()
eq#2(nil()) = [0]
>= [0]
= #true()
eq#3(::(@y,@ys),@x,@xs) = [0]
>= [2]
= and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) = [0]
>= [0]
= #false()
nub(@l) = [1] @l + [0]
>= [1]
= nub#1(@l)
nub#1(::(@x,@xs)) = [1]
>= [1]
= ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) = [1]
>= [1]
= nil()
remove(@x,@l) = [1]
>= [2]
= remove#1(@l,@x)
remove#1(::(@y,@ys),@x) = [2]
>= [2]
= remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) = [2]
>= [1]
= nil()
remove#2(#false(),@x,@y,@ys) = [1]
>= [1]
= ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) = [1]
>= [1]
= remove(@x,@ys)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 9: MI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
nub(@l) -> nub#1(@l)
remove(@x,@l) -> remove#1(@l,@x)
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(nil(),@x,@xs) -> #false()
nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) -> nil()
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0
,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove
,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity Nothing)), miDimension = 1, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity Nothing)):
The following argument positions are considered usable:
uargs(#and) = {1,2},
uargs(::) = {2},
uargs(and) = {1,2},
uargs(nub) = {1},
uargs(remove#2) = {1}
Following symbols are considered usable:
{#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove,remove#1,remove#2}
TcT has computed the following interpretation:
p(#0) = [0]
p(#and) = [1] x_1 + [1] x_2 + [0]
p(#eq) = [0]
p(#equal) = [0]
p(#false) = [0]
p(#neg) = [0]
p(#pos) = [4]
p(#s) = [1]
p(#true) = [0]
p(::) = [1] x_1 + [1] x_2 + [8]
p(and) = [4] x_1 + [8] x_2 + [0]
p(eq) = [0]
p(eq#1) = [0]
p(eq#2) = [0]
p(eq#3) = [0]
p(nil) = [0]
p(nub) = [2] x_1 + [8]
p(nub#1) = [2] x_1 + [0]
p(remove) = [1] x_2 + [0]
p(remove#1) = [1] x_1 + [0]
p(remove#2) = [8] x_1 + [1] x_3 + [1] x_4 + [8]
Following rules are strictly oriented:
nub(@l) = [2] @l + [8]
> [2] @l + [0]
= nub#1(@l)
Following rules are (at-least) weakly oriented:
#and(#false(),#false()) = [0]
>= [0]
= #false()
#and(#false(),#true()) = [0]
>= [0]
= #false()
#and(#true(),#false()) = [0]
>= [0]
= #false()
#and(#true(),#true()) = [0]
>= [0]
= #true()
#eq(#0(),#0()) = [0]
>= [0]
= #true()
#eq(#0(),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#0(),#s(@y)) = [0]
>= [0]
= #false()
#eq(#neg(@x),#0()) = [0]
>= [0]
= #false()
#eq(#neg(@x),#neg(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#0()) = [0]
>= [0]
= #false()
#eq(#pos(@x),#neg(@y)) = [0]
>= [0]
= #false()
#eq(#pos(@x),#pos(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(#s(@x),#0()) = [0]
>= [0]
= #false()
#eq(#s(@x),#s(@y)) = [0]
>= [0]
= #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0]
>= [0]
= #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) = [0]
>= [0]
= #false()
#eq(nil(),::(@y_1,@y_2)) = [0]
>= [0]
= #false()
#eq(nil(),nil()) = [0]
>= [0]
= #true()
#equal(@x,@y) = [0]
>= [0]
= #eq(@x,@y)
and(@x,@y) = [4] @x + [8] @y + [0]
>= [1] @x + [1] @y + [0]
= #and(@x,@y)
eq(@l1,@l2) = [0]
>= [0]
= eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) = [0]
>= [0]
= eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) = [0]
>= [0]
= eq#2(@l2)
eq#2(::(@y,@ys)) = [0]
>= [0]
= #false()
eq#2(nil()) = [0]
>= [0]
= #true()
eq#3(::(@y,@ys),@x,@xs) = [0]
>= [0]
= and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) = [0]
>= [0]
= #false()
nub#1(::(@x,@xs)) = [2] @x + [2] @xs + [16]
>= [1] @x + [2] @xs + [16]
= ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) = [0]
>= [0]
= nil()
remove(@x,@l) = [1] @l + [0]
>= [1] @l + [0]
= remove#1(@l,@x)
remove#1(::(@y,@ys),@x) = [1] @y + [1] @ys + [8]
>= [1] @y + [1] @ys + [8]
= remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) = [0]
>= [0]
= nil()
remove#2(#false(),@x,@y,@ys) = [1] @y + [1] @ys + [8]
>= [1] @y + [1] @ys + [8]
= ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) = [1] @y + [1] @ys + [8]
>= [1] @ys + [0]
= remove(@x,@ys)
* Step 10: MI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
remove(@x,@l) -> remove#1(@l,@x)
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(nil(),@x,@xs) -> #false()
nub(@l) -> nub#1(@l)
nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) -> nil()
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0
,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove
,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity Nothing)), miDimension = 2, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity Nothing)):
The following argument positions are considered usable:
uargs(#and) = {1,2},
uargs(::) = {2},
uargs(and) = {1,2},
uargs(nub) = {1},
uargs(remove#2) = {1}
Following symbols are considered usable:
{#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove,remove#1,remove#2}
TcT has computed the following interpretation:
p(#0) = [0]
[0]
p(#and) = [2 0] x_1 + [1 0] x_2 + [0]
[0 0] [0 0] [0]
p(#eq) = [0 0] x_1 + [0]
[1 2] [0]
p(#equal) = [0 0] x_1 + [0 0] x_2 + [0]
[1 2] [2 4] [0]
p(#false) = [0]
[0]
p(#neg) = [1 0] x_1 + [0]
[0 1] [1]
p(#pos) = [1 3] x_1 + [4]
[0 1] [4]
p(#s) = [1 1] x_1 + [0]
[0 1] [4]
p(#true) = [0]
[0]
p(::) = [0 4] x_1 + [1 4] x_2 + [0]
[0 1] [0 1] [2]
p(and) = [2 0] x_1 + [1 0] x_2 + [0]
[1 0] [0 0] [0]
p(eq) = [0 0] x_1 + [0 1] x_2 + [0]
[0 1] [0 0] [0]
p(eq#1) = [0 1] x_2 + [0]
[0 0] [0]
p(eq#2) = [0]
[0]
p(eq#3) = [0 1] x_1 + [0]
[0 0] [0]
p(nil) = [0]
[0]
p(nub) = [2 0] x_1 + [0]
[0 1] [0]
p(nub#1) = [2 0] x_1 + [0]
[0 1] [0]
p(remove) = [0 2] x_1 + [1 2] x_2 + [0]
[0 0] [0 1] [0]
p(remove#1) = [1 2] x_1 + [0 2] x_2 + [0]
[0 1] [0 0] [0]
p(remove#2) = [2 0] x_1 + [0 2] x_2 + [0 4] x_3 + [1 6] x_4 + [4]
[0 0] [0 0] [0 1] [0 1] [2]
Following rules are strictly oriented:
eq#3(::(@y,@ys),@x,@xs) = [0 1] @y + [0 1] @ys + [2]
[0 0] [0 0] [0]
> [0 1] @ys + [0]
[0 0] [0]
= and(#equal(@x,@y),eq(@xs,@ys))
Following rules are (at-least) weakly oriented:
#and(#false(),#false()) = [0]
[0]
>= [0]
[0]
= #false()
#and(#false(),#true()) = [0]
[0]
>= [0]
[0]
= #false()
#and(#true(),#false()) = [0]
[0]
>= [0]
[0]
= #false()
#and(#true(),#true()) = [0]
[0]
>= [0]
[0]
= #true()
#eq(#0(),#0()) = [0]
[0]
>= [0]
[0]
= #true()
#eq(#0(),#neg(@y)) = [0]
[0]
>= [0]
[0]
= #false()
#eq(#0(),#pos(@y)) = [0]
[0]
>= [0]
[0]
= #false()
#eq(#0(),#s(@y)) = [0]
[0]
>= [0]
[0]
= #false()
#eq(#neg(@x),#0()) = [0 0] @x + [0]
[1 2] [2]
>= [0]
[0]
= #false()
#eq(#neg(@x),#neg(@y)) = [0 0] @x + [0]
[1 2] [2]
>= [0 0] @x + [0]
[1 2] [0]
= #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) = [0 0] @x + [0]
[1 2] [2]
>= [0]
[0]
= #false()
#eq(#pos(@x),#0()) = [0 0] @x + [0]
[1 5] [12]
>= [0]
[0]
= #false()
#eq(#pos(@x),#neg(@y)) = [0 0] @x + [0]
[1 5] [12]
>= [0]
[0]
= #false()
#eq(#pos(@x),#pos(@y)) = [0 0] @x + [0]
[1 5] [12]
>= [0 0] @x + [0]
[1 2] [0]
= #eq(@x,@y)
#eq(#s(@x),#0()) = [0 0] @x + [0]
[1 3] [8]
>= [0]
[0]
= #false()
#eq(#s(@x),#s(@y)) = [0 0] @x + [0]
[1 3] [8]
>= [0 0] @x + [0]
[1 2] [0]
= #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0 0] @x_1 + [0 0] @x_2 + [0]
[0 6] [1 6] [4]
>= [0]
[0]
= #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) = [0 0] @x_1 + [0 0] @x_2 + [0]
[0 6] [1 6] [4]
>= [0]
[0]
= #false()
#eq(nil(),::(@y_1,@y_2)) = [0]
[0]
>= [0]
[0]
= #false()
#eq(nil(),nil()) = [0]
[0]
>= [0]
[0]
= #true()
#equal(@x,@y) = [0 0] @x + [0 0] @y + [0]
[1 2] [2 4] [0]
>= [0 0] @x + [0]
[1 2] [0]
= #eq(@x,@y)
and(@x,@y) = [2 0] @x + [1 0] @y + [0]
[1 0] [0 0] [0]
>= [2 0] @x + [1 0] @y + [0]
[0 0] [0 0] [0]
= #and(@x,@y)
eq(@l1,@l2) = [0 0] @l1 + [0 1] @l2 + [0]
[0 1] [0 0] [0]
>= [0 1] @l2 + [0]
[0 0] [0]
= eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) = [0 1] @l2 + [0]
[0 0] [0]
>= [0 1] @l2 + [0]
[0 0] [0]
= eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) = [0 1] @l2 + [0]
[0 0] [0]
>= [0]
[0]
= eq#2(@l2)
eq#2(::(@y,@ys)) = [0]
[0]
>= [0]
[0]
= #false()
eq#2(nil()) = [0]
[0]
>= [0]
[0]
= #true()
eq#3(nil(),@x,@xs) = [0]
[0]
>= [0]
[0]
= #false()
nub(@l) = [2 0] @l + [0]
[0 1] [0]
>= [2 0] @l + [0]
[0 1] [0]
= nub#1(@l)
nub#1(::(@x,@xs)) = [0 8] @x + [2 8] @xs + [0]
[0 1] [0 1] [2]
>= [0 8] @x + [2 8] @xs + [0]
[0 1] [0 1] [2]
= ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) = [0]
[0]
>= [0]
[0]
= nil()
remove(@x,@l) = [1 2] @l + [0 2] @x + [0]
[0 1] [0 0] [0]
>= [1 2] @l + [0 2] @x + [0]
[0 1] [0 0] [0]
= remove#1(@l,@x)
remove#1(::(@y,@ys),@x) = [0 2] @x + [0 6] @y + [1 6] @ys + [4]
[0 0] [0 1] [0 1] [2]
>= [0 2] @x + [0 6] @y + [1 6] @ys + [4]
[0 0] [0 1] [0 1] [2]
= remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) = [0 2] @x + [0]
[0 0] [0]
>= [0]
[0]
= nil()
remove#2(#false(),@x,@y,@ys) = [0 2] @x + [0 4] @y + [1 6] @ys + [4]
[0 0] [0 1] [0 1] [2]
>= [0 2] @x + [0 4] @y + [1 6] @ys + [0]
[0 0] [0 1] [0 1] [2]
= ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) = [0 2] @x + [0 4] @y + [1 6] @ys + [4]
[0 0] [0 1] [0 1] [2]
>= [0 2] @x + [1 2] @ys + [0]
[0 0] [0 1] [0]
= remove(@x,@ys)
* Step 11: MI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
remove(@x,@l) -> remove#1(@l,@x)
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
nub(@l) -> nub#1(@l)
nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) -> nil()
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0
,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove
,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity Nothing)), miDimension = 2, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity Nothing)):
The following argument positions are considered usable:
uargs(#and) = {1,2},
uargs(::) = {2},
uargs(and) = {1,2},
uargs(nub) = {1},
uargs(remove#2) = {1}
Following symbols are considered usable:
{#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove,remove#1,remove#2}
TcT has computed the following interpretation:
p(#0) = [0]
[0]
p(#and) = [2 0] x_1 + [4 0] x_2 + [0]
[0 0] [0 0] [0]
p(#eq) = [0 0] x_1 + [0]
[1 0] [0]
p(#equal) = [0 0] x_1 + [0 0] x_2 + [0]
[1 4] [1 4] [0]
p(#false) = [0]
[0]
p(#neg) = [1 0] x_1 + [2]
[0 1] [0]
p(#pos) = [1 5] x_1 + [0]
[0 1] [0]
p(#s) = [1 0] x_1 + [1]
[0 0] [0]
p(#true) = [0]
[0]
p(::) = [1 2] x_2 + [0]
[0 1] [1]
p(and) = [2 0] x_1 + [4 2] x_2 + [0]
[0 0] [4 0] [0]
p(eq) = [0]
[0]
p(eq#1) = [0]
[0]
p(eq#2) = [0]
[0]
p(eq#3) = [0]
[0]
p(nil) = [0]
[0]
p(nub) = [2 4] x_1 + [0]
[0 1] [0]
p(nub#1) = [2 4] x_1 + [0]
[0 1] [0]
p(remove) = [1 1] x_2 + [2]
[0 1] [0]
p(remove#1) = [1 1] x_1 + [1]
[0 1] [0]
p(remove#2) = [2 0] x_1 + [1 3] x_4 + [2]
[0 0] [0 1] [1]
Following rules are strictly oriented:
remove(@x,@l) = [1 1] @l + [2]
[0 1] [0]
> [1 1] @l + [1]
[0 1] [0]
= remove#1(@l,@x)
Following rules are (at-least) weakly oriented:
#and(#false(),#false()) = [0]
[0]
>= [0]
[0]
= #false()
#and(#false(),#true()) = [0]
[0]
>= [0]
[0]
= #false()
#and(#true(),#false()) = [0]
[0]
>= [0]
[0]
= #false()
#and(#true(),#true()) = [0]
[0]
>= [0]
[0]
= #true()
#eq(#0(),#0()) = [0]
[0]
>= [0]
[0]
= #true()
#eq(#0(),#neg(@y)) = [0]
[0]
>= [0]
[0]
= #false()
#eq(#0(),#pos(@y)) = [0]
[0]
>= [0]
[0]
= #false()
#eq(#0(),#s(@y)) = [0]
[0]
>= [0]
[0]
= #false()
#eq(#neg(@x),#0()) = [0 0] @x + [0]
[1 0] [2]
>= [0]
[0]
= #false()
#eq(#neg(@x),#neg(@y)) = [0 0] @x + [0]
[1 0] [2]
>= [0 0] @x + [0]
[1 0] [0]
= #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) = [0 0] @x + [0]
[1 0] [2]
>= [0]
[0]
= #false()
#eq(#pos(@x),#0()) = [0 0] @x + [0]
[1 5] [0]
>= [0]
[0]
= #false()
#eq(#pos(@x),#neg(@y)) = [0 0] @x + [0]
[1 5] [0]
>= [0]
[0]
= #false()
#eq(#pos(@x),#pos(@y)) = [0 0] @x + [0]
[1 5] [0]
>= [0 0] @x + [0]
[1 0] [0]
= #eq(@x,@y)
#eq(#s(@x),#0()) = [0 0] @x + [0]
[1 0] [1]
>= [0]
[0]
= #false()
#eq(#s(@x),#s(@y)) = [0 0] @x + [0]
[1 0] [1]
>= [0 0] @x + [0]
[1 0] [0]
= #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0 0] @x_2 + [0]
[1 2] [0]
>= [0]
[0]
= #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) = [0 0] @x_2 + [0]
[1 2] [0]
>= [0]
[0]
= #false()
#eq(nil(),::(@y_1,@y_2)) = [0]
[0]
>= [0]
[0]
= #false()
#eq(nil(),nil()) = [0]
[0]
>= [0]
[0]
= #true()
#equal(@x,@y) = [0 0] @x + [0 0] @y + [0]
[1 4] [1 4] [0]
>= [0 0] @x + [0]
[1 0] [0]
= #eq(@x,@y)
and(@x,@y) = [2 0] @x + [4 2] @y + [0]
[0 0] [4 0] [0]
>= [2 0] @x + [4 0] @y + [0]
[0 0] [0 0] [0]
= #and(@x,@y)
eq(@l1,@l2) = [0]
[0]
>= [0]
[0]
= eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) = [0]
[0]
>= [0]
[0]
= eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) = [0]
[0]
>= [0]
[0]
= eq#2(@l2)
eq#2(::(@y,@ys)) = [0]
[0]
>= [0]
[0]
= #false()
eq#2(nil()) = [0]
[0]
>= [0]
[0]
= #true()
eq#3(::(@y,@ys),@x,@xs) = [0]
[0]
>= [0]
[0]
= and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) = [0]
[0]
>= [0]
[0]
= #false()
nub(@l) = [2 4] @l + [0]
[0 1] [0]
>= [2 4] @l + [0]
[0 1] [0]
= nub#1(@l)
nub#1(::(@x,@xs)) = [2 8] @xs + [4]
[0 1] [1]
>= [2 8] @xs + [4]
[0 1] [1]
= ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) = [0]
[0]
>= [0]
[0]
= nil()
remove#1(::(@y,@ys),@x) = [1 3] @ys + [2]
[0 1] [1]
>= [1 3] @ys + [2]
[0 1] [1]
= remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) = [1]
[0]
>= [0]
[0]
= nil()
remove#2(#false(),@x,@y,@ys) = [1 3] @ys + [2]
[0 1] [1]
>= [1 3] @ys + [2]
[0 1] [1]
= ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) = [1 3] @ys + [2]
[0 1] [1]
>= [1 1] @ys + [2]
[0 1] [0]
= remove(@x,@ys)
* Step 12: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
#and(#false(),#false()) -> #false()
#and(#false(),#true()) -> #false()
#and(#true(),#false()) -> #false()
#and(#true(),#true()) -> #true()
#eq(#0(),#0()) -> #true()
#eq(#0(),#neg(@y)) -> #false()
#eq(#0(),#pos(@y)) -> #false()
#eq(#0(),#s(@y)) -> #false()
#eq(#neg(@x),#0()) -> #false()
#eq(#neg(@x),#neg(@y)) -> #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) -> #false()
#eq(#pos(@x),#0()) -> #false()
#eq(#pos(@x),#neg(@y)) -> #false()
#eq(#pos(@x),#pos(@y)) -> #eq(@x,@y)
#eq(#s(@x),#0()) -> #false()
#eq(#s(@x),#s(@y)) -> #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) -> #false()
#eq(nil(),::(@y_1,@y_2)) -> #false()
#eq(nil(),nil()) -> #true()
#equal(@x,@y) -> #eq(@x,@y)
and(@x,@y) -> #and(@x,@y)
eq(@l1,@l2) -> eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) -> eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) -> eq#2(@l2)
eq#2(::(@y,@ys)) -> #false()
eq#2(nil()) -> #true()
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) -> #false()
nub(@l) -> nub#1(@l)
nub#1(::(@x,@xs)) -> ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) -> nil()
remove(@x,@l) -> remove#1(@l,@x)
remove#1(::(@y,@ys),@x) -> remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) -> nil()
remove#2(#false(),@x,@y,@ys) -> ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) -> remove(@x,@ys)
- Signature:
{#and/2,#eq/2,#equal/2,and/2,eq/2,eq#1/2,eq#2/1,eq#3/3,nub/1,nub#1/1,remove/2,remove#1/2,remove#2/4} / {#0/0
,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove
,remove#1,remove#2} and constructors {#0,#false,#neg,#pos,#s,#true,::,nil}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^2))