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