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: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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)) → f1(foldB'(t, n), B')
foldC'(t, 0') → t
foldC'(t, s'(n)) → f1(foldC'(t, n), C')
f1(t, x) → f'''(t, g'(x))
f'''(triple'(a, b, c), C') → triple'(a, b, s'(c))
f'''(triple'(a, b, c), B') → f1(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)) → f1(fold'(t, x, n), x)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
triple'/0

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)) → f1(foldB'(t, n), B')
foldC'(t, 0') → t
foldC'(t, s'(n)) → f1(foldC'(t, n), C')
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, s'(c))
f'''(triple'(b, c), B') → f1(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)) → f1(fold'(t, x, n), x)

Rewrite Strategy: INNERMOST

Infered types.

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)) → f1(foldB'(t, n), B')
foldC'(t, 0') → t
foldC'(t, s'(n)) → f1(foldC'(t, n), C')
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, s'(c))
f'''(triple'(b, c), B') → f1(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)) → f1(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'
f1 :: 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':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_0':s'3 :: 0':s'
_gen_0':s'4 :: Nat → 0':s'

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

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

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)) → f1(foldB'(t, n), B')
foldC'(t, 0') → t
foldC'(t, s'(n)) → f1(foldC'(t, n), C')
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, s'(c))
f'''(triple'(b, c), B') → f1(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)) → f1(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'
f1 :: 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':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_0':s'3 :: 0':s'
_gen_0':s'4 :: Nat → 0':s'

Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))

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

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

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

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)) → f1(foldB'(t, n), B')
foldC'(t, 0') → t
foldC'(t, s'(n)) → f1(foldC'(t, n), C')
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, s'(c))
f'''(triple'(b, c), B') → f1(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)) → f1(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'
f1 :: 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':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_0':s'3 :: 0':s'
_gen_0':s'4 :: Nat → 0':s'

Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))

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

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

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

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)) → f1(foldB'(t, n), B')
foldC'(t, 0') → t
foldC'(t, s'(n)) → f1(foldC'(t, n), C')
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, s'(c))
f'''(triple'(b, c), B') → f1(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)) → f1(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'
f1 :: 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':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_0':s'3 :: 0':s'
_gen_0':s'4 :: Nat → 0':s'

Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))

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

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

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

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)) → f1(foldB'(t, n), B')
foldC'(t, 0') → t
foldC'(t, s'(n)) → f1(foldC'(t, n), C')
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, s'(c))
f'''(triple'(b, c), B') → f1(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)) → f1(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'
f1 :: 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':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_0':s'3 :: 0':s'
_gen_0':s'4 :: Nat → 0':s'

Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))

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

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

Proved the following rewrite lemma:
foldC'(triple'(0', 0'), _gen_0':s'4(_n204)) → triple'(_gen_0':s'4(0), _gen_0':s'4(0)), rt ∈ Ω(1 + n204)

Induction Base:
foldC'(triple'(0', 0'), _gen_0':s'4(0)) →RΩ(1)
triple'(0', 0')

Induction Step:
foldC'(triple'(0', 0'), _gen_0':s'4(+(_$n205, 1))) →RΩ(1)
f1(foldC'(triple'(0', 0'), _gen_0':s'4(_$n205)), C') →IH
f1(triple'(_gen_0':s'4(0), _gen_0':s'4(0)), C') →RΩ(1)
f'''(triple'(_gen_0':s'4(0), _gen_0':s'4(0)), g'(C')) →RΩ(1)
f'''(triple'(_gen_0':s'4(0), _gen_0':s'4(0)), A') →RΩ(1)
f''''(foldB'(triple'(0', _gen_0':s'4(0)), _gen_0':s'4(0))) →RΩ(1)
f''''(triple'(0', _gen_0':s'4(0))) →RΩ(1)
foldC'(triple'(0', 0'), _gen_0':s'4(0)) →RΩ(1)
triple'(0', 0')

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

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)) → f1(foldB'(t, n), B')
foldC'(t, 0') → t
foldC'(t, s'(n)) → f1(foldC'(t, n), C')
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, s'(c))
f'''(triple'(b, c), B') → f1(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)) → f1(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'
f1 :: 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':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_0':s'3 :: 0':s'
_gen_0':s'4 :: Nat → 0':s'

Lemmas:
foldC'(triple'(0', 0'), _gen_0':s'4(_n204)) → triple'(_gen_0':s'4(0), _gen_0':s'4(0)), rt ∈ Ω(1 + n204)

Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))

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

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

