164.72/123.60 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml

164.72/123.60

164.72/123.60
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), INFINITE).

0 CpxTRS

164.72/123.60

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

164.72/123.60

↳2 CdtProblem

164.72/123.60

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

164.72/123.60

↳4 CdtProblem

164.72/123.60

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

164.72/123.60

↳6 CdtProblem

164.72/123.60

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

164.72/123.60

↳8 CdtProblem

164.72/123.60

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

164.72/123.60

↳10 CdtProblem

164.72/123.60

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

164.72/123.60

↳12 CdtProblem

164.72/123.60

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

164.72/123.60

↳14 CdtProblem

164.72/123.60

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

164.72/123.60

↳16 CdtProblem

164.72/123.60

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

164.72/123.60

↳18 CdtProblem

164.72/123.60

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

164.72/123.60

↳20 CdtProblem

164.72/123.60

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

164.72/123.60

↳22 CdtProblem

164.72/123.60

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

164.72/123.60

↳24 CdtProblem

164.72/123.60

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

164.72/123.60

↳26 CdtProblem

164.72/123.60

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

164.72/123.60

↳28 CdtProblem

164.72/123.60

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

164.72/123.60

↳30 CdtProblem

164.72/123.60

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

164.72/123.60

↳32 CdtProblem

164.72/123.60

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

164.72/123.60

↳34 CdtProblem

164.72/123.60

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

164.72/123.60

↳36 CdtProblem

164.72/123.60

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

164.72/123.60

↳38 CdtProblem

164.72/123.60

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

164.72/123.60

↳40 CdtProblem

164.72/123.60

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

164.72/123.60

↳42 CdtProblem

164.72/123.60

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

164.72/123.60

↳44 CdtProblem

164.72/123.60

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

164.72/123.60

↳46 CdtProblem

164.72/123.60

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

164.72/123.60

↳48 CdtProblem

164.72/123.60

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

164.72/123.60

↳50 CdtProblem

164.72/123.60

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

164.72/123.60

↳52 CdtProblem

164.72/123.60

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

164.72/123.60

↳54 CdtProblem

164.72/123.60

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

164.72/123.60

↳56 CdtProblem

164.72/123.60

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

164.72/123.60

↳58 CdtProblem

164.72/123.60

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

164.72/123.60

↳60 CdtProblem

164.72/123.60

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

164.72/123.60

↳62 CdtProblem

164.72/123.60

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

164.72/123.60

↳64 CdtProblem

164.72/123.60

164.72/123.60 164.72/123.60

164.72/123.60

(0) Obligation:

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

minus(x, 0) → x 164.72/123.60
minus(s(x), s(y)) → minus(x, y) 164.72/123.60
double(0) → 0 164.72/123.60
double(s(x)) → s(s(double(x))) 164.72/123.60
plus(0, y) → y 164.72/123.60
plus(s(x), y) → s(plus(x, y)) 164.72/123.60
plus(s(x), y) → plus(x, s(y)) 164.72/123.60
plus(s(x), y) → s(plus(minus(x, y), double(y)))

Rewrite Strategy: INNERMOST

164.72/123.60

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

Converted CpxTRS to CDT

164.72/123.60

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.72/123.60
minus(s(z0), s(z1)) → minus(z0, z1) 164.72/123.60
double(0) → 0 164.72/123.60
double(s(z0)) → s(s(double(z0))) 164.72/123.60
plus(0, z0) → z0 164.72/123.60
plus(s(z0), z1) → s(plus(z0, z1)) 164.72/123.60
plus(s(z0), z1) → plus(z0, s(z1)) 164.72/123.60
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1)) 164.72/123.60
DOUBLE(s(z0)) → c3(DOUBLE(z0)) 164.72/123.60
PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.72/123.60
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.72/123.60
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1))

S tuples:

MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1)) 164.72/123.60
DOUBLE(s(z0)) → c3(DOUBLE(z0)) 164.72/123.60
PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.72/123.60
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.72/123.60
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1))

K tuples:none
Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

MINUS, DOUBLE, PLUS

Compound Symbols:

c1, c3, c5, c6, c7

164.72/123.60

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

PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.72/123.60
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.72/123.60
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1))

We considered the (Usable) Rules:

minus(z0, 0) → z0 164.72/123.60
minus(s(z0), s(z1)) → minus(z0, z1) 164.72/123.60
double(0) → 0 164.72/123.60
double(s(z0)) → s(s(double(z0)))

And the Tuples:

MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1)) 164.72/123.60
DOUBLE(s(z0)) → c3(DOUBLE(z0)) 164.72/123.60
PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.72/123.60
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.72/123.60
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1))

The order we found is given by the following interpretation:
Polynomial interpretation : 164.72/123.60

POL(0) = 0 164.72/123.60
POL(DOUBLE(x₁)) = 0 164.72/123.60
POL(MINUS(x₁, x₂)) = 0 164.72/123.60
POL(PLUS(x₁, x₂)) = [4]x₁ 164.72/123.60
POL(c1(x₁)) = x₁ 164.72/123.60
POL(c3(x₁)) = x₁ 164.72/123.60
POL(c5(x₁)) = x₁ 164.72/123.60
POL(c6(x₁)) = x₁ 164.72/123.60
POL(c7(x₁, x₂, x₃)) = x₁ + x₂ + x₃ 164.72/123.60
POL(double(x₁)) = [5]x₁ 164.72/123.60
POL(minus(x₁, x₂)) = x₁ 164.72/123.60
POL(s(x₁)) = [2] + x₁

164.72/123.60

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.72/123.60
minus(s(z0), s(z1)) → minus(z0, z1) 164.72/123.60
double(0) → 0 164.72/123.60
double(s(z0)) → s(s(double(z0))) 164.72/123.60
plus(0, z0) → z0 164.72/123.60
plus(s(z0), z1) → s(plus(z0, z1)) 164.72/123.60
plus(s(z0), z1) → plus(z0, s(z1)) 164.72/123.60
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1)) 164.72/123.60
DOUBLE(s(z0)) → c3(DOUBLE(z0)) 164.72/123.60
PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.72/123.60
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.72/123.60
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1))

S tuples:

MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1)) 164.72/123.60
DOUBLE(s(z0)) → c3(DOUBLE(z0))

K tuples:

PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.72/123.60
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.72/123.60
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

MINUS, DOUBLE, PLUS

Compound Symbols:

c1, c3, c5, c6, c7

164.72/123.60

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

MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1))

We considered the (Usable) Rules:

minus(z0, 0) → z0 164.72/123.60
minus(s(z0), s(z1)) → minus(z0, z1) 164.72/123.60
double(0) → 0 164.72/123.60
double(s(z0)) → s(s(double(z0)))

And the Tuples:

MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1)) 164.72/123.60
DOUBLE(s(z0)) → c3(DOUBLE(z0)) 164.72/123.60
PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.72/123.60
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.72/123.60
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1))

The order we found is given by the following interpretation:
Polynomial interpretation : 164.72/123.60

POL(0) = [1] 164.72/123.60
POL(DOUBLE(x₁)) = [3] 164.72/123.60
POL(MINUS(x₁, x₂)) = [3] + x₁ 164.72/123.60
POL(PLUS(x₁, x₂)) = [2]x₁² 164.72/123.60
POL(c1(x₁)) = x₁ 164.72/123.60
POL(c3(x₁)) = x₁ 164.72/123.60
POL(c5(x₁)) = x₁ 164.72/123.60
POL(c6(x₁)) = x₁ 164.72/123.60
POL(c7(x₁, x₂, x₃)) = x₁ + x₂ + x₃ 164.72/123.60
POL(double(x₁)) = 0 164.72/123.60
POL(minus(x₁, x₂)) = x₁ 164.72/123.60
POL(s(x₁)) = [2] + x₁

164.72/123.60

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.72/123.60
minus(s(z0), s(z1)) → minus(z0, z1) 164.72/123.60
double(0) → 0 164.72/123.60
double(s(z0)) → s(s(double(z0))) 164.72/123.60
plus(0, z0) → z0 164.72/123.60
plus(s(z0), z1) → s(plus(z0, z1)) 164.72/123.60
plus(s(z0), z1) → plus(z0, s(z1)) 164.72/123.60
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1)) 164.72/123.60
DOUBLE(s(z0)) → c3(DOUBLE(z0)) 164.72/123.60
PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.72/123.60
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.72/123.60
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1))

S tuples:

DOUBLE(s(z0)) → c3(DOUBLE(z0))

K tuples:

PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.72/123.60
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.72/123.60
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 164.72/123.60
MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

MINUS, DOUBLE, PLUS

Compound Symbols:

c1, c3, c5, c6, c7

164.72/123.60

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

Use narrowing to replace PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) by

PLUS(s(x0), 0) → c7(PLUS(minus(x0, 0), 0), MINUS(x0, 0), DOUBLE(0)) 164.72/123.60
PLUS(s(x0), s(z0)) → c7(PLUS(minus(x0, s(z0)), s(s(double(z0)))), MINUS(x0, s(z0)), DOUBLE(s(z0))) 164.72/123.60
PLUS(s(z0), 0) → c7(PLUS(z0, double(0)), MINUS(z0, 0), DOUBLE(0)) 164.72/123.60
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), double(s(z1))), MINUS(s(z0), s(z1)), DOUBLE(s(z1)))

164.72/123.60

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.72/123.60
minus(s(z0), s(z1)) → minus(z0, z1) 164.72/123.60
double(0) → 0 164.72/123.60
double(s(z0)) → s(s(double(z0))) 164.72/123.60
plus(0, z0) → z0 164.72/123.60
plus(s(z0), z1) → s(plus(z0, z1)) 164.72/123.60
plus(s(z0), z1) → plus(z0, s(z1)) 164.72/123.60
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1)) 164.72/123.60
DOUBLE(s(z0)) → c3(DOUBLE(z0)) 164.72/123.60
PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.72/123.60
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.72/123.60
PLUS(s(x0), 0) → c7(PLUS(minus(x0, 0), 0), MINUS(x0, 0), DOUBLE(0)) 164.72/123.60
PLUS(s(x0), s(z0)) → c7(PLUS(minus(x0, s(z0)), s(s(double(z0)))), MINUS(x0, s(z0)), DOUBLE(s(z0))) 164.72/123.60
PLUS(s(z0), 0) → c7(PLUS(z0, double(0)), MINUS(z0, 0), DOUBLE(0)) 164.72/123.60
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), double(s(z1))), MINUS(s(z0), s(z1)), DOUBLE(s(z1)))

