67.83/43.30 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml

67.83/43.30

67.83/43.30
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^2)).

0 CpxTRS

67.83/43.30

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

67.83/43.30

↳2 CdtProblem

67.83/43.30

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

67.83/43.30

↳4 CdtProblem

67.83/43.30

↳5 CdtNarrowingProof (BOTH BOUNDS(ID, ID))

67.83/43.30

↳6 CdtProblem

67.83/43.30

↳7 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))

67.83/43.30

↳8 CdtProblem

67.83/43.30

↳9 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

67.83/43.30

↳10 CdtProblem

67.83/43.30

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

67.83/43.30

↳12 CdtProblem

67.83/43.30

↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

67.83/43.30

↳14 CdtProblem

67.83/43.30

↳15 CdtNarrowingProof (BOTH BOUNDS(ID, ID))

67.83/43.30

↳16 CdtProblem

67.83/43.30

↳17 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))

67.83/43.30

↳18 CdtProblem

67.83/43.30

↳19 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

67.83/43.30

↳20 CdtProblem

67.83/43.30

↳21 CdtNarrowingProof (BOTH BOUNDS(ID, ID))

67.83/43.30

↳22 CdtProblem

67.83/43.30

↳23 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))

67.83/43.30

↳24 CdtProblem

67.83/43.30

↳25 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

67.83/43.30

↳26 CdtProblem

67.83/43.30

↳27 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

67.83/43.30

↳28 CdtProblem

67.83/43.30

↳29 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

67.83/43.30

↳30 CdtProblem

67.83/43.30

↳31 CdtNarrowingProof (BOTH BOUNDS(ID, ID))

67.83/43.30

↳32 CdtProblem

67.83/43.30

↳33 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))

67.83/43.30

↳34 CdtProblem

67.83/43.30

↳35 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))

67.83/43.30

↳36 CdtProblem

67.83/43.30

↳37 CdtNarrowingProof (BOTH BOUNDS(ID, ID))

67.83/43.30

↳38 CdtProblem

67.83/43.30

↳39 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

67.83/43.30

↳40 CdtProblem

67.83/43.30

↳41 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

67.83/43.30

↳42 CdtProblem

67.83/43.30

↳43 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

67.83/43.30

↳44 CdtProblem

67.83/43.30

↳45 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))

67.83/43.30

↳46 CdtProblem

67.83/43.30

↳47 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

67.83/43.30

↳48 CdtProblem

67.83/43.30

↳49 CdtRewritingProof (BOTH BOUNDS(ID, ID))

67.83/43.30

↳50 CdtProblem

67.83/43.30

↳51 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

67.83/43.30

↳52 CdtProblem

67.83/43.30

↳53 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

67.83/43.30

↳54 CdtProblem

67.83/43.30

↳55 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

67.83/43.30

↳56 CdtProblem

67.83/43.30

↳57 CdtRewritingProof (BOTH BOUNDS(ID, ID))

67.83/43.30

↳58 CdtProblem

67.83/43.30

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

67.83/43.30

↳60 CdtProblem

67.83/43.30

↳61 CdtKnowledgeProof (⇔)

67.83/43.30

↳62 BOUNDS(O(1), O(1))

67.83/43.30

67.83/43.30 67.83/43.30

67.83/43.30

(0) Obligation:

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

cond(true, x) → cond(odd(x), p(x)) 67.83/43.30
odd(0) → false 67.83/43.30
odd(s(0)) → true 67.83/43.30
odd(s(s(x))) → odd(x) 68.02/43.31
p(0) → 0 68.02/43.31
p(s(x)) → x

Rewrite Strategy: INNERMOST

68.02/43.31

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

Converted CpxTRS to CDT

68.02/43.31

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.31
odd(0) → false 68.02/43.31
odd(s(0)) → true 68.02/43.31
odd(s(s(z0))) → odd(z0) 68.02/43.31
p(0) → 0 68.02/43.31
p(s(z0)) → z0

