MAYBE 53.42/27.10 MAYBE 53.42/27.15 53.42/27.15 53.42/27.15 53.42/27.15 53.42/27.15 53.42/27.15 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 53.42/27.15 53.42/27.15 53.42/27.15
53.42/27.15
53.42/27.15
53.42/27.15
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), INFINITE).

0 CpxTRS
53.42/27.15 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
53.42/27.15 
↳2 CdtProblem
53.42/27.15 
↳3 CdtUnreachableProof (⇔)
53.42/27.15 
↳4 CdtProblem
53.42/27.15 
↳5 CdtLeafRemovalProof (ComplexityIfPolyImplication)
53.42/27.15 
↳6 CdtProblem
53.42/27.15 
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
53.42/27.15 
↳8 CdtProblem
53.42/27.15 
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
53.42/27.15 
↳10 CdtProblem
53.42/27.15 
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
53.42/27.15 
↳12 CdtProblem
53.42/27.15 
↳13 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
53.42/27.15 
↳14 CdtProblem
53.42/27.15 
↳15 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
53.42/27.15 
↳16 CdtProblem
53.42/27.15 
↳17 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))))
53.42/27.15 
↳18 CdtProblem
53.42/27.15 
↳19 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
53.42/27.15 
↳20 CdtProblem
53.42/27.15 
↳21 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
53.42/27.15 
↳22 CdtProblem
53.42/27.15 
↳23 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
53.42/27.15 
↳24 CdtProblem
53.42/27.15 
↳25 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))))
53.42/27.15 
↳26 CdtProblem
53.42/27.15 
↳27 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
53.42/27.15 
↳28 CdtProblem
53.42/27.15 
↳29 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
53.42/27.15 
↳30 CdtProblem
53.42/27.15
53.42/27.15 53.42/27.15
53.42/27.15
53.42/27.15

(0) Obligation:

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

+(x, 0) → x 53.42/27.15
+(x, s(y)) → s(+(x, y)) 53.42/27.15
+(0, y) → y 53.42/27.15
+(s(x), y) → s(+(x, y)) 53.42/27.15
+(x, +(y, z)) → +(+(x, y), z) 53.42/27.15
f(g(f(x))) → f(h(s(0), x)) 53.42/27.15
f(g(h(x, y))) → f(h(s(x), y)) 53.42/27.15
f(h(x, h(y, z))) → f(h(+(x, y), z))

Rewrite Strategy: INNERMOST
53.42/27.15
53.42/27.15

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

Converted CpxTRS to CDT
53.42/27.15
53.42/27.15

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, 0) → z0 53.42/27.15
+(z0, s(z1)) → s(+(z0, z1)) 53.42/27.15
+(0, z0) → z0 53.42/27.15
+(s(z0), z1) → s(+(z0, z1)) 53.42/27.15
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 53.42/27.15
f(g(f(z0))) → f(h(s(0), z0)) 53.42/27.15
f(g(h(z0, z1))) → f(h(s(z0), z1)) 53.42/27.15
f(h(z0, h(z1, z2))) → f(h(+(z0, z1), z2))
Tuples:

+'(z0, s(z1)) → c1(+'(z0, z1)) 53.42/27.15
+'(s(z0), z1) → c3(+'(z0, z1)) 53.42/27.15
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.42/27.15
F(g(f(z0))) → c5(F(h(s(0), z0))) 53.42/27.15
F(g(h(z0, z1))) → c6(F(h(s(z0), z1))) 53.42/27.15
F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1))
S tuples:

+'(z0, s(z1)) → c1(+'(z0, z1)) 53.42/27.15
+'(s(z0), z1) → c3(+'(z0, z1)) 53.42/27.15
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.42/27.15
F(g(f(z0))) → c5(F(h(s(0), z0))) 53.42/27.15
F(g(h(z0, z1))) → c6(F(h(s(z0), z1))) 53.42/27.15
F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1))
K tuples:none
Defined Rule Symbols:

+, f

Defined Pair Symbols:

+', F

Compound Symbols:

c1, c3, c4, c5, c6, c7

53.42/27.15
53.42/27.15

(3) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

F(g(f(z0))) → c5(F(h(s(0), z0)))
53.42/27.15
53.42/27.15

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, 0) → z0 53.42/27.15
+(z0, s(z1)) → s(+(z0, z1)) 53.42/27.15
+(0, z0) → z0 53.42/27.15
+(s(z0), z1) → s(+(z0, z1)) 53.42/27.15
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 53.42/27.15
f(g(f(z0))) → f(h(s(0), z0)) 53.42/27.15
f(g(h(z0, z1))) → f(h(s(z0), z1)) 53.42/27.15
f(h(z0, h(z1, z2))) → f(h(+(z0, z1), z2))
Tuples:

+'(z0, s(z1)) → c1(+'(z0, z1)) 53.42/27.15
+'(s(z0), z1) → c3(+'(z0, z1)) 53.42/27.15
F(g(h(z0, z1))) → c6(F(h(s(z0), z1))) 53.42/27.15
F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.42/27.15
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1))
S tuples:

+'(z0, s(z1)) → c1(+'(z0, z1)) 53.42/27.15
+'(s(z0), z1) → c3(+'(z0, z1)) 53.42/27.15
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.42/27.15
F(g(h(z0, z1))) → c6(F(h(s(z0), z1))) 53.42/27.15
F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1))
K tuples:none
Defined Rule Symbols:

+, f

Defined Pair Symbols:

+', F

Compound Symbols:

c1, c3, c6, c7, c4

53.42/27.15
53.42/27.15

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

F(g(h(z0, z1))) → c6(F(h(s(z0), z1)))
53.42/27.15
53.42/27.15

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, 0) → z0 53.42/27.15
+(z0, s(z1)) → s(+(z0, z1)) 53.42/27.15
+(0, z0) → z0 53.42/27.15
+(s(z0), z1) → s(+(z0, z1)) 53.42/27.15
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 53.42/27.15
f(g(f(z0))) → f(h(s(0), z0)) 53.42/27.15
f(g(h(z0, z1))) → f(h(s(z0), z1)) 53.42/27.15
f(h(z0, h(z1, z2))) → f(h(+(z0, z1), z2))
Tuples:

+'(z0, s(z1)) → c1(+'(z0, z1)) 53.42/27.18
+'(s(z0), z1) → c3(+'(z0, z1)) 53.42/27.18
F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.42/27.18
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1))
S tuples:

+'(z0, s(z1)) → c1(+'(z0, z1)) 53.42/27.18
+'(s(z0), z1) → c3(+'(z0, z1)) 53.42/27.18
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.42/27.18
F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1))
K tuples:none
Defined Rule Symbols:

+, f

Defined Pair Symbols:

+', F

Compound Symbols:

c1, c3, c7, c4

53.42/27.18
53.42/27.18

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

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1))
We considered the (Usable) Rules:

+(0, z0) → z0 53.42/27.18
+(s(z0), z1) → s(+(z0, z1)) 53.42/27.18
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 53.42/27.18
+(z0, 0) → z0 53.42/27.18
+(z0, s(z1)) → s(+(z0, z1))
And the Tuples:

+'(z0, s(z1)) → c1(+'(z0, z1)) 53.42/27.18
+'(s(z0), z1) → c3(+'(z0, z1)) 53.42/27.18
F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.42/27.18
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 53.42/27.18

POL(+(x1, x2)) = 0    53.42/27.18
POL(+'(x1, x2)) = 0    53.42/27.18
POL(0) = 0    53.42/27.18
POL(F(x1)) = x1    53.42/27.18
POL(c1(x1)) = x1    53.42/27.18
POL(c3(x1)) = x1    53.42/27.18
POL(c4(x1, x2)) = x1 + x2    53.42/27.18
POL(c7(x1, x2)) = x1 + x2    53.42/27.18
POL(h(x1, x2)) = [4] + x2    53.42/27.18
POL(s(x1)) = 0   
53.42/27.18
53.42/27.18

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, 0) → z0 53.42/27.18
+(z0, s(z1)) → s(+(z0, z1)) 53.42/27.18
+(0, z0) → z0 53.42/27.18
+(s(z0), z1) → s(+(z0, z1)) 53.42/27.18
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 53.42/27.18
f(g(f(z0))) → f(h(s(0), z0)) 53.42/27.18
f(g(h(z0, z1))) → f(h(s(z0), z1)) 53.42/27.18
f(h(z0, h(z1, z2))) → f(h(+(z0, z1), z2))
Tuples:

+'(z0, s(z1)) → c1(+'(z0, z1)) 53.42/27.18
+'(s(z0), z1) → c3(+'(z0, z1)) 53.42/27.18
F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.42/27.18
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1))
S tuples:

+'(z0, s(z1)) → c1(+'(z0, z1)) 53.42/27.18
+'(s(z0), z1) → c3(+'(z0, z1)) 53.42/27.18
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1))
K tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1))
Defined Rule Symbols:

+, f

Defined Pair Symbols:

+', F

Compound Symbols:

c1, c3, c7, c4

53.42/27.18
53.42/27.18

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

+'(z0, s(z1)) → c1(+'(z0, z1))
We considered the (Usable) Rules:

+(0, z0) → z0 53.42/27.18
+(s(z0), z1) → s(+(z0, z1)) 53.42/27.18
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 53.42/27.18
+(z0, 0) → z0 53.42/27.18
+(z0, s(z1)) → s(+(z0, z1))
And the Tuples:

+'(z0, s(z1)) → c1(+'(z0, z1)) 53.42/27.18
+'(s(z0), z1) → c3(+'(z0, z1)) 53.42/27.18
F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.42/27.18
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 53.42/27.18

POL(+(x1, x2)) = x1 + x2    53.42/27.18
POL(+'(x1, x2)) = [2]x2    53.42/27.18
POL(0) = 0    53.42/27.18
POL(F(x1)) = x12    53.42/27.18
POL(c1(x1)) = x1    53.42/27.18
POL(c3(x1)) = x1    53.42/27.18
POL(c4(x1, x2)) = x1 + x2    53.42/27.18
POL(c7(x1, x2)) = x1 + x2    53.42/27.18
POL(h(x1, x2)) = [1] + x1 + x2    53.42/27.18
POL(s(x1)) = [2] + x1   
53.42/27.18
53.42/27.18

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, 0) → z0 53.42/27.18
+(z0, s(z1)) → s(+(z0, z1)) 53.42/27.18
+(0, z0) → z0 53.42/27.18
+(s(z0), z1) → s(+(z0, z1)) 53.42/27.18
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 53.42/27.18
f(g(f(z0))) → f(h(s(0), z0)) 53.42/27.18
f(g(h(z0, z1))) → f(h(s(z0), z1)) 53.42/27.18
f(h(z0, h(z1, z2))) → f(h(+(z0, z1), z2))
Tuples:

+'(z0, s(z1)) → c1(+'(z0, z1)) 53.42/27.18
+'(s(z0), z1) → c3(+'(z0, z1)) 53.42/27.18
F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.42/27.18
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1))
S tuples:

+'(s(z0), z1) → c3(+'(z0, z1)) 53.42/27.18
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1))
K tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.42/27.18
+'(z0, s(z1)) → c1(+'(z0, z1))
Defined Rule Symbols:

+, f

Defined Pair Symbols:

+', F

Compound Symbols:

c1, c3, c7, c4

53.74/27.22
53.74/27.22

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

+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1))
We considered the (Usable) Rules:

+(0, z0) → z0 53.74/27.22
+(s(z0), z1) → s(+(z0, z1)) 53.74/27.22
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 53.74/27.22
+(z0, 0) → z0 53.74/27.22
+(z0, s(z1)) → s(+(z0, z1))
And the Tuples:

+'(z0, s(z1)) → c1(+'(z0, z1)) 53.74/27.22
+'(s(z0), z1) → c3(+'(z0, z1)) 53.74/27.22
F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 53.74/27.22

POL(+(x1, x2)) = [2] + x1 + x2    53.74/27.22
POL(+'(x1, x2)) = [1] + x2    53.74/27.22
POL(0) = 0    53.74/27.22
POL(F(x1)) = x12    53.74/27.22
POL(c1(x1)) = x1    53.74/27.22
POL(c3(x1)) = x1    53.74/27.22
POL(c4(x1, x2)) = x1 + x2    53.74/27.22
POL(c7(x1, x2)) = x1 + x2    53.74/27.22
POL(h(x1, x2)) = [3] + x1 + x2    53.74/27.22
POL(s(x1)) = x1   
53.74/27.22
53.74/27.22

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, 0) → z0 53.74/27.22
+(z0, s(z1)) → s(+(z0, z1)) 53.74/27.22
+(0, z0) → z0 53.74/27.22
+(s(z0), z1) → s(+(z0, z1)) 53.74/27.22
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 53.74/27.22
f(g(f(z0))) → f(h(s(0), z0)) 53.74/27.22
f(g(h(z0, z1))) → f(h(s(z0), z1)) 53.74/27.22
f(h(z0, h(z1, z2))) → f(h(+(z0, z1), z2))
Tuples:

+'(z0, s(z1)) → c1(+'(z0, z1)) 53.74/27.22
+'(s(z0), z1) → c3(+'(z0, z1)) 53.74/27.22
F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1))
S tuples:

+'(s(z0), z1) → c3(+'(z0, z1))
K tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, s(z1)) → c1(+'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1))
Defined Rule Symbols:

+, f

Defined Pair Symbols:

+', F

Compound Symbols:

c1, c3, c7, c4

53.74/27.22
53.74/27.22

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

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

+'(z0, s(s(y1))) → c1(+'(z0, s(y1))) 53.74/27.22
+'(s(y0), s(z1)) → c1(+'(s(y0), z1)) 53.74/27.22
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2)))
53.74/27.22
53.74/27.22

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, 0) → z0 53.74/27.22
+(z0, s(z1)) → s(+(z0, z1)) 53.74/27.22
+(0, z0) → z0 53.74/27.22
+(s(z0), z1) → s(+(z0, z1)) 53.74/27.22
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 53.74/27.22
f(g(f(z0))) → f(h(s(0), z0)) 53.74/27.22
f(g(h(z0, z1))) → f(h(s(z0), z1)) 53.74/27.22
f(h(z0, h(z1, z2))) → f(h(+(z0, z1), z2))
Tuples:

+'(s(z0), z1) → c3(+'(z0, z1)) 53.74/27.22
F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.74/27.22
+'(z0, s(s(y1))) → c1(+'(z0, s(y1))) 53.74/27.22
+'(s(y0), s(z1)) → c1(+'(s(y0), z1)) 53.74/27.22
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2)))
S tuples:

+'(s(z0), z1) → c3(+'(z0, z1))
K tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.74/27.22
+'(z0, s(s(y1))) → c1(+'(z0, s(y1))) 53.74/27.22
+'(s(y0), s(z1)) → c1(+'(s(y0), z1)) 53.74/27.22
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2)))
Defined Rule Symbols:

+, f

Defined Pair Symbols:

+', F

Compound Symbols:

c3, c7, c4, c1

53.74/27.22
53.74/27.22

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

Use forward instantiation to replace +'(s(z0), z1) → c3(+'(z0, z1)) by

+'(s(s(y0)), z1) → c3(+'(s(y0), z1)) 53.74/27.22
+'(s(z0), +(y1, y2)) → c3(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(z0), s(s(y1))) → c3(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(s(y0)), s(y1)) → c3(+'(s(y0), s(y1))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c3(+'(z0, s(+(y1, y2))))
53.74/27.22
53.74/27.22

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, 0) → z0 53.74/27.22
+(z0, s(z1)) → s(+(z0, z1)) 53.74/27.22
+(0, z0) → z0 53.74/27.22
+(s(z0), z1) → s(+(z0, z1)) 53.74/27.22
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 53.74/27.22
f(g(f(z0))) → f(h(s(0), z0)) 53.74/27.22
f(g(h(z0, z1))) → f(h(s(z0), z1)) 53.74/27.22
f(h(z0, h(z1, z2))) → f(h(+(z0, z1), z2))
Tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.74/27.22
+'(z0, s(s(y1))) → c1(+'(z0, s(y1))) 53.74/27.22
+'(s(y0), s(z1)) → c1(+'(s(y0), z1)) 53.74/27.22
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(s(y0)), z1) → c3(+'(s(y0), z1)) 53.74/27.22
+'(s(z0), +(y1, y2)) → c3(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(z0), s(s(y1))) → c3(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(s(y0)), s(y1)) → c3(+'(s(y0), s(y1))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c3(+'(z0, s(+(y1, y2))))
S tuples:

+'(s(s(y0)), z1) → c3(+'(s(y0), z1)) 53.74/27.22
+'(s(z0), +(y1, y2)) → c3(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(z0), s(s(y1))) → c3(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(s(y0)), s(y1)) → c3(+'(s(y0), s(y1))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c3(+'(z0, s(+(y1, y2))))
K tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.74/27.22
+'(z0, s(s(y1))) → c1(+'(z0, s(y1))) 53.74/27.22
+'(s(y0), s(z1)) → c1(+'(s(y0), z1)) 53.74/27.22
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2)))
Defined Rule Symbols:

+, f

Defined Pair Symbols:

F, +'

Compound Symbols:

c7, c4, c1, c3

53.74/27.22
53.74/27.22

(17) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))) transformation)

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

