We consider the following Problem:
Strict Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, rm(N, nil()) -> nil()
, rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
, ifrm(true(), N, add(M, X)) -> rm(N, X)
, ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
, purge(nil()) -> nil()
, purge(add(N, X)) -> add(N, purge(rm(N, X)))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
We consider the following Problem:
Strict Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, rm(N, nil()) -> nil()
, rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
, ifrm(true(), N, add(M, X)) -> rm(N, X)
, ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
, purge(nil()) -> nil()
, purge(add(N, X)) -> add(N, purge(rm(N, X)))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ eq(0(), 0()) -> true()
, eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, rm(N, nil()) -> nil()
, purge(nil()) -> nil()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(eq) = {}, Uargs(s) = {}, Uargs(rm) = {}, Uargs(add) = {2},
Uargs(ifrm) = {1}, Uargs(purge) = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
eq(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
0() = [0]
[0]
true() = [0]
[0]
s(x1) = [0 0] x1 + [0]
[0 0] [0]
false() = [0]
[0]
rm(x1, x2) = [1 1] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
nil() = [0]
[0]
add(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 1] [0 0] [1]
ifrm(x1, x2, x3) = [1 0] x1 + [1 1] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 0] [1]
purge(x1) = [1 1] x1 + [1]
[0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ eq(s(X), s(Y)) -> eq(X, Y)
, rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
, ifrm(true(), N, add(M, X)) -> rm(N, X)
, ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
, purge(add(N, X)) -> add(N, purge(rm(N, X)))}
Weak Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, rm(N, nil()) -> nil()
, purge(nil()) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {ifrm(true(), N, add(M, X)) -> rm(N, X)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(eq) = {}, Uargs(s) = {}, Uargs(rm) = {}, Uargs(add) = {2},
Uargs(ifrm) = {1}, Uargs(purge) = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
eq(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
0() = [0]
[0]
true() = [0]
[0]
s(x1) = [0 0] x1 + [0]
[0 0] [0]
false() = [0]
[0]
rm(x1, x2) = [1 1] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
nil() = [0]
[0]
add(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 1] [0 0] [1]
ifrm(x1, x2, x3) = [1 0] x1 + [1 1] x2 + [0 0] x3 + [2]
[0 0] [0 0] [0 0] [1]
purge(x1) = [1 1] x1 + [0]
[0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ eq(s(X), s(Y)) -> eq(X, Y)
, rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
, ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
, purge(add(N, X)) -> add(N, purge(rm(N, X)))}
Weak Trs:
{ ifrm(true(), N, add(M, X)) -> rm(N, X)
, eq(0(), 0()) -> true()
, eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, rm(N, nil()) -> nil()
, purge(nil()) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(eq) = {}, Uargs(s) = {}, Uargs(rm) = {}, Uargs(add) = {2},
Uargs(ifrm) = {1}, Uargs(purge) = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
eq(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [1 0] [1]
0() = [3]
[0]
true() = [0]
[0]
s(x1) = [0 0] x1 + [0]
[0 0] [0]
false() = [1]
[0]
rm(x1, x2) = [1 1] x1 + [0 0] x2 + [0]
[0 0] [0 0] [1]
nil() = [0]
[0]
add(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 1] [0 0] [0]
ifrm(x1, x2, x3) = [1 0] x1 + [1 1] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 1] [1]
purge(x1) = [1 1] x1 + [1]
[0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ eq(s(X), s(Y)) -> eq(X, Y)
, rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
, purge(add(N, X)) -> add(N, purge(rm(N, X)))}
Weak Trs:
{ ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
, ifrm(true(), N, add(M, X)) -> rm(N, X)
, eq(0(), 0()) -> true()
, eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, rm(N, nil()) -> nil()
, purge(nil()) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {purge(add(N, X)) -> add(N, purge(rm(N, X)))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(eq) = {}, Uargs(s) = {}, Uargs(rm) = {}, Uargs(add) = {2},
Uargs(ifrm) = {1}, Uargs(purge) = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
eq(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [0]
0() = [0]
[0]
true() = [0]
[0]
s(x1) = [0 0] x1 + [0]
[0 0] [0]
false() = [0]
[0]
rm(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
nil() = [0]
[0]
add(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
ifrm(x1, x2, x3) = [1 0] x1 + [0 0] x2 + [0 0] x3 + [3]
[0 0] [0 0] [0 0] [1]
purge(x1) = [1 1] x1 + [0]
[0 0] [2]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ eq(s(X), s(Y)) -> eq(X, Y)
, rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))}
Weak Trs:
{ purge(add(N, X)) -> add(N, purge(rm(N, X)))
, ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
, ifrm(true(), N, add(M, X)) -> rm(N, X)
, eq(0(), 0()) -> true()
, eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, rm(N, nil()) -> nil()
, purge(nil()) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {eq(s(X), s(Y)) -> eq(X, Y)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(eq) = {}, Uargs(s) = {}, Uargs(rm) = {}, Uargs(add) = {2},
Uargs(ifrm) = {1}, Uargs(purge) = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
eq(x1, x2) = [0 0] x1 + [0 2] x2 + [0]
[0 1] [0 0] [2]
0() = [0]
[2]
true() = [0]
[0]
s(x1) = [0 0] x1 + [0]
[0 1] [2]
false() = [0]
[0]
rm(x1, x2) = [0 0] x1 + [1 2] x2 + [0]
[0 0] [0 0] [0]
nil() = [0]
[0]
add(x1, x2) = [0 0] x1 + [1 2] x2 + [0]
[0 1] [0 0] [0]
ifrm(x1, x2, x3) = [1 0] x1 + [0 0] x2 + [1 0] x3 + [0]
[0 0] [0 0] [0 1] [1]
purge(x1) = [1 0] x1 + [1]
[0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs: {rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))}
Weak Trs:
{ eq(s(X), s(Y)) -> eq(X, Y)
, purge(add(N, X)) -> add(N, purge(rm(N, X)))
, ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
, ifrm(true(), N, add(M, X)) -> rm(N, X)
, eq(0(), 0()) -> true()
, eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, rm(N, nil()) -> nil()
, purge(nil()) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
We consider the following Problem:
Strict Trs: {rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))}
Weak Trs:
{ eq(s(X), s(Y)) -> eq(X, Y)
, purge(add(N, X)) -> add(N, purge(rm(N, X)))
, ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
, ifrm(true(), N, add(M, X)) -> rm(N, X)
, eq(0(), 0()) -> true()
, eq(0(), s(X)) -> false()
, eq(s(X), 0()) -> false()
, rm(N, nil()) -> nil()
, purge(nil()) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The following argument positions are usable:
Uargs(eq) = {}, Uargs(s) = {}, Uargs(rm) = {}, Uargs(add) = {2},
Uargs(ifrm) = {1}, Uargs(purge) = {1}
We have the following constructor-based EDA-non-satisfying and IDA(2)-non-satisfying matrix interpretation:
Interpretation Functions:
eq(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 0] [0 0 0] [0]
0() = [0]
[0]
[0]
true() = [0]
[0]
[0]
s(x1) = [1 0 0] x1 + [0]
[0 1 0] [0]
[0 0 0] [0]
false() = [0]
[0]
[0]
rm(x1, x2) = [0 0 0] x1 + [1 1 0] x2 + [1]
[0 0 0] [0 1 0] [0]
[0 0 0] [0 0 0] [0]
nil() = [1]
[0]
[0]
add(x1, x2) = [0 0 0] x1 + [1 2 0] x2 + [2]
[0 0 0] [0 1 0] [2]
[0 0 0] [0 0 0] [0]
ifrm(x1, x2, x3) = [2 0 0] x1 + [0 0 0] x2 + [1 1 0] x3 + [0]
[0 0 0] [0 0 0] [0 1 0] [0]
[0 0 0] [0 0 0] [0 0 0] [0]
purge(x1) = [2 0 0] x1 + [2]
[0 1 1] [0]
[0 0 0] [1]
Hurray, we answered YES(?,O(n^2))