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

(0) Obligation:

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

f4(S(x''), S(x'), x3, x4, S(x)) → f2(S(x''), x', x3, x4, x)
f4(S(x'), 0, x3, x4, S(x)) → f3(x', 0, x3, x4, x)
f2(x1, x2, S(x''), S(x'), S(x)) → f5(x1, x2, S(x''), x', x)
f2(x1, x2, S(x'), 0, S(x)) → f3(x1, x2, x', 0, x)
f4(S(x'), S(x), x3, x4, 0) → 0
f4(S(x), 0, x3, x4, 0) → 0
f2(x1, x2, S(x'), S(x), 0) → 0
f2(x1, x2, S(x), 0, 0) → 0
f0(x1, S(x'), x3, S(x), x5) → f1(x', S(x'), x, S(x), S(x))
f0(x1, S(x), x3, 0, x5) → 0
f6(x1, x2, x3, x4, S(x)) → f0(x1, x2, x4, x3, x)
f5(x1, x2, x3, x4, S(x)) → f6(x2, x1, x3, x4, x)
f3(x1, x2, x3, x4, S(x)) → f4(x1, x2, x4, x3, x)
f1(x1, x2, x3, x4, S(x)) → f2(x2, x1, x3, x4, x)
f6(x1, x2, x3, x4, 0) → 0
f5(x1, x2, x3, x4, 0) → 0
f4(0, x2, x3, x4, x5) → 0
f3(x1, x2, x3, x4, 0) → 0
f2(x1, x2, 0, x4, x5) → 0
f1(x1, x2, x3, x4, 0) → 0
f0(x1, 0, x3, x4, x5) → 0

Rewrite Strategy: INNERMOST

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

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f4(S(z0), S(z1), z2, z3, S(z4)) → f2(S(z0), z1, z2, z3, z4)
f4(S(z0), 0, z1, z2, S(z3)) → f3(z0, 0, z1, z2, z3)
f4(S(z0), S(z1), z2, z3, 0) → 0
f4(S(z0), 0, z1, z2, 0) → 0
f4(0, z0, z1, z2, z3) → 0
f2(z0, z1, S(z2), S(z3), S(z4)) → f5(z0, z1, S(z2), z3, z4)
f2(z0, z1, S(z2), 0, S(z3)) → f3(z0, z1, z2, 0, z3)
f2(z0, z1, S(z2), S(z3), 0) → 0
f2(z0, z1, S(z2), 0, 0) → 0
f2(z0, z1, 0, z2, z3) → 0
f0(z0, S(z1), z2, S(z3), z4) → f1(z1, S(z1), z3, S(z3), S(z3))
f0(z0, S(z1), z2, 0, z3) → 0
f0(z0, 0, z1, z2, z3) → 0
f6(z0, z1, z2, z3, S(z4)) → f0(z0, z1, z3, z2, z4)
f6(z0, z1, z2, z3, 0) → 0
f5(z0, z1, z2, z3, S(z4)) → f6(z1, z0, z2, z3, z4)
f5(z0, z1, z2, z3, 0) → 0
f3(z0, z1, z2, z3, S(z4)) → f4(z0, z1, z3, z2, z4)
f3(z0, z1, z2, z3, 0) → 0
f1(z0, z1, z2, z3, S(z4)) → f2(z1, z0, z2, z3, z4)
f1(z0, z1, z2, z3, 0) → 0

Tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F4(S(z0), S(z1), z2, z3, 0) → c2
F4(S(z0), 0, z1, z2, 0) → c3
F4(0, z0, z1, z2, z3) → c4
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F2(z0, z1, S(z2), S(z3), 0) → c7
F2(z0, z1, S(z2), 0, 0) → c8
F2(z0, z1, 0, z2, z3) → c9
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F0(z0, S(z1), z2, 0, z3) → c11
F0(z0, 0, z1, z2, z3) → c12
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F6(z0, z1, z2, z3, 0) → c14
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F5(z0, z1, z2, z3, 0) → c16
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F3(z0, z1, z2, z3, 0) → c18
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))
F1(z0, z1, z2, z3, 0) → c20

S tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F4(S(z0), S(z1), z2, z3, 0) → c2
F4(S(z0), 0, z1, z2, 0) → c3
F4(0, z0, z1, z2, z3) → c4
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F2(z0, z1, S(z2), S(z3), 0) → c7
F2(z0, z1, S(z2), 0, 0) → c8
F2(z0, z1, 0, z2, z3) → c9
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F0(z0, S(z1), z2, 0, z3) → c11
F0(z0, 0, z1, z2, z3) → c12
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F6(z0, z1, z2, z3, 0) → c14
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F5(z0, z1, z2, z3, 0) → c16
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F3(z0, z1, z2, z3, 0) → c18
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))
F1(z0, z1, z2, z3, 0) → c20

K tuples:none
Defined Rule Symbols:

f4, f2, f0, f6, f5, f3, f1

Defined Pair Symbols:

F4, F2, F0, F6, F5, F3, F1

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20

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

Removed 12 trailing nodes:

F0(z0, 0, z1, z2, z3) → c12
F0(z0, S(z1), z2, 0, z3) → c11
F3(z0, z1, z2, z3, 0) → c18
F4(S(z0), S(z1), z2, z3, 0) → c2
F4(S(z0), 0, z1, z2, 0) → c3
F2(z0, z1, 0, z2, z3) → c9
F2(z0, z1, S(z2), 0, 0) → c8
F6(z0, z1, z2, z3, 0) → c14
F2(z0, z1, S(z2), S(z3), 0) → c7
F5(z0, z1, z2, z3, 0) → c16
F4(0, z0, z1, z2, z3) → c4
F1(z0, z1, z2, z3, 0) → c20

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f4(S(z0), S(z1), z2, z3, S(z4)) → f2(S(z0), z1, z2, z3, z4)
f4(S(z0), 0, z1, z2, S(z3)) → f3(z0, 0, z1, z2, z3)
f4(S(z0), S(z1), z2, z3, 0) → 0
f4(S(z0), 0, z1, z2, 0) → 0
f4(0, z0, z1, z2, z3) → 0
f2(z0, z1, S(z2), S(z3), S(z4)) → f5(z0, z1, S(z2), z3, z4)
f2(z0, z1, S(z2), 0, S(z3)) → f3(z0, z1, z2, 0, z3)
f2(z0, z1, S(z2), S(z3), 0) → 0
f2(z0, z1, S(z2), 0, 0) → 0
f2(z0, z1, 0, z2, z3) → 0
f0(z0, S(z1), z2, S(z3), z4) → f1(z1, S(z1), z3, S(z3), S(z3))
f0(z0, S(z1), z2, 0, z3) → 0
f0(z0, 0, z1, z2, z3) → 0
f6(z0, z1, z2, z3, S(z4)) → f0(z0, z1, z3, z2, z4)
f6(z0, z1, z2, z3, 0) → 0
f5(z0, z1, z2, z3, S(z4)) → f6(z1, z0, z2, z3, z4)
f5(z0, z1, z2, z3, 0) → 0
f3(z0, z1, z2, z3, S(z4)) → f4(z0, z1, z3, z2, z4)
f3(z0, z1, z2, z3, 0) → 0
f1(z0, z1, z2, z3, S(z4)) → f2(z1, z0, z2, z3, z4)
f1(z0, z1, z2, z3, 0) → 0

Tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))

S tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))

K tuples:none
Defined Rule Symbols:

f4, f2, f0, f6, f5, f3, f1

Defined Pair Symbols:

F4, F2, F0, F6, F5, F3, F1

Compound Symbols:

c, c1, c5, c6, c10, c13, c15, c17, c19

(5) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

f4(S(z0), S(z1), z2, z3, S(z4)) → f2(S(z0), z1, z2, z3, z4)
f4(S(z0), 0, z1, z2, S(z3)) → f3(z0, 0, z1, z2, z3)
f4(S(z0), S(z1), z2, z3, 0) → 0
f4(S(z0), 0, z1, z2, 0) → 0
f4(0, z0, z1, z2, z3) → 0
f2(z0, z1, S(z2), S(z3), S(z4)) → f5(z0, z1, S(z2), z3, z4)
f2(z0, z1, S(z2), 0, S(z3)) → f3(z0, z1, z2, 0, z3)
f2(z0, z1, S(z2), S(z3), 0) → 0
f2(z0, z1, S(z2), 0, 0) → 0
f2(z0, z1, 0, z2, z3) → 0
f0(z0, S(z1), z2, S(z3), z4) → f1(z1, S(z1), z3, S(z3), S(z3))
f0(z0, S(z1), z2, 0, z3) → 0
f0(z0, 0, z1, z2, z3) → 0
f6(z0, z1, z2, z3, S(z4)) → f0(z0, z1, z3, z2, z4)
f6(z0, z1, z2, z3, 0) → 0
f5(z0, z1, z2, z3, S(z4)) → f6(z1, z0, z2, z3, z4)
f5(z0, z1, z2, z3, 0) → 0
f3(z0, z1, z2, z3, S(z4)) → f4(z0, z1, z3, z2, z4)
f3(z0, z1, z2, z3, 0) → 0
f1(z0, z1, z2, z3, S(z4)) → f2(z1, z0, z2, z3, z4)
f1(z0, z1, z2, z3, 0) → 0

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))

S tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))