Tuples:

COND(true, z0) → c(COND(odd(z0), p(z0)), ODD(z0), P(z0)) 68.02/43.31
ODD(s(s(z0))) → c3(ODD(z0))

S tuples:

COND(true, z0) → c(COND(odd(z0), p(z0)), ODD(z0), P(z0)) 68.02/43.31
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

68.02/43.31

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

Removed 1 trailing tuple parts

68.02/43.31

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.31
odd(0) → false 68.02/43.31
odd(s(0)) → true 68.02/43.31
odd(s(s(z0))) → odd(z0) 68.02/43.31
p(0) → 0 68.02/43.31
p(s(z0)) → z0

Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.31
COND(true, z0) → c(COND(odd(z0), p(z0)), ODD(z0))

S tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.31
COND(true, z0) → c(COND(odd(z0), p(z0)), ODD(z0))

K tuples:none
Defined Rule Symbols:

cond, odd, p

Defined Pair Symbols:

ODD, COND

Compound Symbols:

c3, c

68.02/43.31

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

Use narrowing to replace COND(true, z0) → c(COND(odd(z0), p(z0)), ODD(z0)) by

COND(true, 0) → c(COND(odd(0), 0), ODD(0)) 68.02/43.31
COND(true, s(z0)) → c(COND(odd(s(z0)), z0), ODD(s(z0))) 68.02/43.31
COND(true, 0) → c(COND(false, p(0)), ODD(0)) 68.02/43.31
COND(true, s(0)) → c(COND(true, p(s(0))), ODD(s(0))) 68.02/43.31
COND(true, s(s(z0))) → c(COND(odd(z0), p(s(s(z0)))), ODD(s(s(z0))))

68.02/43.31

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.31
odd(0) → false 68.02/43.31
odd(s(0)) → true 68.02/43.31
odd(s(s(z0))) → odd(z0) 68.02/43.31
p(0) → 0 68.02/43.31
p(s(z0)) → z0

Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.31
COND(true, 0) → c(COND(odd(0), 0), ODD(0)) 68.02/43.31
COND(true, s(z0)) → c(COND(odd(s(z0)), z0), ODD(s(z0))) 68.02/43.31
COND(true, 0) → c(COND(false, p(0)), ODD(0)) 68.02/43.31
COND(true, s(0)) → c(COND(true, p(s(0))), ODD(s(0))) 68.02/43.31
COND(true, s(s(z0))) → c(COND(odd(z0), p(s(s(z0)))), ODD(s(s(z0))))

S tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.31
COND(true, 0) → c(COND(odd(0), 0), ODD(0)) 68.02/43.31
COND(true, s(z0)) → c(COND(odd(s(z0)), z0), ODD(s(z0))) 68.02/43.31
COND(true, 0) → c(COND(false, p(0)), ODD(0)) 68.02/43.31
COND(true, s(0)) → c(COND(true, p(s(0))), ODD(s(0))) 68.02/43.31
COND(true, s(s(z0))) → c(COND(odd(z0), 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

68.02/43.31

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

Removed 4 trailing tuple parts

68.02/43.31

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.31
odd(0) → false 68.02/43.31
odd(s(0)) → true 68.02/43.31
odd(s(s(z0))) → odd(z0) 68.02/43.31
p(0) → 0 68.02/43.31
p(s(z0)) → z0

Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.31
COND(true, s(z0)) → c(COND(odd(s(z0)), z0), ODD(s(z0))) 68.02/43.31
COND(true, s(s(z0))) → c(COND(odd(z0), p(s(s(z0)))), ODD(s(s(z0)))) 68.02/43.31
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.31
COND(true, 0) → c 68.02/43.31
COND(true, s(0)) → c(COND(true, p(s(0))))

S tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.31
COND(true, s(z0)) → c(COND(odd(s(z0)), z0), ODD(s(z0))) 68.02/43.31
COND(true, s(s(z0))) → c(COND(odd(z0), p(s(s(z0)))), ODD(s(s(z0)))) 68.02/43.31
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.31
COND(true, 0) → c 68.02/43.31
COND(true, s(0)) → c(COND(true, p(s(0))))

K tuples:none
Defined Rule Symbols:

cond, odd, p

Defined Pair Symbols:

ODD, COND

Compound Symbols:

c3, c, c, c

68.02/43.31

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

Removed 1 trailing nodes:

COND(true, 0) → c

68.02/43.31

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.31
odd(0) → false 68.02/43.31
odd(s(0)) → true 68.02/43.31
odd(s(s(z0))) → odd(z0) 68.02/43.31
p(0) → 0 68.02/43.31
p(s(z0)) → z0

Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.31
COND(true, s(z0)) → c(COND(odd(s(z0)), z0), ODD(s(z0))) 68.02/43.31
COND(true, s(s(z0))) → c(COND(odd(z0), p(s(s(z0)))), ODD(s(s(z0)))) 68.02/43.31
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.31
COND(true, 0) → c 68.02/43.31
COND(true, s(0)) → c(COND(true, p(s(0))))

S tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.31
COND(true, s(z0)) → c(COND(odd(s(z0)), z0), ODD(s(z0))) 68.02/43.31
COND(true, s(s(z0))) → c(COND(odd(z0), p(s(s(z0)))), ODD(s(s(z0)))) 68.02/43.31
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.31
COND(true, 0) → c 68.02/43.31
COND(true, s(0)) → c(COND(true, p(s(0))))

K tuples:none
Defined Rule Symbols:

cond, odd, p

Defined Pair Symbols:

ODD, COND

Compound Symbols:

c3, c, c, c

68.02/43.31

(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 68.02/43.31
odd(0) → false 68.02/43.31
odd(s(0)) → true 68.02/43.31
odd(s(s(z0))) → odd(z0)

And the Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.31
COND(true, s(z0)) → c(COND(odd(s(z0)), z0), ODD(s(z0))) 68.02/43.31
COND(true, s(s(z0))) → c(COND(odd(z0), p(s(s(z0)))), ODD(s(s(z0)))) 68.02/43.31
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.31
COND(true, 0) → c 68.02/43.31
COND(true, s(0)) → c(COND(true, p(s(0))))

The order we found is given by the following interpretation:
Polynomial interpretation : 68.02/43.31

POL(0) = 0 68.02/43.31
POL(COND(x₁, x₂)) = [1] 68.02/43.31
POL(ODD(x₁)) = 0 68.02/43.31
POL(c) = 0 68.02/43.31
POL(c(x₁)) = x₁ 68.02/43.31
POL(c(x₁, x₂)) = x₁ + x₂ 68.02/43.31
POL(c3(x₁)) = x₁ 68.02/43.31
POL(false) = 0 68.02/43.31
POL(odd(x₁)) = 0 68.02/43.31
POL(p(x₁)) = [1] 68.02/43.31
POL(s(x₁)) = 0 68.02/43.31
POL(true) = 0

68.02/43.31

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.31
odd(0) → false 68.02/43.31
odd(s(0)) → true 68.02/43.31
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, s(z0)) → c(COND(odd(s(z0)), z0), ODD(s(z0))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), p(s(s(z0)))), ODD(s(s(z0)))) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0))))

S tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, s(z0)) → c(COND(odd(s(z0)), z0), ODD(s(z0))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), p(s(s(z0)))), ODD(s(s(z0)))) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, s(0)) → c(COND(true, 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

68.02/43.37

(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)), z0), ODD(s(z0)))

We considered the (Usable) Rules:

p(s(z0)) → z0 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0)