S tuples:

DOUBLE(s(z0)) → c3(DOUBLE(z0))

K tuples:

PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.72/123.60
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.72/123.60
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 164.72/123.60
MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

MINUS, DOUBLE, PLUS

Compound Symbols:

c1, c3, c5, c6, c7

164.72/123.60

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

Removed 4 trailing tuple parts

164.72/123.60

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.72/123.60
minus(s(z0), s(z1)) → minus(z0, z1) 164.72/123.60
double(0) → 0 164.72/123.60
double(s(z0)) → s(s(double(z0))) 164.72/123.60
plus(0, z0) → z0 164.72/123.60
plus(s(z0), z1) → s(plus(z0, z1)) 164.72/123.60
plus(s(z0), z1) → plus(z0, s(z1)) 164.72/123.60
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1)) 164.72/123.60
DOUBLE(s(z0)) → c3(DOUBLE(z0)) 164.72/123.60
PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.72/123.60
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.72/123.60
PLUS(s(x0), s(z0)) → c7(PLUS(minus(x0, s(z0)), s(s(double(z0)))), MINUS(x0, s(z0)), DOUBLE(s(z0))) 164.72/123.60
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), double(s(z1))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.72/123.60
PLUS(s(x0), 0) → c7(PLUS(minus(x0, 0), 0)) 164.72/123.60
PLUS(s(z0), 0) → c7(PLUS(z0, double(0)))

S tuples:

DOUBLE(s(z0)) → c3(DOUBLE(z0))

K tuples:

PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.72/123.60
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.72/123.60
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 164.72/123.60
MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

MINUS, DOUBLE, PLUS

Compound Symbols:

c1, c3, c5, c6, c7, c7

164.72/123.60

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

Use narrowing to replace PLUS(s(x0), s(z0)) → c7(PLUS(minus(x0, s(z0)), s(s(double(z0)))), MINUS(x0, s(z0)), DOUBLE(s(z0))) by

PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0))), MINUS(x0, s(0)), DOUBLE(s(0))) 164.72/123.60
PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 164.72/123.60
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.72/123.60
PLUS(s(x0), s(x1)) → c7(DOUBLE(s(x1)))

164.72/123.60

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.72/123.60
minus(s(z0), s(z1)) → minus(z0, z1) 164.72/123.60
double(0) → 0 164.72/123.60
double(s(z0)) → s(s(double(z0))) 164.72/123.60
plus(0, z0) → z0 164.72/123.60
plus(s(z0), z1) → s(plus(z0, z1)) 164.72/123.60
plus(s(z0), z1) → plus(z0, s(z1)) 164.72/123.60
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1)) 164.72/123.60
DOUBLE(s(z0)) → c3(DOUBLE(z0)) 164.72/123.60
PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.72/123.60
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.72/123.60
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), double(s(z1))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.72/123.60
PLUS(s(x0), 0) → c7(PLUS(minus(x0, 0), 0)) 164.72/123.60
PLUS(s(z0), 0) → c7(PLUS(z0, double(0))) 164.72/123.60
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0))), MINUS(x0, s(0)), DOUBLE(s(0))) 164.72/123.60
PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 164.72/123.60
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.72/123.60
PLUS(s(x0), s(x1)) → c7(DOUBLE(s(x1)))

S tuples:

DOUBLE(s(z0)) → c3(DOUBLE(z0))

K tuples:

PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.72/123.60
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.72/123.60
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 164.72/123.60
MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

MINUS, DOUBLE, PLUS

Compound Symbols:

c1, c3, c5, c6, c7, c7

164.72/123.60

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

Use narrowing to replace PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), double(s(z1))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) by

PLUS(s(s(x0)), s(z0)) → c7(PLUS(minus(x0, z0), s(s(double(z0)))), MINUS(s(x0), s(z0)), DOUBLE(s(z0))) 164.72/123.60
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, double(s(0))), MINUS(s(z0), s(0)), DOUBLE(s(0))) 164.72/123.60
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), double(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1))))

164.72/123.60

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.92/123.64
minus(s(z0), s(z1)) → minus(z0, z1) 164.92/123.64
double(0) → 0 164.92/123.64
double(s(z0)) → s(s(double(z0))) 164.92/123.64
plus(0, z0) → z0 164.92/123.64
plus(s(z0), z1) → s(plus(z0, z1)) 164.92/123.64
plus(s(z0), z1) → plus(z0, s(z1)) 164.92/123.64
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1)) 164.92/123.64
DOUBLE(s(z0)) → c3(DOUBLE(z0)) 164.92/123.64
PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.92/123.64
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.92/123.64
PLUS(s(x0), 0) → c7(PLUS(minus(x0, 0), 0)) 164.92/123.64
PLUS(s(z0), 0) → c7(PLUS(z0, double(0))) 164.92/123.64
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0))), MINUS(x0, s(0)), DOUBLE(s(0))) 164.92/123.64
PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 164.92/123.64
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.92/123.64
PLUS(s(x0), s(x1)) → c7(DOUBLE(s(x1))) 164.92/123.64
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, double(s(0))), MINUS(s(z0), s(0)), DOUBLE(s(0))) 164.92/123.64
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), double(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1))))

S tuples:

DOUBLE(s(z0)) → c3(DOUBLE(z0))

K tuples:

PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.92/123.64
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.92/123.64
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 164.92/123.64
MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

MINUS, DOUBLE, PLUS

Compound Symbols:

c1, c3, c5, c6, c7, c7

164.92/123.64

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

Use narrowing to replace PLUS(s(x0), 0) → c7(PLUS(minus(x0, 0), 0)) by

PLUS(s(z0), 0) → c7(PLUS(z0, 0))

164.92/123.64

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.92/123.64
minus(s(z0), s(z1)) → minus(z0, z1) 164.92/123.64
double(0) → 0 164.92/123.64
double(s(z0)) → s(s(double(z0))) 164.92/123.64
plus(0, z0) → z0 164.92/123.64
plus(s(z0), z1) → s(plus(z0, z1)) 164.92/123.64
plus(s(z0), z1) → plus(z0, s(z1)) 164.92/123.64
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1)) 164.92/123.64
DOUBLE(s(z0)) → c3(DOUBLE(z0)) 164.92/123.64
PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.92/123.64
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.92/123.64
PLUS(s(z0), 0) → c7(PLUS(z0, double(0))) 164.92/123.64
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0))), MINUS(x0, s(0)), DOUBLE(s(0))) 164.92/123.64
PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 164.92/123.64
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.92/123.64
PLUS(s(x0), s(x1)) → c7(DOUBLE(s(x1))) 164.92/123.64
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, double(s(0))), MINUS(s(z0), s(0)), DOUBLE(s(0))) 164.92/123.64
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), double(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 164.92/123.64
PLUS(s(z0), 0) → c7(PLUS(z0, 0))

S tuples:

DOUBLE(s(z0)) → c3(DOUBLE(z0))

K tuples:

PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.92/123.64
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.92/123.64
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 164.92/123.64
MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

MINUS, DOUBLE, PLUS

Compound Symbols:

c1, c3, c5, c6, c7, c7

164.92/123.64

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

Use narrowing to replace PLUS(s(z0), 0) → c7(PLUS(z0, double(0))) by

PLUS(s(x0), 0) → c7(PLUS(x0, 0))

164.92/123.64

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.92/123.64
minus(s(z0), s(z1)) → minus(z0, z1) 164.92/123.64
double(0) → 0 164.92/123.64
double(s(z0)) → s(s(double(z0))) 164.92/123.64
plus(0, z0) → z0 164.92/123.64
plus(s(z0), z1) → s(plus(z0, z1)) 164.92/123.64
plus(s(z0), z1) → plus(z0, s(z1)) 164.92/123.64
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1)) 164.92/123.64
DOUBLE(s(z0)) → c3(DOUBLE(z0)) 164.92/123.64
PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.92/123.64
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.92/123.64
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0))), MINUS(x0, s(0)), DOUBLE(s(0))) 164.92/123.64
PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 164.92/123.64
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.92/123.64
PLUS(s(x0), s(x1)) → c7(DOUBLE(s(x1))) 164.92/123.64
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, double(s(0))), MINUS(s(z0), s(0)), DOUBLE(s(0))) 164.92/123.64
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), double(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 164.92/123.64
PLUS(s(z0), 0) → c7(PLUS(z0, 0))

S tuples:

DOUBLE(s(z0)) → c3(DOUBLE(z0))

K tuples:

PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.92/123.64
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.92/123.64
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 164.92/123.64
MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

MINUS, DOUBLE, PLUS

Compound Symbols:

c1, c3, c5, c6, c7, c7

164.92/123.64

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

Use forward instantiation to replace MINUS(s(z0), s(z1)) → c1(MINUS(z0, z1)) by

MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1)))

164.92/123.64

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.92/123.64
minus(s(z0), s(z1)) → minus(z0, z1) 164.92/123.64
double(0) → 0 164.92/123.64
double(s(z0)) → s(s(double(z0))) 164.92/123.64
plus(0, z0) → z0 164.92/123.64
plus(s(z0), z1) → s(plus(z0, z1)) 164.92/123.64
plus(s(z0), z1) → plus(z0, s(z1)) 164.92/123.64
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

DOUBLE(s(z0)) → c3(DOUBLE(z0)) 164.92/123.64
PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.92/123.64
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.92/123.64
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0))), MINUS(x0, s(0)), DOUBLE(s(0))) 164.92/123.64
PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 164.92/123.64
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.92/123.64
PLUS(s(x0), s(x1)) → c7(DOUBLE(s(x1))) 164.92/123.64
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, double(s(0))), MINUS(s(z0), s(0)), DOUBLE(s(0))) 164.92/123.64
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), double(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 164.92/123.64
PLUS(s(z0), 0) → c7(PLUS(z0, 0)) 164.92/123.64
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1)))

S tuples:

DOUBLE(s(z0)) → c3(DOUBLE(z0))

K tuples:

PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.92/123.64
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.92/123.64
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 164.92/123.64
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1)))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

DOUBLE, PLUS, MINUS

Compound Symbols:

c3, c5, c6, c7, c7, c1

164.92/123.64

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

Removed 2 trailing tuple parts

164.92/123.64

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.92/123.64
minus(s(z0), s(z1)) → minus(z0, z1) 164.92/123.64
double(0) → 0 164.92/123.64
double(s(z0)) → s(s(double(z0))) 164.92/123.64
plus(0, z0) → z0 164.92/123.64
plus(s(z0), z1) → s(plus(z0, z1)) 164.92/123.64
plus(s(z0), z1) → plus(z0, s(z1)) 164.92/123.64
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

