### (0) Obligation:

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

cond1(true, x) → cond2(even(x), x)
cond2(true, x) → cond1(neq(x, 0), div2(x))
cond2(false, x) → cond1(neq(x, 0), p(x))
neq(0, 0) → false
neq(0, s(x)) → true
neq(s(x), 0) → true
neq(s(x), s(y)) → neq(x, y)
even(0) → true
even(s(0)) → false
even(s(s(x))) → even(x)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(x))) → s(div2(x))
p(0) → 0
p(s(x)) → x

Rewrite Strategy: INNERMOST

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

Converted Cpx (relative) TRS to CDT

### (2) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond1(true, z0) → cond2(even(z0), z0)
cond2(true, z0) → cond1(neq(z0, 0), div2(z0))
cond2(false, z0) → cond1(neq(z0, 0), p(z0))
neq(0, 0) → false
neq(0, s(z0)) → true
neq(s(z0), 0) → true
neq(s(z0), s(y)) → neq(z0, y)
even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0
Tuples:

COND1(true, z0) → c(COND2(even(z0), z0), EVEN(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), NEQ(z0, 0), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)), NEQ(z0, 0), P(z0))
NEQ(0, 0) → c3
NEQ(0, s(z0)) → c4
NEQ(s(z0), 0) → c5
NEQ(s(z0), s(y)) → c6(NEQ(z0, y))
EVEN(0) → c7
EVEN(s(0)) → c8
EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(0) → c10
DIV2(s(0)) → c11
DIV2(s(s(z0))) → c12(DIV2(z0))
P(0) → c13
P(s(z0)) → c14
S tuples:

COND1(true, z0) → c(COND2(even(z0), z0), EVEN(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), NEQ(z0, 0), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)), NEQ(z0, 0), P(z0))
NEQ(0, 0) → c3
NEQ(0, s(z0)) → c4
NEQ(s(z0), 0) → c5
NEQ(s(z0), s(y)) → c6(NEQ(z0, y))
EVEN(0) → c7
EVEN(s(0)) → c8
EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(0) → c10
DIV2(s(0)) → c11
DIV2(s(s(z0))) → c12(DIV2(z0))
P(0) → c13
P(s(z0)) → c14
K tuples:none
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

COND1, COND2, NEQ, EVEN, DIV2, P

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14

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

Removed 10 trailing nodes:

DIV2(s(0)) → c11
DIV2(0) → c10
P(s(z0)) → c14
NEQ(s(z0), 0) → c5
NEQ(0, 0) → c3
NEQ(0, s(z0)) → c4
NEQ(s(z0), s(y)) → c6(NEQ(z0, y))
P(0) → c13
EVEN(0) → c7
EVEN(s(0)) → c8

### (4) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond1(true, z0) → cond2(even(z0), z0)
cond2(true, z0) → cond1(neq(z0, 0), div2(z0))
cond2(false, z0) → cond1(neq(z0, 0), p(z0))
neq(0, 0) → false
neq(0, s(z0)) → true
neq(s(z0), 0) → true
neq(s(z0), s(y)) → neq(z0, y)
even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0
Tuples:

COND1(true, z0) → c(COND2(even(z0), z0), EVEN(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), NEQ(z0, 0), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)), NEQ(z0, 0), P(z0))
EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
S tuples:

COND1(true, z0) → c(COND2(even(z0), z0), EVEN(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), NEQ(z0, 0), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)), NEQ(z0, 0), P(z0))
EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
K tuples:none
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

COND1, COND2, EVEN, DIV2

Compound Symbols:

c, c1, c2, c9, c12

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

Removed 3 trailing tuple parts

### (6) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond1(true, z0) → cond2(even(z0), z0)
cond2(true, z0) → cond1(neq(z0, 0), div2(z0))
cond2(false, z0) → cond1(neq(z0, 0), p(z0))
neq(0, 0) → false
neq(0, s(z0)) → true
neq(s(z0), 0) → true
neq(s(z0), s(y)) → neq(z0, y)
even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0
Tuples:

COND1(true, z0) → c(COND2(even(z0), z0), EVEN(z0))
EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
S tuples:

COND1(true, z0) → c(COND2(even(z0), z0), EVEN(z0))
EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
K tuples:none
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

COND1, EVEN, DIV2, COND2

Compound Symbols:

c, c9, c12, c1, c2

### (7) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

cond1(true, z0) → cond2(even(z0), z0)
cond2(true, z0) → cond1(neq(z0, 0), div2(z0))
cond2(false, z0) → cond1(neq(z0, 0), p(z0))
neq(0, s(z0)) → true
neq(s(z0), s(y)) → neq(z0, y)

### (8) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0
Tuples:

COND1(true, z0) → c(COND2(even(z0), z0), EVEN(z0))
EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
S tuples:

COND1(true, z0) → c(COND2(even(z0), z0), EVEN(z0))
EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
K tuples:none
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

COND1, EVEN, DIV2, COND2

Compound Symbols:

c, c9, c12, c1, c2

### (9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND1(true, z0) → c(COND2(even(z0), z0), EVEN(z0)) by

COND1(true, 0) → c(COND2(true, 0), EVEN(0))
COND1(true, s(0)) → c(COND2(false, s(0)), EVEN(s(0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))

### (10) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, 0) → c(COND2(true, 0), EVEN(0))
COND1(true, s(0)) → c(COND2(false, s(0)), EVEN(s(0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, 0) → c(COND2(true, 0), EVEN(0))
COND1(true, s(0)) → c(COND2(false, s(0)), EVEN(s(0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
K tuples:none
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

c9, c12, c1, c2, c

### (11) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

### (12) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
K tuples:none
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

c9, c12, c1, c2, c, c

### (13) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COND1(true, 0) → c(COND2(true, 0))
We considered the (Usable) Rules:

neq(0, 0) → false
neq(s(z0), 0) → true
And the Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND1(x1, x2)) = [2]x1
POL(COND2(x1, x2)) = [4]x2
POL(DIV2(x1)) = 0
POL(EVEN(x1)) = 0
POL(c(x1)) = x1
POL(c(x1, x2)) = x1 + x2
POL(c1(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c2(x1)) = x1
POL(c9(x1)) = x1
POL(div2(x1)) = 0
POL(even(x1)) = 0
POL(false) = 0
POL(neq(x1, x2)) = [2]x1
POL(p(x1)) = [2]
POL(s(x1)) = [1]
POL(true) = [2]

### (14) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

c9, c12, c1, c2, c, c

### (15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0)) by

COND2(true, 0) → c1(COND1(neq(0, 0), 0), DIV2(0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0), DIV2(s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, 0) → c1(COND1(false, div2(0)), DIV2(0))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))

### (16) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0), DIV2(0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0), DIV2(s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, 0) → c1(COND1(false, div2(0)), DIV2(0))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0), DIV2(0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0), DIV2(s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, 0) → c1(COND1(false, div2(0)), DIV2(0))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

c9, c12, c2, c, c, c1

### (17) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

COND2(true, 0) → c1(COND1(false, div2(0)), DIV2(0))

### (18) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0), DIV2(0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0), DIV2(s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0), DIV2(0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0), DIV2(s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

c9, c12, c2, c, c, c1

### (19) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

### (20) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

c9, c12, c2, c, c, c1, c1

### (21) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

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

COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, 0) → c(COND2(true, 0))

### (22) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

c9, c12, c2, c, c, c1, c1

### (23) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
We considered the (Usable) Rules:

p(s(z0)) → z0
div2(0) → 0
div2(s(s(z0))) → s(div2(z0))
div2(s(0)) → 0
p(0) → 0
And the Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND1(x1, x2)) = [2]x2
POL(COND2(x1, x2)) = [2]x2
POL(DIV2(x1)) = 0
POL(EVEN(x1)) = 0
POL(c(x1)) = x1
POL(c(x1, x2)) = x1 + x2
POL(c1(x1)) = x1
POL(c1(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c2(x1)) = x1
POL(c9(x1)) = x1
POL(div2(x1)) = x1
POL(even(x1)) = [1] + [3]x1
POL(false) = 0
POL(neq(x1, x2)) = 0
POL(p(x1)) = x1
POL(s(x1)) = [1] + x1
POL(true) = 0

### (24) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0)))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

c9, c12, c2, c, c, c1, c1

### (25) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0))) by

COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, 0) → c2(COND1(false, p(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))

### (26) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, 0) → c2(COND1(false, p(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, 0) → c2(COND1(false, p(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c, c1, c1, c2

### (27) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

COND2(false, 0) → c2(COND1(false, p(0)))

### (28) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c, c1, c1, c2

### (29) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

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

COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND1(true, 0) → c(COND2(true, 0))

### (30) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(0, 0) → false
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c, c1, c1, c2

### (31) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

p(0) → 0

### (32) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c, c1, c1, c2

### (33) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
We considered the (Usable) Rules:

p(s(z0)) → z0
div2(0) → 0
div2(s(s(z0))) → s(div2(z0))
div2(s(0)) → 0
And the Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND1(x1, x2)) = [4]x2
POL(COND2(x1, x2)) = [4]x2
POL(DIV2(x1)) = 0
POL(EVEN(x1)) = 0
POL(c(x1)) = x1
POL(c(x1, x2)) = x1 + x2
POL(c1(x1)) = x1
POL(c1(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c2(x1)) = x1
POL(c9(x1)) = x1
POL(div2(x1)) = x1
POL(even(x1)) = 0
POL(false) = 0
POL(neq(x1, x2)) = 0
POL(p(x1)) = x1
POL(s(x1)) = [2] + x1
POL(true) = 0

### (34) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c, c1, c1, c2

### (35) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0)))) by

COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))

### (36) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c1, c1, c2, c

### (37) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
We considered the (Usable) Rules:none
And the Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [4]
POL(COND1(x1, x2)) = [2]
POL(COND2(x1, x2)) = [2]
POL(DIV2(x1)) = 0
POL(EVEN(x1)) = 0
POL(c(x1)) = x1
POL(c(x1, x2)) = x1 + x2
POL(c1(x1)) = x1
POL(c1(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c2(x1)) = x1
POL(c9(x1)) = x1
POL(div2(x1)) = x1
POL(even(x1)) = [3] + [4]x1
POL(false) = 0
POL(neq(x1, x2)) = [4]x2
POL(p(x1)) = [3]
POL(s(x1)) = [4]
POL(true) = [4]

### (38) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c1, c1, c2, c

### (39) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0)))) by

COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(0)))) → c1(COND1(neq(s(s(s(0))), 0), s(0)), DIV2(s(s(s(0)))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))

