*** 1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
#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 DP Rules:
Weak TRS Rules:
#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
basic terms: {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove,remove#1,remove#2}/{#0,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
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:
{}
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.
*** 1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
#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 DP Rules:
Weak TRS Rules:
#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
basic terms: {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove,remove#1,remove#2}/{#0,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
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:
{}
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.
*** 1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
#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 DP Rules:
Weak TRS Rules:
#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
basic terms: {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove,remove#1,remove#2}/{#0,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
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:
{}
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.
*** 1.1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
#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 DP Rules:
Weak TRS Rules:
#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
basic terms: {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove,remove#1,remove#2}/{#0,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
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:
{}
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.
*** 1.1.1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
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 DP Rules:
Weak TRS Rules:
#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
basic terms: {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove,remove#1,remove#2}/{#0,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
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:
{}
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.
*** 1.1.1.1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
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 DP Rules:
Weak TRS Rules:
#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
basic terms: {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove,remove#1,remove#2}/{#0,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
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:
{}
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.
*** 1.1.1.1.1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
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 DP Rules:
Weak TRS Rules:
#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
basic terms: {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove,remove#1,remove#2}/{#0,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
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:
{}
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.
*** 1.1.1.1.1.1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
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 DP Rules:
Weak TRS Rules:
#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
basic terms: {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove,remove#1,remove#2}/{#0,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
Proof:
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:
{#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) = [1]
p(#and) = [2] x1 + [2] x2 + [0]
p(#eq) = [0]
p(#equal) = [0]
p(#false) = [0]
p(#neg) = [1] x1 + [1]
p(#pos) = [1] x1 + [4]
p(#s) = [2]
p(#true) = [0]
p(::) = [1] x2 + [4]
p(and) = [2] x1 + [4] x2 + [0]
p(eq) = [0]
p(eq#1) = [0]
p(eq#2) = [0]
p(eq#3) = [0]
p(nil) = [0]
p(nub) = [2] x1 + [1]
p(nub#1) = [2] x1 + [0]
p(remove) = [1] x2 + [0]
p(remove#1) = [1] x1 + [0]
p(remove#2) = [4] x1 + [1] x4 + [4]
Following rules are strictly oriented:
nub(@l) = [2] @l + [1]
> [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) = [2] @x + [4] @y + [0]
>= [2] @x + [2] @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] @xs + [8]
>= [2] @xs + [5]
= ::(@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] @ys + [4]
>= [1] @ys + [4]
= remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) = [0]
>= [0]
= nil()
remove#2(#false(),@x,@y,@ys) = [1] @ys + [4]
>= [1] @ys + [4]
= ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) = [1] @ys + [4]
>= [1] @ys + [0]
= remove(@x,@ys)
*** 1.1.1.1.1.1.1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
eq#3(::(@y,@ys),@x,@xs) -> and(#equal(@x,@y),eq(@xs,@ys))
remove(@x,@l) -> remove#1(@l,@x)
Weak DP Rules:
Weak TRS Rules:
#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
basic terms: {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove,remove#1,remove#2}/{#0,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
Proof:
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:
{#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]
[1]
p(#and) = [2 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
p(#eq) = [0]
[0]
p(#equal) = [0 0] x1 + [0 0] x2 + [0]
[0 2] [2 0] [0]
p(#false) = [0]
[0]
p(#neg) = [0 0] x1 + [0]
[0 1] [0]
p(#pos) = [0 2] x1 + [0]
[0 1] [1]
p(#s) = [0]
[2]
p(#true) = [0]
[0]
p(::) = [0 0] x1 + [1 2] x2 + [0]
[0 1] [0 1] [1]
p(and) = [2 0] x1 + [1 0] x2 + [0]
[1 0] [0 0] [0]
p(eq) = [0 1] x2 + [0]
[0 0] [0]
p(eq#1) = [0 1] x2 + [0]
[0 0] [0]
p(eq#2) = [0]
[0]
p(eq#3) = [0 1] x1 + [0]
[0 0] [0]
p(nil) = [0]
[0]
p(nub) = [2 0] x1 + [0]
[0 1] [0]
p(nub#1) = [2 0] x1 + [0]
[0 1] [0]
p(remove) = [1 1] x2 + [0]
[0 1] [0]
p(remove#1) = [1 1] x1 + [0]
[0 1] [0]
p(remove#2) = [1 0] x1 + [0 0] x3 + [1
3] x4 + [0]
[0 0] [0 1] [0
1] [1]
Following rules are strictly oriented:
eq#3(::(@y,@ys),@x,@xs) = [0 1] @y + [0 1] @ys + [1]
[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]
>= [0]
[0]
= #false()
#eq(#neg(@x),#neg(@y)) = [0]
[0]
>= [0]
[0]
= #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) = [0]
[0]
>= [0]
[0]
= #false()
#eq(#pos(@x),#0()) = [0]
[0]
>= [0]
[0]
= #false()
#eq(#pos(@x),#neg(@y)) = [0]
[0]
>= [0]
[0]
= #false()
#eq(#pos(@x),#pos(@y)) = [0]
[0]
>= [0]
[0]
= #eq(@x,@y)
#eq(#s(@x),#0()) = [0]
[0]
>= [0]
[0]
= #false()
#eq(#s(@x),#s(@y)) = [0]
[0]
>= [0]
[0]
= #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0]
[0]
>= [0]
[0]
= #and(#eq(@x_1,@y_1)
,#eq(@x_2,@y_2))
#eq(::(@x_1,@x_2),nil()) = [0]
[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]
[0 2] [2 0] [0]
>= [0]
[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 1] @l2 + [0]
[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 0] @x + [2 4] @xs + [0]
[0 1] [0 1] [1]
>= [0 0] @x + [2 4] @xs + [0]
[0 1] [0 1] [1]
= ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) = [0]
[0]
>= [0]
[0]
= nil()
remove(@x,@l) = [1 1] @l + [0]
[0 1] [0]
>= [1 1] @l + [0]
[0 1] [0]
= remove#1(@l,@x)
remove#1(::(@y,@ys),@x) = [0 1] @y + [1 3] @ys + [1]
[0 1] [0 1] [1]
>= [0 1] @y + [1 3] @ys + [0]
[0 1] [0 1] [1]
= remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) = [0]
[0]
>= [0]
[0]
= nil()
remove#2(#false(),@x,@y,@ys) = [0 0] @y + [1 3] @ys + [0]
[0 1] [0 1] [1]
>= [0 0] @y + [1 3] @ys + [0]
[0 1] [0 1] [1]
= ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) = [0 0] @y + [1 3] @ys + [0]
[0 1] [0 1] [1]
>= [1 1] @ys + [0]
[0 1] [0]
= remove(@x,@ys)
*** 1.1.1.1.1.1.1.1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
remove(@x,@l) -> remove#1(@l,@x)
Weak DP Rules:
Weak TRS Rules:
#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
basic terms: {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove,remove#1,remove#2}/{#0,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
Proof:
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:
{#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) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
p(#eq) = [0 0] x1 + [0 0] x2 + [0]
[1 2] [2 0] [2]
p(#equal) = [0 0] x1 + [0 0] x2 + [0]
[2 2] [2 2] [2]
p(#false) = [0]
[0]
p(#neg) = [1 0] x1 + [1]
[0 1] [1]
p(#pos) = [1 3] x1 + [1]
[0 0] [0]
p(#s) = [1 0] x1 + [0]
[0 1] [0]
p(#true) = [0]
[0]
p(::) = [1 2] x2 + [0]
[0 1] [1]
p(and) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
p(eq) = [0 0] x1 + [0 0] x2 + [0]
[3 0] [0 3] [0]
p(eq#1) = [0 0] x1 + [0 0] x2 + [0]
[3 0] [0 3] [0]
p(eq#2) = [0]
[0]
p(eq#3) = [0 0] x1 + [0 0] x3 + [0]
[0 3] [2 1] [0]
p(nil) = [0]
[0]
p(nub) = [2 2] x1 + [0]
[0 1] [0]
p(nub#1) = [2 2] x1 + [0]
[0 1] [0]
p(remove) = [1 1] x2 + [1]
[0 1] [0]
p(remove#1) = [1 1] x1 + [0]
[0 1] [0]
p(remove#2) = [1 0] x1 + [1 3] x4 + [1]
[0 0] [0 1] [1]
Following rules are strictly oriented:
remove(@x,@l) = [1 1] @l + [1]
[0 1] [0]
> [1 1] @l + [0]
[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]
[2]
>= [0]
[0]
= #true()
#eq(#0(),#neg(@y)) = [0 0] @y + [0]
[2 0] [4]
>= [0]
[0]
= #false()
#eq(#0(),#pos(@y)) = [0 0] @y + [0]
[2 6] [4]
>= [0]
[0]
= #false()
#eq(#0(),#s(@y)) = [0 0] @y + [0]
[2 0] [2]
>= [0]
[0]
= #false()
#eq(#neg(@x),#0()) = [0 0] @x + [0]
[1 2] [5]
>= [0]
[0]
= #false()
#eq(#neg(@x),#neg(@y)) = [0 0] @x + [0 0] @y + [0]
[1 2] [2 0] [7]
>= [0 0] @x + [0 0] @y + [0]
[1 2] [2 0] [2]
= #eq(@x,@y)
#eq(#neg(@x),#pos(@y)) = [0 0] @x + [0 0] @y + [0]
[1 2] [2 6] [7]
>= [0]
[0]
= #false()
#eq(#pos(@x),#0()) = [0 0] @x + [0]
[1 3] [3]
>= [0]
[0]
= #false()
#eq(#pos(@x),#neg(@y)) = [0 0] @x + [0 0] @y + [0]
[1 3] [2 0] [5]
>= [0]
[0]
= #false()
#eq(#pos(@x),#pos(@y)) = [0 0] @x + [0 0] @y + [0]
[1 3] [2 6] [5]
>= [0 0] @x + [0 0] @y + [0]
[1 2] [2 0] [2]
= #eq(@x,@y)
#eq(#s(@x),#0()) = [0 0] @x + [0]
[1 2] [2]
>= [0]
[0]
= #false()
#eq(#s(@x),#s(@y)) = [0 0] @x + [0 0] @y + [0]
[1 2] [2 0] [2]
>= [0 0] @x + [0 0] @y + [0]
[1 2] [2 0] [2]
= #eq(@x,@y)
#eq(::(@x_1,@x_2),::(@y_1,@y_2)) = [0 0] @x_2 + [0 0] @y_2 + [0]
[1 4] [2 4] [4]
>= [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 4] [4]
>= [0]
[0]
= #false()
#eq(nil(),::(@y_1,@y_2)) = [0 0] @y_2 + [0]
[2 4] [2]
>= [0]
[0]
= #false()
#eq(nil(),nil()) = [0]
[2]
>= [0]
[0]
= #true()
#equal(@x,@y) = [0 0] @x + [0 0] @y + [0]
[2 2] [2 2] [2]
>= [0 0] @x + [0 0] @y + [0]
[1 2] [2 0] [2]
= #eq(@x,@y)
and(@x,@y) = [1 0] @x + [1 0] @y + [0]
[0 0] [0 0] [0]
>= [1 0] @x + [1 0] @y + [0]
[0 0] [0 0] [0]
= #and(@x,@y)
eq(@l1,@l2) = [0 0] @l1 + [0 0] @l2 + [0]
[3 0] [0 3] [0]
>= [0 0] @l1 + [0 0] @l2 + [0]
[3 0] [0 3] [0]
= eq#1(@l1,@l2)
eq#1(::(@x,@xs),@l2) = [0 0] @l2 + [0 0] @xs + [0]
[0 3] [3 6] [0]
>= [0 0] @l2 + [0 0] @xs + [0]
[0 3] [2 1] [0]
= eq#3(@l2,@x,@xs)
eq#1(nil(),@l2) = [0 0] @l2 + [0]
[0 3] [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] @xs + [0 0] @ys + [0]
[2 1] [0 3] [3]
>= [0]
[0]
= and(#equal(@x,@y),eq(@xs,@ys))
eq#3(nil(),@x,@xs) = [0 0] @xs + [0]
[2 1] [0]
>= [0]
[0]
= #false()
nub(@l) = [2 2] @l + [0]
[0 1] [0]
>= [2 2] @l + [0]
[0 1] [0]
= nub#1(@l)
nub#1(::(@x,@xs)) = [2 6] @xs + [2]
[0 1] [1]
>= [2 6] @xs + [2]
[0 1] [1]
= ::(@x,nub(remove(@x,@xs)))
nub#1(nil()) = [0]
[0]
>= [0]
[0]
= nil()
remove#1(::(@y,@ys),@x) = [1 3] @ys + [1]
[0 1] [1]
>= [1 3] @ys + [1]
[0 1] [1]
= remove#2(eq(@x,@y),@x,@y,@ys)
remove#1(nil(),@x) = [0]
[0]
>= [0]
[0]
= nil()
remove#2(#false(),@x,@y,@ys) = [1 3] @ys + [1]
[0 1] [1]
>= [1 3] @ys + [1]
[0 1] [1]
= ::(@y,remove(@x,@ys))
remove#2(#true(),@x,@y,@ys) = [1 3] @ys + [1]
[0 1] [1]
>= [1 1] @ys + [1]
[0 1] [0]
= remove(@x,@ys)
*** 1.1.1.1.1.1.1.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
#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
basic terms: {#and,#eq,#equal,and,eq,eq#1,eq#2,eq#3,nub,nub#1,remove,remove#1,remove#2}/{#0,#false,#neg,#pos,#s,#true,::,nil}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).