We consider the following 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()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
We consider the following 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()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ and(@x, @y) -> #and(@x, @y)
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, eq#3(nil(), @x, @xs) -> #false()
, nub#1(nil()) -> nil()
, remove#1(nil(), @x) -> nil()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(remove) = {}, Uargs(eq#2) = {}, Uargs(#equal) = {},
Uargs(eq) = {}, Uargs(#eq) = {}, Uargs(::) = {2},
Uargs(and) = {1, 2}, Uargs(remove#1) = {}, Uargs(nub) = {1},
Uargs(#pos) = {}, Uargs(#neg) = {}, Uargs(remove#2) = {1},
Uargs(eq#1) = {}, Uargs(#and) = {1, 2}, Uargs(eq#3) = {},
Uargs(#s) = {}, Uargs(nub#1) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
remove(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [1 1] [0]
eq#2(x1) = [0 0] x1 + [1]
[0 0] [1]
#equal(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
#eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [1]
#true() = [0]
[0]
#false() = [0]
[0]
::(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
remove#1(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
nub(x1) = [1 0] x1 + [0]
[0 0] [0]
#pos(x1) = [0 0] x1 + [0]
[0 0] [0]
#0() = [0]
[0]
#neg(x1) = [0 0] x1 + [0]
[0 0] [0]
remove#2(x1, x2, x3, x4) = [1 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [1]
[0 0] [1 1] [1 1] [0 0] [1]
eq#1(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
#and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
eq#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
#s(x1) = [0 0] x1 + [0]
[0 0] [0]
nub#1(x1) = [0 0] x1 + [1]
[1 0] [0]
nil() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ #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#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys)}
Weak Trs:
{ and(@x, @y) -> #and(@x, @y)
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, eq#3(nil(), @x, @xs) -> #false()
, nub#1(nil()) -> nil()
, remove#1(nil(), @x) -> nil()
, #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()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(remove) = {}, Uargs(eq#2) = {}, Uargs(#equal) = {},
Uargs(eq) = {}, Uargs(#eq) = {}, Uargs(::) = {2},
Uargs(and) = {1, 2}, Uargs(remove#1) = {}, Uargs(nub) = {1},
Uargs(#pos) = {}, Uargs(#neg) = {}, Uargs(remove#2) = {1},
Uargs(eq#1) = {}, Uargs(#and) = {1, 2}, Uargs(eq#3) = {},
Uargs(#s) = {}, Uargs(nub#1) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
remove(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
eq#2(x1) = [0 0] x1 + [1]
[0 0] [1]
#equal(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [1 1] [0]
eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
#eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [1]
#true() = [0]
[0]
#false() = [0]
[0]
::(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
remove#1(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
nub(x1) = [1 0] x1 + [0]
[0 0] [0]
#pos(x1) = [0 0] x1 + [0]
[0 0] [0]
#0() = [0]
[0]
#neg(x1) = [0 0] x1 + [0]
[0 0] [0]
remove#2(x1, x2, x3, x4) = [1 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [1]
[0 0] [1 1] [1 1] [0 0] [1]
eq#1(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
#and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
eq#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
#s(x1) = [0 0] x1 + [0]
[0 0] [0]
nub#1(x1) = [0 0] x1 + [1]
[1 0] [0]
nil() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ #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#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))}
Weak Trs:
{ remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys)
, and(@x, @y) -> #and(@x, @y)
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, eq#3(nil(), @x, @xs) -> #false()
, nub#1(nil()) -> nil()
, remove#1(nil(), @x) -> nil()
, #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()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {eq#1(nil(), @l2) -> eq#2(@l2)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(remove) = {}, Uargs(eq#2) = {}, Uargs(#equal) = {},
Uargs(eq) = {}, Uargs(#eq) = {}, Uargs(::) = {2},
Uargs(and) = {1, 2}, Uargs(remove#1) = {}, Uargs(nub) = {1},
Uargs(#pos) = {}, Uargs(#neg) = {}, Uargs(remove#2) = {1},
Uargs(eq#1) = {}, Uargs(#and) = {1, 2}, Uargs(eq#3) = {},
Uargs(#s) = {}, Uargs(nub#1) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
remove(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
eq#2(x1) = [0 0] x1 + [0]
[0 0] [1]
#equal(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [1 1] [0]
eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
#eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [1]
#true() = [0]
[0]
#false() = [0]
[0]
::(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
remove#1(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
nub(x1) = [1 0] x1 + [0]
[0 0] [0]
#pos(x1) = [0 0] x1 + [0]
[0 0] [0]
#0() = [0]
[0]
#neg(x1) = [0 0] x1 + [0]
[0 0] [0]
remove#2(x1, x2, x3, x4) = [1 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [1]
[0 0] [1 1] [1 1] [0 0] [1]
eq#1(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
#and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
eq#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
#s(x1) = [0 0] x1 + [0]
[0 0] [0]
nub#1(x1) = [0 0] x1 + [1]
[1 0] [0]
nil() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))}
Weak Trs:
{ eq#1(nil(), @l2) -> eq#2(@l2)
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys)
, and(@x, @y) -> #and(@x, @y)
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, eq#3(nil(), @x, @xs) -> #false()
, nub#1(nil()) -> nil()
, remove#1(nil(), @x) -> nil()
, #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()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(remove) = {}, Uargs(eq#2) = {}, Uargs(#equal) = {},
Uargs(eq) = {}, Uargs(#eq) = {}, Uargs(::) = {2},
Uargs(and) = {1, 2}, Uargs(remove#1) = {}, Uargs(nub) = {1},
Uargs(#pos) = {}, Uargs(#neg) = {}, Uargs(remove#2) = {1},
Uargs(eq#1) = {}, Uargs(#and) = {1, 2}, Uargs(eq#3) = {},
Uargs(#s) = {}, Uargs(nub#1) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
remove(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [1 1] [0]
eq#2(x1) = [0 0] x1 + [1]
[0 0] [1]
#equal(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
#eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[1 0] [0 1] [0]
#true() = [0]
[0]
#false() = [0]
[1]
::(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
remove#1(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
nub(x1) = [1 0] x1 + [0]
[0 0] [0]
#pos(x1) = [1 0] x1 + [0]
[0 1] [2]
#0() = [0]
[1]
#neg(x1) = [1 0] x1 + [0]
[0 1] [2]
remove#2(x1, x2, x3, x4) = [1 1] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [1]
[0 0] [1 1] [1 1] [1 1] [1]
eq#1(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
#and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
eq#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
#s(x1) = [1 0] x1 + [0]
[0 1] [2]
nub#1(x1) = [0 0] x1 + [1]
[1 0] [0]
nil() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, remove(@x, @l) -> remove#1(@l, @x)
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)}
Weak Trs:
{ remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, eq#1(nil(), @l2) -> eq#2(@l2)
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys)
, and(@x, @y) -> #and(@x, @y)
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, eq#3(nil(), @x, @xs) -> #false()
, nub#1(nil()) -> nil()
, remove#1(nil(), @x) -> nil()
, #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()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(remove) = {}, Uargs(eq#2) = {}, Uargs(#equal) = {},
Uargs(eq) = {}, Uargs(#eq) = {}, Uargs(::) = {2},
Uargs(and) = {1, 2}, Uargs(remove#1) = {}, Uargs(nub) = {1},
Uargs(#pos) = {}, Uargs(#neg) = {}, Uargs(remove#2) = {1},
Uargs(eq#1) = {}, Uargs(#and) = {1, 2}, Uargs(eq#3) = {},
Uargs(#s) = {}, Uargs(nub#1) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
remove(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
eq#2(x1) = [0 0] x1 + [1]
[0 0] [1]
#equal(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [1 1] [0]
eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
#eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[1 0] [0 1] [0]
#true() = [0]
[0]
#false() = [0]
[1]
::(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
remove#1(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [1 1] [1]
nub(x1) = [1 0] x1 + [0]
[0 0] [0]
#pos(x1) = [1 0] x1 + [0]
[0 1] [2]
#0() = [0]
[1]
#neg(x1) = [1 0] x1 + [0]
[0 1] [2]
remove#2(x1, x2, x3, x4) = [1 1] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0]
[0 0] [1 1] [0 0] [0 0] [1]
eq#1(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
#and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
eq#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
#s(x1) = [1 0] x1 + [0]
[0 1] [2]
nub#1(x1) = [0 0] x1 + [1]
[1 0] [0]
nil() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, nub(@l) -> nub#1(@l)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, remove(@x, @l) -> remove#1(@l, @x)}
Weak Trs:
{ remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, eq#1(nil(), @l2) -> eq#2(@l2)
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys)
, and(@x, @y) -> #and(@x, @y)
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, eq#3(nil(), @x, @xs) -> #false()
, nub#1(nil()) -> nil()
, remove#1(nil(), @x) -> nil()
, #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()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(remove) = {}, Uargs(eq#2) = {}, Uargs(#equal) = {},
Uargs(eq) = {}, Uargs(#eq) = {}, Uargs(::) = {2},
Uargs(and) = {1, 2}, Uargs(remove#1) = {}, Uargs(nub) = {1},
Uargs(#pos) = {}, Uargs(#neg) = {}, Uargs(remove#2) = {1},
Uargs(eq#1) = {}, Uargs(#and) = {1, 2}, Uargs(eq#3) = {},
Uargs(#s) = {}, Uargs(nub#1) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
remove(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
eq#2(x1) = [0 0] x1 + [1]
[0 0] [1]
#equal(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [1 1] [0]
eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [1]
#eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [1]
#true() = [0]
[1]
#false() = [0]
[1]
::(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
remove#1(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [1 1] [1]
nub(x1) = [1 0] x1 + [0]
[0 0] [0]
#pos(x1) = [1 0] x1 + [0]
[0 1] [0]
#0() = [0]
[0]
#neg(x1) = [0 0] x1 + [0]
[0 0] [0]
remove#2(x1, x2, x3, x4) = [1 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [1]
[0 1] [1 1] [0 0] [0 0] [0]
eq#1(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
#and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
eq#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
#s(x1) = [0 0] x1 + [0]
[0 0] [0]
nub#1(x1) = [0 0] x1 + [1]
[1 0] [1]
nil() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, 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:
{ nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, eq#1(nil(), @l2) -> eq#2(@l2)
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys)
, and(@x, @y) -> #and(@x, @y)
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, eq#3(nil(), @x, @xs) -> #false()
, nub#1(nil()) -> nil()
, remove#1(nil(), @x) -> nil()
, #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()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {remove(@x, @l) -> remove#1(@l, @x)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(remove) = {}, Uargs(eq#2) = {}, Uargs(#equal) = {},
Uargs(eq) = {}, Uargs(#eq) = {}, Uargs(::) = {2},
Uargs(and) = {1, 2}, Uargs(remove#1) = {}, Uargs(nub) = {1},
Uargs(#pos) = {}, Uargs(#neg) = {}, Uargs(remove#2) = {1},
Uargs(eq#1) = {}, Uargs(#and) = {1, 2}, Uargs(eq#3) = {},
Uargs(#s) = {}, Uargs(nub#1) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
remove(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[1 1] [0 0] [1]
eq#2(x1) = [0 0] x1 + [1]
[0 0] [1]
#equal(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
#eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 1] [0]
#true() = [0]
[1]
#false() = [0]
[1]
::(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
and(x1, x2) = [1 1] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
remove#1(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [1 1] [1]
nub(x1) = [1 0] x1 + [0]
[0 0] [0]
#pos(x1) = [0 0] x1 + [0]
[0 1] [2]
#0() = [0]
[1]
#neg(x1) = [0 0] x1 + [0]
[0 1] [2]
remove#2(x1, x2, x3, x4) = [1 1] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0]
[0 0] [1 1] [0 0] [0 0] [1]
eq#1(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
#and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
eq#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
#s(x1) = [0 0] x1 + [0]
[0 1] [2]
nub#1(x1) = [0 0] x1 + [1]
[1 0] [1]
nil() = [0]
[1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, nub(@l) -> nub#1(@l)}
Weak Trs:
{ remove(@x, @l) -> remove#1(@l, @x)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, eq#1(nil(), @l2) -> eq#2(@l2)
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys)
, and(@x, @y) -> #and(@x, @y)
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, eq#3(nil(), @x, @xs) -> #false()
, nub#1(nil()) -> nil()
, remove#1(nil(), @x) -> nil()
, #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()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(remove) = {}, Uargs(eq#2) = {}, Uargs(#equal) = {},
Uargs(eq) = {}, Uargs(#eq) = {}, Uargs(::) = {2},
Uargs(and) = {1, 2}, Uargs(remove#1) = {}, Uargs(nub) = {1},
Uargs(#pos) = {}, Uargs(#neg) = {}, Uargs(remove#2) = {1},
Uargs(eq#1) = {}, Uargs(#and) = {1, 2}, Uargs(eq#3) = {},
Uargs(#s) = {}, Uargs(nub#1) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
remove(x1, x2) = [0 0] x1 + [1 2] x2 + [0]
[0 0] [0 0] [0]
eq#2(x1) = [0 0] x1 + [1]
[0 1] [1]
#equal(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
#eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [3]
#true() = [0]
[0]
#false() = [0]
[3]
::(x1, x2) = [0 0] x1 + [1 2] x2 + [0]
[0 0] [0 0] [3]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [3]
remove#1(x1, x2) = [1 2] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
nub(x1) = [1 3] x1 + [0]
[0 0] [0]
#pos(x1) = [1 0] x1 + [0]
[0 1] [0]
#0() = [0]
[0]
#neg(x1) = [0 0] x1 + [0]
[0 0] [0]
remove#2(x1, x2, x3, x4) = [1 0] x1 + [0 0] x2 + [0 0] x3 + [1 2] x4 + [0]
[0 1] [0 0] [0 0] [0 0] [0]
eq#1(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 1] [1]
#and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [3]
eq#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [3]
#s(x1) = [0 0] x1 + [0]
[0 0] [0]
nub#1(x1) = [1 3] x1 + [0]
[0 0] [3]
nil() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, nub(@l) -> nub#1(@l)}
Weak Trs:
{ eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, remove(@x, @l) -> remove#1(@l, @x)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, eq#1(nil(), @l2) -> eq#2(@l2)
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys)
, and(@x, @y) -> #and(@x, @y)
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, eq#3(nil(), @x, @xs) -> #false()
, nub#1(nil()) -> nil()
, remove#1(nil(), @x) -> nil()
, #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()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {nub(@l) -> nub#1(@l)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(remove) = {}, Uargs(eq#2) = {}, Uargs(#equal) = {},
Uargs(eq) = {}, Uargs(#eq) = {}, Uargs(::) = {2},
Uargs(and) = {1, 2}, Uargs(remove#1) = {}, Uargs(nub) = {1},
Uargs(#pos) = {}, Uargs(#neg) = {}, Uargs(remove#2) = {1},
Uargs(eq#1) = {}, Uargs(#and) = {1, 2}, Uargs(eq#3) = {},
Uargs(#s) = {}, Uargs(nub#1) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
remove(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [1]
eq#2(x1) = [0 0] x1 + [1]
[0 0] [1]
#equal(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
#eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [1]
#true() = [0]
[0]
#false() = [0]
[1]
::(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [2]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
remove#1(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [1]
nub(x1) = [1 2] x1 + [1]
[0 0] [3]
#pos(x1) = [1 0] x1 + [0]
[0 1] [0]
#0() = [0]
[0]
#neg(x1) = [0 0] x1 + [0]
[0 0] [0]
remove#2(x1, x2, x3, x4) = [1 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0]
[0 1] [0 0] [0 0] [0 0] [1]
eq#1(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
#and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
eq#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
#s(x1) = [0 0] x1 + [0]
[0 0] [0]
nub#1(x1) = [0 2] x1 + [0]
[0 0] [3]
nil() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, eq(@l1, @l2) -> eq#1(@l1, @l2)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)}
Weak Trs:
{ nub(@l) -> nub#1(@l)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, remove(@x, @l) -> remove#1(@l, @x)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, eq#1(nil(), @l2) -> eq#2(@l2)
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys)
, and(@x, @y) -> #and(@x, @y)
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, eq#3(nil(), @x, @xs) -> #false()
, nub#1(nil()) -> nil()
, remove#1(nil(), @x) -> nil()
, #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()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(remove) = {}, Uargs(eq#2) = {}, Uargs(#equal) = {},
Uargs(eq) = {}, Uargs(#eq) = {}, Uargs(::) = {2},
Uargs(and) = {1, 2}, Uargs(remove#1) = {}, Uargs(nub) = {1},
Uargs(#pos) = {}, Uargs(#neg) = {}, Uargs(remove#2) = {1},
Uargs(eq#1) = {}, Uargs(#and) = {1, 2}, Uargs(eq#3) = {},
Uargs(#s) = {}, Uargs(nub#1) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
remove(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[1 1] [0 0] [3]
eq#2(x1) = [0 0] x1 + [1]
[0 1] [1]
#equal(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
#eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [1]
#true() = [0]
[0]
#false() = [0]
[0]
::(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [3]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
remove#1(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [1 1] [3]
nub(x1) = [1 0] x1 + [1]
[0 0] [3]
#pos(x1) = [0 0] x1 + [0]
[0 0] [0]
#0() = [0]
[0]
#neg(x1) = [0 0] x1 + [0]
[0 0] [0]
remove#2(x1, x2, x3, x4) = [1 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0]
[0 0] [1 1] [0 0] [0 0] [3]
eq#1(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 1] [1]
#and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
eq#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 0] [1]
#s(x1) = [0 0] x1 + [0]
[0 0] [0]
nub#1(x1) = [0 0] x1 + [1]
[0 0] [3]
nil() = [0]
[3]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, eq(@l1, @l2) -> eq#1(@l1, @l2)}
Weak Trs:
{ eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, nub(@l) -> nub#1(@l)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, remove(@x, @l) -> remove#1(@l, @x)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, eq#1(nil(), @l2) -> eq#2(@l2)
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys)
, and(@x, @y) -> #and(@x, @y)
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, eq#3(nil(), @x, @xs) -> #false()
, nub#1(nil()) -> nil()
, remove#1(nil(), @x) -> nil()
, #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()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {#equal(@x, @y) -> #eq(@x, @y)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(remove) = {}, Uargs(eq#2) = {}, Uargs(#equal) = {},
Uargs(eq) = {}, Uargs(#eq) = {}, Uargs(::) = {2},
Uargs(and) = {1, 2}, Uargs(remove#1) = {}, Uargs(nub) = {1},
Uargs(#pos) = {}, Uargs(#neg) = {}, Uargs(remove#2) = {1},
Uargs(eq#1) = {}, Uargs(#and) = {1, 2}, Uargs(eq#3) = {},
Uargs(#s) = {}, Uargs(nub#1) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
remove(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[1 1] [0 0] [1]
eq#2(x1) = [0 0] x1 + [1]
[0 0] [1]
#equal(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [2]
eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
#eq(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [1]
#true() = [0]
[0]
#false() = [0]
[0]
::(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [1 0] [1]
remove#1(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [1 1] [1]
nub(x1) = [1 0] x1 + [0]
[1 0] [2]
#pos(x1) = [0 0] x1 + [0]
[0 0] [0]
#0() = [0]
[0]
#neg(x1) = [0 0] x1 + [0]
[0 0] [0]
remove#2(x1, x2, x3, x4) = [1 0] x1 + [0 0] x2 + [0 0] x3 + [0 0] x4 + [0]
[0 0] [1 1] [0 0] [0 0] [1]
eq#1(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
#and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
eq#3(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
#s(x1) = [0 0] x1 + [0]
[0 0] [0]
nub#1(x1) = [0 0] x1 + [0]
[1 0] [1]
nil() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs: {eq(@l1, @l2) -> eq#1(@l1, @l2)}
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, nub(@l) -> nub#1(@l)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, remove(@x, @l) -> remove#1(@l, @x)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, eq#1(nil(), @l2) -> eq#2(@l2)
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys)
, and(@x, @y) -> #and(@x, @y)
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, eq#3(nil(), @x, @xs) -> #false()
, nub#1(nil()) -> nil()
, remove#1(nil(), @x) -> nil()
, #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()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
We consider the following Problem:
Strict Trs: {eq(@l1, @l2) -> eq#1(@l1, @l2)}
Weak Trs:
{ #equal(@x, @y) -> #eq(@x, @y)
, eq#1(::(@x, @xs), @l2) -> eq#3(@l2, @x, @xs)
, nub(@l) -> nub#1(@l)
, eq#3(::(@y, @ys), @x, @xs) -> and(#equal(@x, @y), eq(@xs, @ys))
, remove(@x, @l) -> remove#1(@l, @x)
, nub#1(::(@x, @xs)) -> ::(@x, nub(remove(@x, @xs)))
, remove#1(::(@y, @ys), @x) -> remove#2(eq(@x, @y), @x, @y, @ys)
, remove#2(#false(), @x, @y, @ys) -> ::(@y, remove(@x, @ys))
, eq#1(nil(), @l2) -> eq#2(@l2)
, remove#2(#true(), @x, @y, @ys) -> remove(@x, @ys)
, and(@x, @y) -> #and(@x, @y)
, eq#2(::(@y, @ys)) -> #false()
, eq#2(nil()) -> #true()
, eq#3(nil(), @x, @xs) -> #false()
, nub#1(nil()) -> nil()
, remove#1(nil(), @x) -> nil()
, #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()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The following argument positions are usable:
Uargs(remove) = {}, Uargs(eq#2) = {}, Uargs(#equal) = {},
Uargs(eq) = {}, Uargs(#eq) = {}, Uargs(::) = {2},
Uargs(and) = {1, 2}, Uargs(remove#1) = {}, Uargs(nub) = {1},
Uargs(#pos) = {}, Uargs(#neg) = {}, Uargs(remove#2) = {1},
Uargs(eq#1) = {}, Uargs(#and) = {1, 2}, Uargs(eq#3) = {},
Uargs(#s) = {}, Uargs(nub#1) = {}
We have the following constructor-based EDA-non-satisfying and IDA(2)-non-satisfying matrix interpretation:
Interpretation Functions:
remove(x1, x2) = [0 0 0] x1 + [1 1 0] x2 + [0]
[0 0 0] [0 0 1] [0]
[0 0 0] [0 0 1] [0]
eq#2(x1) = [0 0 1] x1 + [0]
[2 0 0] [0]
[0 0 0] [0]
#equal(x1, x2) = [0 0 0] x1 + [0 0 1] x2 + [0]
[0 0 0] [0 2 0] [1]
[0 0 0] [0 2 0] [0]
eq(x1, x2) = [0 0 0] x1 + [0 0 1] x2 + [1]
[0 0 0] [2 0 0] [0]
[0 0 0] [2 0 0] [0]
#eq(x1, x2) = [0 0 0] x1 + [0 0 1] x2 + [0]
[0 0 0] [0 2 0] [0]
[0 0 0] [0 0 0] [0]
#true() = [1]
[0]
[0]
#false() = [1]
[0]
[0]
::(x1, x2) = [0 2 0] x1 + [1 1 1] x2 + [1]
[0 0 1] [0 0 1] [0]
[0 0 1] [0 0 1] [2]
and(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [1 0 0] [0]
[0 0 2] [0 0 1] [1]
remove#1(x1, x2) = [1 1 0] x1 + [0 0 0] x2 + [0]
[0 0 1] [0 0 0] [0]
[0 0 1] [0 0 0] [0]
nub(x1) = [2 0 0] x1 + [0]
[0 1 0] [0]
[0 0 1] [0]
#pos(x1) = [0 0 0] x1 + [0]
[0 1 0] [0]
[0 0 1] [1]
#0() = [0]
[0]
[2]
#neg(x1) = [0 0 0] x1 + [0]
[0 1 0] [0]
[0 0 1] [1]
remove#2(x1, x2, x3, x4) = [1 0 0] x1 + [0 0 0] x2 + [0 2 0] x3 + [1 1 2] x4 + [0]
[0 0 0] [0 0 0] [0 0 1] [0 0 1] [0]
[0 0 0] [0 0 0] [0 0 1] [0 0 1] [2]
eq#1(x1, x2) = [0 0 0] x1 + [0 0 1] x2 + [0]
[0 0 0] [2 0 0] [0]
[0 0 0] [2 0 0] [0]
#and(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 0 0] [1 0 0] [0]
[0 0 0] [0 0 0] [0]
eq#3(x1, x2, x3) = [0 0 1] x1 + [0 0 0] x2 + [0 0 0] x3 + [0]
[2 0 0] [0 0 0] [0 0 0] [0]
[2 0 0] [0 0 0] [0 0 0] [0]
#s(x1) = [0 0 0] x1 + [0]
[0 1 0] [0]
[0 0 1] [2]
nub#1(x1) = [2 0 0] x1 + [0]
[0 1 0] [0]
[0 0 1] [0]
nil() = [2]
[2]
[2]
Hurray, we answered YES(?,O(n^2))