### (40) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(0)))) → c1(COND1(neq(s(s(s(0))), 0), s(0)), DIV2(s(s(s(0)))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c1, c1, c2, c

### (41) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

### (42) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(true, s(s(s(0)))) → c3(DIV2(s(s(s(0)))))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0))))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c1, c1, c2, c, c3

### (43) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

COND2(true, s(s(s(0)))) → c3(DIV2(s(s(s(0)))))

### (44) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c1, c1, c2, c, c3

### (45) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0))) by

COND2(true, s(0)) → c1(COND1(true, 0), DIV2(s(0)))
COND2(true, s(s(z0))) → c1(COND1(true, s(div2(z0))), DIV2(s(s(z0))))

### (46) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(true, s(0)) → c1(COND1(true, 0), DIV2(s(0)))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND2(true, s(0)) → c1(COND1(true, 0), DIV2(s(0)))
COND2(true, s(s(z0))) → c1(COND1(true, s(div2(z0))), DIV2(s(s(z0))))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c1, c2, c, c1, c3

### (47) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

COND2(true, s(0)) → c1(COND1(true, 0), DIV2(s(0)))

### (48) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND2(true, s(s(z0))) → c1(COND1(true, s(div2(z0))), DIV2(s(s(z0))))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c1, c2, c, c1, c3

### (49) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
We considered the (Usable) Rules:

