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