We consider the following Problem:
Strict Trs:
{ f(s(x)) -> f(id_inc(c(x, x)))
, f(c(s(x), y)) -> g(c(x, y))
, g(c(s(x), y)) -> g(c(y, x))
, g(c(x, s(y))) -> g(c(y, x))
, g(c(x, x)) -> f(x)
, id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))
, id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs:
{ f(s(x)) -> f(id_inc(c(x, x)))
, f(c(s(x), y)) -> g(c(x, y))
, g(c(s(x), y)) -> g(c(y, x))
, g(c(x, s(y))) -> g(c(y, x))
, g(c(x, x)) -> f(x)
, id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))
, id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {g(c(x, x)) -> f(x)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(f) = {1}, Uargs(s) = {1}, Uargs(id_inc) = {},
Uargs(c) = {1, 2}, Uargs(g) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f(x1) = [1 0] x1 + [1]
[1 0] [1]
s(x1) = [1 0] x1 + [0]
[0 0] [1]
id_inc(x1) = [0 0] x1 + [0]
[0 0] [1]
c(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
g(x1) = [1 0] x1 + [3]
[1 0] [1]
0() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ f(s(x)) -> f(id_inc(c(x, x)))
, f(c(s(x), y)) -> g(c(x, y))
, g(c(s(x), y)) -> g(c(y, x))
, g(c(x, s(y))) -> g(c(y, x))
, id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))
, id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
Weak Trs: {g(c(x, x)) -> f(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {f(c(s(x), y)) -> g(c(x, y))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(f) = {1}, Uargs(s) = {1}, Uargs(id_inc) = {},
Uargs(c) = {1, 2}, Uargs(g) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f(x1) = [1 0] x1 + [1]
[1 0] [1]
s(x1) = [1 0] x1 + [0]
[0 0] [1]
id_inc(x1) = [0 0] x1 + [0]
[0 0] [1]
c(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
g(x1) = [1 0] x1 + [0]
[1 0] [0]
0() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ f(s(x)) -> f(id_inc(c(x, x)))
, g(c(s(x), y)) -> g(c(y, x))
, g(c(x, s(y))) -> g(c(y, x))
, id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))
, id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
Weak Trs:
{ f(c(s(x), y)) -> g(c(x, y))
, g(c(x, x)) -> f(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(f) = {1}, Uargs(s) = {1}, Uargs(id_inc) = {},
Uargs(c) = {1, 2}, Uargs(g) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f(x1) = [1 0] x1 + [0]
[1 0] [0]
s(x1) = [1 0] x1 + [0]
[0 0] [1]
id_inc(x1) = [0 0] x1 + [1]
[0 0] [1]
c(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
g(x1) = [1 0] x1 + [0]
[1 0] [0]
0() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ f(s(x)) -> f(id_inc(c(x, x)))
, g(c(s(x), y)) -> g(c(y, x))
, g(c(x, s(y))) -> g(c(y, x))
, id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))
, id_inc(s(x)) -> s(id_inc(x))}
Weak Trs:
{ id_inc(0()) -> 0()
, id_inc(0()) -> s(0())
, f(c(s(x), y)) -> g(c(x, y))
, g(c(x, x)) -> f(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ g(c(s(x), y)) -> g(c(y, x))
, g(c(x, s(y))) -> g(c(y, x))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(f) = {1}, Uargs(s) = {1}, Uargs(id_inc) = {},
Uargs(c) = {1, 2}, Uargs(g) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f(x1) = [1 0] x1 + [0]
[0 0] [1]
s(x1) = [1 0] x1 + [1]
[0 0] [1]
id_inc(x1) = [0 0] x1 + [1]
[0 0] [1]
c(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
g(x1) = [1 0] x1 + [1]
[0 0] [1]
0() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ f(s(x)) -> f(id_inc(c(x, x)))
, id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))
, id_inc(s(x)) -> s(id_inc(x))}
Weak Trs:
{ g(c(s(x), y)) -> g(c(y, x))
, g(c(x, s(y))) -> g(c(y, x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())
, f(c(s(x), y)) -> g(c(x, y))
, g(c(x, x)) -> f(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 2, cbits 3' on the problem
Strict Trs:
{ f(s(x)) -> f(id_inc(c(x, x)))
, id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))
, id_inc(s(x)) -> s(id_inc(x))}
Weak Trs:
{ g(c(s(x), y)) -> g(c(y, x))
, g(c(x, s(y))) -> g(c(y, x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())
, f(c(s(x), y)) -> g(c(x, y))
, g(c(x, x)) -> f(x)}
StartTerms: basic terms
Strategy: innermost
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {f(s(x)) -> f(id_inc(c(x, x)))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(f) = {1}, Uargs(s) = {1}, Uargs(id_inc) = {},
Uargs(c) = {1, 2}, Uargs(g) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f(x1) = [1 0 2] x1 + [0]
[0 0 0] [1]
[0 0 0] [1]
s(x1) = [1 0 0] x1 + [0]
[0 1 1] [0]
[0 0 0] [2]
id_inc(x1) = [0 0 0] x1 + [0]
[0 0 0] [2]
[0 1 0] [0]
c(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [1]
[0 0 0] [0 0 0] [0]
[0 1 1] [0 1 1] [1]
g(x1) = [1 0 2] x1 + [0]
[0 0 0] [1]
[0 0 0] [1]
0() = [0]
[2]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))
, id_inc(s(x)) -> s(id_inc(x))}
Weak Trs:
{ f(s(x)) -> f(id_inc(c(x, x)))
, g(c(s(x), y)) -> g(c(y, x))
, g(c(x, s(y))) -> g(c(y, x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())
, f(c(s(x), y)) -> g(c(x, y))
, g(c(x, x)) -> f(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 2, cbits 3' on the problem
Strict Trs:
{ id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))
, id_inc(s(x)) -> s(id_inc(x))}
Weak Trs:
{ f(s(x)) -> f(id_inc(c(x, x)))
, g(c(s(x), y)) -> g(c(y, x))
, g(c(x, s(y))) -> g(c(y, x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())
, f(c(s(x), y)) -> g(c(x, y))
, g(c(x, x)) -> f(x)}
StartTerms: basic terms
Strategy: innermost
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {id_inc(s(x)) -> s(id_inc(x))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(f) = {1}, Uargs(s) = {1}, Uargs(id_inc) = {},
Uargs(c) = {1, 2}, Uargs(g) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
f(x1) = [1 2 0] x1 + [2]
[0 0 0] [1]
[0 0 0] [1]
s(x1) = [1 0 0] x1 + [0]
[0 1 0] [1]
[0 0 1] [1]
id_inc(x1) = [0 1 0] x1 + [0]
[0 0 1] [0]
[0 0 1] [1]
c(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [1]
[0 1 0] [0 1 0] [0]
[0 0 0] [0 0 0] [0]
g(x1) = [1 1 0] x1 + [1]
[0 0 0] [1]
[0 0 0] [1]
0() = [0]
[0]
[1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, f(s(x)) -> f(id_inc(c(x, x)))
, g(c(s(x), y)) -> g(c(y, x))
, g(c(x, s(y))) -> g(c(y, x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())
, f(c(s(x), y)) -> g(c(x, y))
, g(c(x, x)) -> f(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, f(s(x)) -> f(id_inc(c(x, x)))
, g(c(s(x), y)) -> g(c(y, x))
, g(c(x, s(y))) -> g(c(y, x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())
, f(c(s(x), y)) -> g(c(x, y))
, g(c(x, x)) -> f(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We have computed the following dependency pairs
Strict DPs: {id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, f^#(s(x)) -> f^#(id_inc(c(x, x)))
, g^#(c(s(x), y)) -> g^#(c(y, x))
, g^#(c(x, s(y))) -> g^#(c(y, x))
, id_inc^#(0()) -> c_6()
, id_inc^#(0()) -> c_7()
, f^#(c(s(x), y)) -> g^#(c(x, y))
, g^#(c(x, x)) -> f^#(x)}
We consider the following Problem:
Strict DPs: {id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, f^#(s(x)) -> f^#(id_inc(c(x, x)))
, g^#(c(s(x), y)) -> g^#(c(y, x))
, g^#(c(x, s(y))) -> g^#(c(y, x))
, id_inc^#(0()) -> c_6()
, id_inc^#(0()) -> c_7()
, f^#(c(s(x), y)) -> g^#(c(x, y))
, g^#(c(x, x)) -> f^#(x)}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, f(s(x)) -> f(id_inc(c(x, x)))
, g(c(s(x), y)) -> g(c(y, x))
, g(c(x, s(y))) -> g(c(y, x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())
, f(c(s(x), y)) -> g(c(x, y))
, g(c(x, x)) -> f(x)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We replace strict/weak-rules by the corresponding usable rules:
Strict Usable Rules: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak Usable Rules:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
We consider the following Problem:
Strict DPs: {id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, f^#(s(x)) -> f^#(id_inc(c(x, x)))
, g^#(c(s(x), y)) -> g^#(c(y, x))
, g^#(c(x, s(y))) -> g^#(c(y, x))
, id_inc^#(0()) -> c_6()
, id_inc^#(0()) -> c_7()
, f^#(c(s(x), y)) -> g^#(c(x, y))
, g^#(c(x, x)) -> f^#(x)}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict DPs: {id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, f^#(s(x)) -> f^#(id_inc(c(x, x)))
, g^#(c(s(x), y)) -> g^#(c(y, x))
, g^#(c(x, s(y))) -> g^#(c(y, x))
, id_inc^#(0()) -> c_6()
, id_inc^#(0()) -> c_7()
, f^#(c(s(x), y)) -> g^#(c(x, y))
, g^#(c(x, x)) -> f^#(x)}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We use following congruence DG for path analysis
->2:{1,2} [ YES(?,O(n^1)) ]
|
|->3:{6} [ YES(O(1),O(1)) ]
|
`->4:{7} [ YES(O(1),O(1)) ]
->1:{3,9,8,5,4} [ YES(O(1),O(1)) ]
Here dependency-pairs are as follows:
Strict DPs:
{1: id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
WeakDPs DPs:
{ 2: id_inc^#(s(x)) -> id_inc^#(x)
, 3: f^#(s(x)) -> f^#(id_inc(c(x, x)))
, 4: g^#(c(s(x), y)) -> g^#(c(y, x))
, 5: g^#(c(x, s(y))) -> g^#(c(y, x))
, 6: id_inc^#(0()) -> c_6()
, 7: id_inc^#(0()) -> c_7()
, 8: f^#(c(s(x), y)) -> g^#(c(x, y))
, 9: g^#(c(x, x)) -> f^#(x)}
* Path 2:{1,2}: YES(?,O(n^1))
---------------------------
We consider the following Problem:
Strict DPs: {id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict DPs: {id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict DPs: {id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
No rule is usable.
We consider the following Problem:
Strict DPs: {id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The problem is match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ c_0(2, 2) -> 2
, id_inc^#_0(2) -> 1
, id_inc^#_1(2) -> 3
, id_inc^#_1(2) -> 4
, c_1_1(3, 4) -> 1
, c_1_1(4, 4) -> 3
, c_1_1(4, 4) -> 4}
* Path 2:{1,2}->3:{6}: YES(O(1),O(1))
-----------------------------------
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 2:{1,2}->3:{6}: YES(O(1),O(1))
-----------------------------------
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 2:{1,2}->3:{6}: YES(O(1),O(1))
-----------------------------------
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 2:{1,2}->4:{7}: YES(O(1),O(1))
-----------------------------------
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 2:{1,2}->4:{7}: YES(O(1),O(1))
-----------------------------------
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 2:{1,2}->4:{7}: YES(O(1),O(1))
-----------------------------------
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
Weak DPs:
{ id_inc^#(s(x)) -> id_inc^#(x)
, id_inc^#(c(x, y)) -> c_1(id_inc^#(x), id_inc^#(y))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 1:{3,9,8,5,4}: YES(O(1),O(1))
----------------------------------
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Strict Trs: {id_inc(c(x, y)) -> c(id_inc(x), id_inc(y))}
Weak Trs:
{ id_inc(s(x)) -> s(id_inc(x))
, id_inc(0()) -> 0()
, id_inc(0()) -> s(0())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
Hurray, we answered YES(?,O(n^1))