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

(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) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative 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'

S is empty.
Rewrite Strategy: INNERMOST

(3) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
f5/1
f5/3
f0/0
f0/2
f0/4
f6/0
f6/3

(4) Obligation:

Runtime Complexity Relative 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, S(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(S(x'), S(x)) → f1(x', S(x'), x, S(x), S(x))
f0(S(x), 0') → 0'
f6(x2, x3, S(x)) → f0(x2, x3)
f5(x1, x3, S(x)) → f6(x1, x3, 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(x2, x3, 0') → 0'
f5(x1, x3, 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(0', x4) → 0'

S is empty.
Rewrite Strategy: INNERMOST

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

Infered types.

(6) Obligation:

Innermost TRS:
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, S(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(S(x'), S(x)) → f1(x', S(x'), x, S(x), S(x))
f0(S(x), 0') → 0'
f6(x2, x3, S(x)) → f0(x2, x3)
f5(x1, x3, S(x)) → f6(x1, x3, 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(x2, x3, 0') → 0'
f5(x1, x3, 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(0', x4) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
f4, f2, f3, f5, f0, f6

They will be analysed ascendingly in the following order:
f4 = f2
f4 = f3
f4 = f5
f4 = f0
f4 = f6
f2 = f3
f2 = f5
f2 = f0
f2 = f6
f3 = f5
f3 = f0
f3 = f6
f5 = f0
f5 = f6
f0 = f6

(8) Obligation:

Innermost TRS:
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, S(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(S(x'), S(x)) → f1(x', S(x'), x, S(x), S(x))
f0(S(x), 0') → 0'
f6(x2, x3, S(x)) → f0(x2, x3)
f5(x1, x3, S(x)) → f6(x1, x3, 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(x2, x3, 0') → 0'
f5(x1, x3, 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(0', x4) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

Generator Equations:
gen_S:0'2_7(0) ⇔ 0'
gen_S:0'2_7(+(x, 1)) ⇔ S(gen_S:0'2_7(x))

The following defined symbols remain to be analysed:
f2, f4, f3, f5, f0, f6

They will be analysed ascendingly in the following order:
f4 = f2
f4 = f3
f4 = f5
f4 = f0
f4 = f6
f2 = f3
f2 = f5
f2 = f0
f2 = f6
f3 = f5
f3 = f0
f3 = f6
f5 = f0
f5 = f6
f0 = f6

(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f2.

(10) Obligation:

Innermost TRS:
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, S(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(S(x'), S(x)) → f1(x', S(x'), x, S(x), S(x))
f0(S(x), 0') → 0'
f6(x2, x3, S(x)) → f0(x2, x3)
f5(x1, x3, S(x)) → f6(x1, x3, 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(x2, x3, 0') → 0'
f5(x1, x3, 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(0', x4) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

Generator Equations:
gen_S:0'2_7(0) ⇔ 0'
gen_S:0'2_7(+(x, 1)) ⇔ S(gen_S:0'2_7(x))

The following defined symbols remain to be analysed:
f5, f4, f3, f0, f6

They will be analysed ascendingly in the following order:
f4 = f2
f4 = f3
f4 = f5
f4 = f0
f4 = f6
f2 = f3
f2 = f5
f2 = f0
f2 = f6
f3 = f5
f3 = f0
f3 = f6
f5 = f0
f5 = f6
f0 = f6

(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f5.

(12) Obligation:

Innermost TRS:
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, S(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(S(x'), S(x)) → f1(x', S(x'), x, S(x), S(x))
f0(S(x), 0') → 0'
f6(x2, x3, S(x)) → f0(x2, x3)
f5(x1, x3, S(x)) → f6(x1, x3, 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(x2, x3, 0') → 0'
f5(x1, x3, 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(0', x4) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

Generator Equations:
gen_S:0'2_7(0) ⇔ 0'
gen_S:0'2_7(+(x, 1)) ⇔ S(gen_S:0'2_7(x))

The following defined symbols remain to be analysed:
f6, f4, f3, f0

They will be analysed ascendingly in the following order:
f4 = f2
f4 = f3
f4 = f5
f4 = f0
f4 = f6
f2 = f3
f2 = f5
f2 = f0
f2 = f6
f3 = f5
f3 = f0
f3 = f6
f5 = f0
f5 = f6
f0 = f6

(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f6.

(14) Obligation:

Innermost TRS:
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, S(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(S(x'), S(x)) → f1(x', S(x'), x, S(x), S(x))
f0(S(x), 0') → 0'
f6(x2, x3, S(x)) → f0(x2, x3)
f5(x1, x3, S(x)) → f6(x1, x3, 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(x2, x3, 0') → 0'
f5(x1, x3, 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(0', x4) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

Generator Equations:
gen_S:0'2_7(0) ⇔ 0'
gen_S:0'2_7(+(x, 1)) ⇔ S(gen_S:0'2_7(x))

The following defined symbols remain to be analysed:
f0, f4, f3

They will be analysed ascendingly in the following order:
f4 = f2
f4 = f3
f4 = f5
f4 = f0
f4 = f6
f2 = f3
f2 = f5
f2 = f0
f2 = f6
f3 = f5
f3 = f0
f3 = f6
f5 = f0
f5 = f6
f0 = f6

(15) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
f0(gen_S:0'2_7(1), gen_S:0'2_7(+(3, n64850_7))) → gen_S:0'2_7(0), rt ∈ Ω(1 + n64850₇)

Induction Base:
f0(gen_S:0'2_7(1), gen_S:0'2_7(+(3, 0))) →_R^Ω(1)
f1(gen_S:0'2_7(0), S(gen_S:0'2_7(0)), gen_S:0'2_7(2), S(gen_S:0'2_7(2)), S(gen_S:0'2_7(2))) →_R^Ω(1)
f2(S(gen_S:0'2_7(0)), gen_S:0'2_7(0), gen_S:0'2_7(2), S(gen_S:0'2_7(2)), gen_S:0'2_7(2)) →_R^Ω(1)
f5(S(gen_S:0'2_7(0)), S(gen_S:0'2_7(1)), gen_S:0'2_7(1)) →_R^Ω(1)
f6(S(gen_S:0'2_7(0)), S(gen_S:0'2_7(1)), gen_S:0'2_7(0)) →_R^Ω(1)
0'

Induction Step:
f0(gen_S:0'2_7(1), gen_S:0'2_7(+(3, +(n64850_7, 1)))) →_R^Ω(1)
f1(gen_S:0'2_7(0), S(gen_S:0'2_7(0)), gen_S:0'2_7(+(3, n64850_7)), S(gen_S:0'2_7(+(3, n64850_7))), S(gen_S:0'2_7(+(3, n64850_7)))) →_R^Ω(1)
f2(S(gen_S:0'2_7(0)), gen_S:0'2_7(0), gen_S:0'2_7(+(3, n64850_7)), S(gen_S:0'2_7(+(3, n64850_7))), gen_S:0'2_7(+(3, n64850_7))) →_R^Ω(1)
f5(S(gen_S:0'2_7(0)), S(gen_S:0'2_7(+(2, n64850_7))), gen_S:0'2_7(+(2, n64850_7))) →_R^Ω(1)
f6(S(gen_S:0'2_7(0)), S(gen_S:0'2_7(+(2, n64850_7))), gen_S:0'2_7(+(1, n64850_7))) →_R^Ω(1)
f0(S(gen_S:0'2_7(0)), S(gen_S:0'2_7(+(2, n64850_7)))) →_IH
gen_S:0'2_7(0)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(16) Complex Obligation (BEST)

(17) Obligation:

Innermost TRS:
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, S(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(S(x'), S(x)) → f1(x', S(x'), x, S(x), S(x))
f0(S(x), 0') → 0'
f6(x2, x3, S(x)) → f0(x2, x3)
f5(x1, x3, S(x)) → f6(x1, x3, 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(x2, x3, 0') → 0'
f5(x1, x3, 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(0', x4) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

Lemmas:
f0(gen_S:0'2_7(1), gen_S:0'2_7(+(3, n64850_7))) → gen_S:0'2_7(0), rt ∈ Ω(1 + n64850₇)

Generator Equations:
gen_S:0'2_7(0) ⇔ 0'
gen_S:0'2_7(+(x, 1)) ⇔ S(gen_S:0'2_7(x))

The following defined symbols remain to be analysed:
f3, f4, f2, f5, f6

They will be analysed ascendingly in the following order:
f4 = f2
f4 = f3
f4 = f5
f4 = f0
f4 = f6
f2 = f3
f2 = f5
f2 = f0
f2 = f6
f3 = f5
f3 = f0
f3 = f6
f5 = f0
f5 = f6
f0 = f6

(18) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f3.

(19) Obligation:

Innermost TRS:
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, S(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(S(x'), S(x)) → f1(x', S(x'), x, S(x), S(x))
f0(S(x), 0') → 0'
f6(x2, x3, S(x)) → f0(x2, x3)
f5(x1, x3, S(x)) → f6(x1, x3, 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(x2, x3, 0') → 0'
f5(x1, x3, 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(0', x4) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

Lemmas:
f0(gen_S:0'2_7(1), gen_S:0'2_7(+(3, n64850_7))) → gen_S:0'2_7(0), rt ∈ Ω(1 + n64850₇)

Generator Equations:
gen_S:0'2_7(0) ⇔ 0'
gen_S:0'2_7(+(x, 1)) ⇔ S(gen_S:0'2_7(x))

The following defined symbols remain to be analysed:
f4, f2, f5, f6

They will be analysed ascendingly in the following order:
f4 = f2
f4 = f3
f4 = f5
f4 = f0
f4 = f6
f2 = f3
f2 = f5
f2 = f0
f2 = f6
f3 = f5
f3 = f0
f3 = f6
f5 = f0
f5 = f6
f0 = f6

(20) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f4.

(21) Obligation:

Innermost TRS:
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, S(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(S(x'), S(x)) → f1(x', S(x'), x, S(x), S(x))
f0(S(x), 0') → 0'
f6(x2, x3, S(x)) → f0(x2, x3)
f5(x1, x3, S(x)) → f6(x1, x3, 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(x2, x3, 0') → 0'
f5(x1, x3, 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(0', x4) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

Lemmas:
f0(gen_S:0'2_7(1), gen_S:0'2_7(+(3, n64850_7))) → gen_S:0'2_7(0), rt ∈ Ω(1 + n64850₇)

Generator Equations:
gen_S:0'2_7(0) ⇔ 0'
gen_S:0'2_7(+(x, 1)) ⇔ S(gen_S:0'2_7(x))

The following defined symbols remain to be analysed:
f2, f5, f6

They will be analysed ascendingly in the following order:
f4 = f2
f4 = f3
f4 = f5
f4 = f0
f4 = f6
f2 = f3
f2 = f5
f2 = f0
f2 = f6
f3 = f5
f3 = f0
f3 = f6
f5 = f0
f5 = f6
f0 = f6

(22) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f2.

(23) Obligation:

Innermost TRS:
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, S(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(S(x'), S(x)) → f1(x', S(x'), x, S(x), S(x))
f0(S(x), 0') → 0'
f6(x2, x3, S(x)) → f0(x2, x3)
f5(x1, x3, S(x)) → f6(x1, x3, 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(x2, x3, 0') → 0'
f5(x1, x3, 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(0', x4) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

Lemmas:
f0(gen_S:0'2_7(1), gen_S:0'2_7(+(3, n64850_7))) → gen_S:0'2_7(0), rt ∈ Ω(1 + n64850₇)

Generator Equations:
gen_S:0'2_7(0) ⇔ 0'
gen_S:0'2_7(+(x, 1)) ⇔ S(gen_S:0'2_7(x))

The following defined symbols remain to be analysed:
f5, f6

They will be analysed ascendingly in the following order:
f4 = f2
f4 = f3
f4 = f5
f4 = f0
f4 = f6
f2 = f3
f2 = f5
f2 = f0
f2 = f6
f3 = f5
f3 = f0
f3 = f6
f5 = f0
f5 = f6
f0 = f6

(24) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f5.

(25) Obligation:

Innermost TRS:
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, S(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(S(x'), S(x)) → f1(x', S(x'), x, S(x), S(x))
f0(S(x), 0') → 0'
f6(x2, x3, S(x)) → f0(x2, x3)
f5(x1, x3, S(x)) → f6(x1, x3, 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(x2, x3, 0') → 0'
f5(x1, x3, 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(0', x4) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

Lemmas:
f0(gen_S:0'2_7(1), gen_S:0'2_7(+(3, n64850_7))) → gen_S:0'2_7(0), rt ∈ Ω(1 + n64850₇)

Generator Equations:
gen_S:0'2_7(0) ⇔ 0'
gen_S:0'2_7(+(x, 1)) ⇔ S(gen_S:0'2_7(x))

The following defined symbols remain to be analysed:
f6

They will be analysed ascendingly in the following order:
f4 = f2
f4 = f3
f4 = f5
f4 = f0
f4 = f6
f2 = f3
f2 = f5
f2 = f0
f2 = f6
f3 = f5
f3 = f0
f3 = f6
f5 = f0
f5 = f6
f0 = f6

(26) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f6.

(27) Obligation:

Innermost TRS:
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, S(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(S(x'), S(x)) → f1(x', S(x'), x, S(x), S(x))
f0(S(x), 0') → 0'
f6(x2, x3, S(x)) → f0(x2, x3)
f5(x1, x3, S(x)) → f6(x1, x3, 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(x2, x3, 0') → 0'
f5(x1, x3, 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(0', x4) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

Lemmas:
f0(gen_S:0'2_7(1), gen_S:0'2_7(+(3, n64850_7))) → gen_S:0'2_7(0), rt ∈ Ω(1 + n64850₇)

Generator Equations:
gen_S:0'2_7(0) ⇔ 0'
gen_S:0'2_7(+(x, 1)) ⇔ S(gen_S:0'2_7(x))

No more defined symbols left to analyse.

(28) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
f0(gen_S:0'2_7(1), gen_S:0'2_7(+(3, n64850_7))) → gen_S:0'2_7(0), rt ∈ Ω(1 + n64850₇)

(29) BOUNDS(n^1, INF)

(30) Obligation:

Innermost TRS:
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, S(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(S(x'), S(x)) → f1(x', S(x'), x, S(x), S(x))
f0(S(x), 0') → 0'
f6(x2, x3, S(x)) → f0(x2, x3)
f5(x1, x3, S(x)) → f6(x1, x3, 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(x2, x3, 0') → 0'
f5(x1, x3, 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(0', x4) → 0'

Types:
f4 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
S :: S:0' → S:0'
f2 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
0' :: S:0'
f3 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f5 :: S:0' → S:0' → S:0' → S:0'
f0 :: S:0' → S:0' → S:0'
f1 :: S:0' → S:0' → S:0' → S:0' → S:0' → S:0'
f6 :: S:0' → S:0' → S:0' → S:0'
hole_S:0'1_7 :: S:0'
gen_S:0'2_7 :: Nat → S:0'

Lemmas:
f0(gen_S:0'2_7(1), gen_S:0'2_7(+(3, n64850_7))) → gen_S:0'2_7(0), rt ∈ Ω(1 + n64850₇)

Generator Equations:
gen_S:0'2_7(0) ⇔ 0'
gen_S:0'2_7(+(x, 1)) ⇔ S(gen_S:0'2_7(x))

No more defined symbols left to analyse.

(31) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
f0(gen_S:0'2_7(1), gen_S:0'2_7(+(3, n64850_7))) → gen_S:0'2_7(0), rt ∈ Ω(1 + n64850₇)

(32) BOUNDS(n^1, INF)