### (0) Obligation:

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

f(x, c(x), c(y)) → f(y, y, f(y, x, y))
f(s(x), y, z) → f(x, s(c(y)), c(z))
f(c(x), x, y) → c(y)
g(x, y) → x
g(x, y) → y

Rewrite Strategy: INNERMOST

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

Converted Cpx (relative) TRS to CDT

### (2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
g(z0, z1) → z0
g(z0, z1) → z1
Tuples:

F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(z0), z0, z1) → c3
G(z0, z1) → c4
G(z0, z1) → c5
S tuples:

F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(z0), z0, z1) → c3
G(z0, z1) → c4
G(z0, z1) → c5
K tuples:none
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c3, c4, c5

### (3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 3 trailing nodes:

F(c(z0), z0, z1) → c3
G(z0, z1) → c4
G(z0, z1) → c5

### (4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
g(z0, z1) → z0
g(z0, z1) → z1
Tuples:

F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
S tuples:

F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
K tuples:none
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F

Compound Symbols:

c1, c2

### (5) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

g(z0, z1) → z0
g(z0, z1) → z1

### (6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
S tuples:

F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c2

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

Use narrowing to replace F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1)) by

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(z0, c(z0), c(c(z0))) → c1(F(c(z0), c(z0), c(c(z0))), F(c(z0), z0, c(z0)))

### (8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(z0, c(z0), c(c(z0))) → c1(F(c(z0), c(z0), c(c(z0))), F(c(z0), z0, c(z0)))
S tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(z0, c(z0), c(c(z0))) → c1(F(c(z0), c(z0), c(c(z0))), F(c(z0), z0, c(z0)))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c1

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

Removed 1 trailing nodes:

F(z0, c(z0), c(c(z0))) → c1(F(c(z0), c(z0), c(c(z0))), F(c(z0), z0, c(z0)))

### (10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
S tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c1

### (11) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

### (12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
S tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c1, c1

### (13) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

### (14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
S tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c1, c3

### (15) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))

### (16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
S tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c1, c3

### (17) CdtRuleRemovalProof (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(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
We considered the (Usable) Rules:none
And the Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F(x1, x2, x3)) = [4]x2
POL(c(x1)) = [2] + x1
POL(c1(x1)) = x1
POL(c2(x1)) = x1
POL(c3(x1)) = x1
POL(f(x1, x2, x3)) = [3] + [2]x2 + [2]x3
POL(s(x1)) = 0

### (18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
S tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
K tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c1, c3

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

Use forward instantiation to replace F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2))) by

F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))

### (20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
S tuples:

F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
K tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c3, c2

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

Use narrowing to replace F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0))))) by

F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0)))))))
F(x0, c(x0), c(s(c(s(c(x0)))))) → c3(F(s(c(s(c(x0)))), s(c(s(c(x0)))), c(c(s(c(s(c(x0))))))))

### (22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0)))))))
F(x0, c(x0), c(s(c(s(c(x0)))))) → c3(F(s(c(s(c(x0)))), s(c(s(c(x0)))), c(c(s(c(s(c(x0))))))))
S tuples:

F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
K tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c3, c2

### (23) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

F(x0, c(x0), c(s(c(s(c(x0)))))) → c3(F(s(c(s(c(x0)))), s(c(s(c(x0)))), c(c(s(c(s(c(x0))))))))

### (24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0)))))))
S tuples:

F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
K tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c3, c2

### (25) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use instantiation to replace F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0))) by

F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))

### (26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0)))))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
S tuples:

F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2)))
K tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c2, c3

### (27) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use instantiation to replace F(s(s(y0)), z1, z2) → c2(F(s(y0), s(c(z1)), c(z2))) by

F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))

### (28) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0)))))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
S tuples:

F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
K tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c3, c2

### (29) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

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

F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))

### (30) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0)))))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
S tuples:

F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
K tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c3, c2

### (31) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use instantiation to replace F(x0, c(x0), c(s(s(z0)))) → c3(F(s(s(z0)), s(s(z0)), f(z0, s(c(s(c(x0)))), c(c(s(s(z0))))))) by

F(c(s(s(z1))), c(c(s(s(z1)))), c(s(s(z1)))) → c3(F(s(s(z1)), s(s(z1)), f(z1, s(c(s(c(c(s(s(z1))))))), c(c(s(s(z1)))))))

### (32) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
F(c(s(s(z1))), c(c(s(s(z1)))), c(s(s(z1)))) → c3(F(s(s(z1)), s(s(z1)), f(z1, s(c(s(c(c(s(s(z1))))))), c(c(s(s(z1)))))))
S tuples:

F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
K tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c3, c2

### (33) CdtRuleRemovalProof (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(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
We considered the (Usable) Rules:none
And the Tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
F(c(s(s(z1))), c(c(s(s(z1)))), c(s(s(z1)))) → c3(F(s(s(z1)), s(s(z1)), f(z1, s(c(s(c(c(s(s(z1))))))), c(c(s(s(z1)))))))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F(x1, x2, x3)) = [2]x1
POL(c(x1)) = [5] + x1
POL(c1(x1)) = x1
POL(c2(x1)) = x1
POL(c3(x1)) = x1
POL(f(x1, x2, x3)) = [1] + [5]x1 + [4]x3
POL(s(x1)) = [4] + x1

### (34) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
Tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
F(c(s(s(z1))), c(c(s(s(z1)))), c(s(s(z1)))) → c3(F(s(s(z1)), s(s(z1)), f(z1, s(c(s(c(c(s(s(z1))))))), c(c(s(s(z1)))))))
S tuples:none
K tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(s(s(z0)), c(s(s(z0))), s(s(z0))) → c2(F(s(z0), s(c(c(s(s(z0))))), c(s(s(z0)))))
F(s(s(z0)), s(c(x1)), c(x2)) → c2(F(s(z0), s(c(s(c(x1)))), c(c(x2))))
F(s(s(x1)), s(s(x1)), y0) → c2(F(s(x1), s(c(s(s(x1)))), c(y0)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c3, c2

### (35) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty