313.24/124.76
313.24/124.76
(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
cond(true, x) → cond(odd(x), p(p(p(x))))
313.24/124.76
odd(0) → false
313.24/124.76
odd(s(0)) → true
313.24/124.76
odd(s(s(x))) → odd(x)
313.24/124.76
p(0) → 0
313.24/124.76
p(s(x)) → x
Rewrite Strategy: INNERMOST
313.24/124.76
313.24/124.76
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
313.24/124.76
313.24/124.76
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
313.24/124.76
odd(0) → false
313.24/124.76
odd(s(0)) → true
313.24/124.76
odd(s(s(z0))) → odd(z0)
313.24/124.76
p(0) → 0
313.24/124.76
p(s(z0)) → z0
Tuples:
COND(true, z0) → c(COND(odd(z0), p(p(p(z0)))), ODD(z0), P(p(p(z0))), P(p(z0)), P(z0))
313.24/124.76
ODD(s(s(z0))) → c3(ODD(z0))
S tuples:
COND(true, z0) → c(COND(odd(z0), p(p(p(z0)))), ODD(z0), P(p(p(z0))), P(p(z0)), P(z0))
313.62/124.82
ODD(s(s(z0))) → c3(ODD(z0))
K tuples:none
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c3
313.62/124.82
313.62/124.82
(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 3 trailing tuple parts
313.62/124.82
313.62/124.82
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
313.62/124.82
odd(0) → false
313.62/124.82
odd(s(0)) → true
313.62/124.82
odd(s(s(z0))) → odd(z0)
313.62/124.82
p(0) → 0
313.62/124.82
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.82
COND(true, z0) → c(COND(odd(z0), p(p(p(z0)))), ODD(z0))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.82
COND(true, z0) → c(COND(odd(z0), p(p(p(z0)))), ODD(z0))
K tuples:none
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c
313.62/124.82
313.62/124.82
(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
COND(
true,
z0) →
c(
COND(
odd(
z0),
p(
p(
p(
z0)))),
ODD(
z0)) by
COND(true, 0) → c(COND(odd(0), p(p(0))), ODD(0))
313.62/124.82
COND(true, s(z0)) → c(COND(odd(s(z0)), p(p(z0))), ODD(s(z0)))
313.62/124.82
COND(true, 0) → c(COND(false, p(p(p(0)))), ODD(0))
313.62/124.82
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))), ODD(s(0)))
313.62/124.82
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(p(s(s(z0)))))), ODD(s(s(z0))))
313.62/124.82
313.62/124.82
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
313.62/124.82
odd(0) → false
313.62/124.82
odd(s(0)) → true
313.62/124.82
odd(s(s(z0))) → odd(z0)
313.62/124.88
p(0) → 0
313.62/124.88
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))), ODD(0))
313.62/124.88
COND(true, s(z0)) → c(COND(odd(s(z0)), p(p(z0))), ODD(s(z0)))
313.62/124.88
COND(true, 0) → c(COND(false, p(p(p(0)))), ODD(0))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))), ODD(s(0)))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(p(s(s(z0)))))), ODD(s(s(z0))))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))), ODD(0))
313.62/124.88
COND(true, s(z0)) → c(COND(odd(s(z0)), p(p(z0))), ODD(s(z0)))
313.62/124.88
COND(true, 0) → c(COND(false, p(p(p(0)))), ODD(0))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))), ODD(s(0)))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(p(s(s(z0)))))), ODD(s(s(z0))))
K tuples:none
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c
313.62/124.88
313.62/124.88
(7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing tuple parts
313.62/124.88
313.62/124.88
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
313.62/124.88
odd(0) → false
313.62/124.88
odd(s(0)) → true
313.62/124.88
odd(s(s(z0))) → odd(z0)
313.62/124.88
p(0) → 0
313.62/124.88
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, s(z0)) → c(COND(odd(s(z0)), p(p(z0))), ODD(s(z0)))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(p(s(s(z0)))))), ODD(s(s(z0))))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, 0) → c
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, s(z0)) → c(COND(odd(s(z0)), p(p(z0))), ODD(s(z0)))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(p(s(s(z0)))))), ODD(s(s(z0))))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, 0) → c
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
K tuples:none
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
313.62/124.88
313.62/124.88
(9) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
COND(true, 0) → c
313.62/124.88
313.62/124.88
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
313.62/124.88
odd(0) → false
313.62/124.88
odd(s(0)) → true
313.62/124.88
odd(s(s(z0))) → odd(z0)
313.62/124.88
p(0) → 0
313.62/124.88
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, s(z0)) → c(COND(odd(s(z0)), p(p(z0))), ODD(s(z0)))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(p(s(s(z0)))))), ODD(s(s(z0))))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, 0) → c
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, s(z0)) → c(COND(odd(s(z0)), p(p(z0))), ODD(s(z0)))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(p(s(s(z0)))))), ODD(s(s(z0))))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, 0) → c
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
K tuples:none
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
313.62/124.88
313.62/124.88
(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.
COND(true, 0) → c
We considered the (Usable) Rules:
p(s(z0)) → z0
313.62/124.88
p(0) → 0
313.62/124.88
odd(0) → false
313.62/124.88
odd(s(0)) → true
313.62/124.88
odd(s(s(z0))) → odd(z0)
And the Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, s(z0)) → c(COND(odd(s(z0)), p(p(z0))), ODD(s(z0)))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(p(s(s(z0)))))), ODD(s(s(z0))))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, 0) → c
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
The order we found is given by the following interpretation:
Polynomial interpretation :
313.62/124.88
POL(0) = [2]
313.62/124.88
POL(COND(x1, x2)) = [1]
313.62/124.88
POL(ODD(x1)) = 0
313.62/124.88
POL(c) = 0
313.62/124.88
POL(c(x1)) = x1
313.62/124.88
POL(c(x1, x2)) = x1 + x2
313.62/124.88
POL(c3(x1)) = x1
313.62/124.88
POL(false) = [5]
313.62/124.88
POL(odd(x1)) = [2] + [4]x1
313.62/124.88
POL(p(x1)) = 0
313.62/124.88
POL(s(x1)) = 0
313.62/124.88
POL(true) = 0
313.62/124.88
313.62/124.88
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
313.62/124.88
odd(0) → false
313.62/124.88
odd(s(0)) → true
313.62/124.88
odd(s(s(z0))) → odd(z0)
313.62/124.88
p(0) → 0
313.62/124.88
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, s(z0)) → c(COND(odd(s(z0)), p(p(z0))), ODD(s(z0)))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(p(s(s(z0)))))), ODD(s(s(z0))))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, 0) → c
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, s(z0)) → c(COND(odd(s(z0)), p(p(z0))), ODD(s(z0)))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(p(s(s(z0)))))), ODD(s(s(z0))))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
K tuples:
COND(true, 0) → c
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
313.62/124.88
313.62/124.88
(13) 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.
COND(true, s(z0)) → c(COND(odd(s(z0)), p(p(z0))), ODD(s(z0)))
We considered the (Usable) Rules:
p(s(z0)) → z0
313.62/124.88
p(0) → 0
313.62/124.88
odd(0) → false
313.62/124.88
odd(s(0)) → true
313.62/124.88
odd(s(s(z0))) → odd(z0)
And the Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, s(z0)) → c(COND(odd(s(z0)), p(p(z0))), ODD(s(z0)))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(p(s(s(z0)))))), ODD(s(s(z0))))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, 0) → c
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
The order we found is given by the following interpretation:
Polynomial interpretation :
313.62/124.88
POL(0) = [2]
313.62/124.88
POL(COND(x1, x2)) = [2]x2
313.62/124.88
POL(ODD(x1)) = 0
313.62/124.88
POL(c) = 0
313.62/124.88
POL(c(x1)) = x1
313.62/124.88
POL(c(x1, x2)) = x1 + x2
313.62/124.88
POL(c3(x1)) = x1
313.62/124.88
POL(false) = [5]
313.62/124.88
POL(odd(x1)) = [2] + [4]x1
313.62/124.88
POL(p(x1)) = x1
313.62/124.88
POL(s(x1)) = [1] + x1
313.62/124.88
POL(true) = 0
313.62/124.88
313.62/124.88
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
313.62/124.88
odd(0) → false
313.62/124.88
odd(s(0)) → true
313.62/124.88
odd(s(s(z0))) → odd(z0)
313.62/124.88
p(0) → 0
313.62/124.88
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, s(z0)) → c(COND(odd(s(z0)), p(p(z0))), ODD(s(z0)))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(p(s(s(z0)))))), ODD(s(s(z0))))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, 0) → c
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(p(s(s(z0)))))), ODD(s(s(z0))))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
K tuples:
COND(true, 0) → c
313.62/124.88
COND(true, s(z0)) → c(COND(odd(s(z0)), p(p(z0))), ODD(s(z0)))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
313.62/124.88
313.62/124.88
(15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
COND(
true,
s(
z0)) →
c(
COND(
odd(
s(
z0)),
p(
p(
z0))),
ODD(
s(
z0))) by
COND(true, s(0)) → c(COND(odd(s(0)), p(0)), ODD(s(0)))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(s(s(z0))), p(z0)), ODD(s(s(z0))))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(0))), ODD(s(0)))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
313.62/124.88
313.62/124.88
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
313.62/124.88
odd(0) → false
313.62/124.88
odd(s(0)) → true
313.62/124.88
odd(s(s(z0))) → odd(z0)
313.62/124.88
p(0) → 0
313.62/124.88
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(p(s(s(z0)))))), ODD(s(s(z0))))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, 0) → c
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
313.62/124.88
COND(true, s(0)) → c(COND(odd(s(0)), p(0)), ODD(s(0)))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(s(s(z0))), p(z0)), ODD(s(s(z0))))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(0))), ODD(s(0)))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(p(s(s(z0)))))), ODD(s(s(z0))))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
K tuples:
COND(true, 0) → c
313.62/124.88
COND(true, s(z0)) → c(COND(odd(s(z0)), p(p(z0))), ODD(s(z0)))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
313.62/124.88
313.62/124.88
(17) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing tuple parts
313.62/124.88
313.62/124.88
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
313.62/124.88
odd(0) → false
313.62/124.88
odd(s(0)) → true
313.62/124.88
odd(s(s(z0))) → odd(z0)
313.62/124.88
p(0) → 0
313.62/124.88
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(p(s(s(z0)))))), ODD(s(s(z0))))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, 0) → c
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(s(s(z0))), p(z0)), ODD(s(s(z0))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
313.62/124.88
COND(true, s(0)) → c(COND(odd(s(0)), p(0)))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(0))))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(p(s(s(z0)))))), ODD(s(s(z0))))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
K tuples:
COND(true, 0) → c
313.62/124.88
COND(true, s(z0)) → c(COND(odd(s(z0)), p(p(z0))), ODD(s(z0)))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
313.62/124.88
313.62/124.88
(19) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
COND(true, 0) → c
313.62/124.88
313.62/124.88
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
313.62/124.88
odd(0) → false
313.62/124.88
odd(s(0)) → true
313.62/124.88
odd(s(s(z0))) → odd(z0)
313.62/124.88
p(0) → 0
313.62/124.88
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(p(s(s(z0)))))), ODD(s(s(z0))))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, 0) → c
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(s(s(z0))), p(z0)), ODD(s(s(z0))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
313.62/124.88
COND(true, s(0)) → c(COND(odd(s(0)), p(0)))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(0))))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(p(s(s(z0)))))), ODD(s(s(z0))))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
K tuples:
COND(true, 0) → c
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
313.62/124.88
313.62/124.88
(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
COND(
true,
s(
s(
z0))) →
c(
COND(
odd(
z0),
p(
p(
p(
s(
s(
z0)))))),
ODD(
s(
s(
z0)))) by
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
313.62/124.88
COND(true, s(s(0))) → c(COND(false, p(p(p(s(s(0)))))), ODD(s(s(0))))
313.62/124.88
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
313.62/124.88
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
313.62/124.88
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
313.62/124.88
313.62/124.88
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
313.62/124.88
odd(0) → false
313.62/124.88
odd(s(0)) → true
313.62/124.88
odd(s(s(z0))) → odd(z0)
313.62/124.88
p(0) → 0
313.62/124.88
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, 0) → c
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(s(s(z0))), p(z0)), ODD(s(s(z0))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
313.62/124.88
COND(true, s(0)) → c(COND(odd(s(0)), p(0)))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(0))))
313.62/124.88
COND(true, s(s(0))) → c(COND(false, p(p(p(s(s(0)))))), ODD(s(s(0))))
313.62/124.88
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
313.62/124.88
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
313.62/124.88
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
313.62/124.88
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
313.62/124.88
COND(true, s(s(0))) → c(COND(false, p(p(p(s(s(0)))))), ODD(s(s(0))))
313.62/124.88
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
313.62/124.88
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
313.62/124.88
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
K tuples:
COND(true, 0) → c
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
313.62/124.88
313.62/124.88
(23) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
313.62/124.88
313.62/124.88
(24) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
313.62/124.88
odd(0) → false
313.62/124.88
odd(s(0)) → true
313.62/124.88
odd(s(s(z0))) → odd(z0)
313.62/124.88
p(0) → 0
313.62/124.88
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, 0) → c
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(s(s(z0))), p(z0)), ODD(s(s(z0))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
313.62/124.88
COND(true, s(0)) → c(COND(odd(s(0)), p(0)))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(0))))
313.62/124.88
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
313.62/124.88
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
313.62/124.88
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
313.62/124.88
COND(true, s(s(0))) → c(ODD(s(s(0))))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
313.62/124.88
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
313.62/124.88
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
313.62/124.88
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
313.62/124.88
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
313.62/124.88
COND(true, s(s(0))) → c(ODD(s(s(0))))
K tuples:
COND(true, 0) → c
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
313.62/124.88
313.62/124.88
(25) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
COND(true, 0) → c
313.62/124.88
313.62/124.88
(26) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
313.62/124.88
odd(0) → false
313.62/124.88
odd(s(0)) → true
313.62/124.88
odd(s(s(z0))) → odd(z0)
313.62/124.88
p(0) → 0
313.62/124.88
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, 0) → c
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(s(s(z0))), p(z0)), ODD(s(s(z0))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
313.62/124.88
COND(true, s(0)) → c(COND(odd(s(0)), p(0)))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(0))))
313.62/124.88
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
313.62/124.88
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
313.62/124.88
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
313.62/124.88
COND(true, s(s(0))) → c(ODD(s(s(0))))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
313.62/124.88
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
313.62/124.88
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
313.62/124.88
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
313.62/124.88
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
313.62/124.88
COND(true, s(s(0))) → c(ODD(s(s(0))))
K tuples:
COND(true, 0) → c
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
313.62/124.88
313.62/124.88
(27) 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.
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
313.62/124.88
COND(true, s(s(0))) → c(ODD(s(s(0))))
We considered the (Usable) Rules:
odd(0) → false
313.62/124.88
odd(s(0)) → true
313.62/124.88
odd(s(s(z0))) → odd(z0)
313.62/124.88
p(s(z0)) → z0
313.62/124.88
p(0) → 0
And the Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, 0) → c
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(s(s(z0))), p(z0)), ODD(s(s(z0))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
313.62/124.88
COND(true, s(0)) → c(COND(odd(s(0)), p(0)))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(0))))
313.62/124.88
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
313.62/124.88
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
313.62/124.88
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
313.62/124.88
COND(true, s(s(0))) → c(ODD(s(s(0))))
The order we found is given by the following interpretation:
Polynomial interpretation :
313.62/124.88
POL(0) = [5]
313.62/124.88
POL(COND(x1, x2)) = [4]
313.62/124.88
POL(ODD(x1)) = 0
313.62/124.88
POL(c) = 0
313.62/124.88
POL(c(x1)) = x1
313.62/124.88
POL(c(x1, x2)) = x1 + x2
313.62/124.88
POL(c3(x1)) = x1
313.62/124.88
POL(false) = [5]
313.62/124.88
POL(odd(x1)) = [2]x1
313.62/124.88
POL(p(x1)) = 0
313.62/124.88
POL(s(x1)) = [5]
313.62/124.88
POL(true) = [4]
313.62/124.88
313.62/124.88
(28) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
313.62/124.88
odd(0) → false
313.62/124.88
odd(s(0)) → true
313.62/124.88
odd(s(s(z0))) → odd(z0)
313.62/124.88
p(0) → 0
313.62/124.88
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, 0) → c
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(s(s(z0))), p(z0)), ODD(s(s(z0))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
313.62/124.88
COND(true, s(0)) → c(COND(odd(s(0)), p(0)))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(0))))
313.62/124.88
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
313.62/124.88
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
313.62/124.88
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
313.62/124.88
COND(true, s(s(0))) → c(ODD(s(s(0))))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
313.62/124.88
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
313.62/124.88
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
313.62/124.88
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
K tuples:
COND(true, 0) → c
313.62/124.88
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
313.62/124.88
COND(true, s(s(0))) → c(ODD(s(s(0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
313.62/124.88
313.62/124.88
(29) 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.
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
We considered the (Usable) Rules:
odd(0) → false
313.62/124.88
odd(s(0)) → true
313.62/124.88
odd(s(s(z0))) → odd(z0)
313.62/124.88
p(s(z0)) → z0
313.62/124.88
p(0) → 0
And the Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, 0) → c
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(s(s(z0))), p(z0)), ODD(s(s(z0))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
313.62/124.88
COND(true, s(0)) → c(COND(odd(s(0)), p(0)))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(0))))
313.62/124.88
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
313.62/124.88
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
313.62/124.88
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
313.62/124.88
COND(true, s(s(0))) → c(ODD(s(s(0))))
The order we found is given by the following interpretation:
Polynomial interpretation :
313.62/124.88
POL(0) = 0
313.62/124.88
POL(COND(x1, x2)) = [4] + x2
313.62/124.88
POL(ODD(x1)) = 0
313.62/124.88
POL(c) = 0
313.62/124.88
POL(c(x1)) = x1
313.62/124.88
POL(c(x1, x2)) = x1 + x2
313.62/124.88
POL(c3(x1)) = x1
313.62/124.88
POL(false) = 0
313.62/124.88
POL(odd(x1)) = [5]x1
313.62/124.88
POL(p(x1)) = x1
313.62/124.88
POL(s(x1)) = [2] + x1
313.62/124.88
POL(true) = [4]
313.62/124.88
313.62/124.88
(30) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
313.62/124.88
odd(0) → false
313.62/124.88
odd(s(0)) → true
313.62/124.88
odd(s(s(z0))) → odd(z0)
313.62/124.88
p(0) → 0
313.62/124.88
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, 0) → c
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(s(s(z0))), p(z0)), ODD(s(s(z0))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
313.62/124.88
COND(true, s(0)) → c(COND(odd(s(0)), p(0)))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(0))))
313.62/124.88
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
313.62/124.88
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
313.62/124.88
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
313.62/124.88
COND(true, s(s(0))) → c(ODD(s(s(0))))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, 0) → c(COND(odd(0), p(p(0))))
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
313.62/124.88
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
313.62/124.88
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
K tuples:
COND(true, 0) → c
313.62/124.88
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
313.62/124.88
COND(true, s(s(0))) → c(ODD(s(s(0))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
313.62/124.88
313.62/124.88
(31) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
COND(
true,
0) →
c(
COND(
odd(
0),
p(
p(
0)))) by
COND(true, 0) → c(COND(odd(0), p(0)))
313.62/124.88
COND(true, 0) → c(COND(false, p(p(0))))
313.62/124.88
313.62/124.88
(32) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
313.62/124.88
odd(0) → false
313.62/124.88
odd(s(0)) → true
313.62/124.88
odd(s(s(z0))) → odd(z0)
313.62/124.88
p(0) → 0
313.62/124.88
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
313.62/124.88
COND(true, 0) → c
313.62/124.88
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(s(s(z0))), p(z0)), ODD(s(s(z0))))
313.62/124.88
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.90
COND(true, s(0)) → c(COND(odd(s(0)), p(0)))
314.02/124.90
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.90
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.90
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.90
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.90
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.90
COND(true, 0) → c(COND(odd(0), p(0)))
314.02/124.90
COND(true, 0) → c(COND(false, p(p(0))))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.90
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
314.02/124.90
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.90
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.90
COND(true, 0) → c(COND(odd(0), p(0)))
314.02/124.90
COND(true, 0) → c(COND(false, p(p(0))))
K tuples:
COND(true, 0) → c
314.02/124.90
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.90
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
314.02/124.90
314.02/124.90
(33) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
314.02/124.90
314.02/124.90
(34) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.90
odd(0) → false
314.02/124.90
odd(s(0)) → true
314.02/124.90
odd(s(s(z0))) → odd(z0)
314.02/124.90
p(0) → 0
314.02/124.90
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.90
COND(true, 0) → c
314.02/124.90
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(s(s(z0))), p(z0)), ODD(s(s(z0))))
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.90
COND(true, s(0)) → c(COND(odd(s(0)), p(0)))
314.02/124.90
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.90
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.90
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.90
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.90
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.90
COND(true, 0) → c(COND(odd(0), p(0)))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.90
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
314.02/124.90
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.90
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.90
COND(true, 0) → c(COND(odd(0), p(0)))
314.02/124.90
COND(true, 0) → c
K tuples:
COND(true, 0) → c
314.02/124.90
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.90
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
314.02/124.90
314.02/124.90
(35) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)
The following tuples could be moved from S to K by knowledge propagation:
COND(true, 0) → c
314.02/124.90
COND(true, 0) → c
314.02/124.90
314.02/124.90
(36) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.90
odd(0) → false
314.02/124.90
odd(s(0)) → true
314.02/124.90
odd(s(s(z0))) → odd(z0)
314.02/124.90
p(0) → 0
314.02/124.90
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.90
COND(true, 0) → c
314.02/124.90
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(s(s(z0))), p(z0)), ODD(s(s(z0))))
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.90
COND(true, s(0)) → c(COND(odd(s(0)), p(0)))
314.02/124.90
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.90
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.90
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.90
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.90
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.90
COND(true, 0) → c(COND(odd(0), p(0)))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.90
COND(true, s(0)) → c(COND(true, p(p(p(s(0))))))
314.02/124.90
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.90
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.90
COND(true, 0) → c(COND(odd(0), p(0)))
K tuples:
COND(true, 0) → c
314.02/124.90
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.90
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
314.02/124.90
314.02/124.90
(37) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
COND(
true,
s(
0)) →
c(
COND(
true,
p(
p(
p(
s(
0)))))) by
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.90
314.02/124.90
(38) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.90
odd(0) → false
314.02/124.90
odd(s(0)) → true
314.02/124.90
odd(s(s(z0))) → odd(z0)
314.02/124.90
p(0) → 0
314.02/124.90
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.90
COND(true, 0) → c
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(s(s(z0))), p(z0)), ODD(s(s(z0))))
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.90
COND(true, s(0)) → c(COND(odd(s(0)), p(0)))
314.02/124.90
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.90
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.90
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.90
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.90
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.90
COND(true, 0) → c(COND(odd(0), p(0)))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.90
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.90
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.90
COND(true, 0) → c(COND(odd(0), p(0)))
314.02/124.90
COND(true, s(0)) → c(COND(true, p(p(0))))
K tuples:
COND(true, 0) → c
314.02/124.90
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.90
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
314.02/124.90
314.02/124.90
(39) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
COND(true, 0) → c
314.02/124.90
314.02/124.90
(40) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.90
odd(0) → false
314.02/124.90
odd(s(0)) → true
314.02/124.90
odd(s(s(z0))) → odd(z0)
314.02/124.90
p(0) → 0
314.02/124.90
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.90
COND(true, 0) → c
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(s(s(z0))), p(z0)), ODD(s(s(z0))))
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.90
COND(true, s(0)) → c(COND(odd(s(0)), p(0)))
314.02/124.90
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.90
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.90
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.90
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.90
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.90
COND(true, 0) → c(COND(odd(0), p(0)))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.90
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.90
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.90
COND(true, 0) → c(COND(odd(0), p(0)))
314.02/124.90
COND(true, s(0)) → c(COND(true, p(p(0))))
K tuples:
COND(true, 0) → c
314.02/124.90
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.90
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
314.02/124.90
314.02/124.90
(41) 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.
COND(true, s(0)) → c(COND(true, p(p(0))))
We considered the (Usable) Rules:
odd(0) → false
314.02/124.90
odd(s(0)) → true
314.02/124.90
odd(s(s(z0))) → odd(z0)
314.02/124.90
p(0) → 0
314.02/124.90
p(s(z0)) → z0
And the Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.90
COND(true, 0) → c
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(s(s(z0))), p(z0)), ODD(s(s(z0))))
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.90
COND(true, s(0)) → c(COND(odd(s(0)), p(0)))
314.02/124.90
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.90
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.90
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.90
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.90
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.90
COND(true, 0) → c(COND(odd(0), p(0)))
The order we found is given by the following interpretation:
Polynomial interpretation :
314.02/124.90
POL(0) = 0
314.02/124.90
POL(COND(x1, x2)) = [4]x2
314.02/124.90
POL(ODD(x1)) = 0
314.02/124.90
POL(c) = 0
314.02/124.90
POL(c(x1)) = x1
314.02/124.90
POL(c(x1, x2)) = x1 + x2
314.02/124.90
POL(c3(x1)) = x1
314.02/124.90
POL(false) = [3]
314.02/124.90
POL(odd(x1)) = 0
314.02/124.90
POL(p(x1)) = x1
314.02/124.90
POL(s(x1)) = [4] + x1
314.02/124.90
POL(true) = 0
314.02/124.90
314.02/124.90
(42) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.90
odd(0) → false
314.02/124.90
odd(s(0)) → true
314.02/124.90
odd(s(s(z0))) → odd(z0)
314.02/124.90
p(0) → 0
314.02/124.90
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.90
COND(true, 0) → c
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(s(s(z0))), p(z0)), ODD(s(s(z0))))
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.90
COND(true, s(0)) → c(COND(odd(s(0)), p(0)))
314.02/124.90
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.90
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.90
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.90
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.90
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.90
COND(true, 0) → c(COND(odd(0), p(0)))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.90
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.90
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.90
COND(true, 0) → c(COND(odd(0), p(0)))
K tuples:
COND(true, 0) → c
314.02/124.90
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.90
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.90
COND(true, s(0)) → c(COND(true, p(p(0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
314.02/124.90
314.02/124.90
(43) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace COND(true, s(s(z0))) → c(COND(odd(s(s(z0))), p(z0)), ODD(s(s(z0)))) by COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.90
314.02/124.90
(44) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.90
odd(0) → false
314.02/124.90
odd(s(0)) → true
314.02/124.90
odd(s(s(z0))) → odd(z0)
314.02/124.90
p(0) → 0
314.02/124.90
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.90
COND(true, 0) → c
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.90
COND(true, s(0)) → c(COND(odd(s(0)), p(0)))
314.02/124.90
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.90
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.90
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.90
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.90
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.90
COND(true, 0) → c(COND(odd(0), p(0)))
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.90
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.90
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.90
COND(true, 0) → c(COND(odd(0), p(0)))
K tuples:
COND(true, 0) → c
314.02/124.90
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.90
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.90
COND(true, s(0)) → c(COND(true, p(p(0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
314.02/124.90
314.02/124.90
(45) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
COND(true, 0) → c
314.02/124.90
314.02/124.90
(46) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.90
odd(0) → false
314.02/124.90
odd(s(0)) → true
314.02/124.90
odd(s(s(z0))) → odd(z0)
314.02/124.90
p(0) → 0
314.02/124.90
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.90
COND(true, 0) → c
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.90
COND(true, s(0)) → c(COND(odd(s(0)), p(0)))
314.02/124.90
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.90
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.90
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.90
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.90
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.90
COND(true, 0) → c(COND(odd(0), p(0)))
314.02/124.90
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.90
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.90
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.90
COND(true, 0) → c(COND(odd(0), p(0)))
K tuples:
COND(true, 0) → c
314.02/124.90
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
314.02/124.91
314.02/124.91
(47) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0)))) by COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
314.02/124.91
(48) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.91
COND(true, 0) → c
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), p(0)))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, 0) → c(COND(odd(0), p(0)))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, 0) → c(COND(odd(0), p(0)))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
314.02/124.91
314.02/124.91
(49) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
COND(true, 0) → c
314.02/124.91
314.02/124.91
(50) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.91
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), p(0)))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, 0) → c(COND(odd(0), p(0)))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, 0) → c(COND(odd(0), p(0)))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
314.02/124.91
314.02/124.91
(51) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace COND(true, s(0)) → c(COND(odd(s(0)), p(0))) by COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
314.02/124.91
(52) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.91
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, 0) → c(COND(odd(0), p(0)))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, 0) → c(COND(odd(0), p(0)))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
314.02/124.91
314.02/124.91
(53) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
COND(true, 0) → c
314.02/124.91
314.02/124.91
(54) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.91
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, 0) → c(COND(odd(0), p(0)))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, 0) → c(COND(odd(0), p(0)))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
314.02/124.91
314.02/124.91
(55) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
COND(
true,
0) →
c(
COND(
odd(
0),
p(
0))) by
COND(true, 0) → c(COND(odd(0), 0))
314.02/124.91
COND(true, 0) → c(COND(false, p(0)))
314.02/124.91
314.02/124.91
(56) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.91
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
COND(true, 0) → c(COND(odd(0), 0))
314.02/124.91
COND(true, 0) → c(COND(false, p(0)))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, 0) → c(COND(odd(0), 0))
314.02/124.91
COND(true, 0) → c(COND(false, p(0)))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
314.02/124.91
314.02/124.91
(57) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
314.02/124.91
314.02/124.91
(58) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.91
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
COND(true, 0) → c(COND(odd(0), 0))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, 0) → c(COND(odd(0), 0))
314.02/124.91
COND(true, 0) → c
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
314.02/124.91
314.02/124.91
(59) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)
The following tuples could be moved from S to K by knowledge propagation:
COND(true, 0) → c
314.02/124.91
COND(true, 0) → c
314.02/124.91
COND(true, 0) → c
314.02/124.91
314.02/124.91
(60) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.91
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
COND(true, 0) → c(COND(odd(0), 0))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, 0) → c(COND(odd(0), 0))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
314.02/124.91
314.02/124.91
(61) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
COND(
true,
0) →
c(
COND(
odd(
0),
0)) by
COND(true, 0) → c(COND(false, 0))
314.02/124.91
314.02/124.91
(62) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.91
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
COND(true, 0) → c(COND(false, 0))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, 0) → c(COND(false, 0))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
314.02/124.91
314.02/124.91
(63) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
314.02/124.91
314.02/124.91
(64) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.91
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, 0) → c
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
314.02/124.91
314.02/124.91
(65) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)
The following tuples could be moved from S to K by knowledge propagation:
COND(true, 0) → c
314.02/124.91
COND(true, 0) → c
314.02/124.91
COND(true, 0) → c
314.02/124.91
COND(true, 0) → c
314.02/124.91
314.02/124.91
(66) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.91
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
S tuples:
ODD(s(s(z0))) → c3(ODD(z0))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
ODD, COND
Compound Symbols:
c3, c, c, c
314.02/124.91
314.02/124.91
(67) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
ODD(
s(
s(
z0))) →
c3(
ODD(
z0)) by
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
314.02/124.91
(68) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
S tuples:
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))), ODD(s(s(s(0)))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(0))) → c(ODD(s(s(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c, c3
314.02/124.91
314.02/124.91
(69) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing tuple parts
314.02/124.91
314.02/124.91
(70) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(0))) → c
S tuples:
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(0))) → c
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c, c3
314.02/124.91
314.02/124.91
(71) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 3 trailing nodes:
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
314.02/124.91
(72) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(0))) → c
S tuples:
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(0))) → c
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c, c3
314.02/124.91
314.02/124.91
(73) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace COND(true, s(0)) → c(COND(true, p(p(0)))) by COND(true, s(0)) → c(COND(true, p(0)))
314.02/124.91
314.02/124.91
(74) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, p(0)))
S tuples:
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(0))) → c
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c, c3
314.02/124.91
314.02/124.91
(75) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 3 trailing nodes:
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
314.02/124.91
(76) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, p(0)))
S tuples:
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(0))) → c
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c, c3
314.02/124.91
314.02/124.91
(77) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
COND(
true,
s(
0)) →
c(
COND(
true,
p(
0))) by
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
314.02/124.91
(78) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
S tuples:
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(0))) → c
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c, c3
314.02/124.91
314.02/124.91
(79) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing nodes:
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
314.02/124.91
(80) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
S tuples:
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(0))) → c
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c, c3
314.02/124.91
314.02/124.91
(81) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace COND(true, s(s(x0))) → c(COND(odd(x0), p(p(s(x0)))), ODD(s(s(x0)))) by COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
314.02/124.91
(82) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
S tuples:
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(p(s(z0)))), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(0))) → c
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c, c3
314.02/124.91
314.02/124.91
(83) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing nodes:
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
314.02/124.91
(84) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
S tuples:
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0))))))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(0))) → c
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c, c3
314.02/124.91
314.02/124.91
(85) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(p(s(s(s(s(z0)))))))), ODD(s(s(s(s(z0)))))) by COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
314.02/124.91
(86) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
S tuples:
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(0))) → c
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c, c3
314.02/124.91
314.02/124.91
(87) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing nodes:
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
314.02/124.91
(88) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
S tuples:
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(0))) → c
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c, c3
314.02/124.91
314.02/124.91
(89) 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.
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
We considered the (Usable) Rules:
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(s(z0)) → z0
314.02/124.91
p(0) → 0
And the Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
The order we found is given by the following interpretation:
Polynomial interpretation :
314.02/124.91
POL(0) = 0
314.02/124.91
POL(COND(x1, x2)) = [2] + [2]x2
314.02/124.91
POL(ODD(x1)) = [1]
314.02/124.91
POL(c) = 0
314.02/124.91
POL(c(x1)) = x1
314.02/124.91
POL(c(x1, x2)) = x1 + x2
314.02/124.91
POL(c3(x1)) = x1
314.02/124.91
POL(false) = [3]
314.02/124.91
POL(odd(x1)) = 0
314.02/124.91
POL(p(x1)) = x1
314.02/124.91
POL(s(x1)) = [4] + x1
314.02/124.91
POL(true) = 0
314.02/124.91
314.02/124.91
(90) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
S tuples:
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(x0))) → c(ODD(s(s(x0))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c, c3
314.02/124.91
314.02/124.91
(91) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
COND(
true,
s(
s(
x0))) →
c(
ODD(
s(
s(
x0)))) by
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
314.02/124.91
314.02/124.91
(92) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
S tuples:
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c, c3
314.02/124.91
314.02/124.91
(93) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing nodes:
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
314.02/124.91
(94) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
S tuples:
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c, c3
314.02/124.91
314.02/124.91
(95) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace COND(true, s(0)) → c(COND(true, p(p(0)))) by COND(true, s(0)) → c(COND(true, p(0)))
314.02/124.91
314.02/124.91
(96) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(0)))
S tuples:
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, p(p(0))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c, c3
314.02/124.91
314.02/124.91
(97) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing nodes:
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
314.02/124.91
(98) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
314.02/124.91
COND(true, s(0)) → c(COND(true, p(0)))
S tuples:
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c, c3
314.02/124.91
314.02/124.91
(99) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
COND(
true,
s(
0)) →
c(
COND(
true,
p(
0))) by
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
314.02/124.91
(100) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
S tuples:
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c, c3
314.02/124.91
314.02/124.91
(101) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing nodes:
COND(true, 0) → c
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
314.02/124.91
(102) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
COND(true, s(0)) → c(COND(odd(s(0)), 0))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
S tuples:
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c, c3
314.02/124.91
314.02/124.91
(103) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace COND(true, s(0)) → c(COND(odd(s(0)), 0)) by COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
314.02/124.91
(104) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
S tuples:
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c3, c
314.02/124.91
314.02/124.91
(105) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 3 trailing nodes:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
314.02/124.91
(106) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
S tuples:
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0))))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c3, c
314.02/124.91
314.02/124.91
(107) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace COND(true, s(s(s(0)))) → c(COND(true, p(p(p(s(s(s(0)))))))) by COND(true, s(s(s(0)))) → c(COND(true, p(p(s(s(0))))))
314.02/124.91
314.02/124.91
(108) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(s(s(0))))))
S tuples:
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(s(s(0))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c3, c
314.02/124.91
314.02/124.91
(109) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 3 trailing nodes:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
314.02/124.91
(110) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(s(s(0))))))
S tuples:
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(s(s(0))))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c3, c
314.02/124.91
314.02/124.91
(111) 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.
COND(true, s(s(s(0)))) → c(COND(true, p(p(s(s(0))))))
We considered the (Usable) Rules:
p(s(z0)) → z0
314.02/124.91
p(0) → 0
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
And the Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(s(s(0))))))
The order we found is given by the following interpretation:
Polynomial interpretation :
314.02/124.91
POL(0) = 0
314.02/124.91
POL(COND(x1, x2)) = [2] + [2]x2
314.02/124.91
POL(ODD(x1)) = [4]
314.02/124.91
POL(c) = 0
314.02/124.91
POL(c(x1)) = x1
314.02/124.91
POL(c(x1, x2)) = x1 + x2
314.02/124.91
POL(c3(x1)) = x1
314.02/124.91
POL(false) = [2]
314.02/124.91
POL(odd(x1)) = [2] + [4]x1
314.02/124.91
POL(p(x1)) = x1
314.02/124.91
POL(s(x1)) = [2] + x1
314.02/124.91
POL(true) = [4]
314.02/124.91
314.02/124.91
(112) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(s(s(0))))))
S tuples:
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(s(s(0))))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c3, c
314.02/124.91
314.02/124.91
(113) 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.
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
We considered the (Usable) Rules:
p(s(z0)) → z0
314.02/124.91
p(0) → 0
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
And the Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(s(s(0))))))
The order we found is given by the following interpretation:
Polynomial interpretation :
314.02/124.91
POL(0) = 0
314.02/124.91
POL(COND(x1, x2)) = x22
314.02/124.91
POL(ODD(x1)) = x1
314.02/124.91
POL(c) = 0
314.02/124.91
POL(c(x1)) = x1
314.02/124.91
POL(c(x1, x2)) = x1 + x2
314.02/124.91
POL(c3(x1)) = x1
314.02/124.91
POL(false) = [3]
314.02/124.91
POL(odd(x1)) = 0
314.02/124.91
POL(p(x1)) = x1
314.02/124.91
POL(s(x1)) = [1] + x1
314.02/124.91
POL(true) = 0
314.02/124.91
314.02/124.91
(114) Obligation:
Complexity Dependency Tuples Problem
Rules:
cond(true, z0) → cond(odd(z0), p(p(p(z0))))
314.02/124.91
odd(0) → false
314.02/124.91
odd(s(0)) → true
314.02/124.91
odd(s(s(z0))) → odd(z0)
314.02/124.91
p(0) → 0
314.02/124.91
p(s(z0)) → z0
Tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(z0))) → c(COND(odd(z0), p(z0)), ODD(s(s(z0))))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(0)) → c(COND(true, 0))
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(s(s(0))))))
S tuples:none
K tuples:
COND(true, 0) → c
314.02/124.91
COND(true, s(s(0))) → c
314.02/124.91
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(p(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))
314.02/124.91
COND(true, s(s(s(s(y0))))) → c(ODD(s(s(s(s(y0))))))
314.02/124.91
COND(true, s(s(s(0)))) → c(COND(true, p(p(s(s(0))))))
314.02/124.91
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))
Defined Rule Symbols:
cond, odd, p
Defined Pair Symbols:
COND, ODD
Compound Symbols:
c, c, c3, c
314.02/124.91
314.02/124.91
(115) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)
The set S is empty
314.02/124.91
314.02/124.91
(116) BOUNDS(O(1), O(1))
314.02/124.91