p(s(z0)) → z0
div2(0) → 0
even(s(0)) → false
even(0) → true
even(s(s(z0))) → even(z0)
div2(s(s(z0))) → s(div2(z0))
div2(s(0)) → 0
And the Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND1(x1, x2)) = [4] + [4]x2
POL(COND2(x1, x2)) = [2]x1 + [4]x2
POL(DIV2(x1)) = 0
POL(EVEN(x1)) = 0
POL(c(x1)) = x1
POL(c(x1, x2)) = x1 + x2
POL(c1(x1)) = x1
POL(c1(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c2(x1)) = x1
POL(c3(x1)) = x1
POL(c9(x1)) = x1
POL(div2(x1)) = [3] + x1
POL(even(x1)) = [2]
POL(false) = [2]
POL(neq(x1, x2)) = 0
POL(p(x1)) = x1
POL(s(x1)) = [4] + x1
POL(true) = [2]

### (50) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c1, c2, c, c1, c3

### (51) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

DIV2(s(s(z0))) → c12(DIV2(z0))
We considered the (Usable) Rules:

p(s(z0)) → z0
div2(0) → 0
div2(s(s(z0))) → s(div2(z0))
div2(s(0)) → 0
And the Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND1(x1, x2)) = [2]x2 + [3]x22
POL(COND2(x1, x2)) = [2]x2 + [3]x22
POL(DIV2(x1)) = [2] + x1
POL(EVEN(x1)) = 0
POL(c(x1)) = x1
POL(c(x1, x2)) = x1 + x2
POL(c1(x1)) = x1
POL(c1(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c2(x1)) = x1
POL(c3(x1)) = x1
POL(c9(x1)) = x1
POL(div2(x1)) = [1] + x1
POL(even(x1)) = 0
POL(false) = 0
POL(neq(x1, x2)) = 0
POL(p(x1)) = x1
POL(s(x1)) = [2] + x1
POL(true) = 0

### (52) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c1, c2, c, c1, c3

### (53) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(true, 0) → c1(COND1(neq(0, 0), 0)) by

COND2(true, 0) → c1(COND1(false, 0))

### (54) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, 0) → c(COND2(true, 0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(true, 0) → c1(COND1(false, 0))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
K tuples:

COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c1, c2, c, c1, c3

### (55) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 4 trailing nodes:

COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND1(true, 0) → c(COND2(true, 0))
COND2(true, 0) → c1(COND1(false, 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))

### (56) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
neq(0, 0) → false
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → z0
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
K tuples:

COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))
Defined Rule Symbols:

even, neq, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c2, c, c1, c1, c3

### (57) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

neq(0, 0) → false

### (58) Obligation:

Complexity Dependency Tuples Problem
Rules:

neq(s(z0), 0) → true
p(s(z0)) → z0
even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
K tuples:

COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))
Defined Rule Symbols:

neq, p, even, div2

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c2, c, c1, c1, c3

### (59) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
We considered the (Usable) Rules:

p(s(z0)) → z0
div2(0) → 0
even(s(0)) → false
even(0) → true
even(s(s(z0))) → even(z0)
div2(s(s(z0))) → s(div2(z0))
div2(s(0)) → 0
And the Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND1(x1, x2)) = [2] + [4]x2
POL(COND2(x1, x2)) = [1] + x1 + [4]x2
POL(DIV2(x1)) = [2]
POL(EVEN(x1)) = 0
POL(c(x1)) = x1
POL(c(x1, x2)) = x1 + x2
POL(c1(x1)) = x1
POL(c1(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c2(x1)) = x1
POL(c3(x1)) = x1
POL(c9(x1)) = x1
POL(div2(x1)) = [3] + x1
POL(even(x1)) = [1]
POL(false) = [1]
POL(neq(x1, x2)) = [4] + [4]x1
POL(p(x1)) = x1
POL(s(x1)) = [4] + x1
POL(true) = 0

### (60) Obligation:

Complexity Dependency Tuples Problem
Rules:

neq(s(z0), 0) → true
p(s(z0)) → z0
even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
K tuples:

COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
Defined Rule Symbols:

neq, p, even, div2

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c2, c, c1, c1, c3

### (61) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) by

COND2(false, s(z0)) → c2(COND1(true, z0))

### (62) Obligation:

Complexity Dependency Tuples Problem
Rules:

neq(s(z0), 0) → true
p(s(z0)) → z0
even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(false, s(z0)) → c2(COND1(true, z0))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
K tuples:

COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
Defined Rule Symbols:

neq, p, even, div2

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c2, c, c1, c1, c3

### (63) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) by

COND2(false, s(z0)) → c2(COND1(true, z0))

### (64) Obligation:

Complexity Dependency Tuples Problem
Rules:

neq(s(z0), 0) → true
p(s(z0)) → z0
even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(false, s(z0)) → c2(COND1(true, z0))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND2(false, s(z0)) → c2(COND1(true, z0))
K tuples:

COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
Defined Rule Symbols:

neq, p, even, div2

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c, c1, c1, c3, c2

### (65) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

p(s(z0)) → z0

### (66) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(false, s(z0)) → c2(COND1(true, z0))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND2(false, s(z0)) → c2(COND1(true, z0))
K tuples:

COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
Defined Rule Symbols:

even, neq, div2

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c, c1, c1, c3, c2

### (67) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COND2(false, s(z0)) → c2(COND1(true, z0))
We considered the (Usable) Rules:

div2(0) → 0
even(s(0)) → false
even(0) → true
even(s(s(z0))) → even(z0)
div2(s(s(z0))) → s(div2(z0))
div2(s(0)) → 0
neq(s(z0), 0) → true
And the Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(false, s(z0)) → c2(COND1(true, z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND1(x1, x2)) = [4]x1 + [2]x2
POL(COND2(x1, x2)) = [4]x1 + [2]x2
POL(DIV2(x1)) = 0
POL(EVEN(x1)) = 0
POL(c(x1)) = x1
POL(c(x1, x2)) = x1 + x2
POL(c1(x1)) = x1
POL(c1(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c2(x1)) = x1
POL(c3(x1)) = x1
POL(c9(x1)) = x1
POL(div2(x1)) = [4] + x1
POL(even(x1)) = [2]
POL(false) = [2]
POL(neq(x1, x2)) = [2]
POL(s(x1)) = [4] + x1
POL(true) = [2]

### (68) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(false, s(z0)) → c2(COND1(true, z0))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
K tuples:

COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND2(false, s(z0)) → c2(COND1(true, z0))
Defined Rule Symbols:

even, neq, div2

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c, c1, c1, c3, c2

### (69) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
We considered the (Usable) Rules:

div2(0) → 0
div2(s(s(z0))) → s(div2(z0))
div2(s(0)) → 0
neq(s(z0), 0) → true
And the Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(false, s(z0)) → c2(COND1(true, z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [2]
POL(COND1(x1, x2)) = [2] + [2]x1 + [4]x2
POL(COND2(x1, x2)) = [4]x2
POL(DIV2(x1)) = [2]
POL(EVEN(x1)) = 0
POL(c(x1)) = x1
POL(c(x1, x2)) = x1 + x2
POL(c1(x1)) = x1
POL(c1(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c2(x1)) = x1
POL(c3(x1)) = x1
POL(c9(x1)) = x1
POL(div2(x1)) = x1
POL(even(x1)) = 0
POL(false) = 0
POL(neq(x1, x2)) = [1]
POL(s(x1)) = [2] + x1
POL(true) = [1]

### (70) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(false, s(z0)) → c2(COND1(true, z0))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
K tuples:

COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND2(false, s(z0)) → c2(COND1(true, z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
Defined Rule Symbols:

even, neq, div2

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c, c1, c1, c3, c2

### (71) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

EVEN(s(s(z0))) → c9(EVEN(z0))
We considered the (Usable) Rules:

div2(0) → 0
div2(s(s(z0))) → s(div2(z0))
div2(s(0)) → 0
And the Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(false, s(z0)) → c2(COND1(true, z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND1(x1, x2)) = [2]x2 + x22
POL(COND2(x1, x2)) = [1] + x22
POL(DIV2(x1)) = 0
POL(EVEN(x1)) = x1
POL(c(x1)) = x1
POL(c(x1, x2)) = x1 + x2
POL(c1(x1)) = x1
POL(c1(x1, x2)) = x1 + x2
POL(c12(x1)) = x1
POL(c2(x1)) = x1
POL(c3(x1)) = x1
POL(c9(x1)) = x1
POL(div2(x1)) = x1
POL(even(x1)) = 0
POL(false) = 0
POL(neq(x1, x2)) = 0
POL(s(x1)) = [2] + x1
POL(true) = 0

### (72) Obligation:

Complexity Dependency Tuples Problem
Rules:

even(0) → true
even(s(0)) → false
even(s(s(z0))) → even(z0)
neq(s(z0), 0) → true
div2(0) → 0
div2(s(0)) → 0
div2(s(s(z0))) → s(div2(z0))
Tuples:

EVEN(s(s(z0))) → c9(EVEN(z0))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0))))
COND2(true, s(s(s(s(z0))))) → c1(COND1(neq(s(s(s(s(z0)))), 0), s(s(div2(z0)))), DIV2(s(s(s(s(z0))))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0)))
COND2(false, s(z0)) → c2(COND1(true, z0))
S tuples:none
K tuples:

COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0))
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
DIV2(s(s(z0))) → c12(DIV2(z0))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
COND2(false, s(z0)) → c2(COND1(true, z0))
COND1(true, s(0)) → c(COND2(false, s(0)))
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0)))))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
EVEN(s(s(z0))) → c9(EVEN(z0))
Defined Rule Symbols:

even, neq, div2

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

c9, c12, c, c, c1, c1, c3, c2

### (73) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty