YES(O(1), O(n^2)) 225.14/75.36 YES(O(1), O(n^2)) 225.14/75.38 225.14/75.38 225.14/75.38 225.14/75.38 225.14/75.38 225.14/75.38 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 225.14/75.38 225.14/75.38 225.14/75.38
225.14/75.38
225.14/75.38
225.14/75.38
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^2)).

0 CpxTRS
225.14/75.38 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳2 CdtProblem
225.14/75.38 
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳4 CdtProblem
225.14/75.38 
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳6 CdtProblem
225.14/75.38 
↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳8 CdtProblem
225.14/75.38 
↳9 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳10 CdtProblem
225.14/75.38 
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
225.14/75.38 
↳12 CdtProblem
225.14/75.38 
↳13 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳14 CdtProblem
225.14/75.38 
↳15 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳16 CdtProblem
225.14/75.38 
↳17 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳18 CdtProblem
225.14/75.38 
↳19 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳20 CdtProblem
225.14/75.38 
↳21 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
225.14/75.38 
↳22 CdtProblem
225.14/75.38 
↳23 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳24 CdtProblem
225.14/75.38 
↳25 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳26 CdtProblem
225.14/75.38 
↳27 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳28 CdtProblem
225.14/75.38 
↳29 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳30 CdtProblem
225.14/75.38 
↳31 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
225.14/75.38 
↳32 CdtProblem
225.14/75.38 
↳33 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳34 CdtProblem
225.14/75.38 
↳35 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳36 CdtProblem
225.14/75.38 
↳37 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
225.14/75.38 
↳38 CdtProblem
225.14/75.38 
↳39 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳40 CdtProblem
225.14/75.38 
↳41 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳42 CdtProblem
225.14/75.38 
↳43 CdtLeafRemovalProof (ComplexityIfPolyImplication)
225.14/75.38 
↳44 CdtProblem
225.14/75.38 
↳45 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳46 CdtProblem
225.14/75.38 
↳47 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳48 CdtProblem
225.14/75.38 
↳49 CdtLeafRemovalProof (ComplexityIfPolyImplication)
225.14/75.38 
↳50 CdtProblem
225.14/75.38 
↳51 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
225.14/75.38 
↳52 CdtProblem
225.14/75.38 
↳53 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
225.14/75.38 
↳54 CdtProblem
225.14/75.38 
↳55 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳56 CdtProblem
225.14/75.38 
↳57 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳58 CdtProblem
225.14/75.38 
↳59 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳60 CdtProblem
225.14/75.38 
↳61 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
225.14/75.38 
↳62 CdtProblem
225.14/75.38 
↳63 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳64 CdtProblem
225.14/75.38 
↳65 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳66 CdtProblem
225.14/75.38 
↳67 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳68 CdtProblem
225.14/75.38 
↳69 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
225.14/75.38 
↳70 CdtProblem
225.14/75.38 
↳71 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
225.14/75.39 
↳72 CdtProblem
225.14/75.39 
↳73 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
225.14/75.39 
↳74 CdtProblem
225.14/75.39 
↳75 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
225.14/75.39 
↳76 CdtProblem
225.14/75.39 
↳77 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
225.14/75.39 
↳78 CdtProblem
225.14/75.39 
↳79 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
225.14/75.39 
↳80 CdtProblem
225.14/75.39 
↳81 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
225.14/75.39 
↳82 CdtProblem
225.14/75.39 
↳83 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
225.14/75.39 
↳84 CdtProblem
225.14/75.39 
↳85 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
225.14/75.39 
↳86 CdtProblem
225.14/75.39 
↳87 SIsEmptyProof (BOTH BOUNDS(ID, ID))
225.14/75.39 
↳88 BOUNDS(O(1), O(1))
225.14/75.39
225.14/75.39 225.14/75.39
225.14/75.39
225.14/75.39

(0) Obligation:

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

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

Rewrite Strategy: INNERMOST
225.14/75.39
225.14/75.39

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

Converted CpxTRS to CDT
225.14/75.39
225.14/75.39

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

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

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

COND1, COND2, NEQ, EVEN, DIV2

Compound Symbols:

c, c1, c2, c6, c9, c12

225.14/75.39
225.14/75.39

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

Removed 4 trailing tuple parts
225.14/75.39
225.14/75.39

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

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

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

COND1, EVEN, DIV2, COND2, NEQ

Compound Symbols:

c, c9, c12, c1, c2, c6

225.14/75.39
225.14/75.39

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

Removed 1 trailing nodes:

NEQ(s(z0), s(y)) → c6
225.14/75.39
225.14/75.39

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

COND1(true, z0) → c(COND2(even(z0), z0), EVEN(z0)) 225.14/75.39
EVEN(s(s(z0))) → c9(EVEN(z0)) 225.14/75.39
DIV2(s(s(z0))) → c12(DIV2(z0)) 225.14/75.39
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0)) 225.14/75.39
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

225.14/75.39
225.14/75.39

(7) 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)) 225.14/75.39
COND1(true, s(0)) → c(COND2(false, s(0)), EVEN(s(0))) 225.14/75.39
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
225.14/75.39
225.14/75.39

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 225.14/75.39
DIV2(s(s(z0))) → c12(DIV2(z0)) 225.14/75.39
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0)) 225.14/75.39
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0))) 225.14/75.39
COND1(true, 0) → c(COND2(true, 0), EVEN(0)) 225.14/75.39
COND1(true, s(0)) → c(COND2(false, s(0)), EVEN(s(0))) 225.14/75.39
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)) 225.14/75.39
DIV2(s(s(z0))) → c12(DIV2(z0)) 225.14/75.39
COND2(true, z0) → c1(COND1(neq(z0, 0), div2(z0)), DIV2(z0)) 225.14/75.39
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0))) 225.14/75.39
COND1(true, 0) → c(COND2(true, 0), EVEN(0)) 225.14/75.39
COND1(true, s(0)) → c(COND2(false, s(0)), EVEN(s(0))) 225.14/75.39
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0))))
K tuples:none
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

c9, c12, c1, c2, c

225.14/75.39
225.14/75.39

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

Removed 2 trailing tuple parts
225.14/75.39
225.14/75.39

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

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

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

c9, c12, c1, c2, c, c

225.14/75.39
225.14/75.39

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

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

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

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

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

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

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

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

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

c9, c12, c1, c2, c, c

226.00/75.40
226.00/75.40

(13) 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)) 226.00/75.40
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0), DIV2(s(0))) 226.00/75.40
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0)))) 226.00/75.40
COND2(true, 0) → c1(COND1(false, div2(0)), DIV2(0)) 226.00/75.40
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0)))
226.00/75.40
226.00/75.40

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.00/75.47
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.00/75.47
COND2(false, z0) → c2(COND1(neq(z0, 0), p(z0))) 226.00/75.47
COND1(true, s(s(z0))) → c(COND2(even(z0), s(s(z0))), EVEN(s(s(z0)))) 226.00/75.47
COND1(true, s(0)) → c(COND2(false, s(0))) 226.00/75.47
COND2(true, 0) → c1(COND1(neq(0, 0), 0), DIV2(0)) 226.00/75.47
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0), DIV2(s(0))) 226.00/75.47
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0)))) 226.00/75.47
COND2(true, 0) → c1(COND1(false, div2(0)), DIV2(0)) 226.00/75.47
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:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

c9, c12, c2, c, c, c1

226.00/75.47
226.00/75.47

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

Removed 4 trailing tuple parts
226.00/75.47
226.00/75.47

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

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

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

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

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

226.00/75.47
226.00/75.47

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

Removed 1 trailing nodes:

COND2(true, 0) → c1
226.00/75.47
226.00/75.47

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

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

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

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

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

226.00/75.47
226.00/75.47

(19) 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)) 226.00/75.47
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.00/75.47
COND2(true, 0) → c1 226.00/75.47
COND1(true, 0) → c(COND2(true, 0)) 226.00/75.47
COND1(true, 0) → c(COND2(true, 0))
226.00/75.47
226.00/75.47

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

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

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

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

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

226.00/75.47
226.00/75.47

(21) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

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

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

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

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

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

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

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

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND2, COND1

Compound Symbols:

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

226.00/75.47
226.00/75.47

(23) 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)) 226.00/75.47
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.00/75.47
COND2(false, 0) → c2(COND1(false, p(0))) 226.00/75.47
COND2(false, s(z0)) → c2(COND1(true, p(s(z0))))
226.00/75.47
226.00/75.47

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

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

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

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.00/75.47
226.00/75.47

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

Removed 1 trailing tuple parts
226.00/75.47
226.00/75.47

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

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

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

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.00/75.47
226.00/75.47

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

Removed 2 trailing nodes:

COND2(false, 0) → c2 226.36/75.51
COND2(true, 0) → c1
226.36/75.51
226.36/75.51

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

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

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

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.51
226.36/75.51

(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)) 226.36/75.51
COND1(true, 0) → c(COND2(true, 0))
226.36/75.51
226.36/75.51

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

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

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

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.51
226.36/75.51

(31) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

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

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

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

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

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

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

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

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.51
226.36/75.51

(33) 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)))) 226.36/75.51
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.51
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.51
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
226.36/75.51
226.36/75.51

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

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

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

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.51
226.36/75.51

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

Removed 1 trailing nodes:

COND2(true, 0) → c1
226.36/75.51
226.36/75.51

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

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

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

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.51
226.36/75.51

(37) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

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

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

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

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

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.51
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.51
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.51
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0))) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.51
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.51
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.51
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)) 226.36/75.51
COND2(true, 0) → c1(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.51
COND2(true, 0) → c1 226.36/75.51
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0)))) 226.36/75.51
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.51
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.51
226.36/75.51

(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)))) 226.36/75.51
COND2(true, s(s(s(0)))) → c1(COND1(neq(s(s(s(0))), 0), s(0)), DIV2(s(s(s(0))))) 226.36/75.51
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)))))) 226.36/75.51
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.51
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
226.36/75.51
226.36/75.51

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.51
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.51
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.51
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.51
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0))) 226.36/75.51
COND2(true, 0) → c1(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.51
COND2(true, 0) → c1 226.36/75.51
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.51
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.51
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.51
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.51
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.51
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.51
COND2(true, s(s(s(0)))) → c1(COND1(neq(s(s(s(0))), 0), s(0)), DIV2(s(s(s(0))))) 226.36/75.51
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)))))) 226.36/75.51
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.51
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0))))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.51
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.51
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.51
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0))) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.51
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.51
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.51
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)) 226.36/75.51
COND2(true, 0) → c1(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.51
COND2(true, 0) → c1 226.36/75.51
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0)))) 226.36/75.51
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.51
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.51
226.36/75.51

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

Split RHS of tuples not part of any SCC
226.36/75.51
226.36/75.51

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.51
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.51
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.51
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.51
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0))) 226.36/75.51
COND2(true, 0) → c1(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.51
COND2(true, 0) → c1 226.36/75.51
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.51
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.51
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.51
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.51
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.51
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.51
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)))))) 226.36/75.51
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.51
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.51
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0))) 226.36/75.51
COND2(true, s(s(s(0)))) → c3(DIV2(s(s(s(0)))))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.51
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.51
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.51
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0))) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.51
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.51
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.51
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)) 226.36/75.51
COND2(true, 0) → c1(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.51
COND2(true, 0) → c1 226.36/75.51
COND2(true, s(s(z0))) → c1(COND1(neq(s(s(z0)), 0), s(div2(z0))), DIV2(s(s(z0)))) 226.36/75.51
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.51
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.51
226.36/75.51

(43) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

COND2(true, s(s(s(0)))) → c3(DIV2(s(s(s(0)))))
Removed 1 trailing nodes:

COND2(true, 0) → c1
226.36/75.51
226.36/75.51

(44) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.51
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.51
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.51
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.51
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0))) 226.36/75.51
COND2(true, 0) → c1(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.51
COND2(true, 0) → c1 226.36/75.51
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.51
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.51
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.51
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.51
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.51
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.51
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)))))) 226.36/75.51
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.51
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.51
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)) 226.36/75.51
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.51
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.51
COND2(true, s(z0)) → c1(COND1(true, div2(s(z0))), DIV2(s(z0))) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.51
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.51
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.51
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)) 226.36/75.51
COND2(true, 0) → c1(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.51
COND2(true, 0) → c1 226.36/75.51
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.51
COND1(true, s(s(x0))) → c(EVEN(s(s(x0))))
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.51
226.36/75.51

(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))) 226.36/75.51
COND2(true, s(s(z0))) → c1(COND1(true, s(div2(z0))), DIV2(s(s(z0))))
226.36/75.51
226.36/75.51

(46) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.51
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.51
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.51
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.51
COND2(true, 0) → c1(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.51
COND2(true, 0) → c1 226.36/75.51
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.51
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.51
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.51
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.51
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.51
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.51
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)))))) 226.36/75.51
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.51
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.51
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0))) 226.36/75.51
COND2(true, s(0)) → c1(COND1(true, 0), DIV2(s(0)))
S tuples:

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

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

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.51
226.36/75.51

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

Removed 1 trailing tuple parts
226.36/75.51
226.36/75.51

(48) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.51
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.51
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.51
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.51
COND2(true, 0) → c1(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.51
COND2(true, 0) → c1 226.36/75.51
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.51
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.51
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.51
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.51
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.51
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.51
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)))))) 226.36/75.51
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.51
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.51
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0))) 226.36/75.51
COND2(true, s(0)) → c1(COND1(true, 0))
S tuples:

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

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

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.51
226.36/75.51

(49) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

COND2(true, s(0)) → c1(COND1(true, 0))
Removed 1 trailing nodes:

COND2(true, 0) → c1
226.36/75.51
226.36/75.51

(50) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.51
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.51
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.51
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.51
COND2(true, 0) → c1(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.51
COND2(true, 0) → c1 226.36/75.51
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.51
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.51
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.51
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.51
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.51
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.51
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)))))) 226.36/75.51
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.51
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.51
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)) 226.36/75.51
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.51
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.51
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.51
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.51
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.51
COND2(true, s(s(z0))) → c1(COND1(true, s(div2(z0))), DIV2(s(s(z0))))
K tuples:

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

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.51
226.36/75.51

(51) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

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

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.51
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.51
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.51
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.51
COND2(true, 0) → c1(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.51
COND2(true, 0) → c1 226.36/75.51
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.51
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.51
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.51
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.51
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.51
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.51
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)))))) 226.36/75.51
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.51
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.51
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 : 226.36/75.51

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

(52) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.51
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.51
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.51
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.51
COND2(true, 0) → c1(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.51
COND2(true, 0) → c1 226.36/75.51
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.51
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.51
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.51
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.51
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.51
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.51
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)))))) 226.36/75.51
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.51
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.51
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)) 226.36/75.51
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.51
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.51
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.51
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.51
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)) 226.36/75.51
COND2(true, 0) → c1(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.51
COND2(true, 0) → c1 226.36/75.51
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.51
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.51
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0))))
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.51
226.36/75.51

(53) CdtPolyRedPairProof (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:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.51
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.51
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.51
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.51
COND2(true, 0) → c1(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.51
COND2(true, 0) → c1 226.36/75.51
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.51
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.51
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.51
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.51
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.51
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.51
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)))))) 226.36/75.51
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.51
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.51
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 : 226.36/75.51

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

(54) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.51
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.51
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.51
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.51
COND2(true, 0) → c1(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.51
COND2(true, 0) → c1 226.36/75.51
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.51
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.51
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.51
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.51
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.52
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.52
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.52
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)))))) 226.36/75.52
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.52
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.52
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)) 226.36/75.52
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.52
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.52
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.52
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.52
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)) 226.36/75.52
COND2(true, 0) → c1(COND1(neq(0, 0), 0)) 226.36/75.52
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.52
COND2(true, 0) → c1 226.36/75.52
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.52
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.52
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.52
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.52
DIV2(s(s(z0))) → c12(DIV2(z0))
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.52
226.36/75.52

(55) 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))
226.36/75.52
226.36/75.52