And the Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, s(z0)) → c(COND(odd(s(z0)), z0), ODD(s(z0))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), p(s(s(z0)))), ODD(s(s(z0)))) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0))))

The order we found is given by the following interpretation:
Polynomial interpretation : 68.02/43.37

POL(0) = [2] 68.02/43.37
POL(COND(x₁, x₂)) = [4]x₂ 68.02/43.37
POL(ODD(x₁)) = 0 68.02/43.37
POL(c) = 0 68.02/43.37
POL(c(x₁)) = x₁ 68.02/43.37
POL(c(x₁, x₂)) = x₁ + x₂ 68.02/43.37
POL(c3(x₁)) = x₁ 68.02/43.37
POL(false) = [5] 68.02/43.37
POL(odd(x₁)) = [2] + [4]x₁ 68.02/43.37
POL(p(x₁)) = x₁ 68.02/43.37
POL(s(x₁)) = [4] + x₁ 68.02/43.37
POL(true) = [4]

68.02/43.37

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, s(z0)) → c(COND(odd(s(z0)), z0), ODD(s(z0))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), p(s(s(z0)))), ODD(s(s(z0)))) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0))))

S tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), p(s(s(z0)))), ODD(s(s(z0)))) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0))))

K tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(z0)) → c(COND(odd(s(z0)), z0), ODD(s(z0)))

Defined Rule Symbols:

cond, odd, p

Defined Pair Symbols:

ODD, COND

Compound Symbols:

c3, c, c, c

68.02/43.37

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

Use narrowing to replace COND(true, s(z0)) → c(COND(odd(s(z0)), z0), ODD(s(z0))) by

COND(true, s(0)) → c(COND(true, 0), ODD(s(0))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0))))

68.02/43.37

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), p(s(s(z0)))), ODD(s(s(z0)))) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0), ODD(s(0))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0))))

S tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), p(s(s(z0)))), ODD(s(s(z0)))) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0))))

K tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(z0)) → c(COND(odd(s(z0)), z0), ODD(s(z0)))

Defined Rule Symbols:

cond, odd, p

Defined Pair Symbols:

ODD, COND

Compound Symbols:

c3, c, c, c

68.02/43.37

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

Removed 1 trailing tuple parts

68.02/43.37

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), p(s(s(z0)))), ODD(s(s(z0)))) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0))

S tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), p(s(s(z0)))), ODD(s(s(z0)))) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0))))

K tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(z0)) → c(COND(odd(s(z0)), z0), ODD(s(z0)))

Defined Rule Symbols:

cond, odd, p

Defined Pair Symbols:

ODD, COND

Compound Symbols:

c3, c, c, c

68.02/43.37

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

Removed 1 trailing nodes:

COND(true, 0) → c

68.02/43.37

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), p(s(s(z0)))), ODD(s(s(z0)))) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0))

S tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), p(s(s(z0)))), ODD(s(s(z0)))) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, s(0)) → c(COND(true, 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

68.02/43.37

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

Use narrowing to replace COND(true, s(s(z0))) → c(COND(odd(z0), p(s(s(z0)))), ODD(s(s(z0)))) by

COND(true, s(s(x0))) → c(COND(odd(x0), s(x0)), ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(COND(false, p(s(s(0)))), ODD(s(s(0)))) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0))))

68.02/43.37

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(0))) → c(COND(false, p(s(s(0)))), ODD(s(s(0)))) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0))))

S tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(s(x0))) → c(COND(odd(x0), s(x0)), ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(COND(false, p(s(s(0)))), ODD(s(s(0)))) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
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

68.02/43.37

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

Removed 1 trailing tuple parts

68.02/43.37

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0))))

S tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(s(x0))) → c(COND(odd(x0), s(x0)), ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
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

68.02/43.37

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

Removed 1 trailing nodes:

COND(true, 0) → c

68.02/43.37

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0))))

S tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(s(x0))) → c(COND(odd(x0), s(x0)), ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
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

68.02/43.37

(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)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0))))