DOUBLE(s(z0)) → c3(DOUBLE(z0)) 164.92/123.64
PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.92/123.64
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.92/123.64
PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 164.92/123.64
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.92/123.64
PLUS(s(x0), s(x1)) → c7(DOUBLE(s(x1))) 164.92/123.64
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), double(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 164.92/123.64
PLUS(s(z0), 0) → c7(PLUS(z0, 0)) 164.92/123.64
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1))) 164.92/123.64
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0))), DOUBLE(s(0))) 164.92/123.64
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, double(s(0))), DOUBLE(s(0)))

S tuples:

DOUBLE(s(z0)) → c3(DOUBLE(z0))

K tuples:

PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.92/123.64
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.92/123.64
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 164.92/123.64
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1)))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

DOUBLE, PLUS, MINUS

Compound Symbols:

c3, c5, c6, c7, c7, c1, c7

164.92/123.64

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

Use forward instantiation to replace DOUBLE(s(z0)) → c3(DOUBLE(z0)) by

DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0)))

164.92/123.64

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.92/123.64
minus(s(z0), s(z1)) → minus(z0, z1) 164.92/123.64
double(0) → 0 164.92/123.64
double(s(z0)) → s(s(double(z0))) 164.92/123.64
plus(0, z0) → z0 164.92/123.64
plus(s(z0), z1) → s(plus(z0, z1)) 164.92/123.64
plus(s(z0), z1) → plus(z0, s(z1)) 164.92/123.64
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.92/123.64
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.92/123.64
PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 164.92/123.64
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.92/123.64
PLUS(s(x0), s(x1)) → c7(DOUBLE(s(x1))) 164.92/123.64
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), double(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 164.92/123.64
PLUS(s(z0), 0) → c7(PLUS(z0, 0)) 164.92/123.64
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1))) 164.92/123.64
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0))), DOUBLE(s(0))) 164.92/123.64
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, double(s(0))), DOUBLE(s(0))) 164.92/123.64
DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0)))

S tuples:

DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0)))

K tuples:

PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.92/123.65
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.92/123.65
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 164.92/123.65
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1)))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, MINUS, DOUBLE

Compound Symbols:

c5, c6, c7, c7, c1, c7, c3

164.92/123.65

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

Removed 2 trailing tuple parts

164.92/123.65

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.92/123.65
minus(s(z0), s(z1)) → minus(z0, z1) 164.92/123.65
double(0) → 0 164.92/123.65
double(s(z0)) → s(s(double(z0))) 164.92/123.68
plus(0, z0) → z0 164.92/123.68
plus(s(z0), z1) → s(plus(z0, z1)) 164.92/123.68
plus(s(z0), z1) → plus(z0, s(z1)) 164.92/123.68
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.92/123.68
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.92/123.68
PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 164.92/123.68
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.92/123.68
PLUS(s(x0), s(x1)) → c7(DOUBLE(s(x1))) 164.92/123.68
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), double(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 164.92/123.68
PLUS(s(z0), 0) → c7(PLUS(z0, 0)) 164.92/123.68
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1))) 164.92/123.68
DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0))) 164.92/123.68
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0)))) 164.92/123.68
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, double(s(0))))

S tuples:

DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0)))

K tuples:

PLUS(s(z0), z1) → c5(PLUS(z0, z1)) 164.92/123.68
PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.92/123.68
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 164.92/123.68
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1)))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, MINUS, DOUBLE

Compound Symbols:

c5, c6, c7, c7, c1, c3

164.92/123.68

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

Use forward instantiation to replace PLUS(s(z0), z1) → c5(PLUS(z0, z1)) by

PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 164.92/123.68
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 164.92/123.68
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 164.92/123.68
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 164.92/123.68
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.68
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 164.92/123.68
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 164.92/123.68
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0)))

164.92/123.68

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.92/123.68
minus(s(z0), s(z1)) → minus(z0, z1) 164.92/123.68
double(0) → 0 164.92/123.68
double(s(z0)) → s(s(double(z0))) 164.92/123.68
plus(0, z0) → z0 164.92/123.68
plus(s(z0), z1) → s(plus(z0, z1)) 164.92/123.68
plus(s(z0), z1) → plus(z0, s(z1)) 164.92/123.68
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.92/123.68
PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 164.92/123.68
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.92/123.68
PLUS(s(x0), s(x1)) → c7(DOUBLE(s(x1))) 164.92/123.68
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), double(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 164.92/123.68
PLUS(s(z0), 0) → c7(PLUS(z0, 0)) 164.92/123.68
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1))) 164.92/123.68
DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0))) 164.92/123.68
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0)))) 164.92/123.68
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, double(s(0)))) 164.92/123.68
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 164.92/123.68
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 164.92/123.68
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 164.92/123.68
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 164.92/123.68
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.68
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 164.92/123.68
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 164.92/123.68
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0)))

S tuples:

DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0)))

K tuples:

PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.92/123.68
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 164.92/123.68
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1))) 164.92/123.68
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 164.92/123.68
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 164.92/123.68
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 164.92/123.68
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 164.92/123.68
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.68
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 164.92/123.68
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 164.92/123.68
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0)))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, MINUS, DOUBLE

Compound Symbols:

c6, c7, c7, c1, c3, c5

164.92/123.68

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

Used rewriting to replace PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), double(s(s(z1)))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) by PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(double(s(z1))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1))))

164.92/123.68

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.92/123.68
minus(s(z0), s(z1)) → minus(z0, z1) 164.92/123.68
double(0) → 0 164.92/123.68
double(s(z0)) → s(s(double(z0))) 164.92/123.68
plus(0, z0) → z0 164.92/123.68
plus(s(z0), z1) → s(plus(z0, z1)) 164.92/123.68
plus(s(z0), z1) → plus(z0, s(z1)) 164.92/123.68
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.92/123.68
PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 164.92/123.68
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.92/123.68
PLUS(s(x0), s(x1)) → c7(DOUBLE(s(x1))) 164.92/123.68
PLUS(s(z0), 0) → c7(PLUS(z0, 0)) 164.92/123.68
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1))) 164.92/123.68
DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0))) 164.92/123.68
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0)))) 164.92/123.68
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, double(s(0)))) 164.92/123.68
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 164.92/123.68
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 164.92/123.68
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 164.92/123.68
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 164.92/123.68
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.68
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 164.92/123.68
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 164.92/123.68
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 164.92/123.68
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(double(s(z1))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1))))

S tuples:

DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0)))

K tuples:

PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.92/123.68
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 164.92/123.68
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1))) 164.92/123.68
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 164.92/123.68
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 164.92/123.68
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 164.92/123.68
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 164.92/123.68
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.68
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 164.92/123.68
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 164.92/123.68
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0)))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, MINUS, DOUBLE

Compound Symbols:

c6, c7, c7, c1, c3, c5

164.92/123.68

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

Used rewriting to replace PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, double(s(0)))) by PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, s(s(double(0)))))

164.92/123.68

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.92/123.68
minus(s(z0), s(z1)) → minus(z0, z1) 164.92/123.68
double(0) → 0 164.92/123.68
double(s(z0)) → s(s(double(z0))) 164.92/123.68
plus(0, z0) → z0 164.92/123.68
plus(s(z0), z1) → s(plus(z0, z1)) 164.92/123.68
plus(s(z0), z1) → plus(z0, s(z1)) 164.92/123.68
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.92/123.68
PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 164.92/123.68
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.92/123.68
PLUS(s(x0), s(x1)) → c7(DOUBLE(s(x1))) 164.92/123.68
PLUS(s(z0), 0) → c7(PLUS(z0, 0)) 164.92/123.68
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1))) 164.92/123.68
DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0))) 164.92/123.68
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0)))) 164.92/123.68
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 164.92/123.68
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 164.92/123.68
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 164.92/123.68
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 164.92/123.68
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.68
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 164.92/123.69
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 164.92/123.69
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 164.92/123.69
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(double(s(z1))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 164.92/123.69
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, s(s(double(0)))))

S tuples:

DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0)))

K tuples:

PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) 164.92/123.69
PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 164.92/123.69
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1))) 164.92/123.69
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 164.92/123.69
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 164.92/123.69
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 164.92/123.69
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.69
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 164.92/123.69
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 164.92/123.69
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0)))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, MINUS, DOUBLE

Compound Symbols:

c6, c7, c7, c1, c3, c5

164.92/123.69

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

Use forward instantiation to replace PLUS(s(z0), z1) → c6(PLUS(z0, s(z1))) by

PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 164.92/123.69
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 164.92/123.69
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 164.92/123.69
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 164.92/123.69
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 164.92/123.69
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 164.92/123.69
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1))))

164.92/123.69

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.92/123.69
minus(s(z0), s(z1)) → minus(z0, z1) 164.92/123.69
double(0) → 0 164.92/123.69
double(s(z0)) → s(s(double(z0))) 164.92/123.69
plus(0, z0) → z0 164.92/123.69
plus(s(z0), z1) → s(plus(z0, z1)) 164.92/123.69
plus(s(z0), z1) → plus(z0, s(z1)) 164.92/123.69
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 164.92/123.69
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.92/123.69
PLUS(s(x0), s(x1)) → c7(DOUBLE(s(x1))) 164.92/123.69
PLUS(s(z0), 0) → c7(PLUS(z0, 0)) 164.92/123.69
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1))) 164.92/123.69
DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0))) 164.92/123.69
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0)))) 164.92/123.69
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 164.92/123.69
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 164.92/123.69
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 164.92/123.69
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.69
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 164.92/123.69
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 164.92/123.69
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 164.92/123.69
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(double(s(z1))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 164.92/123.69
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, s(s(double(0))))) 164.92/123.69
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 164.92/123.69
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 164.92/123.69
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 164.92/123.69
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 164.92/123.69
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 164.92/123.69
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 164.92/123.69
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1))))

S tuples:

DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0)))

K tuples:

PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 164.92/123.69
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1))) 164.92/123.69
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 164.92/123.69
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 164.92/123.69
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 164.92/123.69
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.69
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 164.92/123.69
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 164.92/123.69
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 164.92/123.69
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 164.92/123.69
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 164.92/123.69
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 164.92/123.69
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 164.92/123.69
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 164.92/123.69
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 164.92/123.69
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1))))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, MINUS, DOUBLE

Compound Symbols:

c7, c7, c1, c3, c5, c6

164.92/123.69

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

