We consider the following Problem:
Strict Trs:
{ xor(x, F()) -> x
, xor(x, neg(x)) -> F()
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()
, impl(x, y) -> xor(and(x, y), xor(x, T()))
, or(x, y) -> xor(and(x, y), xor(x, y))
, equiv(x, y) -> xor(x, xor(y, T()))
, neg(x) -> xor(x, T())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
Arguments of following rules are not normal-forms:
{xor(x, neg(x)) -> F()}
All above mentioned rules can be savely removed.
We consider the following Problem:
Strict Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()
, impl(x, y) -> xor(and(x, y), xor(x, T()))
, or(x, y) -> xor(and(x, y), xor(x, y))
, equiv(x, y) -> xor(x, xor(y, T()))
, neg(x) -> xor(x, T())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()
, impl(x, y) -> xor(and(x, y), xor(x, T()))
, or(x, y) -> xor(and(x, y), xor(x, y))
, equiv(x, y) -> xor(x, xor(y, T()))
, neg(x) -> xor(x, T())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We have computed the following dependency pairs
Strict DPs:
{ xor^#(x, F()) -> c_1()
, and^#(x, T()) -> c_2()
, and^#(x, F()) -> c_3()
, and^#(x, x) -> c_4()
, and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))
, xor^#(x, x) -> c_6()
, impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))
, or^#(x, y) -> xor^#(and(x, y), xor(x, y))
, equiv^#(x, y) -> xor^#(x, xor(y, T()))
, neg^#(x) -> xor^#(x, T())}
We consider the following Problem:
Strict DPs:
{ xor^#(x, F()) -> c_1()
, and^#(x, T()) -> c_2()
, and^#(x, F()) -> c_3()
, and^#(x, x) -> c_4()
, and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))
, xor^#(x, x) -> c_6()
, impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))
, or^#(x, y) -> xor^#(and(x, y), xor(x, y))
, equiv^#(x, y) -> xor^#(x, xor(y, T()))
, neg^#(x) -> xor^#(x, T())}
Strict Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()
, impl(x, y) -> xor(and(x, y), xor(x, T()))
, or(x, y) -> xor(and(x, y), xor(x, y))
, equiv(x, y) -> xor(x, xor(y, T()))
, neg(x) -> xor(x, T())}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We replace strict/weak-rules by the corresponding usable rules:
Strict Usable Rules:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
We consider the following Problem:
Strict DPs:
{ xor^#(x, F()) -> c_1()
, and^#(x, T()) -> c_2()
, and^#(x, F()) -> c_3()
, and^#(x, x) -> c_4()
, and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))
, xor^#(x, x) -> c_6()
, impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))
, or^#(x, y) -> xor^#(and(x, y), xor(x, y))
, equiv^#(x, y) -> xor^#(x, xor(y, T()))
, neg^#(x) -> xor^#(x, T())}
Strict Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs:
{and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))}
TRS Component:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
Interpretation of constant growth:
----------------------------------
The following argument positions are usable:
Uargs(xor) = {1, 2}, Uargs(neg) = {}, Uargs(and) = {},
Uargs(impl) = {}, Uargs(or) = {}, Uargs(equiv) = {},
Uargs(xor^#) = {1, 2}, Uargs(and^#) = {}, Uargs(impl^#) = {},
Uargs(or^#) = {}, Uargs(equiv^#) = {}, Uargs(neg^#) = {}
We have the following constructor-based EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
xor(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 2] [3]
F() = [0]
[0]
neg(x1) = [0 0] x1 + [0]
[0 0] [0]
and(x1, x2) = [1 1] x1 + [0 0] x2 + [1]
[0 2] [0 0] [0]
T() = [0]
[0]
impl(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
or(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
equiv(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
xor^#(x1, x2) = [2 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
c_1() = [0]
[0]
and^#(x1, x2) = [2 2] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
c_2() = [0]
[0]
c_3() = [0]
[0]
c_4() = [0]
[0]
c_6() = [0]
[0]
impl^#(x1, x2) = [3 2] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
or^#(x1, x2) = [3 2] x1 + [2 0] x2 + [0]
[0 0] [0 0] [0]
equiv^#(x1, x2) = [2 0] x1 + [2 0] x2 + [0]
[0 0] [0 0] [0]
neg^#(x1) = [2 0] x1 + [0]
[0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{ xor^#(x, F()) -> c_1()
, and^#(x, T()) -> c_2()
, and^#(x, F()) -> c_3()
, and^#(x, x) -> c_4()
, xor^#(x, x) -> c_6()
, impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))
, or^#(x, y) -> xor^#(and(x, y), xor(x, y))
, equiv^#(x, y) -> xor^#(x, xor(y, T()))
, neg^#(x) -> xor^#(x, T())}
Weak DPs: {and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))}
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We use following congruence DG for path analysis
->9:{2} [ YES(O(1),O(1)) ]
->8:{3} [ YES(O(1),O(1)) ]
->7:{4} [ YES(O(1),O(1)) ]
->5:{6} [ YES(O(1),O(1)) ]
|
|->10:{1} [ YES(O(1),O(1)) ]
|
`->6:{5} [ YES(O(1),O(1)) ]
->4:{7} [ YES(O(1),O(1)) ]
|
|->10:{1} [ YES(O(1),O(1)) ]
|
`->6:{5} [ YES(O(1),O(1)) ]
->3:{8} [ YES(O(1),O(1)) ]
|
|->10:{1} [ YES(O(1),O(1)) ]
|
`->6:{5} [ YES(O(1),O(1)) ]
->2:{9} [ YES(O(1),O(1)) ]
|
`->6:{5} [ YES(O(1),O(1)) ]
->1:{10} [ subsumed ]
|
|->10:{1} [ YES(O(1),O(1)) ]
|
`->6:{5} [ YES(O(1),O(1)) ]
Here dependency-pairs are as follows:
Strict DPs:
{ 1: xor^#(x, F()) -> c_1()
, 2: and^#(x, T()) -> c_2()
, 3: and^#(x, F()) -> c_3()
, 4: and^#(x, x) -> c_4()
, 5: xor^#(x, x) -> c_6()
, 6: impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))
, 7: or^#(x, y) -> xor^#(and(x, y), xor(x, y))
, 8: equiv^#(x, y) -> xor^#(x, xor(y, T()))
, 9: neg^#(x) -> xor^#(x, T())}
WeakDPs DPs:
{10: and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))}
* Path 9:{2}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Strict DPs: {and^#(x, T()) -> c_2()}
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: and^#(x, T()) -> c_2()
together with the congruence-graph
->1:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: and^#(x, T()) -> c_2()}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{1: and^#(x, T()) -> c_2()}
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
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
* Path 8:{3}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Strict DPs: {and^#(x, F()) -> c_3()}
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: and^#(x, F()) -> c_3()
together with the congruence-graph
->1:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: and^#(x, F()) -> c_3()}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{1: and^#(x, F()) -> c_3()}
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
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
* Path 7:{4}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Strict DPs: {and^#(x, x) -> c_4()}
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: and^#(x, x) -> c_4()
together with the congruence-graph
->1:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: and^#(x, x) -> c_4()}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{1: and^#(x, x) -> c_4()}
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
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
* Path 5:{6}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Strict DPs: {impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))}
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))
together with the congruence-graph
->1:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{1: impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))}
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
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
* Path 5:{6}->10:{1}: YES(O(1),O(1))
----------------------------------
We consider the following Problem:
Strict DPs: {xor^#(x, F()) -> c_1()}
Weak DPs: {impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))}
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: xor^#(x, F()) -> c_1()
2: impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))
-->_1 xor^#(x, F()) -> c_1() :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: xor^#(x, F()) -> c_1()}
WeakDPs DPs:
{2: impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))
, 1: xor^#(x, F()) -> c_1()}
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
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
* Path 5:{6}->6:{5}: YES(O(1),O(1))
---------------------------------
We consider the following Problem:
Strict DPs: {xor^#(x, x) -> c_6()}
Weak DPs: {impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))}
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: xor^#(x, x) -> c_6()
2: impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))
-->_1 xor^#(x, x) -> c_6() :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: xor^#(x, x) -> c_6()}
WeakDPs DPs:
{2: impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: impl^#(x, y) -> xor^#(and(x, y), xor(x, T()))
, 1: xor^#(x, x) -> c_6()}
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
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
* Path 4:{7}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Strict DPs: {or^#(x, y) -> xor^#(and(x, y), xor(x, y))}
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: or^#(x, y) -> xor^#(and(x, y), xor(x, y))
together with the congruence-graph
->1:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: or^#(x, y) -> xor^#(and(x, y), xor(x, y))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{1: or^#(x, y) -> xor^#(and(x, y), xor(x, y))}
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
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
* Path 4:{7}->10:{1}: YES(O(1),O(1))
----------------------------------
We consider the following Problem:
Strict DPs: {xor^#(x, F()) -> c_1()}
Weak DPs: {or^#(x, y) -> xor^#(and(x, y), xor(x, y))}
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: xor^#(x, F()) -> c_1()
2: or^#(x, y) -> xor^#(and(x, y), xor(x, y))
-->_1 xor^#(x, F()) -> c_1() :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: xor^#(x, F()) -> c_1()}
WeakDPs DPs:
{2: or^#(x, y) -> xor^#(and(x, y), xor(x, y))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: or^#(x, y) -> xor^#(and(x, y), xor(x, y))
, 1: xor^#(x, F()) -> c_1()}
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
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
* Path 4:{7}->6:{5}: YES(O(1),O(1))
---------------------------------
We consider the following Problem:
Strict DPs: {xor^#(x, x) -> c_6()}
Weak DPs: {or^#(x, y) -> xor^#(and(x, y), xor(x, y))}
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: xor^#(x, x) -> c_6()
2: or^#(x, y) -> xor^#(and(x, y), xor(x, y))
-->_1 xor^#(x, x) -> c_6() :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: xor^#(x, x) -> c_6()}
WeakDPs DPs:
{2: or^#(x, y) -> xor^#(and(x, y), xor(x, y))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: or^#(x, y) -> xor^#(and(x, y), xor(x, y))
, 1: xor^#(x, x) -> c_6()}
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
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
* Path 3:{8}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Strict DPs: {equiv^#(x, y) -> xor^#(x, xor(y, T()))}
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: equiv^#(x, y) -> xor^#(x, xor(y, T()))
together with the congruence-graph
->1:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: equiv^#(x, y) -> xor^#(x, xor(y, T()))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{1: equiv^#(x, y) -> xor^#(x, xor(y, T()))}
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
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
* Path 3:{8}->10:{1}: YES(O(1),O(1))
----------------------------------
We consider the following Problem:
Strict DPs: {xor^#(x, F()) -> c_1()}
Weak DPs: {equiv^#(x, y) -> xor^#(x, xor(y, T()))}
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: xor^#(x, F()) -> c_1()
2: equiv^#(x, y) -> xor^#(x, xor(y, T()))
-->_1 xor^#(x, F()) -> c_1() :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: xor^#(x, F()) -> c_1()}
WeakDPs DPs:
{2: equiv^#(x, y) -> xor^#(x, xor(y, T()))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: equiv^#(x, y) -> xor^#(x, xor(y, T()))
, 1: xor^#(x, F()) -> c_1()}
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
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
* Path 3:{8}->6:{5}: YES(O(1),O(1))
---------------------------------
We consider the following Problem:
Strict DPs: {xor^#(x, x) -> c_6()}
Weak DPs: {equiv^#(x, y) -> xor^#(x, xor(y, T()))}
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: xor^#(x, x) -> c_6()
2: equiv^#(x, y) -> xor^#(x, xor(y, T()))
-->_1 xor^#(x, x) -> c_6() :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: xor^#(x, x) -> c_6()}
WeakDPs DPs:
{2: equiv^#(x, y) -> xor^#(x, xor(y, T()))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: equiv^#(x, y) -> xor^#(x, xor(y, T()))
, 1: xor^#(x, x) -> c_6()}
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
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
* Path 2:{9}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Strict DPs: {neg^#(x) -> xor^#(x, T())}
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: neg^#(x) -> xor^#(x, T())
together with the congruence-graph
->1:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: neg^#(x) -> xor^#(x, T())}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{1: neg^#(x) -> xor^#(x, T())}
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
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
* Path 2:{9}->6:{5}: YES(O(1),O(1))
---------------------------------
We consider the following Problem:
Strict DPs: {xor^#(x, x) -> c_6()}
Weak DPs: {neg^#(x) -> xor^#(x, T())}
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: xor^#(x, x) -> c_6()
2: neg^#(x) -> xor^#(x, T()) -->_1 xor^#(x, x) -> c_6() :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: xor^#(x, x) -> c_6()}
WeakDPs DPs:
{2: neg^#(x) -> xor^#(x, T())}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: neg^#(x) -> xor^#(x, T())
, 1: xor^#(x, x) -> c_6()}
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
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
* Path 1:{10}: subsumed
---------------------
This path is subsumed by the proof of paths 1:{10}->10:{1},
1:{10}->6:{5}.
* Path 1:{10}->10:{1}: YES(O(1),O(1))
-----------------------------------
We consider the following Problem:
Strict DPs: {xor^#(x, F()) -> c_1()}
Weak DPs: {and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))}
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: xor^#(x, F()) -> c_1()
2: and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))
-->_1 xor^#(x, F()) -> c_1() :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: xor^#(x, F()) -> c_1()}
WeakDPs DPs:
{2: and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))
, 1: xor^#(x, F()) -> c_1()}
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
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
* Path 1:{10}->6:{5}: YES(O(1),O(1))
----------------------------------
We consider the following Problem:
Strict DPs: {xor^#(x, x) -> c_6()}
Weak DPs: {and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))}
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: xor^#(x, x) -> c_6()
2: and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))
-->_1 xor^#(x, x) -> c_6() :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: xor^#(x, x) -> c_6()}
WeakDPs DPs:
{2: and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: and^#(xor(x, y), z) -> xor^#(and(x, z), and(y, z))
, 1: xor^#(x, x) -> c_6()}
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ xor(x, F()) -> x
, and(x, T()) -> x
, and(x, F()) -> F()
, and(x, x) -> x
, and(xor(x, y), z) -> xor(and(x, z), and(y, z))
, xor(x, x) -> F()}
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))