(56) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.52
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.52
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.52
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.52
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.52
COND2(true, 0) → c1 226.36/75.52
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.52
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.52
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.52
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.52
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.52
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.52
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.52
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.52
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)))))) 226.36/75.52
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.52
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.52
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0))) 226.36/75.52
COND2(true, 0) → c1(COND1(false, 0))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.52
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.52
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.52
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.52
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.52
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)) 226.36/75.52
COND2(true, 0) → c1(COND1(neq(0, 0), 0)) 226.36/75.52
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.52
COND2(true, 0) → c1 226.36/75.52
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.52
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.52
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.52
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.52
DIV2(s(s(z0))) → c12(DIV2(z0))
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.52
226.36/75.52

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

Removed 1 trailing tuple parts
226.36/75.52
226.36/75.52

(58) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.52
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.52
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.52
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.52
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.52
COND2(true, 0) → c1 226.36/75.52
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.52
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.53
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)))))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.53
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)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
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)) 226.36/75.53
COND2(true, 0) → c1(COND1(neq(0, 0), 0)) 226.36/75.53
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0))
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.53
226.36/75.53

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

Removed 4 trailing nodes:

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

(60) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.53
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)))))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.53
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)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
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)) 226.36/75.53
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0))
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.53
226.36/75.53

(61) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

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

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.53
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)))))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.53
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 : 226.36/75.53

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

(62) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.53
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)))))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.53
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)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
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)) 226.36/75.53
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.53
226.36/75.53

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

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

COND2(true, s(0)) → c1(COND1(true, 0))
226.36/75.53
226.36/75.53

(64) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.53
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)))))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0))) 226.36/75.53
COND2(true, s(0)) → c1(COND1(true, 0))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
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)) 226.36/75.53
COND2(true, s(0)) → c1(COND1(neq(s(0), 0), 0)) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.53
226.36/75.53

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

Removed 4 trailing nodes:

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

(66) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.53
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)))))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.53
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)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
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)) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.53
226.36/75.53

(67) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

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

COND2(false, 0) → c2(COND1(false, 0))
226.36/75.53
226.36/75.53

(68) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.53
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)))))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0))) 226.36/75.53
COND2(false, 0) → c2(COND1(false, 0))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
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)) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.53
226.36/75.53

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

Removed 1 trailing tuple parts
226.36/75.53
226.36/75.53

(70) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.53
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)))))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0))) 226.36/75.53
COND2(false, 0) → c2
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
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)) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND2(false, 0) → c2(COND1(neq(0, 0), 0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.53
226.36/75.53

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

Removed 3 trailing nodes:

COND2(false, 0) → c2 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND1(true, 0) → c(COND2(true, 0))
226.36/75.53
226.36/75.53

(72) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.53
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)))))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.53
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)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
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)) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.53
226.36/75.53

(73) 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))
226.36/75.53
226.36/75.53

(74) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.53
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)))))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0))) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, z0))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
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)) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND2(false, s(z0)) → c2(COND1(neq(s(z0), 0), z0)) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.53
226.36/75.53

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

Removed 2 trailing nodes:

COND2(true, 0) → c1 226.36/75.53
COND1(true, 0) → c(COND2(true, 0))
226.36/75.53
226.36/75.53

(76) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.53
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)))))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0))) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, z0))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, p(s(z0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
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)) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.53
226.36/75.53

(77) 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))
226.36/75.53
226.36/75.53

(78) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.53
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)))))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0))) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, z0))
S tuples:

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

COND1(true, 0) → c(COND2(true, 0)) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.53
226.36/75.53

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

Removed 2 trailing nodes:

COND2(true, 0) → c1 226.36/75.53
COND1(true, 0) → c(COND2(true, 0))
226.36/75.53
226.36/75.53

(80) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.53
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)))))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0))) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, z0))
S tuples:

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

COND1(true, 0) → c(COND2(true, 0)) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0))))
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.53
226.36/75.53