Proved the following rewrite lemma:
foldB'(triple'(0', 0'), _gen_0':s'4(_n4830)) → triple'(_gen_0':s'4(0), _gen_0':s'4(0)), rt ∈ Ω(1 + n4830)

Induction Base:
foldB'(triple'(0', 0'), _gen_0':s'4(0)) →RΩ(1)
triple'(0', 0')

Induction Step:
foldB'(triple'(0', 0'), _gen_0':s'4(+(_$n4831, 1))) →RΩ(1)
f1(foldB'(triple'(0', 0'), _gen_0':s'4(_$n4831)), B') →IH
f1(triple'(_gen_0':s'4(0), _gen_0':s'4(0)), B') →RΩ(1)
f'''(triple'(_gen_0':s'4(0), _gen_0':s'4(0)), g'(B')) →RΩ(1)
f'''(triple'(_gen_0':s'4(0), _gen_0':s'4(0)), A') →RΩ(1)
f''''(foldB'(triple'(0', _gen_0':s'4(0)), _gen_0':s'4(0))) →RΩ(1)
f''''(triple'(0', _gen_0':s'4(0))) →RΩ(1)
foldC'(triple'(0', 0'), _gen_0':s'4(0)) →LΩ(1)
triple'(_gen_0':s'4(0), _gen_0':s'4(0))

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

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)) → f1(foldB'(t, n), B')
foldC'(t, 0') → t
foldC'(t, s'(n)) → f1(foldC'(t, n), C')
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, s'(c))
f'''(triple'(b, c), B') → f1(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)) → f1(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'
f1 :: 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':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_0':s'3 :: 0':s'
_gen_0':s'4 :: Nat → 0':s'

Lemmas:
foldC'(triple'(0', 0'), _gen_0':s'4(_n204)) → triple'(_gen_0':s'4(0), _gen_0':s'4(0)), rt ∈ Ω(1 + n204)
foldB'(triple'(0', 0'), _gen_0':s'4(_n4830)) → triple'(_gen_0':s'4(0), _gen_0':s'4(0)), rt ∈ Ω(1 + n4830)

Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))

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

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

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

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)) → f1(foldB'(t, n), B')
foldC'(t, 0') → t
foldC'(t, s'(n)) → f1(foldC'(t, n), C')
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, s'(c))
f'''(triple'(b, c), B') → f1(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)) → f1(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'
f1 :: 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':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_0':s'3 :: 0':s'
_gen_0':s'4 :: Nat → 0':s'

Lemmas:
foldC'(triple'(0', 0'), _gen_0':s'4(_n204)) → triple'(_gen_0':s'4(0), _gen_0':s'4(0)), rt ∈ Ω(1 + n204)
foldB'(triple'(0', 0'), _gen_0':s'4(_n4830)) → triple'(_gen_0':s'4(0), _gen_0':s'4(0)), rt ∈ Ω(1 + n4830)

Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))

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

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

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

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)) → f1(foldB'(t, n), B')
foldC'(t, 0') → t
foldC'(t, s'(n)) → f1(foldC'(t, n), C')
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, s'(c))
f'''(triple'(b, c), B') → f1(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)) → f1(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'
f1 :: 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':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_0':s'3 :: 0':s'
_gen_0':s'4 :: Nat → 0':s'

Lemmas:
foldC'(triple'(0', 0'), _gen_0':s'4(_n204)) → triple'(_gen_0':s'4(0), _gen_0':s'4(0)), rt ∈ Ω(1 + n204)
foldB'(triple'(0', 0'), _gen_0':s'4(_n4830)) → triple'(_gen_0':s'4(0), _gen_0':s'4(0)), rt ∈ Ω(1 + n4830)

Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))

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

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

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

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)) → f1(foldB'(t, n), B')
foldC'(t, 0') → t
foldC'(t, s'(n)) → f1(foldC'(t, n), C')
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, s'(c))
f'''(triple'(b, c), B') → f1(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)) → f1(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'
f1 :: 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':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_0':s'3 :: 0':s'
_gen_0':s'4 :: Nat → 0':s'

Lemmas:
foldC'(triple'(0', 0'), _gen_0':s'4(_n204)) → triple'(_gen_0':s'4(0), _gen_0':s'4(0)), rt ∈ Ω(1 + n204)
foldB'(triple'(0', 0'), _gen_0':s'4(_n4830)) → triple'(_gen_0':s'4(0), _gen_0':s'4(0)), rt ∈ Ω(1 + n4830)

Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))

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

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

Proved the following rewrite lemma:
foldC'(triple'(0', 0'), _gen_0':s'4(_n10111)) → triple'(_gen_0':s'4(0), _gen_0':s'4(0)), rt ∈ Ω(1 + n10111)

