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