We considered the (Usable) Rules:

odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(s(z0)) → z0

And the Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0))))

The order we found is given by the following interpretation:
Polynomial interpretation : 68.02/43.37

POL(0) = [5] 68.02/43.37
POL(COND(x₁, x₂)) = [2] 68.02/43.37
POL(ODD(x₁)) = 0 68.02/43.37
POL(c) = 0 68.02/43.37
POL(c(x₁)) = x₁ 68.02/43.37
POL(c(x₁, x₂)) = x₁ + x₂ 68.02/43.37
POL(c3(x₁)) = x₁ 68.02/43.37
POL(false) = [5] 68.02/43.37
POL(odd(x₁)) = [5] + x₁ 68.02/43.37
POL(p(x₁)) = [1] 68.02/43.37
POL(s(x₁)) = 0 68.02/43.37
POL(true) = 0

68.02/43.37

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0))))

S tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(s(x0))) → c(COND(odd(x0), s(x0)), ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))

K tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
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

68.02/43.37

(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), s(z0)), ODD(s(s(z0))))

We considered the (Usable) Rules:

odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(s(z0)) → z0

And the Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0))))

The order we found is given by the following interpretation:
Polynomial interpretation : 68.02/43.37

POL(0) = [1] 68.02/43.37
POL(COND(x₁, x₂)) = [2]x₂ 68.02/43.37
POL(ODD(x₁)) = 0 68.02/43.37
POL(c) = 0 68.02/43.37
POL(c(x₁)) = x₁ 68.02/43.37
POL(c(x₁, x₂)) = x₁ + x₂ 68.02/43.37
POL(c3(x₁)) = x₁ 68.02/43.37
POL(false) = 0 68.02/43.37
POL(odd(x₁)) = 0 68.02/43.37
POL(p(x₁)) = x₁ 68.02/43.37
POL(s(x₁)) = [1] + x₁ 68.02/43.37
POL(true) = 0

68.02/43.37

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0))))

S tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, 0) → c(COND(odd(0), 0)) 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))

K tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0))))

Defined Rule Symbols:

cond, odd, p

Defined Pair Symbols:

ODD, COND

Compound Symbols:

c3, c, c, c

68.02/43.37

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

68.02/43.37

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0)))) 68.02/43.37
COND(true, 0) → c(COND(false, 0))

S tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, 0) → c(COND(false, 0))

K tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0))))

Defined Rule Symbols:

cond, odd, p

Defined Pair Symbols:

ODD, COND

Compound Symbols:

c3, c, c, c

68.02/43.37

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

Removed 1 trailing tuple parts

68.02/43.37

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0))))

S tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, 0) → c

K tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0))))

Defined Rule Symbols:

cond, odd, p

Defined Pair Symbols:

ODD, COND

Compound Symbols:

c3, c, c, c

68.02/43.37

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

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

COND(true, 0) → c 68.02/43.37
COND(true, 0) → c

68.02/43.37

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0))))

S tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, s(0)) → c(COND(true, p(s(0)))) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))

K tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0))))

Defined Rule Symbols:

cond, odd, p

Defined Pair Symbols:

ODD, COND

Compound Symbols:

c3, c, c, c

68.02/43.37

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

Use narrowing to replace COND(true, s(0)) → c(COND(true, p(s(0)))) by

COND(true, s(0)) → c(COND(true, 0))

68.02/43.37

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0))))

S tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0))

K tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0))))

Defined Rule Symbols:

cond, odd, p

Defined Pair Symbols:

ODD, COND

Compound Symbols:

c3, c, c, c

68.02/43.37

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

Removed 2 trailing nodes:

COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, 0) → c

68.02/43.37

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0))))

S tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0))

K tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0))))

Defined Rule Symbols:

cond, odd, p

Defined Pair Symbols:

ODD, COND

Compound Symbols:

c3, c, c, c