Use forward instantiation to replace PLUS(s(x0), s(x1)) → c7(DOUBLE(s(x1))) by

PLUS(s(z0), s(s(y0))) → c7(DOUBLE(s(s(y0))))

164.92/123.69

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.92/123.69
minus(s(z0), s(z1)) → minus(z0, z1) 164.92/123.69
double(0) → 0 164.92/123.69
double(s(z0)) → s(s(double(z0))) 164.92/123.69
plus(0, z0) → z0 164.92/123.69
plus(s(z0), z1) → s(plus(z0, z1)) 164.92/123.69
plus(s(z0), z1) → plus(z0, s(z1)) 164.92/123.69
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 164.92/123.69
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.92/123.69
PLUS(s(z0), 0) → c7(PLUS(z0, 0)) 164.92/123.69
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1))) 164.92/123.69
DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0))) 164.92/123.69
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0)))) 164.92/123.69
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 164.92/123.69
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 164.92/123.69
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 164.92/123.69
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.69
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 164.92/123.69
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 164.92/123.69
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 164.92/123.69
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(double(s(z1))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 164.92/123.69
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, s(s(double(0))))) 164.92/123.69
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 164.92/123.69
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 164.92/123.69
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 164.92/123.69
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 164.92/123.69
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 164.92/123.69
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 164.92/123.69
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.69
PLUS(s(z0), s(s(y0))) → c7(DOUBLE(s(s(y0))))

S tuples:

DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0)))

K tuples:

PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 164.92/123.69
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1))) 164.92/123.69
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 164.92/123.69
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 164.92/123.69
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 164.92/123.69
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.69
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 164.92/123.69
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 164.92/123.69
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 164.92/123.69
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 164.92/123.69
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 164.92/123.69
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 164.92/123.69
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 164.92/123.69
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 164.92/123.69
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 164.92/123.69
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1))))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, MINUS, DOUBLE

Compound Symbols:

c7, c7, c1, c3, c5, c6

164.92/123.69

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

Used rewriting to replace PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(double(s(z1))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) by PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(s(s(double(z1)))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1))))

164.92/123.69

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.92/123.69
minus(s(z0), s(z1)) → minus(z0, z1) 164.92/123.69
double(0) → 0 164.92/123.69
double(s(z0)) → s(s(double(z0))) 164.92/123.69
plus(0, z0) → z0 164.92/123.69
plus(s(z0), z1) → s(plus(z0, z1)) 164.92/123.69
plus(s(z0), z1) → plus(z0, s(z1)) 164.92/123.69
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 164.92/123.69
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.92/123.69
PLUS(s(z0), 0) → c7(PLUS(z0, 0)) 164.92/123.69
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1))) 164.92/123.69
DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0))) 164.92/123.69
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0)))) 164.92/123.69
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 164.92/123.69
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 164.92/123.69
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 164.92/123.69
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.69
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 164.92/123.69
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 164.92/123.69
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 164.92/123.69
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, s(s(double(0))))) 164.92/123.69
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 164.92/123.69
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 164.92/123.69
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 164.92/123.69
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 164.92/123.69
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 164.92/123.69
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 164.92/123.69
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.69
PLUS(s(z0), s(s(y0))) → c7(DOUBLE(s(s(y0)))) 164.92/123.69
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(s(s(double(z1)))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1))))

S tuples:

DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0)))

K tuples:

PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 164.92/123.69
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1))) 164.92/123.69
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 164.92/123.69
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 164.92/123.69
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 164.92/123.69
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.69
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 164.92/123.69
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 164.92/123.69
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 164.92/123.69
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 164.92/123.69
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 164.92/123.69
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 164.92/123.69
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 164.92/123.69
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 164.92/123.69
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 164.92/123.69
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1))))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, MINUS, DOUBLE

Compound Symbols:

c7, c7, c1, c3, c5, c6

164.92/123.69

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

Use forward instantiation to replace PLUS(s(z0), 0) → c7(PLUS(z0, 0)) by

PLUS(s(s(y0)), 0) → c7(PLUS(s(y0), 0)) 164.92/123.69
PLUS(s(s(s(y0))), 0) → c7(PLUS(s(s(y0)), 0)) 164.92/123.69
PLUS(s(s(s(s(y0)))), 0) → c7(PLUS(s(s(s(y0))), 0)) 164.92/123.69
PLUS(s(s(s(s(s(y0))))), 0) → c7(PLUS(s(s(s(s(y0)))), 0))

164.92/123.69

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.92/123.69
minus(s(z0), s(z1)) → minus(z0, z1) 164.92/123.69
double(0) → 0 164.92/123.69
double(s(z0)) → s(s(double(z0))) 164.92/123.69
plus(0, z0) → z0 164.92/123.69
plus(s(z0), z1) → s(plus(z0, z1)) 164.92/123.69
plus(s(z0), z1) → plus(z0, s(z1)) 164.92/123.69
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 164.92/123.69
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.92/123.69
PLUS(s(z0), 0) → c7(PLUS(z0, 0)) 164.92/123.69
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1))) 164.92/123.69
DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0))) 164.92/123.69
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0)))) 164.92/123.69
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 164.92/123.69
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 164.92/123.69
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 164.92/123.69
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.69
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 164.92/123.69
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 164.92/123.69
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 164.92/123.69
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, s(s(double(0))))) 164.92/123.69
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 164.92/123.69
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 164.92/123.69
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 164.92/123.69
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 164.92/123.69
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 164.92/123.69
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 164.92/123.69
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.69
PLUS(s(z0), s(s(y0))) → c7(DOUBLE(s(s(y0)))) 164.92/123.69
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(s(s(double(z1)))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 164.92/123.69
PLUS(s(s(y0)), 0) → c7(PLUS(s(y0), 0)) 164.92/123.69
PLUS(s(s(s(y0))), 0) → c7(PLUS(s(s(y0)), 0)) 164.92/123.69
PLUS(s(s(s(s(y0)))), 0) → c7(PLUS(s(s(s(y0))), 0)) 164.92/123.69
PLUS(s(s(s(s(s(y0))))), 0) → c7(PLUS(s(s(s(s(y0)))), 0))

S tuples:

DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0)))

K tuples:

PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 164.92/123.69
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1))) 164.92/123.69
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 164.92/123.69
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 164.92/123.69
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 164.92/123.69
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.69
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 164.92/123.69
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 164.92/123.69
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 164.92/123.69
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 164.92/123.69
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 164.92/123.69
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 164.92/123.69
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 164.92/123.69
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 164.92/123.69
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 164.92/123.69
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1))))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, MINUS, DOUBLE

Compound Symbols:

c7, c7, c1, c3, c5, c6

164.92/123.69

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

Use forward instantiation to replace PLUS(s(x0), 0) → c7(PLUS(x0, 0)) by

PLUS(s(s(y0)), 0) → c7(PLUS(s(y0), 0)) 164.92/123.69
PLUS(s(s(s(y0))), 0) → c7(PLUS(s(s(y0)), 0)) 164.92/123.69
PLUS(s(s(s(s(y0)))), 0) → c7(PLUS(s(s(s(y0))), 0)) 164.92/123.69
PLUS(s(s(s(s(s(y0))))), 0) → c7(PLUS(s(s(s(s(y0)))), 0)) 164.92/123.69
PLUS(s(s(s(s(s(s(y0)))))), 0) → c7(PLUS(s(s(s(s(s(y0))))), 0))

164.92/123.69

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.92/123.69
minus(s(z0), s(z1)) → minus(z0, z1) 164.92/123.69
double(0) → 0 164.92/123.69
double(s(z0)) → s(s(double(z0))) 164.92/123.69
plus(0, z0) → z0 164.92/123.69
plus(s(z0), z1) → s(plus(z0, z1)) 164.92/123.69
plus(s(z0), z1) → plus(z0, s(z1)) 164.92/123.69
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 164.92/123.69
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.92/123.69
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1))) 164.92/123.69
DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0))) 164.92/123.69
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0)))) 164.92/123.69
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 164.92/123.69
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 164.92/123.69
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 164.92/123.69
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 164.92/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.70
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 164.92/123.70
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 164.92/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 164.92/123.70
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, s(s(double(0))))) 164.92/123.70
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 164.92/123.70
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 164.92/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 164.92/123.70
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 164.92/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 164.92/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 164.92/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 164.92/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 164.92/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 164.92/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.70
PLUS(s(z0), s(s(y0))) → c7(DOUBLE(s(s(y0)))) 164.92/123.70
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(s(s(double(z1)))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 164.92/123.70
PLUS(s(s(y0)), 0) → c7(PLUS(s(y0), 0)) 164.92/123.70
PLUS(s(s(s(y0))), 0) → c7(PLUS(s(s(y0)), 0)) 164.92/123.70
PLUS(s(s(s(s(y0)))), 0) → c7(PLUS(s(s(s(y0))), 0)) 164.92/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c7(PLUS(s(s(s(s(y0)))), 0)) 164.92/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c7(PLUS(s(s(s(s(s(y0))))), 0))

S tuples:

DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0)))

K tuples:

PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 164.92/123.70
MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1))) 164.92/123.70
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 164.92/123.70
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 164.92/123.70
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 164.92/123.70
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 164.92/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.70
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 164.92/123.70
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 164.92/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 164.92/123.70
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 164.92/123.70
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 164.92/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 164.92/123.70
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 164.92/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 164.92/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 164.92/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 164.92/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 164.92/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 164.92/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1))))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, MINUS, DOUBLE

Compound Symbols:

c7, c1, c3, c7, c5, c6

164.92/123.70

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

Use forward instantiation to replace MINUS(s(s(y0)), s(s(y1))) → c1(MINUS(s(y0), s(y1))) by

MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1))))

164.92/123.70

(44) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.92/123.70
minus(s(z0), s(z1)) → minus(z0, z1) 164.92/123.70
double(0) → 0 164.92/123.70
double(s(z0)) → s(s(double(z0))) 164.92/123.70
plus(0, z0) → z0 164.92/123.70
plus(s(z0), z1) → s(plus(z0, z1)) 164.92/123.70
plus(s(z0), z1) → plus(z0, s(z1)) 164.92/123.70
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 164.92/123.70
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.92/123.70
DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0))) 164.92/123.70
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0)))) 164.92/123.70
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 164.92/123.70
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 164.92/123.70
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 164.92/123.70
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 164.92/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.70
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 164.92/123.70
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 164.92/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 164.92/123.70
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, s(s(double(0))))) 164.92/123.70
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 164.92/123.70
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 164.92/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 164.92/123.70
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 164.92/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 164.92/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 164.92/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 164.92/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 164.92/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 164.92/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.70
PLUS(s(z0), s(s(y0))) → c7(DOUBLE(s(s(y0)))) 164.92/123.70
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(s(s(double(z1)))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 164.92/123.70
PLUS(s(s(y0)), 0) → c7(PLUS(s(y0), 0)) 164.92/123.70
PLUS(s(s(s(y0))), 0) → c7(PLUS(s(s(y0)), 0)) 164.92/123.70
PLUS(s(s(s(s(y0)))), 0) → c7(PLUS(s(s(s(y0))), 0)) 164.92/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c7(PLUS(s(s(s(s(y0)))), 0)) 164.92/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c7(PLUS(s(s(s(s(s(y0))))), 0)) 164.92/123.70
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1))))

