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

(0) Obligation:

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

not(x) → if(x, false, true)
and(x, y) → if(x, y, false)
or(x, y) → if(x, true, y)
implies(x, y) → if(x, y, true)
=(x, x) → true
=(x, y) → if(x, y, not(y))
if(true, x, y) → x
if(false, x, y) → y
if(x, x, if(x, false, true)) → true
=(x, y) → if(x, y, if(y, false, true))

Rewrite Strategy: INNERMOST

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

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

not(z0) → if(z0, false, true)
and(z0, z1) → if(z0, z1, false)
or(z0, z1) → if(z0, true, z1)
implies(z0, z1) → if(z0, z1, true)
=(z0, z0) → true
=(z0, z1) → if(z0, z1, not(z1))
=(z0, z1) → if(z0, z1, if(z1, false, true))
if(true, z0, z1) → z0
if(false, z0, z1) → z1
if(z0, z0, if(z0, false, true)) → true

Tuples:

NOT(z0) → c(IF(z0, false, true))
AND(z0, z1) → c1(IF(z0, z1, false))
OR(z0, z1) → c2(IF(z0, true, z1))
IMPLIES(z0, z1) → c3(IF(z0, z1, true))
='(z0, z1) → c5(IF(z0, z1, not(z1)), NOT(z1))
='(z0, z1) → c6(IF(z0, z1, if(z1, false, true)), IF(z1, false, true))

S tuples:

NOT(z0) → c(IF(z0, false, true))
AND(z0, z1) → c1(IF(z0, z1, false))
OR(z0, z1) → c2(IF(z0, true, z1))
IMPLIES(z0, z1) → c3(IF(z0, z1, true))
='(z0, z1) → c5(IF(z0, z1, not(z1)), NOT(z1))
='(z0, z1) → c6(IF(z0, z1, if(z1, false, true)), IF(z1, false, true))

K tuples:none
Defined Rule Symbols:

not, and, or, implies, =, if

Defined Pair Symbols:

NOT, AND, OR, IMPLIES, ='

Compound Symbols:

c, c1, c2, c3, c5, c6

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

Removed 6 trailing nodes:

OR(z0, z1) → c2(IF(z0, true, z1))
IMPLIES(z0, z1) → c3(IF(z0, z1, true))
NOT(z0) → c(IF(z0, false, true))
='(z0, z1) → c6(IF(z0, z1, if(z1, false, true)), IF(z1, false, true))
AND(z0, z1) → c1(IF(z0, z1, false))
='(z0, z1) → c5(IF(z0, z1, not(z1)), NOT(z1))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

not(z0) → if(z0, false, true)
and(z0, z1) → if(z0, z1, false)
or(z0, z1) → if(z0, true, z1)
implies(z0, z1) → if(z0, z1, true)
=(z0, z0) → true
=(z0, z1) → if(z0, z1, not(z1))
=(z0, z1) → if(z0, z1, if(z1, false, true))
if(true, z0, z1) → z0
if(false, z0, z1) → z1
if(z0, z0, if(z0, false, true)) → true

Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:

not, and, or, implies, =, if

Defined Pair Symbols:none

Compound Symbols:none

(5) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(6) BOUNDS(O(1), O(1))