68.02/43.37

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

We considered the (Usable) Rules:

odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(s(z0)) → z0

And the Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0))))

The order we found is given by the following interpretation:
Polynomial interpretation : 68.02/43.37

POL(0) = 0 68.02/43.37
POL(COND(x₁, x₂)) = [4]x₂ 68.02/43.37
POL(ODD(x₁)) = 0 68.02/43.37
POL(c) = 0 68.02/43.37
POL(c(x₁)) = x₁ 68.02/43.37
POL(c(x₁, x₂)) = x₁ + x₂ 68.02/43.37
POL(c3(x₁)) = x₁ 68.02/43.37
POL(false) = [3] 68.02/43.37
POL(odd(x₁)) = 0 68.02/43.37
POL(p(x₁)) = x₁ 68.02/43.37
POL(s(x₁)) = [4] + x₁ 68.02/43.37
POL(true) = 0

68.02/43.37

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0))))

S tuples:

ODD(s(s(z0))) → c3(ODD(z0)) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0))))))

K tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0))

Defined Rule Symbols:

cond, odd, p

Defined Pair Symbols:

ODD, COND

Compound Symbols:

c3, c, c, c

68.02/43.37

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

68.02/43.37

(44) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0)))) 68.02/43.37
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))

S tuples:

COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))), ODD(s(s(s(0))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0))))

K tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(0))) → c(ODD(s(s(0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0))

Defined Rule Symbols:

cond, odd, p

Defined Pair Symbols:

COND, ODD

Compound Symbols:

c, c, c, c3

68.02/43.37

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

Removed 2 trailing tuple parts

68.02/43.37

(46) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0)))) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0)))))) 68.02/43.37
COND(true, s(s(0))) → c

S tuples:

COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0)))) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))))

K tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(0))) → c

Defined Rule Symbols:

cond, odd, p

Defined Pair Symbols:

COND, ODD

Compound Symbols:

c, c, c, c3

68.02/43.37

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

Removed 3 trailing nodes:

COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(s(0))) → c

68.02/43.37

(48) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0)))) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0)))))) 68.02/43.37
COND(true, s(s(0))) → c

S tuples:

COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) 68.02/43.37
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0)))) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))))

K tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(0))) → c

Defined Rule Symbols:

cond, odd, p

Defined Pair Symbols:

COND, ODD

Compound Symbols:

c, c, c, c3

68.02/43.37

(49) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), p(s(s(s(s(z0)))))), ODD(s(s(s(s(z0)))))) by COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), s(s(s(z0)))), ODD(s(s(s(s(z0))))))

68.02/43.37

(50) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0)))) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0)))))) 68.02/43.37
COND(true, s(s(0))) → c 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), s(s(s(z0)))), ODD(s(s(s(s(z0))))))

S tuples:

ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0)))) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0)))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), s(s(s(z0)))), ODD(s(s(s(s(z0))))))

K tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(0))) → c

Defined Rule Symbols:

cond, odd, p

Defined Pair Symbols:

COND, ODD

Compound Symbols:

c, c, c, c3

68.02/43.37

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

Removed 3 trailing nodes:

COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, 0) → c 68.02/43.37
COND(true, s(s(0))) → c

68.02/43.37

(52) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.37
odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(0) → 0 68.02/43.37
p(s(z0)) → z0

Tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0)))) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0)))))) 68.02/43.37
COND(true, s(s(0))) → c 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), s(s(s(z0)))), ODD(s(s(s(s(z0))))))

S tuples:

ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0)))) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0)))))) 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), s(s(s(z0)))), ODD(s(s(s(s(z0))))))

K tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(0))) → c

Defined Rule Symbols:

cond, odd, p

Defined Pair Symbols:

COND, ODD

Compound Symbols:

c, c, c, c3

68.02/43.37

(53) 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), s(s(s(z0)))), ODD(s(s(s(s(z0))))))

