### (0) Obligation:

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

g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Rewrite Strategy: FULL

### (1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
foldB(t, s(n)) →+ f(foldB(t, n), B)
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [n / s(n)].
The result substitution is [ ].

### (3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

### (4) Obligation:

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

g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0', c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

S is empty.
Rewrite Strategy: FULL

### (5) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
triple/0

### (6) Obligation:

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

g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

S is empty.
Rewrite Strategy: FULL

Infered types.

### (8) Obligation:

TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

### (9) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
foldB, f, foldC, f', f'', fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

### (10) Obligation:

TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
f, foldB, foldC, f', f'', fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

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

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

### (12) Obligation:

TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
f', foldB, foldC, f'', fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

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

Could not prove a rewrite lemma for the defined symbol f'.

### (14) Obligation:

TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
f'', foldB, foldC, fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

### (15) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f''.

### (16) Obligation:

TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
foldC, foldB, fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

### (17) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
foldC(triple(0', 0'), gen_0':s4_0(n143_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n1430)

Induction Base:
foldC(triple(0', 0'), gen_0':s4_0(0)) →RΩ(1)
triple(0', 0')

Induction Step:
foldC(triple(0', 0'), gen_0':s4_0(+(n143_0, 1))) →RΩ(1)
f(foldC(triple(0', 0'), gen_0':s4_0(n143_0)), C) →IH
f(triple(gen_0':s4_0(0), gen_0':s4_0(0)), C) →RΩ(1)
f'(triple(gen_0':s4_0(0), gen_0':s4_0(0)), g(C)) →RΩ(1)
f'(triple(gen_0':s4_0(0), gen_0':s4_0(0)), A) →RΩ(1)
f''(foldB(triple(0', gen_0':s4_0(0)), gen_0':s4_0(0))) →RΩ(1)
f''(triple(0', gen_0':s4_0(0))) →RΩ(1)
foldC(triple(0', 0'), gen_0':s4_0(0)) →RΩ(1)
triple(0', 0')

We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

### (19) Obligation:

TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n143_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n1430)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
foldB, f, f', f'', fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

### (20) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
foldB(triple(0', 0'), gen_0':s4_0(n2097_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n20970)

Induction Base:
foldB(triple(0', 0'), gen_0':s4_0(0)) →RΩ(1)
triple(0', 0')

Induction Step:
foldB(triple(0', 0'), gen_0':s4_0(+(n2097_0, 1))) →RΩ(1)
f(foldB(triple(0', 0'), gen_0':s4_0(n2097_0)), B) →IH
f(triple(gen_0':s4_0(0), gen_0':s4_0(0)), B) →RΩ(1)
f'(triple(gen_0':s4_0(0), gen_0':s4_0(0)), g(B)) →RΩ(1)
f'(triple(gen_0':s4_0(0), gen_0':s4_0(0)), A) →RΩ(1)
f''(foldB(triple(0', gen_0':s4_0(0)), gen_0':s4_0(0))) →RΩ(1)
f''(triple(0', gen_0':s4_0(0))) →RΩ(1)
foldC(triple(0', 0'), gen_0':s4_0(0)) →LΩ(1)
triple(gen_0':s4_0(0), gen_0':s4_0(0))

We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

### (22) Obligation:

TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n143_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n1430)
foldB(triple(0', 0'), gen_0':s4_0(n2097_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n20970)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
f, foldC, f', f'', fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

### (23) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

### (24) Obligation:

TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n143_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n1430)
foldB(triple(0', 0'), gen_0':s4_0(n2097_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n20970)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
f', foldC, f'', fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

### (25) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f'.

### (26) Obligation:

TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n143_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n1430)
foldB(triple(0', 0'), gen_0':s4_0(n2097_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n20970)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
f'', foldC, fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

### (27) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f''.

### (28) Obligation:

TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n143_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n1430)
foldB(triple(0', 0'), gen_0':s4_0(n2097_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n20970)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
foldC, fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

### (29) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
foldC(triple(0', 0'), gen_0':s4_0(n4174_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n41740)

Induction Base:
foldC(triple(0', 0'), gen_0':s4_0(0)) →RΩ(1)
triple(0', 0')

Induction Step:
foldC(triple(0', 0'), gen_0':s4_0(+(n4174_0, 1))) →RΩ(1)
f(foldC(triple(0', 0'), gen_0':s4_0(n4174_0)), C) →IH
f(triple(gen_0':s4_0(0), gen_0':s4_0(0)), C) →RΩ(1)
f'(triple(gen_0':s4_0(0), gen_0':s4_0(0)), g(C)) →RΩ(1)
f'(triple(gen_0':s4_0(0), gen_0':s4_0(0)), A) →RΩ(1)
f''(foldB(triple(0', gen_0':s4_0(0)), gen_0':s4_0(0))) →LΩ(1)
f''(triple(gen_0':s4_0(0), gen_0':s4_0(0))) →RΩ(1)
foldC(triple(gen_0':s4_0(0), 0'), gen_0':s4_0(0)) →RΩ(1)
triple(gen_0':s4_0(0), 0')

We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

### (31) Obligation:

TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n4174_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n41740)
foldB(triple(0', 0'), gen_0':s4_0(n2097_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n20970)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
fold

### (32) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
fold(triple(0', 0'), A, gen_0':s4_0(n6349_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n63490)

Induction Base:
fold(triple(0', 0'), A, gen_0':s4_0(0)) →RΩ(1)
triple(0', 0')

Induction Step:
fold(triple(0', 0'), A, gen_0':s4_0(+(n6349_0, 1))) →RΩ(1)
f(fold(triple(0', 0'), A, gen_0':s4_0(n6349_0)), A) →IH
f(triple(gen_0':s4_0(0), gen_0':s4_0(0)), A) →RΩ(1)
f'(triple(gen_0':s4_0(0), gen_0':s4_0(0)), g(A)) →RΩ(1)
f'(triple(gen_0':s4_0(0), gen_0':s4_0(0)), A) →RΩ(1)
f''(foldB(triple(0', gen_0':s4_0(0)), gen_0':s4_0(0))) →LΩ(1)
f''(triple(gen_0':s4_0(0), gen_0':s4_0(0))) →RΩ(1)
foldC(triple(gen_0':s4_0(0), 0'), gen_0':s4_0(0)) →LΩ(1)
triple(gen_0':s4_0(0), gen_0':s4_0(0))

We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

### (34) Obligation:

TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n4174_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n41740)
foldB(triple(0', 0'), gen_0':s4_0(n2097_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n20970)
fold(triple(0', 0'), A, gen_0':s4_0(n6349_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n63490)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

No more defined symbols left to analyse.

### (35) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
foldC(triple(0', 0'), gen_0':s4_0(n4174_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n41740)

### (37) Obligation:

TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n4174_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n41740)
foldB(triple(0', 0'), gen_0':s4_0(n2097_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n20970)
fold(triple(0', 0'), A, gen_0':s4_0(n6349_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n63490)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

No more defined symbols left to analyse.

### (38) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
foldC(triple(0', 0'), gen_0':s4_0(n4174_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n41740)

### (40) Obligation:

TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n4174_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n41740)
foldB(triple(0', 0'), gen_0':s4_0(n2097_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n20970)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

No more defined symbols left to analyse.

### (41) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
foldC(triple(0', 0'), gen_0':s4_0(n4174_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n41740)

### (43) Obligation:

TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n143_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n1430)
foldB(triple(0', 0'), gen_0':s4_0(n2097_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n20970)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

No more defined symbols left to analyse.

### (44) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
foldC(triple(0', 0'), gen_0':s4_0(n143_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n1430)

### (46) Obligation:

TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(b, c), C) → triple(b, s(c))
f'(triple(b, c), B) → f(triple(b, c), A)
f'(triple(b, c), A) → f''(foldB(triple(0', c), b))
f''(triple(b, c)) → foldC(triple(b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0'), gen_0':s4_0(n143_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n1430)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

No more defined symbols left to analyse.

### (47) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
foldC(triple(0', 0'), gen_0':s4_0(n143_0)) → triple(gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n1430)