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

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

(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(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(s(z0), 0) → true
neq(0, 0) → false
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(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:

div2(0) → 0
div2(s(s(z0))) → s(div2(z0))
p(0) → 0
p(s(z0)) → z0
div2(s(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(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:

div2(0) → 0
div2(s(s(z0))) → s(div2(z0))
p(s(z0)) → 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(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)

Removed 1 leading nodes:

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)

Removed 1 leading nodes:

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

div2(0) → 0
div2(s(s(z0))) → s(div2(z0))
even(0) → true
p(s(z0)) → z0
even(s(0)) → false
div2(s(0)) → 0
even(s(s(z0))) → even(z0)
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) 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))

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

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

Removed 4 trailing nodes:

COND2(true, 0) → c1(COND1(false, 0))
COND2(false, 0) → c2(COND1(neq(0, 0), 0))
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0))
COND1(true, 0) → c(COND2(true, 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, 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))
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:

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, c2, c, c1, c1, c3

(55) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

neq(0, 0) → false

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

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:

neq, p, even, div2

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

(57) CdtRuleRemovalProof (UPPER BOUND(ADD(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:

div2(0) → 0
neq(s(z0), 0) → true
div2(s(s(z0))) → s(div2(z0))
even(0) → true
p(s(z0)) → z0
even(s(0)) → false
div2(s(0)) → 0
even(s(s(z0))) → even(z0)
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)) = [4] + [4]x1 + [2]x2   
POL(COND2(x1, x2)) = [4]x1 + [2]x2   
POL(DIV2(x1)) = [4]   
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)) = [4]   
POL(false) = [4]   
POL(neq(x1, x2)) = [3] + [5]x2   
POL(p(x1)) = x1   
POL(s(x1)) = [4] + x1   
POL(true) = [3]   

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

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

(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(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))
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(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))))
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(true, p(s(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)))
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))
DIV2(s(s(z0))) → c12(DIV2(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))))
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

(63) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

p(s(z0)) → z0

(64) 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))
DIV2(s(s(z0))) → c12(DIV2(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))))
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

(65) CdtRuleRemovalProof (UPPER BOUND(ADD(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)))))
We considered the (Usable) Rules:

div2(0) → 0
neq(s(z0), 0) → true
div2(s(s(z0))) → s(div2(z0))
even(0) → true
even(s(0)) → false
div2(s(0)) → 0
even(s(s(z0))) → even(z0)
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]x1 + x2   
POL(COND2(x1, x2)) = x1 + x2   
POL(DIV2(x1)) = 0   
POL(EVEN(x1)) = [1]   
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)) = [1]   
POL(false) = 0   
POL(neq(x1, x2)) = [1] + [2]x2   
POL(s(x1)) = [2] + x1   
POL(true) = [1]   

(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))
DIV2(s(s(z0))) → c12(DIV2(z0))
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))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
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)))))
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(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
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)) = x2   
POL(COND2(x1, x2)) = 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)) = [1] + x1   
POL(even(x1)) = [2]   
POL(false) = 0   
POL(neq(x1, x2)) = [3] + x2   
POL(s(x1)) = [1] + x1   
POL(true) = 0   

(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))
DIV2(s(s(z0))) → c12(DIV2(z0))
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))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
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)))))
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(n^1)) transformation)

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

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
neq(s(z0), 0) → true
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)) = [1] + x1 + x2   
POL(COND2(x1, x2)) = [1] + 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)) = x1   
POL(even(x1)) = 0   
POL(false) = [1]   
POL(neq(x1, x2)) = [1]   
POL(s(x1)) = [1] + 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))
DIV2(s(s(z0))) → c12(DIV2(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))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
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)))))
COND2(false, s(z0)) → c2(COND1(true, z0))
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(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:

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)) = [3] + [2]x22   
POL(COND2(x1, x2)) = [2] + [2]x22   
POL(DIV2(x1)) = [3] + x1   
POL(EVEN(x1)) = [1]   
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:

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))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
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)))))
COND2(false, s(z0)) → c2(COND1(true, z0))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
DIV2(s(s(z0))) → c12(DIV2(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) CdtRuleRemovalProof (UPPER BOUND(ADD(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   

(74) 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))))
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
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)))))
COND2(false, s(z0)) → c2(COND1(true, z0))
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0))))))
DIV2(s(s(z0))) → c12(DIV2(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

(75) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(76) BOUNDS(1, 1)