S tuples:

DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0)))

K tuples:

PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 164.92/123.70
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 164.92/123.70
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 164.92/123.70
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 164.92/123.70
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 164.92/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.70
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 164.92/123.70
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 164.92/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 164.92/123.70
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 164.92/123.70
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 164.92/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 164.92/123.70
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 164.92/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 164.92/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 164.92/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 164.92/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 164.92/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 164.92/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.70
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1))))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, DOUBLE, MINUS

Compound Symbols:

c7, c3, c7, c5, c6, c1

164.92/123.70

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

Use forward instantiation to replace DOUBLE(s(s(y0))) → c3(DOUBLE(s(y0))) by

DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0))))

164.92/123.70

(46) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 164.92/123.70
minus(s(z0), s(z1)) → minus(z0, z1) 164.92/123.70
double(0) → 0 164.92/123.70
double(s(z0)) → s(s(double(z0))) 164.92/123.70
plus(0, z0) → z0 164.92/123.70
plus(s(z0), z1) → s(plus(z0, z1)) 164.92/123.70
plus(s(z0), z1) → plus(z0, s(z1)) 164.92/123.70
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 164.92/123.70
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 164.92/123.70
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0)))) 164.92/123.70
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 164.92/123.70
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 164.92/123.70
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 164.92/123.70
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 164.92/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.70
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 164.92/123.70
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 164.92/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 164.92/123.70
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, s(s(double(0))))) 164.92/123.70
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 164.92/123.70
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 164.92/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 164.92/123.70
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 164.92/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 164.92/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 164.92/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 164.92/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 164.92/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 164.92/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 164.92/123.70
PLUS(s(z0), s(s(y0))) → c7(DOUBLE(s(s(y0)))) 164.92/123.70
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(s(s(double(z1)))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 164.92/123.70
PLUS(s(s(y0)), 0) → c7(PLUS(s(y0), 0)) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c7(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c7(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c7(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c7(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1)))) 165.25/123.70
DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0))))

S tuples:

DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0))))

K tuples:

PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 165.25/123.70
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 165.25/123.70
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 165.25/123.70
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 165.25/123.70
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 165.25/123.70
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 165.25/123.70
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1))))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, MINUS, DOUBLE

Compound Symbols:

c7, c7, c5, c6, c1, c3

165.25/123.70

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

Used rewriting to replace PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, s(s(double(0))))) by PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, s(s(0))))

165.25/123.70

(48) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 165.25/123.70
minus(s(z0), s(z1)) → minus(z0, z1) 165.25/123.70
double(0) → 0 165.25/123.70
double(s(z0)) → s(s(double(z0))) 165.25/123.70
plus(0, z0) → z0 165.25/123.70
plus(s(z0), z1) → s(plus(z0, z1)) 165.25/123.70
plus(s(z0), z1) → plus(z0, s(z1)) 165.25/123.70
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 165.25/123.70
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 165.25/123.70
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0)))) 165.25/123.70
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 165.25/123.70
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 165.25/123.70
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 165.25/123.70
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 165.25/123.70
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 165.25/123.70
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(z0), s(s(y0))) → c7(DOUBLE(s(s(y0)))) 165.25/123.70
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(s(s(double(z1)))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 165.25/123.70
PLUS(s(s(y0)), 0) → c7(PLUS(s(y0), 0)) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c7(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c7(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c7(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c7(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1)))) 165.25/123.70
DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0)))) 165.25/123.70
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, s(s(0))))

S tuples:

DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0))))

K tuples:

PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 165.25/123.70
PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) 165.25/123.70
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 165.25/123.70
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 165.25/123.70
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 165.25/123.70
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 165.25/123.70
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1))))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, MINUS, DOUBLE

Compound Symbols:

c7, c7, c5, c6, c1, c3

165.25/123.70

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

Use forward instantiation to replace PLUS(s(s(y0)), z1) → c5(PLUS(s(y0), z1)) by