(81) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, z0))
We considered the (Usable) Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.53
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.53
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.53
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.53
COND2(true, 0) → c1 226.36/75.53
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.53
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.53
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.53
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.53
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.53
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)))))) 226.36/75.53
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.53
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0))) 226.36/75.53
COND2(false, s(z0)) → c2(COND1(true, z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 226.36/75.53

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

(82) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.54
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.54
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.54
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.54
COND2(true, 0) → c1 226.36/75.54
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.54
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.54
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.54
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.54
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.54
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)))))) 226.36/75.54
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.54
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.54
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0))) 226.36/75.54
COND2(false, s(z0)) → c2(COND1(true, z0))
S tuples:

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.54
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)) 226.36/75.54
COND2(true, 0) → c1 226.36/75.54
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.54
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.54
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.54
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.54
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.54
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.54
COND2(false, s(z0)) → c2(COND1(true, z0))
Defined Rule Symbols:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.54
226.36/75.54

(83) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

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:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.54
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.54
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.54
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.54
COND2(true, 0) → c1 226.36/75.54
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.54
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.54
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.54
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.54
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.54
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)))))) 226.36/75.54
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.54
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.54
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0))) 226.36/75.54
COND2(false, s(z0)) → c2(COND1(true, z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 226.36/75.54

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

(84) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.54
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.54
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.54
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.54
COND2(true, 0) → c1 226.36/75.54
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.54
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.54
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.54
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.54
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.54
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)))))) 226.36/75.54
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.54
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.54
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0))) 226.36/75.54
COND2(false, s(z0)) → c2(COND1(true, z0))
S tuples:

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

COND1(true, 0) → c(COND2(true, 0)) 226.36/75.54
COND2(true, 0) → c1 226.36/75.54
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.54
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.54
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.54
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.54
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.54
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.54
COND2(false, s(z0)) → c2(COND1(true, z0)) 226.36/75.54
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:

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.54
226.36/75.54

(85) CdtPolyRedPairProof (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:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.54
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.54
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.54
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.54
COND2(true, 0) → c1 226.36/75.54
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.54
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.54
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.54
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.54
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.54
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)))))) 226.36/75.54
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.54
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.54
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0))) 226.36/75.54
COND2(false, s(z0)) → c2(COND1(true, z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 226.36/75.54

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

(86) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

EVEN(s(s(z0))) → c9(EVEN(z0)) 226.36/75.54
DIV2(s(s(z0))) → c12(DIV2(z0)) 226.36/75.54
COND1(true, 0) → c(COND2(true, 0)) 226.36/75.54
COND1(true, s(0)) → c(COND2(false, s(0))) 226.36/75.54
COND2(true, 0) → c1 226.36/75.54
COND1(true, s(s(0))) → c(COND2(true, s(s(0))), EVEN(s(s(0)))) 226.36/75.54
COND1(true, s(s(s(0)))) → c(COND2(false, s(s(s(0)))), EVEN(s(s(s(0))))) 226.36/75.54
COND1(true, s(s(s(s(z0))))) → c(COND2(even(z0), s(s(s(s(z0))))), EVEN(s(s(s(s(z0)))))) 226.36/75.54
COND1(true, s(s(x0))) → c(EVEN(s(s(x0)))) 226.36/75.54
COND2(true, s(s(0))) → c1(COND1(neq(s(s(0)), 0), s(0)), DIV2(s(s(0)))) 226.36/75.54
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)))))) 226.36/75.54
COND2(true, s(s(x0))) → c1(COND1(true, s(div2(x0))), DIV2(s(s(x0)))) 226.36/75.54
COND2(true, s(s(x0))) → c1(DIV2(s(s(x0)))) 226.36/75.54
COND2(true, s(s(s(0)))) → c3(COND1(neq(s(s(s(0))), 0), s(0))) 226.36/75.54
COND2(false, s(z0)) → c2(COND1(true, z0))
S tuples:none
K tuples:

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

cond1, cond2, neq, even, div2, p

Defined Pair Symbols:

EVEN, DIV2, COND1, COND2

Compound Symbols:

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

226.36/75.54
226.36/75.54

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

The set S is empty
226.36/75.54
226.36/75.54

(88) BOUNDS(O(1), O(1))

226.36/75.54
226.36/75.54
226.72/75.66 EOF