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
foldf(x, nil) → x
foldf(x, cons(y, z)) → f(foldf(x, z), y)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, cons(C, c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) → foldf(triple(a, b, nil), c)

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'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(a, b, c), C') → triple'(a, b, cons'(C', c))
f'''(triple'(a, b, c), B') → f1(triple'(a, b, c), A')
f'''(triple'(a, b, c), A') → f''''(foldf'(triple'(cons'(A', a), nil', c), b))
f''''(triple'(a, b, c)) → foldf'(triple'(a, b, nil'), c)

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'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, cons'(C', c))
f'''(triple'(b, c), B') → f1(triple'(b, c), A')
f'''(triple'(b, c), A') → f''''(foldf'(triple'(nil', c), b))
f''''(triple'(b, c)) → foldf'(triple'(b, nil'), c)

Rewrite Strategy: INNERMOST


Infered types.


Rules:
g'(A') → A'
g'(B') → A'
g'(B') → B'
g'(C') → A'
g'(C') → B'
g'(C') → C'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, cons'(C', c))
f'''(triple'(b, c), B') → f1(triple'(b, c), A')
f'''(triple'(b, c), A') → f''''(foldf'(triple'(nil', c), b))
f''''(triple'(b, c)) → foldf'(triple'(b, nil'), c)

Types:
g' :: A':B':C' → A':B':C'
A' :: A':B':C'
B' :: A':B':C'
C' :: A':B':C'
foldf' :: triple' → nil':cons' → triple'
nil' :: nil':cons'
cons' :: A':B':C' → nil':cons' → nil':cons'
f1 :: triple' → A':B':C' → triple'
f''' :: triple' → A':B':C' → triple'
triple' :: nil':cons' → nil':cons' → triple'
f'''' :: triple' → triple'
_hole_A':B':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_nil':cons'3 :: nil':cons'
_gen_nil':cons'4 :: Nat → nil':cons'


Heuristically decided to analyse the following defined symbols:
foldf', f1, f''', f''''

They will be analysed ascendingly in the following order:
foldf' = f1
foldf' = f'''
foldf' = f''''
f1 = f'''
f1 = f''''
f''' = f''''


Rules:
g'(A') → A'
g'(B') → A'
g'(B') → B'
g'(C') → A'
g'(C') → B'
g'(C') → C'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, cons'(C', c))
f'''(triple'(b, c), B') → f1(triple'(b, c), A')
f'''(triple'(b, c), A') → f''''(foldf'(triple'(nil', c), b))
f''''(triple'(b, c)) → foldf'(triple'(b, nil'), c)

Types:
g' :: A':B':C' → A':B':C'
A' :: A':B':C'
B' :: A':B':C'
C' :: A':B':C'
foldf' :: triple' → nil':cons' → triple'
nil' :: nil':cons'
cons' :: A':B':C' → nil':cons' → nil':cons'
f1 :: triple' → A':B':C' → triple'
f''' :: triple' → A':B':C' → triple'
triple' :: nil':cons' → nil':cons' → triple'
f'''' :: triple' → triple'
_hole_A':B':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_nil':cons'3 :: nil':cons'
_gen_nil':cons'4 :: Nat → nil':cons'

Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(A', _gen_nil':cons'4(x))

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

They will be analysed ascendingly in the following order:
foldf' = f1
foldf' = f'''
foldf' = f''''
f1 = f'''
f1 = 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'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, cons'(C', c))
f'''(triple'(b, c), B') → f1(triple'(b, c), A')
f'''(triple'(b, c), A') → f''''(foldf'(triple'(nil', c), b))
f''''(triple'(b, c)) → foldf'(triple'(b, nil'), c)

Types:
g' :: A':B':C' → A':B':C'
A' :: A':B':C'
B' :: A':B':C'
C' :: A':B':C'
foldf' :: triple' → nil':cons' → triple'
nil' :: nil':cons'
cons' :: A':B':C' → nil':cons' → nil':cons'
f1 :: triple' → A':B':C' → triple'
f''' :: triple' → A':B':C' → triple'
triple' :: nil':cons' → nil':cons' → triple'
f'''' :: triple' → triple'
_hole_A':B':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_nil':cons'3 :: nil':cons'
_gen_nil':cons'4 :: Nat → nil':cons'

Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(A', _gen_nil':cons'4(x))

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

They will be analysed ascendingly in the following order:
foldf' = f1
foldf' = f'''
foldf' = f''''
f1 = f'''
f1 = 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'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, cons'(C', c))
f'''(triple'(b, c), B') → f1(triple'(b, c), A')
f'''(triple'(b, c), A') → f''''(foldf'(triple'(nil', c), b))
f''''(triple'(b, c)) → foldf'(triple'(b, nil'), c)

Types:
g' :: A':B':C' → A':B':C'
A' :: A':B':C'
B' :: A':B':C'
C' :: A':B':C'
foldf' :: triple' → nil':cons' → triple'
nil' :: nil':cons'
cons' :: A':B':C' → nil':cons' → nil':cons'
f1 :: triple' → A':B':C' → triple'
f''' :: triple' → A':B':C' → triple'
triple' :: nil':cons' → nil':cons' → triple'
f'''' :: triple' → triple'
_hole_A':B':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_nil':cons'3 :: nil':cons'
_gen_nil':cons'4 :: Nat → nil':cons'

Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(A', _gen_nil':cons'4(x))

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

They will be analysed ascendingly in the following order:
foldf' = f1
foldf' = f'''
foldf' = f''''
f1 = f'''
f1 = 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'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, cons'(C', c))
f'''(triple'(b, c), B') → f1(triple'(b, c), A')
f'''(triple'(b, c), A') → f''''(foldf'(triple'(nil', c), b))
f''''(triple'(b, c)) → foldf'(triple'(b, nil'), c)

Types:
g' :: A':B':C' → A':B':C'
A' :: A':B':C'
B' :: A':B':C'
C' :: A':B':C'
foldf' :: triple' → nil':cons' → triple'
nil' :: nil':cons'
cons' :: A':B':C' → nil':cons' → nil':cons'
f1 :: triple' → A':B':C' → triple'
f''' :: triple' → A':B':C' → triple'
triple' :: nil':cons' → nil':cons' → triple'
f'''' :: triple' → triple'
_hole_A':B':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_nil':cons'3 :: nil':cons'
_gen_nil':cons'4 :: Nat → nil':cons'

Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(A', _gen_nil':cons'4(x))

The following defined symbols remain to be analysed:
foldf'

They will be analysed ascendingly in the following order:
foldf' = f1
foldf' = f'''
foldf' = f''''
f1 = f'''
f1 = f''''
f''' = f''''


Proved the following rewrite lemma:
foldf'(triple'(nil', nil'), _gen_nil':cons'4(_n224)) → triple'(_gen_nil':cons'4(0), _gen_nil':cons'4(0)), rt ∈ Ω(1 + n224)

Induction Base:
foldf'(triple'(nil', nil'), _gen_nil':cons'4(0)) →RΩ(1)
triple'(nil', nil')

Induction Step:
foldf'(triple'(nil', nil'), _gen_nil':cons'4(+(_$n225, 1))) →RΩ(1)
f1(foldf'(triple'(nil', nil'), _gen_nil':cons'4(_$n225)), A') →IH
f1(triple'(_gen_nil':cons'4(0), _gen_nil':cons'4(0)), A') →RΩ(1)
f'''(triple'(_gen_nil':cons'4(0), _gen_nil':cons'4(0)), g'(A')) →RΩ(1)
f'''(triple'(_gen_nil':cons'4(0), _gen_nil':cons'4(0)), A') →RΩ(1)
f''''(foldf'(triple'(nil', _gen_nil':cons'4(0)), _gen_nil':cons'4(0))) →RΩ(1)
f''''(triple'(nil', _gen_nil':cons'4(0))) →RΩ(1)
foldf'(triple'(nil', nil'), _gen_nil':cons'4(0)) →RΩ(1)
triple'(nil', nil')

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'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, cons'(C', c))
f'''(triple'(b, c), B') → f1(triple'(b, c), A')
f'''(triple'(b, c), A') → f''''(foldf'(triple'(nil', c), b))
f''''(triple'(b, c)) → foldf'(triple'(b, nil'), c)

Types:
g' :: A':B':C' → A':B':C'
A' :: A':B':C'
B' :: A':B':C'
C' :: A':B':C'
foldf' :: triple' → nil':cons' → triple'
nil' :: nil':cons'
cons' :: A':B':C' → nil':cons' → nil':cons'
f1 :: triple' → A':B':C' → triple'
f''' :: triple' → A':B':C' → triple'
triple' :: nil':cons' → nil':cons' → triple'
f'''' :: triple' → triple'
_hole_A':B':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_nil':cons'3 :: nil':cons'
_gen_nil':cons'4 :: Nat → nil':cons'

Lemmas:
foldf'(triple'(nil', nil'), _gen_nil':cons'4(_n224)) → triple'(_gen_nil':cons'4(0), _gen_nil':cons'4(0)), rt ∈ Ω(1 + n224)

Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(A', _gen_nil':cons'4(x))

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

They will be analysed ascendingly in the following order:
foldf' = f1
foldf' = f'''
foldf' = f''''
f1 = f'''
f1 = 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'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, cons'(C', c))
f'''(triple'(b, c), B') → f1(triple'(b, c), A')
f'''(triple'(b, c), A') → f''''(foldf'(triple'(nil', c), b))
f''''(triple'(b, c)) → foldf'(triple'(b, nil'), c)

Types:
g' :: A':B':C' → A':B':C'
A' :: A':B':C'
B' :: A':B':C'
C' :: A':B':C'
foldf' :: triple' → nil':cons' → triple'
nil' :: nil':cons'
cons' :: A':B':C' → nil':cons' → nil':cons'
f1 :: triple' → A':B':C' → triple'
f''' :: triple' → A':B':C' → triple'
triple' :: nil':cons' → nil':cons' → triple'
f'''' :: triple' → triple'
_hole_A':B':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_nil':cons'3 :: nil':cons'
_gen_nil':cons'4 :: Nat → nil':cons'

Lemmas:
foldf'(triple'(nil', nil'), _gen_nil':cons'4(_n224)) → triple'(_gen_nil':cons'4(0), _gen_nil':cons'4(0)), rt ∈ Ω(1 + n224)

Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(A', _gen_nil':cons'4(x))

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

They will be analysed ascendingly in the following order:
foldf' = f1
foldf' = f'''
foldf' = f''''
f1 = f'''
f1 = 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'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, cons'(C', c))
f'''(triple'(b, c), B') → f1(triple'(b, c), A')
f'''(triple'(b, c), A') → f''''(foldf'(triple'(nil', c), b))
f''''(triple'(b, c)) → foldf'(triple'(b, nil'), c)

Types:
g' :: A':B':C' → A':B':C'
A' :: A':B':C'
B' :: A':B':C'
C' :: A':B':C'
foldf' :: triple' → nil':cons' → triple'
nil' :: nil':cons'
cons' :: A':B':C' → nil':cons' → nil':cons'
f1 :: triple' → A':B':C' → triple'
f''' :: triple' → A':B':C' → triple'
triple' :: nil':cons' → nil':cons' → triple'
f'''' :: triple' → triple'
_hole_A':B':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_nil':cons'3 :: nil':cons'
_gen_nil':cons'4 :: Nat → nil':cons'

Lemmas:
foldf'(triple'(nil', nil'), _gen_nil':cons'4(_n224)) → triple'(_gen_nil':cons'4(0), _gen_nil':cons'4(0)), rt ∈ Ω(1 + n224)

Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(A', _gen_nil':cons'4(x))

The following defined symbols remain to be analysed:
f''''

They will be analysed ascendingly in the following order:
foldf' = f1
foldf' = f'''
foldf' = f''''
f1 = f'''
f1 = 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'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, cons'(C', c))
f'''(triple'(b, c), B') → f1(triple'(b, c), A')
f'''(triple'(b, c), A') → f''''(foldf'(triple'(nil', c), b))
f''''(triple'(b, c)) → foldf'(triple'(b, nil'), c)

Types:
g' :: A':B':C' → A':B':C'
A' :: A':B':C'
B' :: A':B':C'
C' :: A':B':C'
foldf' :: triple' → nil':cons' → triple'
nil' :: nil':cons'
cons' :: A':B':C' → nil':cons' → nil':cons'
f1 :: triple' → A':B':C' → triple'
f''' :: triple' → A':B':C' → triple'
triple' :: nil':cons' → nil':cons' → triple'
f'''' :: triple' → triple'
_hole_A':B':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_nil':cons'3 :: nil':cons'
_gen_nil':cons'4 :: Nat → nil':cons'

Lemmas:
foldf'(triple'(nil', nil'), _gen_nil':cons'4(_n224)) → triple'(_gen_nil':cons'4(0), _gen_nil':cons'4(0)), rt ∈ Ω(1 + n224)

Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(A', _gen_nil':cons'4(x))

No more defined symbols left to analyse.


The lowerbound Ω(n) was proven with the following lemma:
foldf'(triple'(nil', nil'), _gen_nil':cons'4(_n224)) → triple'(_gen_nil':cons'4(0), _gen_nil':cons'4(0)), rt ∈ Ω(1 + n224)