PLUS(s(s(z0)), s(s(y1))) → c5(PLUS(s(z0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 165.25/123.70
PLUS(s(s(z0)), s(0)) → c5(PLUS(s(z0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c5(PLUS(s(s(y0)), z1)) 165.25/123.70
PLUS(s(s(s(y0))), s(s(y1))) → c5(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c5(PLUS(s(s(s(y0))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(s(y1))) → c5(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c5(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(0)) → c5(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c5(PLUS(s(s(s(y0))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), z1) → c5(PLUS(s(s(s(s(y0)))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c5(PLUS(s(s(s(s(s(y0))))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c5(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c5(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c5(PLUS(s(s(s(s(y0)))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c5(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c5(PLUS(s(s(s(s(s(s(y0)))))), 0))

165.25/123.70

(50) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 165.25/123.70
minus(s(z0), s(z1)) → minus(z0, z1) 165.25/123.70
double(0) → 0 165.25/123.70
double(s(z0)) → s(s(double(z0))) 165.25/123.70
plus(0, z0) → z0 165.25/123.70
plus(s(z0), z1) → s(plus(z0, z1)) 165.25/123.70
plus(s(z0), z1) → plus(z0, s(z1)) 165.25/123.70
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 165.25/123.70
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 165.25/123.70
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0)))) 165.25/123.70
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 165.25/123.70
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 165.25/123.70
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 165.25/123.70
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 165.25/123.70
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(z0), s(s(y0))) → c7(DOUBLE(s(s(y0)))) 165.25/123.70
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(s(s(double(z1)))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 165.25/123.70
PLUS(s(s(y0)), 0) → c7(PLUS(s(y0), 0)) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c7(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c7(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c7(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c7(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1)))) 165.25/123.70
DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0)))) 165.25/123.70
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, s(s(0)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c5(PLUS(s(s(y0)), z1)) 165.25/123.70
PLUS(s(s(s(y0))), s(s(y1))) → c5(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c5(PLUS(s(s(s(y0))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(s(y1))) → c5(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c5(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(0)) → c5(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c5(PLUS(s(s(s(y0))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), z1) → c5(PLUS(s(s(s(s(y0)))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c5(PLUS(s(s(s(s(s(y0))))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c5(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c5(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c5(PLUS(s(s(s(s(y0)))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c5(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c5(PLUS(s(s(s(s(s(s(y0)))))), 0))

S tuples:

DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0))))

K tuples:

PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 165.25/123.70
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 165.25/123.70
PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 165.25/123.70
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 165.25/123.70
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 165.25/123.70
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c5(PLUS(s(s(y0)), z1)) 165.25/123.70
PLUS(s(s(s(y0))), s(s(y1))) → c5(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c5(PLUS(s(s(s(y0))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(s(y1))) → c5(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c5(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(0)) → c5(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c5(PLUS(s(s(s(y0))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), z1) → c5(PLUS(s(s(s(s(y0)))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c5(PLUS(s(s(s(s(s(y0))))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c5(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c5(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c5(PLUS(s(s(s(s(y0)))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c5(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c5(PLUS(s(s(s(s(s(s(y0)))))), 0))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, MINUS, DOUBLE

Compound Symbols:

c7, c7, c5, c6, c1, c3

165.25/123.70

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

Use forward instantiation to replace PLUS(s(s(y0)), s(y1)) → c5(PLUS(s(y0), s(y1))) by

PLUS(s(s(z0)), s(s(y1))) → c5(PLUS(s(z0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), s(z1)) → c5(PLUS(s(s(y0)), s(z1))) 165.25/123.70
PLUS(s(s(z0)), s(0)) → c5(PLUS(s(z0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(s(y1))) → c5(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(z1)) → c5(PLUS(s(s(s(y0))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(s(y1))) → c5(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(0)) → c5(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(z1)) → c5(PLUS(s(s(s(s(y0)))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(z1)) → c5(PLUS(s(s(s(s(s(y0))))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(s(y1))) → c5(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(0)) → c5(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)) → c5(PLUS(s(s(s(s(s(s(y0)))))), s(z1)))

165.25/123.70

(52) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 165.25/123.70
minus(s(z0), s(z1)) → minus(z0, z1) 165.25/123.70
double(0) → 0 165.25/123.70
double(s(z0)) → s(s(double(z0))) 165.25/123.70
plus(0, z0) → z0 165.25/123.70
plus(s(z0), z1) → s(plus(z0, z1)) 165.25/123.70
plus(s(z0), z1) → plus(z0, s(z1)) 165.25/123.70
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 165.25/123.70
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 165.25/123.70
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0)))) 165.25/123.70
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 165.25/123.70
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 165.25/123.70
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 165.25/123.70
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(z0), s(s(y0))) → c7(DOUBLE(s(s(y0)))) 165.25/123.70
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(s(s(double(z1)))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 165.25/123.70
PLUS(s(s(y0)), 0) → c7(PLUS(s(y0), 0)) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c7(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c7(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c7(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c7(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1)))) 165.25/123.70
DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0)))) 165.25/123.70
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, s(s(0)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c5(PLUS(s(s(y0)), z1)) 165.25/123.70
PLUS(s(s(s(y0))), s(s(y1))) → c5(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c5(PLUS(s(s(s(y0))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(s(y1))) → c5(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c5(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(0)) → c5(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c5(PLUS(s(s(s(y0))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), z1) → c5(PLUS(s(s(s(s(y0)))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c5(PLUS(s(s(s(s(s(y0))))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c5(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c5(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c5(PLUS(s(s(s(s(y0)))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c5(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c5(PLUS(s(s(s(s(s(s(y0)))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(s(y1))) → c5(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(0)) → c5(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)) → c5(PLUS(s(s(s(s(s(s(y0)))))), s(z1)))

S tuples:

DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0))))

K tuples:

PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 165.25/123.70
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) 165.25/123.70
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 165.25/123.70
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 165.25/123.70
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c5(PLUS(s(s(y0)), z1)) 165.25/123.70
PLUS(s(s(s(y0))), s(s(y1))) → c5(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c5(PLUS(s(s(s(y0))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(s(y1))) → c5(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c5(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(0)) → c5(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c5(PLUS(s(s(s(y0))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), z1) → c5(PLUS(s(s(s(s(y0)))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c5(PLUS(s(s(s(s(s(y0))))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c5(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c5(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c5(PLUS(s(s(s(s(y0)))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c5(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c5(PLUS(s(s(s(s(s(s(y0)))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(s(y1))) → c5(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(0)) → c5(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)) → c5(PLUS(s(s(s(s(s(s(y0)))))), s(z1)))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, MINUS, DOUBLE

Compound Symbols:

c7, c7, c5, c6, c1, c3

165.25/123.70

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

Use forward instantiation to replace PLUS(s(s(y0)), 0) → c5(PLUS(s(y0), 0)) by

PLUS(s(s(s(y0))), 0) → c5(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c5(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c5(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c5(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c5(PLUS(s(s(s(s(s(s(y0)))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0) → c5(PLUS(s(s(s(s(s(s(s(y0))))))), 0))

165.25/123.70

(54) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 165.25/123.70
minus(s(z0), s(z1)) → minus(z0, z1) 165.25/123.70
double(0) → 0 165.25/123.70
double(s(z0)) → s(s(double(z0))) 165.25/123.70
plus(0, z0) → z0 165.25/123.70
plus(s(z0), z1) → s(plus(z0, z1)) 165.25/123.70
plus(s(z0), z1) → plus(z0, s(z1)) 165.25/123.70
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 165.25/123.70
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 165.25/123.70
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0)))) 165.25/123.70
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 165.25/123.70
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 165.25/123.70
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(z0), s(s(y0))) → c7(DOUBLE(s(s(y0)))) 165.25/123.70
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(s(s(double(z1)))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 165.25/123.70
PLUS(s(s(y0)), 0) → c7(PLUS(s(y0), 0)) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c7(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c7(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c7(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c7(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1)))) 165.25/123.70
DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0)))) 165.25/123.70
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, s(s(0)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c5(PLUS(s(s(y0)), z1)) 165.25/123.70
PLUS(s(s(s(y0))), s(s(y1))) → c5(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c5(PLUS(s(s(s(y0))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(s(y1))) → c5(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c5(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(0)) → c5(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c5(PLUS(s(s(s(y0))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), z1) → c5(PLUS(s(s(s(s(y0)))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c5(PLUS(s(s(s(s(s(y0))))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c5(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c5(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c5(PLUS(s(s(s(s(y0)))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c5(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c5(PLUS(s(s(s(s(s(s(y0)))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(s(y1))) → c5(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(0)) → c5(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)) → c5(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0) → c5(PLUS(s(s(s(s(s(s(s(y0))))))), 0))

S tuples:

DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0))))

K tuples:

PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 165.25/123.70
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) 165.25/123.70
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 165.25/123.70
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c5(PLUS(s(s(y0)), z1)) 165.25/123.70
PLUS(s(s(s(y0))), s(s(y1))) → c5(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c5(PLUS(s(s(s(y0))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(s(y1))) → c5(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c5(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(0)) → c5(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c5(PLUS(s(s(s(y0))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), z1) → c5(PLUS(s(s(s(s(y0)))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c5(PLUS(s(s(s(s(s(y0))))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c5(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c5(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c5(PLUS(s(s(s(s(y0)))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c5(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c5(PLUS(s(s(s(s(s(s(y0)))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(s(y1))) → c5(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(0)) → c5(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)) → c5(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0) → c5(PLUS(s(s(s(s(s(s(s(y0))))))), 0))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, MINUS, DOUBLE

Compound Symbols:

c7, c7, c5, c6, c1, c3

165.25/123.70

(55) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace PLUS(s(s(y0)), z1) → c6(PLUS(s(y0), s(z1))) by

PLUS(s(s(z0)), s(y1)) → c6(PLUS(s(z0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 165.25/123.70
PLUS(s(s(z0)), 0) → c6(PLUS(s(z0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), z1) → c6(PLUS(s(s(s(s(y0)))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), z1) → c6(PLUS(s(s(s(s(s(y0))))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c6(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c6(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), z1) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), s(y1)) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c6(PLUS(s(s(s(s(s(y0))))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(s(y0)))))))), z1) → c6(PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)))

165.25/123.70

(56) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 165.25/123.70
minus(s(z0), s(z1)) → minus(z0, z1) 165.25/123.70
double(0) → 0 165.25/123.70
double(s(z0)) → s(s(double(z0))) 165.25/123.70
plus(0, z0) → z0 165.25/123.70
plus(s(z0), z1) → s(plus(z0, z1)) 165.25/123.70
plus(s(z0), z1) → plus(z0, s(z1)) 165.25/123.70
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 165.25/123.70
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 165.25/123.70
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0)))) 165.25/123.70
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 165.25/123.70
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(z0), s(s(y0))) → c7(DOUBLE(s(s(y0)))) 165.25/123.70
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(s(s(double(z1)))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 165.25/123.70
PLUS(s(s(y0)), 0) → c7(PLUS(s(y0), 0)) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c7(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c7(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c7(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c7(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1)))) 165.25/123.70
DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0)))) 165.25/123.70
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, s(s(0)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c5(PLUS(s(s(y0)), z1)) 165.25/123.70
PLUS(s(s(s(y0))), s(s(y1))) → c5(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c5(PLUS(s(s(s(y0))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(s(y1))) → c5(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c5(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(0)) → c5(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c5(PLUS(s(s(s(y0))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), z1) → c5(PLUS(s(s(s(s(y0)))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c5(PLUS(s(s(s(s(s(y0))))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c5(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c5(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c5(PLUS(s(s(s(s(y0)))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c5(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c5(PLUS(s(s(s(s(s(s(y0)))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(s(y1))) → c5(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(0)) → c5(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)) → c5(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0) → c5(PLUS(s(s(s(s(s(s(s(y0))))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), z1) → c6(PLUS(s(s(s(s(y0)))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), z1) → c6(PLUS(s(s(s(s(s(y0))))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c6(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c6(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), z1) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), s(y1)) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c6(PLUS(s(s(s(s(s(y0))))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(s(y0)))))))), z1) → c6(PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)))

S tuples:

DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0))))

K tuples:

PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 165.25/123.70
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 165.25/123.70
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c5(PLUS(s(s(y0)), z1)) 165.25/123.70
PLUS(s(s(s(y0))), s(s(y1))) → c5(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c5(PLUS(s(s(s(y0))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(s(y1))) → c5(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c5(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(0)) → c5(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c5(PLUS(s(s(s(y0))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), z1) → c5(PLUS(s(s(s(s(y0)))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c5(PLUS(s(s(s(s(s(y0))))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c5(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c5(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c5(PLUS(s(s(s(s(y0)))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c5(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c5(PLUS(s(s(s(s(s(s(y0)))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(s(y1))) → c5(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(0)) → c5(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)) → c5(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0) → c5(PLUS(s(s(s(s(s(s(s(y0))))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), z1) → c6(PLUS(s(s(s(s(y0)))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), z1) → c6(PLUS(s(s(s(s(s(y0))))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c6(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c6(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), z1) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), s(y1)) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c6(PLUS(s(s(s(s(s(y0))))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(s(y0)))))))), z1) → c6(PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, MINUS, DOUBLE

Compound Symbols:

c7, c7, c5, c6, c1, c3

165.25/123.70

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

Use forward instantiation to replace PLUS(s(z0), s(s(y0))) → c7(DOUBLE(s(s(y0)))) by

PLUS(s(z0), s(s(s(y0)))) → c7(DOUBLE(s(s(s(y0)))))

165.25/123.70

(58) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 165.25/123.70
minus(s(z0), s(z1)) → minus(z0, z1) 165.25/123.70
double(0) → 0 165.25/123.70
double(s(z0)) → s(s(double(z0))) 165.25/123.70
plus(0, z0) → z0 165.25/123.70
plus(s(z0), z1) → s(plus(z0, z1)) 165.25/123.70
plus(s(z0), z1) → plus(z0, s(z1)) 165.25/123.70
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 165.25/123.70
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 165.25/123.70
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0)))) 165.25/123.70
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 165.25/123.70
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(s(s(double(z1)))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 165.25/123.70
PLUS(s(s(y0)), 0) → c7(PLUS(s(y0), 0)) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c7(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c7(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c7(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c7(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1)))) 165.25/123.70
DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0)))) 165.25/123.70
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, s(s(0)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c5(PLUS(s(s(y0)), z1)) 165.25/123.70
PLUS(s(s(s(y0))), s(s(y1))) → c5(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c5(PLUS(s(s(s(y0))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(s(y1))) → c5(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c5(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(0)) → c5(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c5(PLUS(s(s(s(y0))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), z1) → c5(PLUS(s(s(s(s(y0)))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c5(PLUS(s(s(s(s(s(y0))))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c5(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c5(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c5(PLUS(s(s(s(s(y0)))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c5(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c5(PLUS(s(s(s(s(s(s(y0)))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(s(y1))) → c5(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(0)) → c5(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)) → c5(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0) → c5(PLUS(s(s(s(s(s(s(s(y0))))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), z1) → c6(PLUS(s(s(s(s(y0)))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), z1) → c6(PLUS(s(s(s(s(s(y0))))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c6(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c6(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), z1) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), s(y1)) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c6(PLUS(s(s(s(s(s(y0))))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(s(y0)))))))), z1) → c6(PLUS(s(s(s(s(s(s(s(y0))))))), s(z1))) 165.25/123.70
PLUS(s(z0), s(s(s(y0)))) → c7(DOUBLE(s(s(s(y0)))))

S tuples:

DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0))))

K tuples:

PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 165.25/123.70
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 165.25/123.70
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c5(PLUS(s(s(y0)), z1)) 165.25/123.70
PLUS(s(s(s(y0))), s(s(y1))) → c5(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c5(PLUS(s(s(s(y0))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(s(y1))) → c5(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c5(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(0)) → c5(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c5(PLUS(s(s(s(y0))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), z1) → c5(PLUS(s(s(s(s(y0)))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c5(PLUS(s(s(s(s(s(y0))))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c5(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c5(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c5(PLUS(s(s(s(s(y0)))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c5(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c5(PLUS(s(s(s(s(s(s(y0)))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(s(y1))) → c5(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(0)) → c5(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)) → c5(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0) → c5(PLUS(s(s(s(s(s(s(s(y0))))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), z1) → c6(PLUS(s(s(s(s(y0)))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), z1) → c6(PLUS(s(s(s(s(s(y0))))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c6(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c6(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), z1) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), s(y1)) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c6(PLUS(s(s(s(s(s(y0))))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(s(y0)))))))), z1) → c6(PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, MINUS, DOUBLE

Compound Symbols:

c7, c7, c5, c6, c1, c3

165.25/123.70

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

Use forward instantiation to replace PLUS(s(s(y0)), 0) → c7(PLUS(s(y0), 0)) by

PLUS(s(s(s(s(y0)))), 0) → c7(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c7(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c7(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c7(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c7(PLUS(s(s(s(s(s(s(y0)))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0) → c7(PLUS(s(s(s(s(s(s(s(y0))))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(s(s(s(y0))))))))), 0) → c7(PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0))

165.25/123.70

(60) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 165.25/123.70
minus(s(z0), s(z1)) → minus(z0, z1) 165.25/123.70
double(0) → 0 165.25/123.70
double(s(z0)) → s(s(double(z0))) 165.25/123.70
plus(0, z0) → z0 165.25/123.70
plus(s(z0), z1) → s(plus(z0, z1)) 165.25/123.70
plus(s(z0), z1) → plus(z0, s(z1)) 165.25/123.70
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 165.25/123.70
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 165.25/123.70
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0)))) 165.25/123.70
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 165.25/123.70
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(s(s(double(z1)))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 165.25/123.70
PLUS(s(s(y0)), 0) → c7(PLUS(s(y0), 0)) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c7(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c7(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c7(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c7(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1)))) 165.25/123.70
DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0)))) 165.25/123.70
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, s(s(0)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c5(PLUS(s(s(y0)), z1)) 165.25/123.70
PLUS(s(s(s(y0))), s(s(y1))) → c5(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c5(PLUS(s(s(s(y0))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(s(y1))) → c5(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c5(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(0)) → c5(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c5(PLUS(s(s(s(y0))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), z1) → c5(PLUS(s(s(s(s(y0)))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c5(PLUS(s(s(s(s(s(y0))))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c5(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c5(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c5(PLUS(s(s(s(s(y0)))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c5(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c5(PLUS(s(s(s(s(s(s(y0)))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(s(y1))) → c5(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(0)) → c5(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)) → c5(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0) → c5(PLUS(s(s(s(s(s(s(s(y0))))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), z1) → c6(PLUS(s(s(s(s(y0)))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), z1) → c6(PLUS(s(s(s(s(s(y0))))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c6(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c6(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), z1) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), s(y1)) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c6(PLUS(s(s(s(s(s(y0))))), s(0))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(s(y0)))))))), z1) → c6(PLUS(s(s(s(s(s(s(s(y0))))))), s(z1))) 165.25/123.70
PLUS(s(z0), s(s(s(y0)))) → c7(DOUBLE(s(s(s(y0))))) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c7(PLUS(s(s(s(s(s(s(y0)))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0) → c7(PLUS(s(s(s(s(s(s(s(y0))))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(s(s(s(y0))))))))), 0) → c7(PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0))

S tuples:

DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0))))

K tuples:

PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 165.25/123.70
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 165.25/123.70
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 165.25/123.70
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.70
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), z1) → c5(PLUS(s(s(y0)), z1)) 165.25/123.70
PLUS(s(s(s(y0))), s(s(y1))) → c5(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(y1)) → c5(PLUS(s(s(s(y0))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(s(y1))) → c5(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.70
PLUS(s(s(s(y0))), 0) → c5(PLUS(s(s(y0)), 0)) 165.25/123.70
PLUS(s(s(s(s(y0)))), s(0)) → c5(PLUS(s(s(s(y0))), s(0))) 165.25/123.70
PLUS(s(s(s(s(y0)))), z1) → c5(PLUS(s(s(s(y0))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), z1) → c5(PLUS(s(s(s(s(y0)))), z1)) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c5(PLUS(s(s(s(s(s(y0))))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(y0)))), 0) → c5(PLUS(s(s(s(y0))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), 0) → c5(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(y0))))), s(y1)) → c5(PLUS(s(s(s(s(y0)))), s(y1))) 165.25/123.70
PLUS(s(s(s(s(s(s(y0)))))), 0) → c5(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.70
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c5(PLUS(s(s(s(s(s(s(y0)))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), s(s(y1))) → c5(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), s(0)) → c5(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)) → c5(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0) → c5(PLUS(s(s(s(s(s(s(s(y0))))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), z1) → c6(PLUS(s(s(s(s(y0)))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), z1) → c6(PLUS(s(s(s(s(s(y0))))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c6(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), 0) → c6(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), z1) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), s(y1)) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), 0) → c6(PLUS(s(s(s(s(s(y0))))), s(0))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(y0)))))))), z1) → c6(PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, MINUS, DOUBLE

Compound Symbols:

c7, c7, c5, c6, c1, c3

165.25/123.71

(61) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace PLUS(s(s(y0)), 0) → c7(PLUS(s(y0), 0)) by

PLUS(s(s(s(s(y0)))), 0) → c7(PLUS(s(s(s(y0))), 0)) 165.25/123.71
PLUS(s(s(s(y0))), 0) → c7(PLUS(s(s(y0)), 0)) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), 0) → c7(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), 0) → c7(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c7(PLUS(s(s(s(s(s(s(y0)))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0) → c7(PLUS(s(s(s(s(s(s(s(y0))))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(s(y0))))))))), 0) → c7(PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(s(s(y0)))))))))), 0) → c7(PLUS(s(s(s(s(s(s(s(s(s(y0))))))))), 0))

165.25/123.71

(62) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 165.25/123.71
minus(s(z0), s(z1)) → minus(z0, z1) 165.25/123.71
double(0) → 0 165.25/123.71
double(s(z0)) → s(s(double(z0))) 165.25/123.71
plus(0, z0) → z0 165.25/123.71
plus(s(z0), z1) → s(plus(z0, z1)) 165.25/123.71
plus(s(z0), z1) → plus(z0, s(z1)) 165.25/123.71
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 165.25/123.71
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 165.25/123.71
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0)))) 165.25/123.71
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 165.25/123.71
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.71
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 165.25/123.71
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.71
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 165.25/123.71
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 165.25/123.71
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 165.25/123.71
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 165.25/123.71
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(s(s(double(z1)))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 165.25/123.71
PLUS(s(s(s(y0))), 0) → c7(PLUS(s(s(y0)), 0)) 165.25/123.71
PLUS(s(s(s(s(y0)))), 0) → c7(PLUS(s(s(s(y0))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), 0) → c7(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), 0) → c7(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.71
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1)))) 165.25/123.71
DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0)))) 165.25/123.71
PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, s(s(0)))) 165.25/123.71
PLUS(s(s(s(y0))), z1) → c5(PLUS(s(s(y0)), z1)) 165.25/123.71
PLUS(s(s(s(y0))), s(s(y1))) → c5(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(y0)))), s(y1)) → c5(PLUS(s(s(s(y0))), s(y1))) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), s(s(y1))) → c5(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(y0))), 0) → c5(PLUS(s(s(y0)), 0)) 165.25/123.71
PLUS(s(s(s(s(y0)))), s(0)) → c5(PLUS(s(s(s(y0))), s(0))) 165.25/123.71
PLUS(s(s(s(s(y0)))), z1) → c5(PLUS(s(s(s(y0))), z1)) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), z1) → c5(PLUS(s(s(s(s(y0)))), z1)) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c5(PLUS(s(s(s(s(s(y0))))), s(y1))) 165.25/123.71
PLUS(s(s(s(s(y0)))), 0) → c5(PLUS(s(s(s(y0))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), 0) → c5(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), s(y1)) → c5(PLUS(s(s(s(s(y0)))), s(y1))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), 0) → c5(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c5(PLUS(s(s(s(s(s(s(y0)))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), s(s(y1))) → c5(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), s(0)) → c5(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)) → c5(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0) → c5(PLUS(s(s(s(s(s(s(s(y0))))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), z1) → c6(PLUS(s(s(s(s(y0)))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), z1) → c6(PLUS(s(s(s(s(s(y0))))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c6(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), 0) → c6(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), z1) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), s(y1)) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), 0) → c6(PLUS(s(s(s(s(s(y0))))), s(0))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(y0)))))))), z1) → c6(PLUS(s(s(s(s(s(s(s(y0))))))), s(z1))) 165.25/123.71
PLUS(s(z0), s(s(s(y0)))) → c7(DOUBLE(s(s(s(y0))))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c7(PLUS(s(s(s(s(s(s(y0)))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0) → c7(PLUS(s(s(s(s(s(s(s(y0))))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(s(y0))))))))), 0) → c7(PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(s(s(y0)))))))))), 0) → c7(PLUS(s(s(s(s(s(s(s(s(s(y0))))))))), 0))

S tuples:

DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0))))

K tuples:

PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 165.25/123.71
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 165.25/123.71
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.71
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 165.25/123.71
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.71
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 165.25/123.71
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 165.25/123.71
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 165.25/123.71
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 165.25/123.71
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.71
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(y0))), z1) → c5(PLUS(s(s(y0)), z1)) 165.25/123.71
PLUS(s(s(s(y0))), s(s(y1))) → c5(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(y0)))), s(y1)) → c5(PLUS(s(s(s(y0))), s(y1))) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), s(s(y1))) → c5(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(y0))), 0) → c5(PLUS(s(s(y0)), 0)) 165.25/123.71
PLUS(s(s(s(s(y0)))), s(0)) → c5(PLUS(s(s(s(y0))), s(0))) 165.25/123.71
PLUS(s(s(s(s(y0)))), z1) → c5(PLUS(s(s(s(y0))), z1)) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), z1) → c5(PLUS(s(s(s(s(y0)))), z1)) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c5(PLUS(s(s(s(s(s(y0))))), s(y1))) 165.25/123.71
PLUS(s(s(s(s(y0)))), 0) → c5(PLUS(s(s(s(y0))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), 0) → c5(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), s(y1)) → c5(PLUS(s(s(s(s(y0)))), s(y1))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), 0) → c5(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c5(PLUS(s(s(s(s(s(s(y0)))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), s(s(y1))) → c5(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), s(0)) → c5(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)) → c5(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0) → c5(PLUS(s(s(s(s(s(s(s(y0))))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), z1) → c6(PLUS(s(s(s(s(y0)))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), z1) → c6(PLUS(s(s(s(s(s(y0))))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c6(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), 0) → c6(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), z1) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), s(y1)) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), 0) → c6(PLUS(s(s(s(s(s(y0))))), s(0))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(y0)))))))), z1) → c6(PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, MINUS, DOUBLE

Compound Symbols:

c7, c7, c5, c6, c1, c3

165.25/123.71

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

Use forward instantiation to replace PLUS(s(s(z0)), s(0)) → c7(PLUS(z0, s(s(0)))) by

PLUS(s(s(s(y0))), s(0)) → c7(PLUS(s(y0), s(s(0)))) 165.25/123.71
PLUS(s(s(s(s(y0)))), s(0)) → c7(PLUS(s(s(y0)), s(s(0)))) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), s(0)) → c7(PLUS(s(s(s(y0))), s(s(0)))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), s(0)) → c7(PLUS(s(s(s(s(y0)))), s(s(0)))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), s(0)) → c7(PLUS(s(s(s(s(s(y0))))), s(s(0)))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(y0)))))))), s(0)) → c7(PLUS(s(s(s(s(s(s(y0)))))), s(s(0)))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(s(y0))))))))), s(0)) → c7(PLUS(s(s(s(s(s(s(s(y0))))))), s(s(0)))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(s(s(y0)))))))))), s(0)) → c7(PLUS(s(s(s(s(s(s(s(s(y0)))))))), s(s(0))))

165.25/123.71

(64) Obligation:

Complexity Dependency Tuples Problem
Rules:

minus(z0, 0) → z0 165.25/123.71
minus(s(z0), s(z1)) → minus(z0, z1) 165.25/123.71
double(0) → 0 165.25/123.71
double(s(z0)) → s(s(double(z0))) 165.25/123.71
plus(0, z0) → z0 165.25/123.71
plus(s(z0), z1) → s(plus(z0, z1)) 165.25/123.71
plus(s(z0), z1) → plus(z0, s(z1)) 165.25/123.71
plus(s(z0), z1) → s(plus(minus(z0, z1), double(z1)))

Tuples:

PLUS(s(x0), s(s(z0))) → c7(PLUS(minus(x0, s(s(z0))), s(s(s(s(double(z0)))))), MINUS(x0, s(s(z0))), DOUBLE(s(s(z0)))) 165.25/123.71
PLUS(s(s(z0)), s(z1)) → c7(PLUS(minus(z0, z1), s(s(double(z1)))), MINUS(s(z0), s(z1)), DOUBLE(s(z1))) 165.25/123.71
PLUS(s(x0), s(0)) → c7(PLUS(minus(x0, s(0)), s(s(0)))) 165.25/123.71
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 165.25/123.71
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.71
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 165.25/123.71
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.71
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 165.25/123.71
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 165.25/123.71
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 165.25/123.71
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 165.25/123.71
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(z0))), s(s(z1))) → c7(PLUS(minus(z0, z1), s(s(s(s(double(z1)))))), MINUS(s(s(z0)), s(s(z1))), DOUBLE(s(s(z1)))) 165.25/123.71
PLUS(s(s(s(y0))), 0) → c7(PLUS(s(s(y0)), 0)) 165.25/123.71
PLUS(s(s(s(s(y0)))), 0) → c7(PLUS(s(s(s(y0))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), 0) → c7(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), 0) → c7(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.71
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1)))) 165.25/123.71
DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0)))) 165.25/123.71
PLUS(s(s(s(y0))), z1) → c5(PLUS(s(s(y0)), z1)) 165.25/123.71
PLUS(s(s(s(y0))), s(s(y1))) → c5(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(y0)))), s(y1)) → c5(PLUS(s(s(s(y0))), s(y1))) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), s(s(y1))) → c5(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(y0))), 0) → c5(PLUS(s(s(y0)), 0)) 165.25/123.71
PLUS(s(s(s(s(y0)))), s(0)) → c5(PLUS(s(s(s(y0))), s(0))) 165.25/123.71
PLUS(s(s(s(s(y0)))), z1) → c5(PLUS(s(s(s(y0))), z1)) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), z1) → c5(PLUS(s(s(s(s(y0)))), z1)) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c5(PLUS(s(s(s(s(s(y0))))), s(y1))) 165.25/123.71
PLUS(s(s(s(s(y0)))), 0) → c5(PLUS(s(s(s(y0))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), 0) → c5(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), s(y1)) → c5(PLUS(s(s(s(s(y0)))), s(y1))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), 0) → c5(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c5(PLUS(s(s(s(s(s(s(y0)))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), s(s(y1))) → c5(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), s(0)) → c5(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)) → c5(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0) → c5(PLUS(s(s(s(s(s(s(s(y0))))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), z1) → c6(PLUS(s(s(s(s(y0)))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), z1) → c6(PLUS(s(s(s(s(s(y0))))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c6(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), 0) → c6(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), z1) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), s(y1)) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), 0) → c6(PLUS(s(s(s(s(s(y0))))), s(0))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(y0)))))))), z1) → c6(PLUS(s(s(s(s(s(s(s(y0))))))), s(z1))) 165.25/123.71
PLUS(s(z0), s(s(s(y0)))) → c7(DOUBLE(s(s(s(y0))))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c7(PLUS(s(s(s(s(s(s(y0)))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0) → c7(PLUS(s(s(s(s(s(s(s(y0))))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(s(y0))))))))), 0) → c7(PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(s(s(y0)))))))))), 0) → c7(PLUS(s(s(s(s(s(s(s(s(s(y0))))))))), 0)) 165.25/123.71
PLUS(s(s(s(y0))), s(0)) → c7(PLUS(s(y0), s(s(0)))) 165.25/123.71
PLUS(s(s(s(s(y0)))), s(0)) → c7(PLUS(s(s(y0)), s(s(0)))) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), s(0)) → c7(PLUS(s(s(s(y0))), s(s(0)))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), s(0)) → c7(PLUS(s(s(s(s(y0)))), s(s(0)))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), s(0)) → c7(PLUS(s(s(s(s(s(y0))))), s(s(0)))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(y0)))))))), s(0)) → c7(PLUS(s(s(s(s(s(s(y0)))))), s(s(0)))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(s(y0))))))))), s(0)) → c7(PLUS(s(s(s(s(s(s(s(y0))))))), s(s(0)))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(s(s(y0)))))))))), s(0)) → c7(PLUS(s(s(s(s(s(s(s(s(y0)))))))), s(s(0))))

S tuples:

DOUBLE(s(s(s(y0)))) → c3(DOUBLE(s(s(y0))))

K tuples:

PLUS(s(z0), z1) → c7(PLUS(minus(z0, z1), double(z1)), MINUS(z0, z1), DOUBLE(z1)) 165.25/123.71
PLUS(s(s(y0)), s(s(y1))) → c5(PLUS(s(y0), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(y0))), s(y1)) → c5(PLUS(s(s(y0)), s(y1))) 165.25/123.71
PLUS(s(s(s(s(y0)))), s(s(y1))) → c5(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.71
PLUS(s(s(y0)), s(0)) → c5(PLUS(s(y0), s(0))) 165.25/123.71
PLUS(s(s(s(y0))), s(0)) → c5(PLUS(s(s(y0)), s(0))) 165.25/123.71
PLUS(s(s(y0)), s(y1)) → c6(PLUS(s(y0), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(y0))), z1) → c6(PLUS(s(s(y0)), s(z1))) 165.25/123.71
PLUS(s(s(y0)), 0) → c6(PLUS(s(y0), s(0))) 165.25/123.71
PLUS(s(s(s(y0))), s(y1)) → c6(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(y0)))), z1) → c6(PLUS(s(s(s(y0))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), s(y1)) → c6(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(y0))), 0) → c6(PLUS(s(s(y0)), s(0))) 165.25/123.71
PLUS(s(s(s(s(y0)))), 0) → c6(PLUS(s(s(s(y0))), s(0))) 165.25/123.71
PLUS(s(s(s(s(y0)))), s(y1)) → c6(PLUS(s(s(s(y0))), s(s(y1)))) 165.25/123.71
MINUS(s(s(s(y0))), s(s(s(y1)))) → c1(MINUS(s(s(y0)), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(y0))), z1) → c5(PLUS(s(s(y0)), z1)) 165.25/123.71
PLUS(s(s(s(y0))), s(s(y1))) → c5(PLUS(s(s(y0)), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(y0)))), s(y1)) → c5(PLUS(s(s(s(y0))), s(y1))) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), s(s(y1))) → c5(PLUS(s(s(s(s(y0)))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(y0))), 0) → c5(PLUS(s(s(y0)), 0)) 165.25/123.71
PLUS(s(s(s(s(y0)))), s(0)) → c5(PLUS(s(s(s(y0))), s(0))) 165.25/123.71
PLUS(s(s(s(s(y0)))), z1) → c5(PLUS(s(s(s(y0))), z1)) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), z1) → c5(PLUS(s(s(s(s(y0)))), z1)) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c5(PLUS(s(s(s(s(s(y0))))), s(y1))) 165.25/123.71
PLUS(s(s(s(s(y0)))), 0) → c5(PLUS(s(s(s(y0))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), 0) → c5(PLUS(s(s(s(s(y0)))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), s(y1)) → c5(PLUS(s(s(s(s(y0)))), s(y1))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), 0) → c5(PLUS(s(s(s(s(s(y0))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), 0) → c5(PLUS(s(s(s(s(s(s(y0)))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), s(s(y1))) → c5(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), s(0)) → c5(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)) → c5(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(y0)))))))), 0) → c5(PLUS(s(s(s(s(s(s(s(y0))))))), 0)) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), z1) → c6(PLUS(s(s(s(s(y0)))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), z1) → c6(PLUS(s(s(s(s(s(y0))))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), s(y1)) → c6(PLUS(s(s(s(s(s(y0))))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(s(y0))))), 0) → c6(PLUS(s(s(s(s(y0)))), s(0))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), z1) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(z1))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(y0))))))), s(y1)) → c6(PLUS(s(s(s(s(s(s(y0)))))), s(s(y1)))) 165.25/123.71
PLUS(s(s(s(s(s(s(y0)))))), 0) → c6(PLUS(s(s(s(s(s(y0))))), s(0))) 165.25/123.71
PLUS(s(s(s(s(s(s(s(s(y0)))))))), z1) → c6(PLUS(s(s(s(s(s(s(s(y0))))))), s(z1)))

Defined Rule Symbols:

minus, double, plus

Defined Pair Symbols:

PLUS, MINUS, DOUBLE

Compound Symbols:

c7, c7, c5, c6, c1, c3

165.25/123.71