We considered the (Usable) Rules:

odd(0) → false 68.02/43.37
odd(s(0)) → true 68.02/43.37
odd(s(s(z0))) → odd(z0) 68.02/43.37
p(s(z0)) → z0

And the Tuples:

COND(true, 0) → c 68.02/43.37
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.37
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.37
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.37
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0)))) 68.02/43.37
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0)))))) 68.02/43.37
COND(true, s(s(0))) → c 68.02/43.37
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), s(s(s(z0)))), ODD(s(s(s(s(z0))))))

The order we found is given by the following interpretation:
Polynomial interpretation : 68.02/43.37

POL(0) = 0 68.02/43.37
POL(COND(x₁, x₂)) = [4] + [4]x₂ 68.02/43.37
POL(ODD(x₁)) = [5] 68.02/43.37
POL(c) = 0 68.02/43.37
POL(c(x₁)) = x₁ 68.02/43.37
POL(c(x₁, x₂)) = x₁ + x₂ 68.02/43.37
POL(c3(x₁)) = x₁ 68.02/43.37
POL(false) = 0 68.02/43.37
POL(odd(x₁)) = [2]x₁ 68.02/43.37
POL(p(x₁)) = x₁ 68.02/43.37
POL(s(x₁)) = [3] + x₁ 68.02/43.37
POL(true) = 0

68.02/43.37

(54) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.38
odd(0) → false 68.02/43.38
odd(s(0)) → true 68.02/43.38
odd(s(s(z0))) → odd(z0) 68.02/43.38
p(0) → 0 68.02/43.38
p(s(z0)) → z0

Tuples:

COND(true, 0) → c 68.02/43.38
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.38
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.38
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.38
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0)))) 68.02/43.38
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0)))))) 68.02/43.38
COND(true, s(s(0))) → c 68.02/43.38
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), s(s(s(z0)))), ODD(s(s(s(s(z0))))))

S tuples:

ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0)))) 68.02/43.38
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))))

K tuples:

COND(true, 0) → c 68.02/43.38
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.38
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.38
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.38
COND(true, s(s(0))) → c 68.02/43.38
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), 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

68.02/43.38

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

odd(0) → false 68.02/43.38
odd(s(0)) → true 68.02/43.38
odd(s(s(z0))) → odd(z0) 68.02/43.38
p(s(z0)) → z0

And the Tuples:

COND(true, 0) → c 68.02/43.38
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.38
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.38
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.38
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0)))) 68.02/43.38
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0)))))) 68.02/43.38
COND(true, s(s(0))) → c 68.02/43.38
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), s(s(s(z0)))), ODD(s(s(s(s(z0))))))

The order we found is given by the following interpretation:
Polynomial interpretation : 68.02/43.38

POL(0) = [2] 68.02/43.38
POL(COND(x₁, x₂)) = [2]x₂² + [2]x₁·x₂ 68.02/43.38
POL(ODD(x₁)) = [2]x₁ 68.02/43.38
POL(c) = 0 68.02/43.38
POL(c(x₁)) = x₁ 68.02/43.38
POL(c(x₁, x₂)) = x₁ + x₂ 68.02/43.38
POL(c3(x₁)) = x₁ 68.02/43.38
POL(false) = [2] 68.02/43.38
POL(odd(x₁)) = [3] 68.02/43.38
POL(p(x₁)) = x₁ 68.02/43.38
POL(s(x₁)) = [2] + x₁ 68.02/43.38
POL(true) = 0

68.02/43.38

(56) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.38
odd(0) → false 68.02/43.38
odd(s(0)) → true 68.02/43.38
odd(s(s(z0))) → odd(z0) 68.02/43.38
p(0) → 0 68.02/43.38
p(s(z0)) → z0

Tuples:

