We consider the following Problem:
Strict Trs:
{ f(x, nil()) -> g(nil(), x)
, f(x, g(y, z)) -> g(f(x, y), z)
, ++(x, nil()) -> x
, ++(x, g(y, z)) -> g(++(x, y), z)
, null(nil()) -> true()
, null(g(x, y)) -> false()
, mem(nil(), y) -> false()
, mem(g(x, y), z) -> or(=(y, z), mem(x, z))
, mem(x, max(x)) -> not(null(x))
, max(g(g(nil(), x), y)) -> max'(x, y)
, max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs:
{ f(x, nil()) -> g(nil(), x)
, f(x, g(y, z)) -> g(f(x, y), z)
, ++(x, nil()) -> x
, ++(x, g(y, z)) -> g(++(x, y), z)
, null(nil()) -> true()
, null(g(x, y)) -> false()
, mem(nil(), y) -> false()
, mem(g(x, y), z) -> or(=(y, z), mem(x, z))
, mem(x, max(x)) -> not(null(x))
, max(g(g(nil(), x), y)) -> max'(x, y)
, max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ null(nil()) -> true()
, null(g(x, y)) -> false()
, mem(nil(), y) -> false()
, max(g(g(nil(), x), y)) -> max'(x, y)
, max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u())}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(f) = {}, Uargs(g) = {1}, Uargs(++) = {}, Uargs(null) = {},
Uargs(mem) = {}, Uargs(or) = {2}, Uargs(=) = {}, Uargs(max) = {},
Uargs(not) = {1}, Uargs(max') = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
nil() = [0]
[0]
g(x1, x2) = [1 0] x1 + [0 0] x2 + [1]
[0 1] [1 0] [1]
++(x1, x2) = [1 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
null(x1) = [0 0] x1 + [1]
[0 0] [1]
true() = [0]
[0]
false() = [0]
[0]
mem(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
or(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
=(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
max(x1) = [0 1] x1 + [1]
[0 0] [1]
not(x1) = [1 0] x1 + [0]
[0 0] [1]
max'(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [1]
u() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ f(x, nil()) -> g(nil(), x)
, f(x, g(y, z)) -> g(f(x, y), z)
, ++(x, nil()) -> x
, ++(x, g(y, z)) -> g(++(x, y), z)
, mem(g(x, y), z) -> or(=(y, z), mem(x, z))
, mem(x, max(x)) -> not(null(x))}
Weak Trs:
{ null(nil()) -> true()
, null(g(x, y)) -> false()
, mem(nil(), y) -> false()
, max(g(g(nil(), x), y)) -> max'(x, y)
, max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {++(x, nil()) -> x}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(f) = {}, Uargs(g) = {1}, Uargs(++) = {}, Uargs(null) = {},
Uargs(mem) = {}, Uargs(or) = {2}, Uargs(=) = {}, Uargs(max) = {},
Uargs(not) = {1}, Uargs(max') = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 0] [1]
nil() = [0]
[0]
g(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
++(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 0] [1]
null(x1) = [0 0] x1 + [0]
[0 0] [1]
true() = [0]
[0]
false() = [0]
[0]
mem(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
or(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
=(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
max(x1) = [1 0] x1 + [1]
[0 0] [1]
not(x1) = [1 0] x1 + [1]
[0 0] [1]
max'(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [1]
u() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ f(x, nil()) -> g(nil(), x)
, f(x, g(y, z)) -> g(f(x, y), z)
, ++(x, g(y, z)) -> g(++(x, y), z)
, mem(g(x, y), z) -> or(=(y, z), mem(x, z))
, mem(x, max(x)) -> not(null(x))}
Weak Trs:
{ ++(x, nil()) -> x
, null(nil()) -> true()
, null(g(x, y)) -> false()
, mem(nil(), y) -> false()
, max(g(g(nil(), x), y)) -> max'(x, y)
, max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {mem(x, max(x)) -> not(null(x))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(f) = {}, Uargs(g) = {1}, Uargs(++) = {}, Uargs(null) = {},
Uargs(mem) = {}, Uargs(or) = {2}, Uargs(=) = {}, Uargs(max) = {},
Uargs(not) = {1}, Uargs(max') = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 0] [1]
nil() = [1]
[0]
g(x1, x2) = [1 0] x1 + [1 0] x2 + [2]
[0 0] [0 0] [1]
++(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 0] [1]
null(x1) = [0 0] x1 + [0]
[0 0] [1]
true() = [0]
[0]
false() = [0]
[0]
mem(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
or(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
=(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
max(x1) = [1 0] x1 + [2]
[0 1] [0]
not(x1) = [1 0] x1 + [0]
[0 0] [1]
max'(x1, x2) = [1 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
u() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ f(x, nil()) -> g(nil(), x)
, f(x, g(y, z)) -> g(f(x, y), z)
, ++(x, g(y, z)) -> g(++(x, y), z)
, mem(g(x, y), z) -> or(=(y, z), mem(x, z))}
Weak Trs:
{ mem(x, max(x)) -> not(null(x))
, ++(x, nil()) -> x
, null(nil()) -> true()
, null(g(x, y)) -> false()
, mem(nil(), y) -> false()
, max(g(g(nil(), x), y)) -> max'(x, y)
, max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {f(x, nil()) -> g(nil(), x)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(f) = {}, Uargs(g) = {1}, Uargs(++) = {}, Uargs(null) = {},
Uargs(mem) = {}, Uargs(or) = {2}, Uargs(=) = {}, Uargs(max) = {},
Uargs(not) = {1}, Uargs(max') = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 0] [1]
nil() = [0]
[0]
g(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
++(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 0] [1]
null(x1) = [0 0] x1 + [0]
[0 0] [1]
true() = [0]
[0]
false() = [0]
[0]
mem(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [1]
or(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 0] [1]
=(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 1] [0]
max(x1) = [1 0] x1 + [1]
[0 0] [1]
not(x1) = [1 0] x1 + [0]
[0 0] [1]
max'(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [1]
u() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ f(x, g(y, z)) -> g(f(x, y), z)
, ++(x, g(y, z)) -> g(++(x, y), z)
, mem(g(x, y), z) -> or(=(y, z), mem(x, z))}
Weak Trs:
{ f(x, nil()) -> g(nil(), x)
, mem(x, max(x)) -> not(null(x))
, ++(x, nil()) -> x
, null(nil()) -> true()
, null(g(x, y)) -> false()
, mem(nil(), y) -> false()
, max(g(g(nil(), x), y)) -> max'(x, y)
, max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {mem(g(x, y), z) -> or(=(y, z), mem(x, z))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(f) = {}, Uargs(g) = {1}, Uargs(++) = {}, Uargs(null) = {},
Uargs(mem) = {}, Uargs(or) = {2}, Uargs(=) = {}, Uargs(max) = {},
Uargs(not) = {1}, Uargs(max') = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[1 1] [0 1] [3]
nil() = [0]
[0]
g(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 1] [1 0] [2]
++(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 1] [0 1] [1]
null(x1) = [1 0] x1 + [0]
[0 0] [0]
true() = [0]
[0]
false() = [0]
[0]
mem(x1, x2) = [1 1] x1 + [0 1] x2 + [3]
[0 0] [0 0] [1]
or(x1, x2) = [0 0] x1 + [1 1] x2 + [0]
[0 0] [0 0] [1]
=(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
max(x1) = [0 1] x1 + [1]
[0 0] [0]
not(x1) = [1 0] x1 + [1]
[0 0] [1]
max'(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
u() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ f(x, g(y, z)) -> g(f(x, y), z)
, ++(x, g(y, z)) -> g(++(x, y), z)}
Weak Trs:
{ mem(g(x, y), z) -> or(=(y, z), mem(x, z))
, f(x, nil()) -> g(nil(), x)
, mem(x, max(x)) -> not(null(x))
, ++(x, nil()) -> x
, null(nil()) -> true()
, null(g(x, y)) -> false()
, mem(nil(), y) -> false()
, max(g(g(nil(), x), y)) -> max'(x, y)
, max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {++(x, g(y, z)) -> g(++(x, y), z)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(f) = {}, Uargs(g) = {1}, Uargs(++) = {}, Uargs(null) = {},
Uargs(mem) = {}, Uargs(or) = {2}, Uargs(=) = {}, Uargs(max) = {},
Uargs(not) = {1}, Uargs(max') = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[1 0] [0 1] [1]
nil() = [0]
[0]
g(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 1] [1 0] [1]
++(x1, x2) = [1 0] x1 + [0 1] x2 + [1]
[0 1] [0 1] [0]
null(x1) = [0 1] x1 + [3]
[0 1] [3]
true() = [0]
[0]
false() = [0]
[0]
mem(x1, x2) = [0 1] x1 + [0 0] x2 + [3]
[0 0] [0 0] [1]
or(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
=(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
max(x1) = [0 1] x1 + [1]
[0 0] [1]
not(x1) = [1 0] x1 + [0]
[0 0] [1]
max'(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [1]
u() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs: {f(x, g(y, z)) -> g(f(x, y), z)}
Weak Trs:
{ ++(x, g(y, z)) -> g(++(x, y), z)
, mem(g(x, y), z) -> or(=(y, z), mem(x, z))
, f(x, nil()) -> g(nil(), x)
, mem(x, max(x)) -> not(null(x))
, ++(x, nil()) -> x
, null(nil()) -> true()
, null(g(x, y)) -> false()
, mem(nil(), y) -> false()
, max(g(g(nil(), x), y)) -> max'(x, y)
, max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {f(x, g(y, z)) -> g(f(x, y), z)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(f) = {}, Uargs(g) = {1}, Uargs(++) = {}, Uargs(null) = {},
Uargs(mem) = {}, Uargs(or) = {2}, Uargs(=) = {}, Uargs(max) = {},
Uargs(not) = {1}, Uargs(max') = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f(x1, x2) = [1 0] x1 + [0 1] x2 + [0]
[1 0] [0 1] [2]
nil() = [0]
[0]
g(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [1 0] [1]
++(x1, x2) = [1 0] x1 + [0 1] x2 + [0]
[0 1] [0 1] [0]
null(x1) = [0 0] x1 + [0]
[0 0] [1]
true() = [0]
[0]
false() = [0]
[0]
mem(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
[0 0] [0 0] [1]
or(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
=(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
max(x1) = [1 0] x1 + [1]
[1 0] [1]
not(x1) = [1 0] x1 + [1]
[0 0] [1]
max'(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 0] [1 0] [0]
u() = [1]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Weak Trs:
{ f(x, g(y, z)) -> g(f(x, y), z)
, ++(x, g(y, z)) -> g(++(x, y), z)
, mem(g(x, y), z) -> or(=(y, z), mem(x, z))
, f(x, nil()) -> g(nil(), x)
, mem(x, max(x)) -> not(null(x))
, ++(x, nil()) -> x
, null(nil()) -> true()
, null(g(x, y)) -> false()
, mem(nil(), y) -> false()
, max(g(g(nil(), x), y)) -> max'(x, y)
, max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ f(x, g(y, z)) -> g(f(x, y), z)
, ++(x, g(y, z)) -> g(++(x, y), z)
, mem(g(x, y), z) -> or(=(y, z), mem(x, z))
, f(x, nil()) -> g(nil(), x)
, mem(x, max(x)) -> not(null(x))
, ++(x, nil()) -> x
, null(nil()) -> true()
, null(g(x, y)) -> false()
, mem(nil(), y) -> false()
, max(g(g(nil(), x), y)) -> max'(x, y)
, max(g(g(g(x, y), z), u())) -> max'(max(g(g(x, y), z)), u())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
Hurray, we answered YES(?,O(n^1))