Induction Base:
foldC'(triple'(0', 0'), _gen_0':s'4(0)) →RΩ(1)
triple'(0', 0')

Induction Step:
foldC'(triple'(0', 0'), _gen_0':s'4(+(_$n10112, 1))) →RΩ(1)
f1(foldC'(triple'(0', 0'), _gen_0':s'4(_$n10112)), C') →IH
f1(triple'(_gen_0':s'4(0), _gen_0':s'4(0)), C') →RΩ(1)
f'''(triple'(_gen_0':s'4(0), _gen_0':s'4(0)), g'(C')) →RΩ(1)
f'''(triple'(_gen_0':s'4(0), _gen_0':s'4(0)), A') →RΩ(1)
f''''(foldB'(triple'(0', _gen_0':s'4(0)), _gen_0':s'4(0))) →LΩ(1)
f''''(triple'(_gen_0':s'4(0), _gen_0':s'4(0))) →RΩ(1)
foldC'(triple'(_gen_0':s'4(0), 0'), _gen_0':s'4(0)) →RΩ(1)
triple'(_gen_0':s'4(0), 0')

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

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)) → f1(foldB'(t, n), B')
foldC'(t, 0') → t
foldC'(t, s'(n)) → f1(foldC'(t, n), C')
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, s'(c))
f'''(triple'(b, c), B') → f1(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)) → f1(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'
f1 :: 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':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_0':s'3 :: 0':s'
_gen_0':s'4 :: Nat → 0':s'

Lemmas:
foldC'(triple'(0', 0'), _gen_0':s'4(_n10111)) → triple'(_gen_0':s'4(0), _gen_0':s'4(0)), rt ∈ Ω(1 + n10111)
foldB'(triple'(0', 0'), _gen_0':s'4(_n4830)) → triple'(_gen_0':s'4(0), _gen_0':s'4(0)), rt ∈ Ω(1 + n4830)

Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))

The following defined symbols remain to be analysed:
fold'

Proved the following rewrite lemma:
fold'(triple'(0', 0'), A', _gen_0':s'4(_n16248)) → triple'(_gen_0':s'4(0), _gen_0':s'4(0)), rt ∈ Ω(1 + n16248)

Induction Base:
fold'(triple'(0', 0'), A', _gen_0':s'4(0)) →RΩ(1)
triple'(0', 0')

Induction Step:
fold'(triple'(0', 0'), A', _gen_0':s'4(+(_$n16249, 1))) →RΩ(1)
f1(fold'(triple'(0', 0'), A', _gen_0':s'4(_$n16249)), A') →IH
f1(triple'(_gen_0':s'4(0), _gen_0':s'4(0)), A') →RΩ(1)
f'''(triple'(_gen_0':s'4(0), _gen_0':s'4(0)), g'(A')) →RΩ(1)
f'''(triple'(_gen_0':s'4(0), _gen_0':s'4(0)), A') →RΩ(1)
f''''(foldB'(triple'(0', _gen_0':s'4(0)), _gen_0':s'4(0))) →LΩ(1)
f''''(triple'(_gen_0':s'4(0), _gen_0':s'4(0))) →RΩ(1)
foldC'(triple'(_gen_0':s'4(0), 0'), _gen_0':s'4(0)) →LΩ(1)
triple'(_gen_0':s'4(0), _gen_0':s'4(0))

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

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)) → f1(foldB'(t, n), B')
foldC'(t, 0') → t
foldC'(t, s'(n)) → f1(foldC'(t, n), C')
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, s'(c))
f'''(triple'(b, c), B') → f1(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)) → f1(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'
f1 :: 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':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_0':s'3 :: 0':s'
_gen_0':s'4 :: Nat → 0':s'

Lemmas:
foldC'(triple'(0', 0'), _gen_0':s'4(_n10111)) → triple'(_gen_0':s'4(0), _gen_0':s'4(0)), rt ∈ Ω(1 + n10111)
foldB'(triple'(0', 0'), _gen_0':s'4(_n4830)) → triple'(_gen_0':s'4(0), _gen_0':s'4(0)), rt ∈ Ω(1 + n4830)
fold'(triple'(0', 0'), A', _gen_0':s'4(_n16248)) → triple'(_gen_0':s'4(0), _gen_0':s'4(0)), rt ∈ Ω(1 + n16248)

Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
foldC'(triple'(0', 0'), _gen_0':s'4(_n10111)) → triple'(_gen_0':s'4(0), _gen_0':s'4(0)), rt ∈ Ω(1 + n10111)