K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:

F4, F2, F0, F6, F5, F3, F1

Compound Symbols:

c, c1, c5, c6, c10, c13, c15, c17, c19

(7) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

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

F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))

We considered the (Usable) Rules:none
And the Tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))

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

POL(0) = 0   
POL(F0(x₁, x₂, x₃, x₄, x₅)) = [1] + [4]x₂   
POL(F1(x₁, x₂, x₃, x₄, x₅)) = [1] + [4]x₂   
POL(F2(x₁, x₂, x₃, x₄, x₅)) = [1] + [4]x₁   
POL(F3(x₁, x₂, x₃, x₄, x₅)) = [1] + [4]x₁   
POL(F4(x₁, x₂, x₃, x₄, x₅)) = [1] + [4]x₁   
POL(F5(x₁, x₂, x₃, x₄, x₅)) = [1] + [4]x₁   
POL(F6(x₁, x₂, x₃, x₄, x₅)) = [1] + [4]x₂   
POL(S(x₁)) = [4] + x₁   
POL(c(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c15(x₁)) = x₁   
POL(c17(x₁)) = x₁   
POL(c19(x₁)) = x₁   
POL(c5(x₁)) = x₁   
POL(c6(x₁)) = x₁   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))

S tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))

K tuples:

F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))

Defined Rule Symbols:none