+'(s(z0), s(s(y1))) → c3(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(s(y0)), s(y1)) → c3(+'(s(y0), s(y1))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c3(+'(z0, s(+(y1, y2))))
We considered the (Usable) Rules:

+(0, z0) → z0 53.74/27.22
+(s(z0), z1) → s(+(z0, z1)) 53.74/27.22
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 53.74/27.22
+(z0, 0) → z0 53.74/27.22
+(z0, s(z1)) → s(+(z0, z1))
And the Tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.74/27.22
+'(z0, s(s(y1))) → c1(+'(z0, s(y1))) 53.74/27.22
+'(s(y0), s(z1)) → c1(+'(s(y0), z1)) 53.74/27.22
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(s(y0)), z1) → c3(+'(s(y0), z1)) 53.74/27.22
+'(s(z0), +(y1, y2)) → c3(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(z0), s(s(y1))) → c3(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(s(y0)), s(y1)) → c3(+'(s(y0), s(y1))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c3(+'(z0, s(+(y1, y2))))
The order we found is given by the following interpretation:
Polynomial interpretation : 53.74/27.22

POL(+(x1, x2)) = x1 + x2    53.74/27.22
POL(+'(x1, x2)) = x22 + x1·x2    53.74/27.22
POL(0) = [1]    53.74/27.22
POL(F(x1)) = x13    53.74/27.22
POL(c1(x1)) = x1    53.74/27.22
POL(c3(x1)) = x1    53.74/27.22
POL(c4(x1, x2)) = x1 + x2    53.74/27.22
POL(c7(x1, x2)) = x1 + x2    53.74/27.22
POL(h(x1, x2)) = [1] + x1 + x2    53.74/27.22
POL(s(x1)) = [1] + x1   
53.74/27.22
53.74/27.22

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, 0) → z0 53.74/27.22
+(z0, s(z1)) → s(+(z0, z1)) 53.74/27.22
+(0, z0) → z0 53.74/27.22
+(s(z0), z1) → s(+(z0, z1)) 53.74/27.22
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 53.74/27.22
f(g(f(z0))) → f(h(s(0), z0)) 53.74/27.22
f(g(h(z0, z1))) → f(h(s(z0), z1)) 53.74/27.22
f(h(z0, h(z1, z2))) → f(h(+(z0, z1), z2))
Tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.74/27.22
+'(z0, s(s(y1))) → c1(+'(z0, s(y1))) 53.74/27.22
+'(s(y0), s(z1)) → c1(+'(s(y0), z1)) 53.74/27.22
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(s(y0)), z1) → c3(+'(s(y0), z1)) 53.74/27.22
+'(s(z0), +(y1, y2)) → c3(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(z0), s(s(y1))) → c3(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(s(y0)), s(y1)) → c3(+'(s(y0), s(y1))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c3(+'(z0, s(+(y1, y2))))
S tuples:

+'(s(s(y0)), z1) → c3(+'(s(y0), z1)) 53.74/27.22
+'(s(z0), +(y1, y2)) → c3(+'(z0, +(y1, y2)))
K tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.74/27.22
+'(z0, s(s(y1))) → c1(+'(z0, s(y1))) 53.74/27.22
+'(s(y0), s(z1)) → c1(+'(s(y0), z1)) 53.74/27.22
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(z0), s(s(y1))) → c3(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(s(y0)), s(y1)) → c3(+'(s(y0), s(y1))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c3(+'(z0, s(+(y1, y2))))
Defined Rule Symbols:

+, f

Defined Pair Symbols:

F, +'

Compound Symbols:

c7, c4, c1, c3

53.74/27.22
53.74/27.22

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

Use forward instantiation to replace +'(z0, s(s(y1))) → c1(+'(z0, s(y1))) by

+'(z0, s(s(s(y1)))) → c1(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(z1))) → c1(+'(s(y0), s(z1))) 53.74/27.22
+'(z0, s(s(+(y1, y2)))) → c1(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(s(s(y0)), s(s(z1))) → c1(+'(s(s(y0)), s(z1))) 53.74/27.22
+'(s(y0), s(s(s(y1)))) → c1(+'(s(y0), s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(+(y1, y2)))) → c1(+'(s(y0), s(+(y1, y2))))
53.74/27.22
53.74/27.22

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, 0) → z0 53.74/27.22
+(z0, s(z1)) → s(+(z0, z1)) 53.74/27.22
+(0, z0) → z0 53.74/27.22
+(s(z0), z1) → s(+(z0, z1)) 53.74/27.22
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 53.74/27.22
f(g(f(z0))) → f(h(s(0), z0)) 53.74/27.22
f(g(h(z0, z1))) → f(h(s(z0), z1)) 53.74/27.22
f(h(z0, h(z1, z2))) → f(h(+(z0, z1), z2))
Tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.74/27.22
+'(s(y0), s(z1)) → c1(+'(s(y0), z1)) 53.74/27.22
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(s(y0)), z1) → c3(+'(s(y0), z1)) 53.74/27.22
+'(s(z0), +(y1, y2)) → c3(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(z0), s(s(y1))) → c3(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(s(y0)), s(y1)) → c3(+'(s(y0), s(y1))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c3(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(z0, s(s(s(y1)))) → c1(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(z1))) → c1(+'(s(y0), s(z1))) 53.74/27.22
+'(z0, s(s(+(y1, y2)))) → c1(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(s(s(y0)), s(s(z1))) → c1(+'(s(s(y0)), s(z1))) 53.74/27.22
+'(s(y0), s(s(s(y1)))) → c1(+'(s(y0), s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(+(y1, y2)))) → c1(+'(s(y0), s(+(y1, y2))))
S tuples:

+'(s(s(y0)), z1) → c3(+'(s(y0), z1)) 53.74/27.22
+'(s(z0), +(y1, y2)) → c3(+'(z0, +(y1, y2)))
K tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.74/27.22
+'(s(y0), s(z1)) → c1(+'(s(y0), z1)) 53.74/27.22
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(z0), s(s(y1))) → c3(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(s(y0)), s(y1)) → c3(+'(s(y0), s(y1))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c3(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(z0, s(s(s(y1)))) → c1(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(z1))) → c1(+'(s(y0), s(z1))) 53.74/27.22
+'(z0, s(s(+(y1, y2)))) → c1(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(s(s(y0)), s(s(z1))) → c1(+'(s(s(y0)), s(z1))) 53.74/27.22
+'(s(y0), s(s(s(y1)))) → c1(+'(s(y0), s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(+(y1, y2)))) → c1(+'(s(y0), s(+(y1, y2))))
Defined Rule Symbols:

+, f

Defined Pair Symbols:

F, +'

Compound Symbols:

c7, c4, c1, c3

53.74/27.22
53.74/27.22

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

Use forward instantiation to replace +'(s(y0), s(z1)) → c1(+'(s(y0), z1)) by

+'(s(z0), s(+(y1, y2))) → c1(+'(s(z0), +(y1, y2))) 53.74/27.22
+'(s(z0), s(s(y1))) → c1(+'(s(z0), s(y1))) 53.74/27.22
+'(s(z0), s(s(+(y1, y2)))) → c1(+'(s(z0), s(+(y1, y2)))) 53.74/27.22
+'(s(s(y0)), s(z1)) → c1(+'(s(s(y0)), z1)) 53.74/27.22
+'(s(z0), s(s(s(y1)))) → c1(+'(s(z0), s(s(y1)))) 53.74/27.22
+'(s(s(y0)), s(s(y1))) → c1(+'(s(s(y0)), s(y1))) 53.74/27.22
+'(s(z0), s(s(s(s(y1))))) → c1(+'(s(z0), s(s(s(y1))))) 53.74/27.22
+'(s(z0), s(s(s(+(y1, y2))))) → c1(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(y0)), s(s(s(y1)))) → c1(+'(s(s(y0)), s(s(y1))))
53.74/27.22
53.74/27.22

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, 0) → z0 53.74/27.22
+(z0, s(z1)) → s(+(z0, z1)) 53.74/27.22
+(0, z0) → z0 53.74/27.22
+(s(z0), z1) → s(+(z0, z1)) 53.74/27.22
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 53.74/27.22
f(g(f(z0))) → f(h(s(0), z0)) 53.74/27.22
f(g(h(z0, z1))) → f(h(s(z0), z1)) 53.74/27.22
f(h(z0, h(z1, z2))) → f(h(+(z0, z1), z2))
Tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.74/27.22
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(s(y0)), z1) → c3(+'(s(y0), z1)) 53.74/27.22
+'(s(z0), +(y1, y2)) → c3(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(z0), s(s(y1))) → c3(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(s(y0)), s(y1)) → c3(+'(s(y0), s(y1))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c3(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(z0, s(s(s(y1)))) → c1(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(z1))) → c1(+'(s(y0), s(z1))) 53.74/27.22
+'(z0, s(s(+(y1, y2)))) → c1(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(s(s(y0)), s(s(z1))) → c1(+'(s(s(y0)), s(z1))) 53.74/27.22
+'(s(y0), s(s(s(y1)))) → c1(+'(s(y0), s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(+(y1, y2)))) → c1(+'(s(y0), s(+(y1, y2)))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c1(+'(s(z0), +(y1, y2))) 53.74/27.22
+'(s(s(y0)), s(z1)) → c1(+'(s(s(y0)), z1)) 53.74/27.22
+'(s(z0), s(s(s(s(y1))))) → c1(+'(s(z0), s(s(s(y1))))) 53.74/27.22
+'(s(z0), s(s(s(+(y1, y2))))) → c1(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(y0)), s(s(s(y1)))) → c1(+'(s(s(y0)), s(s(y1))))
S tuples:

+'(s(s(y0)), z1) → c3(+'(s(y0), z1)) 53.74/27.22
+'(s(z0), +(y1, y2)) → c3(+'(z0, +(y1, y2)))
K tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.74/27.22
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(z0), s(s(y1))) → c3(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(s(y0)), s(y1)) → c3(+'(s(y0), s(y1))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c3(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(z0, s(s(s(y1)))) → c1(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(z1))) → c1(+'(s(y0), s(z1))) 53.74/27.22
+'(z0, s(s(+(y1, y2)))) → c1(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(s(s(y0)), s(s(z1))) → c1(+'(s(s(y0)), s(z1))) 53.74/27.22
+'(s(y0), s(s(s(y1)))) → c1(+'(s(y0), s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(+(y1, y2)))) → c1(+'(s(y0), s(+(y1, y2)))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c1(+'(s(z0), +(y1, y2))) 53.74/27.22
+'(s(s(y0)), s(z1)) → c1(+'(s(s(y0)), z1)) 53.74/27.22
+'(s(z0), s(s(s(s(y1))))) → c1(+'(s(z0), s(s(s(y1))))) 53.74/27.22
+'(s(z0), s(s(s(+(y1, y2))))) → c1(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(y0)), s(s(s(y1)))) → c1(+'(s(s(y0)), s(s(y1))))
Defined Rule Symbols:

+, f

Defined Pair Symbols:

F, +'

Compound Symbols:

c7, c4, c1, c3

53.74/27.22
53.74/27.22

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

Use forward instantiation to replace +'(s(s(y0)), z1) → c3(+'(s(y0), z1)) by

+'(s(s(z0)), +(y1, y2)) → c3(+'(s(z0), +(y1, y2))) 53.74/27.22
+'(s(s(z0)), s(+(y1, y2))) → c3(+'(s(z0), s(+(y1, y2)))) 53.74/27.22
+'(s(s(s(y0))), z1) → c3(+'(s(s(y0)), z1)) 53.74/27.22
+'(s(s(z0)), s(s(y1))) → c3(+'(s(z0), s(s(y1)))) 53.74/27.22
+'(s(s(s(y0))), s(y1)) → c3(+'(s(s(y0)), s(y1))) 53.74/27.22
+'(s(s(z0)), s(s(s(y1)))) → c3(+'(s(z0), s(s(s(y1))))) 53.74/27.22
+'(s(s(z0)), s(s(+(y1, y2)))) → c3(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(s(y0))), s(s(y1))) → c3(+'(s(s(y0)), s(s(y1)))) 53.74/27.22
+'(s(s(z0)), s(s(s(s(y1))))) → c3(+'(s(z0), s(s(s(s(y1)))))) 53.74/27.22
+'(s(s(z0)), s(s(s(+(y1, y2))))) → c3(+'(s(z0), s(s(s(+(y1, y2)))))) 53.74/27.22
+'(s(s(s(y0))), s(s(s(y1)))) → c3(+'(s(s(y0)), s(s(s(y1)))))
53.74/27.22
53.74/27.22

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, 0) → z0 53.74/27.22
+(z0, s(z1)) → s(+(z0, z1)) 53.74/27.22
+(0, z0) → z0 53.74/27.22
+(s(z0), z1) → s(+(z0, z1)) 53.74/27.22
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 53.74/27.22
f(g(f(z0))) → f(h(s(0), z0)) 53.74/27.22
f(g(h(z0, z1))) → f(h(s(z0), z1)) 53.74/27.22
f(h(z0, h(z1, z2))) → f(h(+(z0, z1), z2))
Tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.74/27.22
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(z0), +(y1, y2)) → c3(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(z0), s(s(y1))) → c3(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(s(y0)), s(y1)) → c3(+'(s(y0), s(y1))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c3(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(z0, s(s(s(y1)))) → c1(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(z1))) → c1(+'(s(y0), s(z1))) 53.74/27.22
+'(z0, s(s(+(y1, y2)))) → c1(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(s(s(y0)), s(s(z1))) → c1(+'(s(s(y0)), s(z1))) 53.74/27.22
+'(s(y0), s(s(s(y1)))) → c1(+'(s(y0), s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(+(y1, y2)))) → c1(+'(s(y0), s(+(y1, y2)))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c1(+'(s(z0), +(y1, y2))) 53.74/27.22
+'(s(s(y0)), s(z1)) → c1(+'(s(s(y0)), z1)) 53.74/27.22
+'(s(z0), s(s(s(s(y1))))) → c1(+'(s(z0), s(s(s(y1))))) 53.74/27.22
+'(s(z0), s(s(s(+(y1, y2))))) → c1(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(y0)), s(s(s(y1)))) → c1(+'(s(s(y0)), s(s(y1)))) 53.74/27.22
+'(s(s(z0)), +(y1, y2)) → c3(+'(s(z0), +(y1, y2))) 53.74/27.22
+'(s(s(z0)), s(+(y1, y2))) → c3(+'(s(z0), s(+(y1, y2)))) 53.74/27.22
+'(s(s(s(y0))), z1) → c3(+'(s(s(y0)), z1)) 53.74/27.22
+'(s(s(z0)), s(s(y1))) → c3(+'(s(z0), s(s(y1)))) 53.74/27.22
+'(s(s(s(y0))), s(y1)) → c3(+'(s(s(y0)), s(y1))) 53.74/27.22
+'(s(s(z0)), s(s(s(y1)))) → c3(+'(s(z0), s(s(s(y1))))) 53.74/27.22
+'(s(s(z0)), s(s(+(y1, y2)))) → c3(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(s(y0))), s(s(y1))) → c3(+'(s(s(y0)), s(s(y1)))) 53.74/27.22
+'(s(s(z0)), s(s(s(s(y1))))) → c3(+'(s(z0), s(s(s(s(y1)))))) 53.74/27.22
+'(s(s(z0)), s(s(s(+(y1, y2))))) → c3(+'(s(z0), s(s(s(+(y1, y2)))))) 53.74/27.22
+'(s(s(s(y0))), s(s(s(y1)))) → c3(+'(s(s(y0)), s(s(s(y1)))))
S tuples:

+'(s(z0), +(y1, y2)) → c3(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(s(z0)), +(y1, y2)) → c3(+'(s(z0), +(y1, y2))) 53.74/27.22
+'(s(s(z0)), s(+(y1, y2))) → c3(+'(s(z0), s(+(y1, y2)))) 53.74/27.22
+'(s(s(s(y0))), z1) → c3(+'(s(s(y0)), z1)) 53.74/27.22
+'(s(s(z0)), s(s(y1))) → c3(+'(s(z0), s(s(y1)))) 53.74/27.22
+'(s(s(s(y0))), s(y1)) → c3(+'(s(s(y0)), s(y1))) 53.74/27.22
+'(s(s(z0)), s(s(s(y1)))) → c3(+'(s(z0), s(s(s(y1))))) 53.74/27.22
+'(s(s(z0)), s(s(+(y1, y2)))) → c3(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(s(y0))), s(s(y1))) → c3(+'(s(s(y0)), s(s(y1)))) 53.74/27.22
+'(s(s(z0)), s(s(s(s(y1))))) → c3(+'(s(z0), s(s(s(s(y1)))))) 53.74/27.22
+'(s(s(z0)), s(s(s(+(y1, y2))))) → c3(+'(s(z0), s(s(s(+(y1, y2)))))) 53.74/27.22
+'(s(s(s(y0))), s(s(s(y1)))) → c3(+'(s(s(y0)), s(s(s(y1)))))
K tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.74/27.22
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(z0), s(s(y1))) → c3(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(s(y0)), s(y1)) → c3(+'(s(y0), s(y1))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c3(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(z0, s(s(s(y1)))) → c1(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(z1))) → c1(+'(s(y0), s(z1))) 53.74/27.22
+'(z0, s(s(+(y1, y2)))) → c1(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(s(s(y0)), s(s(z1))) → c1(+'(s(s(y0)), s(z1))) 53.74/27.22
+'(s(y0), s(s(s(y1)))) → c1(+'(s(y0), s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(+(y1, y2)))) → c1(+'(s(y0), s(+(y1, y2)))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c1(+'(s(z0), +(y1, y2))) 53.74/27.22
+'(s(s(y0)), s(z1)) → c1(+'(s(s(y0)), z1)) 53.74/27.22
+'(s(z0), s(s(s(s(y1))))) → c1(+'(s(z0), s(s(s(y1))))) 53.74/27.22
+'(s(z0), s(s(s(+(y1, y2))))) → c1(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(y0)), s(s(s(y1)))) → c1(+'(s(s(y0)), s(s(y1))))
Defined Rule Symbols:

+, f

Defined Pair Symbols:

F, +'

Compound Symbols:

c7, c4, c1, c3

53.74/27.22
53.74/27.22

(25) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))) transformation)

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

+'(s(s(z0)), s(+(y1, y2))) → c3(+'(s(z0), s(+(y1, y2)))) 53.74/27.22
+'(s(s(z0)), s(s(y1))) → c3(+'(s(z0), s(s(y1)))) 53.74/27.22
+'(s(s(s(y0))), s(y1)) → c3(+'(s(s(y0)), s(y1))) 53.74/27.22
+'(s(s(z0)), s(s(s(y1)))) → c3(+'(s(z0), s(s(s(y1))))) 53.74/27.22
+'(s(s(z0)), s(s(+(y1, y2)))) → c3(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(s(y0))), s(s(y1))) → c3(+'(s(s(y0)), s(s(y1)))) 53.74/27.22
+'(s(s(z0)), s(s(s(s(y1))))) → c3(+'(s(z0), s(s(s(s(y1)))))) 53.74/27.22
+'(s(s(z0)), s(s(s(+(y1, y2))))) → c3(+'(s(z0), s(s(s(+(y1, y2)))))) 53.74/27.22
+'(s(s(s(y0))), s(s(s(y1)))) → c3(+'(s(s(y0)), s(s(s(y1)))))
We considered the (Usable) Rules:

+(0, z0) → z0 53.74/27.22
+(s(z0), z1) → s(+(z0, z1)) 53.74/27.22
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 53.74/27.22
+(z0, 0) → z0 53.74/27.22
+(z0, s(z1)) → s(+(z0, z1))
And the Tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.74/27.22
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(z0), +(y1, y2)) → c3(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(z0), s(s(y1))) → c3(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(s(y0)), s(y1)) → c3(+'(s(y0), s(y1))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c3(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(z0, s(s(s(y1)))) → c1(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(z1))) → c1(+'(s(y0), s(z1))) 53.74/27.22
+'(z0, s(s(+(y1, y2)))) → c1(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(s(s(y0)), s(s(z1))) → c1(+'(s(s(y0)), s(z1))) 53.74/27.22
+'(s(y0), s(s(s(y1)))) → c1(+'(s(y0), s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(+(y1, y2)))) → c1(+'(s(y0), s(+(y1, y2)))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c1(+'(s(z0), +(y1, y2))) 53.74/27.22
+'(s(s(y0)), s(z1)) → c1(+'(s(s(y0)), z1)) 53.74/27.22
+'(s(z0), s(s(s(s(y1))))) → c1(+'(s(z0), s(s(s(y1))))) 53.74/27.22
+'(s(z0), s(s(s(+(y1, y2))))) → c1(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(y0)), s(s(s(y1)))) → c1(+'(s(s(y0)), s(s(y1)))) 53.74/27.22
+'(s(s(z0)), +(y1, y2)) → c3(+'(s(z0), +(y1, y2))) 53.74/27.22
+'(s(s(z0)), s(+(y1, y2))) → c3(+'(s(z0), s(+(y1, y2)))) 53.74/27.22
+'(s(s(s(y0))), z1) → c3(+'(s(s(y0)), z1)) 53.74/27.22
+'(s(s(z0)), s(s(y1))) → c3(+'(s(z0), s(s(y1)))) 53.74/27.22
+'(s(s(s(y0))), s(y1)) → c3(+'(s(s(y0)), s(y1))) 53.74/27.22
+'(s(s(z0)), s(s(s(y1)))) → c3(+'(s(z0), s(s(s(y1))))) 53.74/27.22
+'(s(s(z0)), s(s(+(y1, y2)))) → c3(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(s(y0))), s(s(y1))) → c3(+'(s(s(y0)), s(s(y1)))) 53.74/27.22
+'(s(s(z0)), s(s(s(s(y1))))) → c3(+'(s(z0), s(s(s(s(y1)))))) 53.74/27.22
+'(s(s(z0)), s(s(s(+(y1, y2))))) → c3(+'(s(z0), s(s(s(+(y1, y2)))))) 53.74/27.22
+'(s(s(s(y0))), s(s(s(y1)))) → c3(+'(s(s(y0)), s(s(s(y1)))))
The order we found is given by the following interpretation:
Polynomial interpretation : 53.74/27.22

POL(+(x1, x2)) = x1 + x2    53.74/27.22
POL(+'(x1, x2)) = x22 + x1·x2    53.74/27.22
POL(0) = [1]    53.74/27.22
POL(F(x1)) = x13    53.74/27.22
POL(c1(x1)) = x1    53.74/27.22
POL(c3(x1)) = x1    53.74/27.22
POL(c4(x1, x2)) = x1 + x2    53.74/27.22
POL(c7(x1, x2)) = x1 + x2    53.74/27.22
POL(h(x1, x2)) = [1] + x1 + x2    53.74/27.22
POL(s(x1)) = [1] + x1   
53.74/27.22
53.74/27.22

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, 0) → z0 53.74/27.22
+(z0, s(z1)) → s(+(z0, z1)) 53.74/27.22
+(0, z0) → z0 53.74/27.22
+(s(z0), z1) → s(+(z0, z1)) 53.74/27.22
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 53.74/27.22
f(g(f(z0))) → f(h(s(0), z0)) 53.74/27.22
f(g(h(z0, z1))) → f(h(s(z0), z1)) 53.74/27.22
f(h(z0, h(z1, z2))) → f(h(+(z0, z1), z2))
Tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.74/27.22
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(z0), +(y1, y2)) → c3(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(z0), s(s(y1))) → c3(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(s(y0)), s(y1)) → c3(+'(s(y0), s(y1))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c3(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(z0, s(s(s(y1)))) → c1(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(z1))) → c1(+'(s(y0), s(z1))) 53.74/27.22
+'(z0, s(s(+(y1, y2)))) → c1(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(s(s(y0)), s(s(z1))) → c1(+'(s(s(y0)), s(z1))) 53.74/27.22
+'(s(y0), s(s(s(y1)))) → c1(+'(s(y0), s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(+(y1, y2)))) → c1(+'(s(y0), s(+(y1, y2)))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c1(+'(s(z0), +(y1, y2))) 53.74/27.22
+'(s(s(y0)), s(z1)) → c1(+'(s(s(y0)), z1)) 53.74/27.22
+'(s(z0), s(s(s(s(y1))))) → c1(+'(s(z0), s(s(s(y1))))) 53.74/27.22
+'(s(z0), s(s(s(+(y1, y2))))) → c1(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(y0)), s(s(s(y1)))) → c1(+'(s(s(y0)), s(s(y1)))) 53.74/27.22
+'(s(s(z0)), +(y1, y2)) → c3(+'(s(z0), +(y1, y2))) 53.74/27.22
+'(s(s(z0)), s(+(y1, y2))) → c3(+'(s(z0), s(+(y1, y2)))) 53.74/27.22
+'(s(s(s(y0))), z1) → c3(+'(s(s(y0)), z1)) 53.74/27.22
+'(s(s(z0)), s(s(y1))) → c3(+'(s(z0), s(s(y1)))) 53.74/27.22
+'(s(s(s(y0))), s(y1)) → c3(+'(s(s(y0)), s(y1))) 53.74/27.22
+'(s(s(z0)), s(s(s(y1)))) → c3(+'(s(z0), s(s(s(y1))))) 53.74/27.22
+'(s(s(z0)), s(s(+(y1, y2)))) → c3(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(s(y0))), s(s(y1))) → c3(+'(s(s(y0)), s(s(y1)))) 53.74/27.22
+'(s(s(z0)), s(s(s(s(y1))))) → c3(+'(s(z0), s(s(s(s(y1)))))) 53.74/27.22
+'(s(s(z0)), s(s(s(+(y1, y2))))) → c3(+'(s(z0), s(s(s(+(y1, y2)))))) 53.74/27.22
+'(s(s(s(y0))), s(s(s(y1)))) → c3(+'(s(s(y0)), s(s(s(y1)))))
S tuples:

+'(s(z0), +(y1, y2)) → c3(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(s(z0)), +(y1, y2)) → c3(+'(s(z0), +(y1, y2))) 53.74/27.22
+'(s(s(s(y0))), z1) → c3(+'(s(s(y0)), z1))
K tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.74/27.22
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(z0), s(s(y1))) → c3(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(s(y0)), s(y1)) → c3(+'(s(y0), s(y1))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c3(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(z0, s(s(s(y1)))) → c1(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(z1))) → c1(+'(s(y0), s(z1))) 53.74/27.22
+'(z0, s(s(+(y1, y2)))) → c1(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(s(s(y0)), s(s(z1))) → c1(+'(s(s(y0)), s(z1))) 53.74/27.22
+'(s(y0), s(s(s(y1)))) → c1(+'(s(y0), s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(+(y1, y2)))) → c1(+'(s(y0), s(+(y1, y2)))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c1(+'(s(z0), +(y1, y2))) 53.74/27.22
+'(s(s(y0)), s(z1)) → c1(+'(s(s(y0)), z1)) 53.74/27.22
+'(s(z0), s(s(s(s(y1))))) → c1(+'(s(z0), s(s(s(y1))))) 53.74/27.22
+'(s(z0), s(s(s(+(y1, y2))))) → c1(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(y0)), s(s(s(y1)))) → c1(+'(s(s(y0)), s(s(y1)))) 53.74/27.22
+'(s(s(z0)), s(+(y1, y2))) → c3(+'(s(z0), s(+(y1, y2)))) 53.74/27.22
+'(s(s(z0)), s(s(y1))) → c3(+'(s(z0), s(s(y1)))) 53.74/27.22
+'(s(s(s(y0))), s(y1)) → c3(+'(s(s(y0)), s(y1))) 53.74/27.22
+'(s(s(z0)), s(s(s(y1)))) → c3(+'(s(z0), s(s(s(y1))))) 53.74/27.22
+'(s(s(z0)), s(s(+(y1, y2)))) → c3(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(s(y0))), s(s(y1))) → c3(+'(s(s(y0)), s(s(y1)))) 53.74/27.22
+'(s(s(z0)), s(s(s(s(y1))))) → c3(+'(s(z0), s(s(s(s(y1)))))) 53.74/27.22
+'(s(s(z0)), s(s(s(+(y1, y2))))) → c3(+'(s(z0), s(s(s(+(y1, y2)))))) 53.74/27.22
+'(s(s(s(y0))), s(s(s(y1)))) → c3(+'(s(s(y0)), s(s(s(y1)))))
Defined Rule Symbols:

+, f

Defined Pair Symbols:

F, +'

Compound Symbols:

c7, c4, c1, c3

53.74/27.22
53.74/27.22

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

Use forward instantiation to replace +'(s(z0), s(s(y1))) → c3(+'(z0, s(s(y1)))) by

+'(s(s(y0)), s(s(z1))) → c3(+'(s(y0), s(s(z1)))) 53.74/27.22
+'(s(s(s(y0))), s(s(z1))) → c3(+'(s(s(y0)), s(s(z1)))) 53.74/27.22
+'(s(z0), s(s(s(y1)))) → c3(+'(z0, s(s(s(y1))))) 53.74/27.22
+'(s(z0), s(s(+(y1, y2)))) → c3(+'(z0, s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(y0)), s(s(s(y1)))) → c3(+'(s(y0), s(s(s(y1))))) 53.74/27.22
+'(s(s(y0)), s(s(+(y1, y2)))) → c3(+'(s(y0), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(y0)), s(s(s(s(y1))))) → c3(+'(s(y0), s(s(s(s(y1)))))) 53.74/27.22
+'(s(s(y0)), s(s(s(+(y1, y2))))) → c3(+'(s(y0), s(s(s(+(y1, y2)))))) 53.74/27.22
+'(s(s(s(y0))), s(s(s(y1)))) → c3(+'(s(s(y0)), s(s(s(y1))))) 53.74/27.22
+'(s(s(s(s(y0)))), s(s(z1))) → c3(+'(s(s(s(y0))), s(s(z1)))) 53.74/27.22
+'(s(s(s(y0))), s(s(+(y1, y2)))) → c3(+'(s(s(y0)), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(s(y0))), s(s(s(s(y1))))) → c3(+'(s(s(y0)), s(s(s(s(y1)))))) 53.74/27.22
+'(s(s(s(y0))), s(s(s(+(y1, y2))))) → c3(+'(s(s(y0)), s(s(s(+(y1, y2)))))) 53.74/27.22
+'(s(s(s(s(y0)))), s(s(s(y1)))) → c3(+'(s(s(s(y0))), s(s(s(y1)))))
53.74/27.22
53.74/27.22

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, 0) → z0 53.74/27.22
+(z0, s(z1)) → s(+(z0, z1)) 53.74/27.22
+(0, z0) → z0 53.74/27.22
+(s(z0), z1) → s(+(z0, z1)) 53.74/27.22
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 53.74/27.22
f(g(f(z0))) → f(h(s(0), z0)) 53.74/27.22
f(g(h(z0, z1))) → f(h(s(z0), z1)) 53.74/27.22
f(h(z0, h(z1, z2))) → f(h(+(z0, z1), z2))
Tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.74/27.22
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(z0), +(y1, y2)) → c3(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(s(y0)), s(y1)) → c3(+'(s(y0), s(y1))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c3(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(z0, s(s(s(y1)))) → c1(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(z1))) → c1(+'(s(y0), s(z1))) 53.74/27.22
+'(z0, s(s(+(y1, y2)))) → c1(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(s(s(y0)), s(s(z1))) → c1(+'(s(s(y0)), s(z1))) 53.74/27.22
+'(s(y0), s(s(s(y1)))) → c1(+'(s(y0), s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(+(y1, y2)))) → c1(+'(s(y0), s(+(y1, y2)))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c1(+'(s(z0), +(y1, y2))) 53.74/27.22
+'(s(s(y0)), s(z1)) → c1(+'(s(s(y0)), z1)) 53.74/27.22
+'(s(z0), s(s(s(s(y1))))) → c1(+'(s(z0), s(s(s(y1))))) 53.74/27.22
+'(s(z0), s(s(s(+(y1, y2))))) → c1(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(y0)), s(s(s(y1)))) → c1(+'(s(s(y0)), s(s(y1)))) 53.74/27.22
+'(s(s(z0)), +(y1, y2)) → c3(+'(s(z0), +(y1, y2))) 53.74/27.22
+'(s(s(z0)), s(+(y1, y2))) → c3(+'(s(z0), s(+(y1, y2)))) 53.74/27.22
+'(s(s(s(y0))), z1) → c3(+'(s(s(y0)), z1)) 53.74/27.22
+'(s(s(z0)), s(s(y1))) → c3(+'(s(z0), s(s(y1)))) 53.74/27.22
+'(s(s(s(y0))), s(y1)) → c3(+'(s(s(y0)), s(y1))) 53.74/27.22
+'(s(s(z0)), s(s(s(y1)))) → c3(+'(s(z0), s(s(s(y1))))) 53.74/27.22
+'(s(s(z0)), s(s(+(y1, y2)))) → c3(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(s(y0))), s(s(y1))) → c3(+'(s(s(y0)), s(s(y1)))) 53.74/27.22
+'(s(s(z0)), s(s(s(s(y1))))) → c3(+'(s(z0), s(s(s(s(y1)))))) 53.74/27.22
+'(s(s(z0)), s(s(s(+(y1, y2))))) → c3(+'(s(z0), s(s(s(+(y1, y2)))))) 53.74/27.22
+'(s(s(s(y0))), s(s(s(y1)))) → c3(+'(s(s(y0)), s(s(s(y1))))) 53.74/27.22
+'(s(z0), s(s(s(y1)))) → c3(+'(z0, s(s(s(y1))))) 53.74/27.22
+'(s(z0), s(s(+(y1, y2)))) → c3(+'(z0, s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(s(s(y0)))), s(s(z1))) → c3(+'(s(s(s(y0))), s(s(z1)))) 53.74/27.22
+'(s(s(s(y0))), s(s(+(y1, y2)))) → c3(+'(s(s(y0)), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(s(y0))), s(s(s(s(y1))))) → c3(+'(s(s(y0)), s(s(s(s(y1)))))) 53.74/27.22
+'(s(s(s(y0))), s(s(s(+(y1, y2))))) → c3(+'(s(s(y0)), s(s(s(+(y1, y2)))))) 53.74/27.22
+'(s(s(s(s(y0)))), s(s(s(y1)))) → c3(+'(s(s(s(y0))), s(s(s(y1)))))
S tuples:

+'(s(z0), +(y1, y2)) → c3(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(s(z0)), +(y1, y2)) → c3(+'(s(z0), +(y1, y2))) 53.74/27.22
+'(s(s(s(y0))), z1) → c3(+'(s(s(y0)), z1))
K tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.22
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.74/27.22
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2))) 53.74/27.22
+'(s(s(y0)), s(y1)) → c3(+'(s(y0), s(y1))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c3(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(z0, s(s(s(y1)))) → c1(+'(z0, s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(z1))) → c1(+'(s(y0), s(z1))) 53.74/27.22
+'(z0, s(s(+(y1, y2)))) → c1(+'(z0, s(+(y1, y2)))) 53.74/27.22
+'(s(s(y0)), s(s(z1))) → c1(+'(s(s(y0)), s(z1))) 53.74/27.22
+'(s(y0), s(s(s(y1)))) → c1(+'(s(y0), s(s(y1)))) 53.74/27.22
+'(s(y0), s(s(+(y1, y2)))) → c1(+'(s(y0), s(+(y1, y2)))) 53.74/27.22
+'(s(z0), s(+(y1, y2))) → c1(+'(s(z0), +(y1, y2))) 53.74/27.22
+'(s(s(y0)), s(z1)) → c1(+'(s(s(y0)), z1)) 53.74/27.22
+'(s(z0), s(s(s(s(y1))))) → c1(+'(s(z0), s(s(s(y1))))) 53.74/27.22
+'(s(z0), s(s(s(+(y1, y2))))) → c1(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(y0)), s(s(s(y1)))) → c1(+'(s(s(y0)), s(s(y1)))) 53.74/27.22
+'(s(s(z0)), s(+(y1, y2))) → c3(+'(s(z0), s(+(y1, y2)))) 53.74/27.22
+'(s(s(z0)), s(s(y1))) → c3(+'(s(z0), s(s(y1)))) 53.74/27.22
+'(s(s(s(y0))), s(y1)) → c3(+'(s(s(y0)), s(y1))) 53.74/27.22
+'(s(s(z0)), s(s(s(y1)))) → c3(+'(s(z0), s(s(s(y1))))) 53.74/27.22
+'(s(s(z0)), s(s(+(y1, y2)))) → c3(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(s(y0))), s(s(y1))) → c3(+'(s(s(y0)), s(s(y1)))) 53.74/27.22
+'(s(s(z0)), s(s(s(s(y1))))) → c3(+'(s(z0), s(s(s(s(y1)))))) 53.74/27.22
+'(s(s(z0)), s(s(s(+(y1, y2))))) → c3(+'(s(z0), s(s(s(+(y1, y2)))))) 53.74/27.22
+'(s(s(s(y0))), s(s(s(y1)))) → c3(+'(s(s(y0)), s(s(s(y1))))) 53.74/27.22
+'(s(z0), s(s(s(y1)))) → c3(+'(z0, s(s(s(y1))))) 53.74/27.22
+'(s(z0), s(s(+(y1, y2)))) → c3(+'(z0, s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(s(s(y0)))), s(s(z1))) → c3(+'(s(s(s(y0))), s(s(z1)))) 53.74/27.22
+'(s(s(s(y0))), s(s(+(y1, y2)))) → c3(+'(s(s(y0)), s(s(+(y1, y2))))) 53.74/27.22
+'(s(s(s(y0))), s(s(s(s(y1))))) → c3(+'(s(s(y0)), s(s(s(s(y1)))))) 53.74/27.22
+'(s(s(s(y0))), s(s(s(+(y1, y2))))) → c3(+'(s(s(y0)), s(s(s(+(y1, y2)))))) 53.74/27.22
+'(s(s(s(s(y0)))), s(s(s(y1)))) → c3(+'(s(s(s(y0))), s(s(s(y1)))))
Defined Rule Symbols:

+, f

Defined Pair Symbols:

F, +'

Compound Symbols:

c7, c4, c1, c3

53.74/27.22
53.74/27.22

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

Use forward instantiation to replace +'(s(s(y0)), s(y1)) → c3(+'(s(y0), s(y1))) by

+'(s(s(z0)), s(+(y1, y2))) → c3(+'(s(z0), s(+(y1, y2)))) 53.74/27.23
+'(s(s(s(y0))), s(z1)) → c3(+'(s(s(y0)), s(z1))) 53.74/27.23
+'(s(s(z0)), s(s(s(y1)))) → c3(+'(s(z0), s(s(s(y1))))) 53.74/27.23
+'(s(s(z0)), s(s(y1))) → c3(+'(s(z0), s(s(y1)))) 53.74/27.23
+'(s(s(z0)), s(s(+(y1, y2)))) → c3(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.23
+'(s(s(s(y0))), s(s(y1))) → c3(+'(s(s(y0)), s(s(y1)))) 53.74/27.23
+'(s(s(z0)), s(s(s(s(y1))))) → c3(+'(s(z0), s(s(s(s(y1)))))) 53.74/27.23
+'(s(s(z0)), s(s(s(+(y1, y2))))) → c3(+'(s(z0), s(s(s(+(y1, y2)))))) 53.74/27.23
+'(s(s(s(y0))), s(s(s(y1)))) → c3(+'(s(s(y0)), s(s(s(y1))))) 53.74/27.23
+'(s(s(s(y0))), s(+(y1, y2))) → c3(+'(s(s(y0)), s(+(y1, y2)))) 53.74/27.23
+'(s(s(s(s(y0)))), s(z1)) → c3(+'(s(s(s(y0))), s(z1))) 53.74/27.23
+'(s(s(s(y0))), s(s(+(y1, y2)))) → c3(+'(s(s(y0)), s(s(+(y1, y2))))) 53.74/27.23
+'(s(s(s(s(y0)))), s(s(y1))) → c3(+'(s(s(s(y0))), s(s(y1)))) 53.74/27.23
+'(s(s(s(y0))), s(s(s(s(y1))))) → c3(+'(s(s(y0)), s(s(s(s(y1)))))) 53.74/27.23
+'(s(s(s(y0))), s(s(s(+(y1, y2))))) → c3(+'(s(s(y0)), s(s(s(+(y1, y2)))))) 53.74/27.23
+'(s(s(s(s(y0)))), s(s(s(y1)))) → c3(+'(s(s(s(y0))), s(s(s(y1))))) 53.74/27.23
+'(s(s(s(s(s(y0))))), s(s(y1))) → c3(+'(s(s(s(s(y0)))), s(s(y1)))) 53.74/27.23
+'(s(s(s(s(y0)))), s(s(+(y1, y2)))) → c3(+'(s(s(s(y0))), s(s(+(y1, y2))))) 53.74/27.23
+'(s(s(s(s(y0)))), s(s(s(s(y1))))) → c3(+'(s(s(s(y0))), s(s(s(s(y1)))))) 53.74/27.23
+'(s(s(s(s(y0)))), s(s(s(+(y1, y2))))) → c3(+'(s(s(s(y0))), s(s(s(+(y1, y2)))))) 53.74/27.23
+'(s(s(s(s(s(y0))))), s(s(s(y1)))) → c3(+'(s(s(s(s(y0)))), s(s(s(y1)))))
53.74/27.23
53.74/27.23

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(z0, 0) → z0 53.74/27.23
+(z0, s(z1)) → s(+(z0, z1)) 53.74/27.23
+(0, z0) → z0 53.74/27.23
+(s(z0), z1) → s(+(z0, z1)) 53.74/27.23
+(z0, +(z1, z2)) → +(+(z0, z1), z2) 53.74/27.23
f(g(f(z0))) → f(h(s(0), z0)) 53.74/27.23
f(g(h(z0, z1))) → f(h(s(z0), z1)) 53.74/27.23
f(h(z0, h(z1, z2))) → f(h(+(z0, z1), z2))
Tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.23
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.74/27.23
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2))) 53.74/27.23
+'(s(z0), +(y1, y2)) → c3(+'(z0, +(y1, y2))) 53.74/27.23
+'(s(z0), s(+(y1, y2))) → c3(+'(z0, s(+(y1, y2)))) 53.74/27.23
+'(z0, s(s(s(y1)))) → c1(+'(z0, s(s(y1)))) 53.74/27.23
+'(s(y0), s(s(z1))) → c1(+'(s(y0), s(z1))) 53.74/27.23
+'(z0, s(s(+(y1, y2)))) → c1(+'(z0, s(+(y1, y2)))) 53.74/27.23
+'(s(s(y0)), s(s(z1))) → c1(+'(s(s(y0)), s(z1))) 53.74/27.23
+'(s(y0), s(s(s(y1)))) → c1(+'(s(y0), s(s(y1)))) 53.74/27.23
+'(s(y0), s(s(+(y1, y2)))) → c1(+'(s(y0), s(+(y1, y2)))) 53.74/27.23
+'(s(z0), s(+(y1, y2))) → c1(+'(s(z0), +(y1, y2))) 53.74/27.23
+'(s(s(y0)), s(z1)) → c1(+'(s(s(y0)), z1)) 53.74/27.23
+'(s(z0), s(s(s(s(y1))))) → c1(+'(s(z0), s(s(s(y1))))) 53.74/27.23
+'(s(z0), s(s(s(+(y1, y2))))) → c1(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.23
+'(s(s(y0)), s(s(s(y1)))) → c1(+'(s(s(y0)), s(s(y1)))) 53.74/27.23
+'(s(s(z0)), +(y1, y2)) → c3(+'(s(z0), +(y1, y2))) 53.74/27.23
+'(s(s(z0)), s(+(y1, y2))) → c3(+'(s(z0), s(+(y1, y2)))) 53.74/27.23
+'(s(s(s(y0))), z1) → c3(+'(s(s(y0)), z1)) 53.74/27.23
+'(s(s(z0)), s(s(y1))) → c3(+'(s(z0), s(s(y1)))) 53.74/27.23
+'(s(s(s(y0))), s(y1)) → c3(+'(s(s(y0)), s(y1))) 53.74/27.23
+'(s(s(z0)), s(s(s(y1)))) → c3(+'(s(z0), s(s(s(y1))))) 53.74/27.23
+'(s(s(z0)), s(s(+(y1, y2)))) → c3(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.23
+'(s(s(s(y0))), s(s(y1))) → c3(+'(s(s(y0)), s(s(y1)))) 53.74/27.23
+'(s(s(z0)), s(s(s(s(y1))))) → c3(+'(s(z0), s(s(s(s(y1)))))) 53.74/27.23
+'(s(s(z0)), s(s(s(+(y1, y2))))) → c3(+'(s(z0), s(s(s(+(y1, y2)))))) 53.74/27.23
+'(s(s(s(y0))), s(s(s(y1)))) → c3(+'(s(s(y0)), s(s(s(y1))))) 53.74/27.23
+'(s(z0), s(s(s(y1)))) → c3(+'(z0, s(s(s(y1))))) 53.74/27.23
+'(s(z0), s(s(+(y1, y2)))) → c3(+'(z0, s(s(+(y1, y2))))) 53.74/27.23
+'(s(s(s(s(y0)))), s(s(z1))) → c3(+'(s(s(s(y0))), s(s(z1)))) 53.74/27.23
+'(s(s(s(y0))), s(s(+(y1, y2)))) → c3(+'(s(s(y0)), s(s(+(y1, y2))))) 53.74/27.23
+'(s(s(s(y0))), s(s(s(s(y1))))) → c3(+'(s(s(y0)), s(s(s(s(y1)))))) 53.74/27.23
+'(s(s(s(y0))), s(s(s(+(y1, y2))))) → c3(+'(s(s(y0)), s(s(s(+(y1, y2)))))) 53.74/27.23
+'(s(s(s(s(y0)))), s(s(s(y1)))) → c3(+'(s(s(s(y0))), s(s(s(y1))))) 53.74/27.23
+'(s(s(s(y0))), s(+(y1, y2))) → c3(+'(s(s(y0)), s(+(y1, y2)))) 53.74/27.23
+'(s(s(s(s(y0)))), s(z1)) → c3(+'(s(s(s(y0))), s(z1))) 53.74/27.23
+'(s(s(s(s(s(y0))))), s(s(y1))) → c3(+'(s(s(s(s(y0)))), s(s(y1)))) 53.74/27.23
+'(s(s(s(s(y0)))), s(s(+(y1, y2)))) → c3(+'(s(s(s(y0))), s(s(+(y1, y2))))) 53.74/27.23
+'(s(s(s(s(y0)))), s(s(s(s(y1))))) → c3(+'(s(s(s(y0))), s(s(s(s(y1)))))) 53.74/27.23
+'(s(s(s(s(y0)))), s(s(s(+(y1, y2))))) → c3(+'(s(s(s(y0))), s(s(s(+(y1, y2)))))) 53.74/27.23
+'(s(s(s(s(s(y0))))), s(s(s(y1)))) → c3(+'(s(s(s(s(y0)))), s(s(s(y1)))))
S tuples:

+'(s(z0), +(y1, y2)) → c3(+'(z0, +(y1, y2))) 53.74/27.23
+'(s(s(z0)), +(y1, y2)) → c3(+'(s(z0), +(y1, y2))) 53.74/27.23
+'(s(s(s(y0))), z1) → c3(+'(s(s(y0)), z1))
K tuples:

F(h(z0, h(z1, z2))) → c7(F(h(+(z0, z1), z2)), +'(z0, z1)) 53.74/27.23
+'(z0, +(z1, z2)) → c4(+'(+(z0, z1), z2), +'(z0, z1)) 53.74/27.23
+'(z0, s(+(y1, y2))) → c1(+'(z0, +(y1, y2))) 53.74/27.23
+'(s(z0), s(+(y1, y2))) → c3(+'(z0, s(+(y1, y2)))) 53.74/27.23
+'(z0, s(s(s(y1)))) → c1(+'(z0, s(s(y1)))) 53.74/27.23
+'(s(y0), s(s(z1))) → c1(+'(s(y0), s(z1))) 53.74/27.23
+'(z0, s(s(+(y1, y2)))) → c1(+'(z0, s(+(y1, y2)))) 53.74/27.23
+'(s(s(y0)), s(s(z1))) → c1(+'(s(s(y0)), s(z1))) 53.74/27.23
+'(s(y0), s(s(s(y1)))) → c1(+'(s(y0), s(s(y1)))) 53.74/27.23
+'(s(y0), s(s(+(y1, y2)))) → c1(+'(s(y0), s(+(y1, y2)))) 53.74/27.23
+'(s(z0), s(+(y1, y2))) → c1(+'(s(z0), +(y1, y2))) 53.74/27.23
+'(s(s(y0)), s(z1)) → c1(+'(s(s(y0)), z1)) 53.74/27.23
+'(s(z0), s(s(s(s(y1))))) → c1(+'(s(z0), s(s(s(y1))))) 53.74/27.23
+'(s(z0), s(s(s(+(y1, y2))))) → c1(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.23
+'(s(s(y0)), s(s(s(y1)))) → c1(+'(s(s(y0)), s(s(y1)))) 53.74/27.23
+'(s(s(z0)), s(+(y1, y2))) → c3(+'(s(z0), s(+(y1, y2)))) 53.74/27.23
+'(s(s(z0)), s(s(y1))) → c3(+'(s(z0), s(s(y1)))) 53.74/27.23
+'(s(s(s(y0))), s(y1)) → c3(+'(s(s(y0)), s(y1))) 53.74/27.23
+'(s(s(z0)), s(s(s(y1)))) → c3(+'(s(z0), s(s(s(y1))))) 53.74/27.23
+'(s(s(z0)), s(s(+(y1, y2)))) → c3(+'(s(z0), s(s(+(y1, y2))))) 53.74/27.23
+'(s(s(s(y0))), s(s(y1))) → c3(+'(s(s(y0)), s(s(y1)))) 53.74/27.23
+'(s(s(z0)), s(s(s(s(y1))))) → c3(+'(s(z0), s(s(s(s(y1)))))) 53.74/27.23
+'(s(s(z0)), s(s(s(+(y1, y2))))) → c3(+'(s(z0), s(s(s(+(y1, y2)))))) 53.74/27.23
+'(s(s(s(y0))), s(s(s(y1)))) → c3(+'(s(s(y0)), s(s(s(y1))))) 53.74/27.23
+'(s(z0), s(s(s(y1)))) → c3(+'(z0, s(s(s(y1))))) 53.74/27.23
+'(s(z0), s(s(+(y1, y2)))) → c3(+'(z0, s(s(+(y1, y2))))) 53.74/27.23
+'(s(s(s(s(y0)))), s(s(z1))) → c3(+'(s(s(s(y0))), s(s(z1)))) 53.74/27.23
+'(s(s(s(y0))), s(s(+(y1, y2)))) → c3(+'(s(s(y0)), s(s(+(y1, y2))))) 53.74/27.23
+'(s(s(s(y0))), s(s(s(s(y1))))) → c3(+'(s(s(y0)), s(s(s(s(y1)))))) 53.74/27.23
+'(s(s(s(y0))), s(s(s(+(y1, y2))))) → c3(+'(s(s(y0)), s(s(s(+(y1, y2)))))) 53.74/27.23
+'(s(s(s(s(y0)))), s(s(s(y1)))) → c3(+'(s(s(s(y0))), s(s(s(y1))))) 53.74/27.23
+'(s(s(s(y0))), s(+(y1, y2))) → c3(+'(s(s(y0)), s(+(y1, y2)))) 53.74/27.23
+'(s(s(s(s(y0)))), s(z1)) → c3(+'(s(s(s(y0))), s(z1))) 53.74/27.23
+'(s(s(s(s(s(y0))))), s(s(y1))) → c3(+'(s(s(s(s(y0)))), s(s(y1)))) 53.74/27.23
+'(s(s(s(s(y0)))), s(s(+(y1, y2)))) → c3(+'(s(s(s(y0))), s(s(+(y1, y2))))) 53.74/27.23
+'(s(s(s(s(y0)))), s(s(s(s(y1))))) → c3(+'(s(s(s(y0))), s(s(s(s(y1)))))) 53.74/27.23
+'(s(s(s(s(y0)))), s(s(s(+(y1, y2))))) → c3(+'(s(s(s(y0))), s(s(s(+(y1, y2)))))) 53.74/27.23
+'(s(s(s(s(s(y0))))), s(s(s(y1)))) → c3(+'(s(s(s(s(y0)))), s(s(s(y1)))))
Defined Rule Symbols:

+, f

Defined Pair Symbols:

F, +'

Compound Symbols:

c7, c4, c1, c3

53.74/27.23
53.74/27.23
53.74/27.26 EOF