COND(true, 0) → c 68.02/43.38
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.38
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.38
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.38
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0)))) 68.02/43.38
COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0)))))) 68.02/43.38
COND(true, s(s(0))) → c 68.02/43.38
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), s(s(s(z0)))), ODD(s(s(s(s(z0))))))

S tuples:

COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0))))))

K tuples:

COND(true, 0) → c 68.02/43.38
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.38
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.38
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.38
COND(true, s(s(0))) → c 68.02/43.38
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), s(s(s(z0)))), ODD(s(s(s(s(z0)))))) 68.02/43.38
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, c, c3

68.02/43.38

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

Used rewriting to replace COND(true, s(s(s(0)))) → c(COND(true, p(s(s(s(0)))))) by COND(true, s(s(s(0)))) → c(COND(true, s(s(0))))

68.02/43.38

(58) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.38
odd(0) → false 68.02/43.38
odd(s(0)) → true 68.02/43.38
odd(s(s(z0))) → odd(z0) 68.02/43.38
p(0) → 0 68.02/43.38
p(s(z0)) → z0

Tuples:

COND(true, 0) → c 68.02/43.38
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.38
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.38
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.38
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0)))) 68.02/43.38
COND(true, s(s(0))) → c 68.02/43.38
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), s(s(s(z0)))), ODD(s(s(s(s(z0)))))) 68.02/43.38
COND(true, s(s(s(0)))) → c(COND(true, s(s(0))))

S tuples:

COND(true, s(s(s(0)))) → c(COND(true, s(s(0))))

K tuples:

COND(true, 0) → c 68.02/43.38
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.38
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.38
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.38
COND(true, s(s(0))) → c 68.02/43.38
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), s(s(s(z0)))), ODD(s(s(s(s(z0)))))) 68.02/43.38
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, c, c3

68.02/43.38

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

Removed 3 trailing nodes:

COND(true, s(0)) → c(COND(true, 0)) 68.02/43.38
COND(true, 0) → c 68.02/43.38
COND(true, s(s(0))) → c

68.02/43.38

(60) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0) → cond(odd(z0), p(z0)) 68.02/43.38
odd(0) → false 68.02/43.38
odd(s(0)) → true 68.02/43.38
odd(s(s(z0))) → odd(z0) 68.02/43.38
p(0) → 0 68.02/43.38
p(s(z0)) → z0

Tuples:

COND(true, 0) → c 68.02/43.38
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.38
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.38
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.38
ODD(s(s(s(s(y0))))) → c3(ODD(s(s(y0)))) 68.02/43.38
COND(true, s(s(0))) → c 68.02/43.38
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), s(s(s(z0)))), ODD(s(s(s(s(z0)))))) 68.02/43.38
COND(true, s(s(s(0)))) → c(COND(true, s(s(0))))

S tuples:

COND(true, s(s(s(0)))) → c(COND(true, s(s(0))))

K tuples:

COND(true, 0) → c 68.02/43.38
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.38
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.38
COND(true, s(0)) → c(COND(true, 0)) 68.02/43.38
COND(true, s(s(0))) → c 68.02/43.38
COND(true, s(s(s(s(z0))))) → c(COND(odd(z0), s(s(s(z0)))), ODD(s(s(s(s(z0)))))) 68.02/43.38
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, c, c3

68.02/43.38

(61) CdtKnowledgeProof (EQUIVALENT transformation)

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

COND(true, s(s(s(0)))) → c(COND(true, s(s(0)))) 68.02/43.38
COND(true, s(s(z0))) → c(COND(odd(z0), s(z0)), ODD(s(s(z0)))) 68.02/43.38
COND(true, s(s(x0))) → c(COND(odd(x0), s(x0)), ODD(s(s(x0)))) 68.02/43.38
COND(true, s(s(x0))) → c(ODD(s(s(x0)))) 68.02/43.38
COND(true, s(s(0))) → c

Now S is empty

68.02/43.38

(62) BOUNDS(O(1), O(1))

68.02/43.38