(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
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)
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
xor(z0, F) → z0
xor(z0, neg(z0)) → F
xor(z0, z0) → F
and(z0, T) → z0
and(z0, F) → F
and(z0, z0) → z0
and(xor(z0, z1), z2) → xor(and(z0, z2), and(z1, z2))
impl(z0, z1) → xor(and(z0, z1), xor(z0, T))
or(z0, z1) → xor(and(z0, z1), xor(z0, z1))
equiv(z0, z1) → xor(z0, xor(z1, T))
neg(z0) → xor(z0, T)
Tuples:
AND(xor(z0, z1), z2) → c6(XOR(and(z0, z2), and(z1, z2)), AND(z0, z2), AND(z1, z2))
IMPL(z0, z1) → c7(XOR(and(z0, z1), xor(z0, T)), AND(z0, z1), XOR(z0, T))
OR(z0, z1) → c8(XOR(and(z0, z1), xor(z0, z1)), AND(z0, z1), XOR(z0, z1))
EQUIV(z0, z1) → c9(XOR(z0, xor(z1, T)), XOR(z1, T))
NEG(z0) → c10(XOR(z0, T))
S tuples:
AND(xor(z0, z1), z2) → c6(XOR(and(z0, z2), and(z1, z2)), AND(z0, z2), AND(z1, z2))
IMPL(z0, z1) → c7(XOR(and(z0, z1), xor(z0, T)), AND(z0, z1), XOR(z0, T))
OR(z0, z1) → c8(XOR(and(z0, z1), xor(z0, z1)), AND(z0, z1), XOR(z0, z1))
EQUIV(z0, z1) → c9(XOR(z0, xor(z1, T)), XOR(z1, T))
NEG(z0) → c10(XOR(z0, T))
K tuples:none
Defined Rule Symbols:
xor, and, impl, or, equiv, neg
Defined Pair Symbols:
AND, IMPL, OR, EQUIV, NEG
Compound Symbols:
c6, c7, c8, c9, c10
(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing nodes:
EQUIV(z0, z1) → c9(XOR(z0, xor(z1, T)), XOR(z1, T))
NEG(z0) → c10(XOR(z0, T))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
xor(z0, F) → z0
xor(z0, neg(z0)) → F
xor(z0, z0) → F
and(z0, T) → z0
and(z0, F) → F
and(z0, z0) → z0
and(xor(z0, z1), z2) → xor(and(z0, z2), and(z1, z2))
impl(z0, z1) → xor(and(z0, z1), xor(z0, T))
or(z0, z1) → xor(and(z0, z1), xor(z0, z1))
equiv(z0, z1) → xor(z0, xor(z1, T))
neg(z0) → xor(z0, T)
Tuples:
AND(xor(z0, z1), z2) → c6(XOR(and(z0, z2), and(z1, z2)), AND(z0, z2), AND(z1, z2))
IMPL(z0, z1) → c7(XOR(and(z0, z1), xor(z0, T)), AND(z0, z1), XOR(z0, T))
OR(z0, z1) → c8(XOR(and(z0, z1), xor(z0, z1)), AND(z0, z1), XOR(z0, z1))
S tuples:
AND(xor(z0, z1), z2) → c6(XOR(and(z0, z2), and(z1, z2)), AND(z0, z2), AND(z1, z2))
IMPL(z0, z1) → c7(XOR(and(z0, z1), xor(z0, T)), AND(z0, z1), XOR(z0, T))
OR(z0, z1) → c8(XOR(and(z0, z1), xor(z0, z1)), AND(z0, z1), XOR(z0, z1))
K tuples:none
Defined Rule Symbols:
xor, and, impl, or, equiv, neg
Defined Pair Symbols:
AND, IMPL, OR
Compound Symbols:
c6, c7, c8
(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 5 trailing tuple parts
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
xor(z0, F) → z0
xor(z0, neg(z0)) → F
xor(z0, z0) → F
and(z0, T) → z0
and(z0, F) → F
and(z0, z0) → z0
and(xor(z0, z1), z2) → xor(and(z0, z2), and(z1, z2))
impl(z0, z1) → xor(and(z0, z1), xor(z0, T))
or(z0, z1) → xor(and(z0, z1), xor(z0, z1))
equiv(z0, z1) → xor(z0, xor(z1, T))
neg(z0) → xor(z0, T)
Tuples:
AND(xor(z0, z1), z2) → c6(AND(z0, z2), AND(z1, z2))
IMPL(z0, z1) → c7(AND(z0, z1))
OR(z0, z1) → c8(AND(z0, z1))
S tuples:
AND(xor(z0, z1), z2) → c6(AND(z0, z2), AND(z1, z2))
IMPL(z0, z1) → c7(AND(z0, z1))
OR(z0, z1) → c8(AND(z0, z1))
K tuples:none
Defined Rule Symbols:
xor, and, impl, or, equiv, neg
Defined Pair Symbols:
AND, IMPL, OR
Compound Symbols:
c6, c7, c8
(7) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
IMPL(z0, z1) → c7(AND(z0, z1))
OR(z0, z1) → c8(AND(z0, z1))
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
xor(z0, F) → z0
xor(z0, neg(z0)) → F
xor(z0, z0) → F
and(z0, T) → z0
and(z0, F) → F
and(z0, z0) → z0
and(xor(z0, z1), z2) → xor(and(z0, z2), and(z1, z2))
impl(z0, z1) → xor(and(z0, z1), xor(z0, T))
or(z0, z1) → xor(and(z0, z1), xor(z0, z1))
equiv(z0, z1) → xor(z0, xor(z1, T))
neg(z0) → xor(z0, T)
Tuples:
AND(xor(z0, z1), z2) → c6(AND(z0, z2), AND(z1, z2))
IMPL(z0, z1) → c7(AND(z0, z1))
OR(z0, z1) → c8(AND(z0, z1))
S tuples:
AND(xor(z0, z1), z2) → c6(AND(z0, z2), AND(z1, z2))
K tuples:
IMPL(z0, z1) → c7(AND(z0, z1))
OR(z0, z1) → c8(AND(z0, z1))
Defined Rule Symbols:
xor, and, impl, or, equiv, neg
Defined Pair Symbols:
AND, IMPL, OR
Compound Symbols:
c6, c7, c8
(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
AND(xor(z0, z1), z2) → c6(AND(z0, z2), AND(z1, z2))
We considered the (Usable) Rules:none
And the Tuples:
AND(xor(z0, z1), z2) → c6(AND(z0, z2), AND(z1, z2))
IMPL(z0, z1) → c7(AND(z0, z1))
OR(z0, z1) → c8(AND(z0, z1))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(AND(x1, x2)) = [4] + [2]x1
POL(IMPL(x1, x2)) = [5] + [5]x1
POL(OR(x1, x2)) = [5] + [3]x1
POL(c6(x1, x2)) = x1 + x2
POL(c7(x1)) = x1
POL(c8(x1)) = x1
POL(xor(x1, x2)) = [4] + [4]x1 + [4]x2
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
xor(z0, F) → z0
xor(z0, neg(z0)) → F
xor(z0, z0) → F
and(z0, T) → z0
and(z0, F) → F
and(z0, z0) → z0
and(xor(z0, z1), z2) → xor(and(z0, z2), and(z1, z2))
impl(z0, z1) → xor(and(z0, z1), xor(z0, T))
or(z0, z1) → xor(and(z0, z1), xor(z0, z1))
equiv(z0, z1) → xor(z0, xor(z1, T))
neg(z0) → xor(z0, T)
Tuples:
AND(xor(z0, z1), z2) → c6(AND(z0, z2), AND(z1, z2))
IMPL(z0, z1) → c7(AND(z0, z1))
OR(z0, z1) → c8(AND(z0, z1))
S tuples:none
K tuples:
IMPL(z0, z1) → c7(AND(z0, z1))
OR(z0, z1) → c8(AND(z0, z1))
AND(xor(z0, z1), z2) → c6(AND(z0, z2), AND(z1, z2))
Defined Rule Symbols:
xor, and, impl, or, equiv, neg
Defined Pair Symbols:
AND, IMPL, OR
Compound Symbols:
c6, c7, c8
(11) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(12) BOUNDS(O(1), O(1))