Defined Pair Symbols:

F4, F2, F0, F6, F5, F3, F1

Compound Symbols:

c, c1, c5, c6, c10, c13, c15, c17, c19

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

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

F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))

We considered the (Usable) Rules:none
And the Tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))

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

POL(0) = [4]   
POL(F0(x₁, x₂, x₃, x₄, x₅)) = x₂ + [2]x₄   
POL(F1(x₁, x₂, x₃, x₄, x₅)) = [4] + x₂ + [2]x₃   
POL(F2(x₁, x₂, x₃, x₄, x₅)) = x₁ + [2]x₃   
POL(F3(x₁, x₂, x₃, x₄, x₅)) = x₁ + [2]x₃ + [2]x₄   
POL(F4(x₁, x₂, x₃, x₄, x₅)) = x₁ + [2]x₃ + [2]x₄   
POL(F5(x₁, x₂, x₃, x₄, x₅)) = x₁ + [2]x₃   
POL(F6(x₁, x₂, x₃, x₄, x₅)) = x₂ + [2]x₃   
POL(S(x₁)) = [4] + x₁   
POL(c(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c15(x₁)) = x₁   
POL(c17(x₁)) = x₁   
POL(c19(x₁)) = x₁   
POL(c5(x₁)) = x₁   
POL(c6(x₁)) = x₁   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))

S tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))

K tuples:

F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))

Defined Rule Symbols:none

Defined Pair Symbols:

F4, F2, F0, F6, F5, F3, F1

Compound Symbols:

c, c1, c5, c6, c10, c13, c15, c17, c19

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

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

F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))

We considered the (Usable) Rules:none
And the Tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))

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

POL(0) = [2]   
POL(F0(x₁, x₂, x₃, x₄, x₅)) = [4]x₂ + [2]x₄   
POL(F1(x₁, x₂, x₃, x₄, x₅)) = [4]x₂ + [2]x₃   
POL(F2(x₁, x₂, x₃, x₄, x₅)) = [4]x₁ + [2]x₃   
POL(F3(x₁, x₂, x₃, x₄, x₅)) = [3] + [4]x₁ + [2]x₃ + [2]x₄   
POL(F4(x₁, x₂, x₃, x₄, x₅)) = [4]x₁ + [2]x₃ + [2]x₄   
POL(F5(x₁, x₂, x₃, x₄, x₅)) = [4]x₁ + [2]x₃   
POL(F6(x₁, x₂, x₃, x₄, x₅)) = [4]x₂ + [2]x₃   
POL(S(x₁)) = [4] + x₁   
POL(c(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c13(x₁)) = x₁   
POL(c15(x₁)) = x₁   
POL(c17(x₁)) = x₁   
POL(c19(x₁)) = x₁   
POL(c5(x₁)) = x₁   
POL(c6(x₁)) = x₁   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))

S tuples:

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))

K tuples:

F4(S(z0), 0, z1, z2, S(z3)) → c1(F3(z0, 0, z1, z2, z3))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4))

Defined Rule Symbols:none

Defined Pair Symbols:

F4, F2, F0, F6, F5, F3, F1

Compound Symbols:

c, c1, c5, c6, c10, c13, c15, c17, c19

(13) CdtKnowledgeProof (EQUIVALENT transformation)

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

F4(S(z0), S(z1), z2, z3, S(z4)) → c(F2(S(z0), z1, z2, z3, z4))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F2(z0, z1, S(z2), S(z3), S(z4)) → c5(F5(z0, z1, S(z2), z3, z4))
F2(z0, z1, S(z2), 0, S(z3)) → c6(F3(z0, z1, z2, 0, z3))
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4))
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
F0(z0, S(z1), z2, S(z3), z4) → c10(F1(z1, S(z1), z3, S(z3), S(z3)))

Now S is empty

(14) BOUNDS(1, 1)