The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

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))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

not(z0) → xor(z0, true)
or(z0, z1) → xor(and(z0, z1), xor(z0, z1))
implies(z0, z1) → xor(and(z0, z1), xor(z0, true))
and(z0, true) → z0
and(z0, false) → false
and(z0, z0) → z0
and(xor(z0, z1), z2) → xor(and(z0, z2), and(z1, z2))
xor(z0, false) → z0
xor(z0, z0) → false

Tuples:

NOT(z0) → c(XOR(z0, true))
OR(z0, z1) → c1(XOR(and(z0, z1), xor(z0, z1)), AND(z0, z1), XOR(z0, z1))
IMPLIES(z0, z1) → c2(XOR(and(z0, z1), xor(z0, true)), AND(z0, z1), XOR(z0, true))
AND(xor(z0, z1), z2) → c6(XOR(and(z0, z2), and(z1, z2)), AND(z0, z2), AND(z1, z2))

S tuples:

NOT(z0) → c(XOR(z0, true))
OR(z0, z1) → c1(XOR(and(z0, z1), xor(z0, z1)), AND(z0, z1), XOR(z0, z1))
IMPLIES(z0, z1) → c2(XOR(and(z0, z1), xor(z0, true)), AND(z0, z1), XOR(z0, true))
AND(xor(z0, z1), z2) → c6(XOR(and(z0, z2), and(z1, z2)), AND(z0, z2), AND(z1, z2))

K tuples:none
Defined Rule Symbols:

not, or, implies, and, xor

Defined Pair Symbols:

NOT, OR, IMPLIES, AND

Compound Symbols:

c, c1, c2, c6

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

NOT(z0) → c(XOR(z0, true))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

not(z0) → xor(z0, true)
or(z0, z1) → xor(and(z0, z1), xor(z0, z1))
implies(z0, z1) → xor(and(z0, z1), xor(z0, true))
and(z0, true) → z0
and(z0, false) → false
and(z0, z0) → z0
and(xor(z0, z1), z2) → xor(and(z0, z2), and(z1, z2))
xor(z0, false) → z0
xor(z0, z0) → false

Tuples:

OR(z0, z1) → c1(XOR(and(z0, z1), xor(z0, z1)), AND(z0, z1), XOR(z0, z1))
IMPLIES(z0, z1) → c2(XOR(and(z0, z1), xor(z0, true)), AND(z0, z1), XOR(z0, true))
AND(xor(z0, z1), z2) → c6(XOR(and(z0, z2), and(z1, z2)), AND(z0, z2), AND(z1, z2))

S tuples:

OR(z0, z1) → c1(XOR(and(z0, z1), xor(z0, z1)), AND(z0, z1), XOR(z0, z1))
IMPLIES(z0, z1) → c2(XOR(and(z0, z1), xor(z0, true)), AND(z0, z1), XOR(z0, true))
AND(xor(z0, z1), z2) → c6(XOR(and(z0, z2), and(z1, z2)), AND(z0, z2), AND(z1, z2))

K tuples:none
Defined Rule Symbols:

not, or, implies, and, xor

Defined Pair Symbols:

OR, IMPLIES, AND

Compound Symbols:

c1, c2, c6

(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 5 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

not(z0) → xor(z0, true)
or(z0, z1) → xor(and(z0, z1), xor(z0, z1))
implies(z0, z1) → xor(and(z0, z1), xor(z0, true))
and(z0, true) → z0
and(z0, false) → false
and(z0, z0) → z0
and(xor(z0, z1), z2) → xor(and(z0, z2), and(z1, z2))
xor(z0, false) → z0
xor(z0, z0) → false

Tuples:

OR(z0, z1) → c1(AND(z0, z1))
IMPLIES(z0, z1) → c2(AND(z0, z1))
AND(xor(z0, z1), z2) → c6(AND(z0, z2), AND(z1, z2))

S tuples:

OR(z0, z1) → c1(AND(z0, z1))
IMPLIES(z0, z1) → c2(AND(z0, z1))
AND(xor(z0, z1), z2) → c6(AND(z0, z2), AND(z1, z2))

K tuples:none
Defined Rule Symbols:

not, or, implies, and, xor

Defined Pair Symbols:

OR, IMPLIES, AND

Compound Symbols:

c1, c2, c6

(7) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

OR(z0, z1) → c1(AND(z0, z1))
IMPLIES(z0, z1) → c2(AND(z0, z1))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

not(z0) → xor(z0, true)
or(z0, z1) → xor(and(z0, z1), xor(z0, z1))
implies(z0, z1) → xor(and(z0, z1), xor(z0, true))
and(z0, true) → z0
and(z0, false) → false
and(z0, z0) → z0
and(xor(z0, z1), z2) → xor(and(z0, z2), and(z1, z2))
xor(z0, false) → z0
xor(z0, z0) → false

Tuples:

OR(z0, z1) → c1(AND(z0, z1))
IMPLIES(z0, z1) → c2(AND(z0, z1))
AND(xor(z0, z1), z2) → c6(AND(z0, z2), AND(z1, z2))

S tuples:

AND(xor(z0, z1), z2) → c6(AND(z0, z2), AND(z1, z2))

K tuples:

OR(z0, z1) → c1(AND(z0, z1))
IMPLIES(z0, z1) → c2(AND(z0, z1))

Defined Rule Symbols:

not, or, implies, and, xor

Defined Pair Symbols:

OR, IMPLIES, AND

Compound Symbols:

c1, c2, c6

(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:

OR(z0, z1) → c1(AND(z0, z1))
IMPLIES(z0, z1) → c2(AND(z0, z1))
AND(xor(z0, z1), z2) → c6(AND(z0, z2), AND(z1, z2))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(AND(x₁, x₂)) = [4] + [2]x₁   
POL(IMPLIES(x₁, x₂)) = [4] + [5]x₁   
POL(OR(x₁, x₂)) = [5] + [4]x₁   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c6(x₁, x₂)) = x₁ + x₂   
POL(xor(x₁, x₂)) = [4] + [4]x₁ + [4]x₂   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

not(z0) → xor(z0, true)
or(z0, z1) → xor(and(z0, z1), xor(z0, z1))
implies(z0, z1) → xor(and(z0, z1), xor(z0, true))
and(z0, true) → z0
and(z0, false) → false
and(z0, z0) → z0
and(xor(z0, z1), z2) → xor(and(z0, z2), and(z1, z2))
xor(z0, false) → z0
xor(z0, z0) → false

Tuples:

OR(z0, z1) → c1(AND(z0, z1))
IMPLIES(z0, z1) → c2(AND(z0, z1))
AND(xor(z0, z1), z2) → c6(AND(z0, z2), AND(z1, z2))

S tuples:none
K tuples:

OR(z0, z1) → c1(AND(z0, z1))
IMPLIES(z0, z1) → c2(AND(z0, z1))
AND(xor(z0, z1), z2) → c6(AND(z0, z2), AND(z1, z2))

Defined Rule Symbols:

not, or, implies, and, xor

Defined Pair Symbols:

OR, IMPLIES, AND

Compound Symbols:

c1, c2, c6

(11) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(12) BOUNDS(O(1), O(1))