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

f(s(x)) → f(id_inc(c(x, x)))
f(c(s(x), y)) → g(c(x, y))
g(c(s(x), y)) → g(c(y, x))
g(c(x, s(y))) → g(c(y, x))
g(c(x, x)) → f(x)
id_inc(c(x, y)) → c(id_inc(x), id_inc(y))
id_inc(s(x)) → s(id_inc(x))
id_inc(0) → 0
id_inc(0) → s(0)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

f'(s'(x)) → f'(id_inc'(c'(x, x)))
f'(c'(s'(x), y)) → g'(c'(x, y))
g'(c'(s'(x), y)) → g'(c'(y, x))
g'(c'(x, s'(y))) → g'(c'(y, x))
g'(c'(x, x)) → f'(x)
id_inc'(c'(x, y)) → c'(id_inc'(x), id_inc'(y))
id_inc'(s'(x)) → s'(id_inc'(x))
id_inc'(0') → 0'
id_inc'(0') → s'(0')

Rewrite Strategy: INNERMOST

Infered types.

Rules:
f'(s'(x)) → f'(id_inc'(c'(x, x)))
f'(c'(s'(x), y)) → g'(c'(x, y))
g'(c'(s'(x), y)) → g'(c'(y, x))
g'(c'(x, s'(y))) → g'(c'(y, x))
g'(c'(x, x)) → f'(x)
id_inc'(c'(x, y)) → c'(id_inc'(x), id_inc'(y))
id_inc'(s'(x)) → s'(id_inc'(x))
id_inc'(0') → 0'
id_inc'(0') → s'(0')

Types:
f' :: s':c':0' → f':g'
s' :: s':c':0' → s':c':0'
id_inc' :: s':c':0' → s':c':0'
c' :: s':c':0' → s':c':0' → s':c':0'
g' :: s':c':0' → f':g'
0' :: s':c':0'
_hole_f':g'1 :: f':g'
_hole_s':c':0'2 :: s':c':0'
_gen_s':c':0'3 :: Nat → s':c':0'

Heuristically decided to analyse the following defined symbols:
f', id_inc', g'

They will be analysed ascendingly in the following order:
id_inc' < f'
f' = g'

Rules:
f'(s'(x)) → f'(id_inc'(c'(x, x)))
f'(c'(s'(x), y)) → g'(c'(x, y))
g'(c'(s'(x), y)) → g'(c'(y, x))
g'(c'(x, s'(y))) → g'(c'(y, x))
g'(c'(x, x)) → f'(x)
id_inc'(c'(x, y)) → c'(id_inc'(x), id_inc'(y))
id_inc'(s'(x)) → s'(id_inc'(x))
id_inc'(0') → 0'
id_inc'(0') → s'(0')

Types:
f' :: s':c':0' → f':g'
s' :: s':c':0' → s':c':0'
id_inc' :: s':c':0' → s':c':0'
c' :: s':c':0' → s':c':0' → s':c':0'
g' :: s':c':0' → f':g'
0' :: s':c':0'
_hole_f':g'1 :: f':g'
_hole_s':c':0'2 :: s':c':0'
_gen_s':c':0'3 :: Nat → s':c':0'

Generator Equations:
_gen_s':c':0'3(0) ⇔ 0'
_gen_s':c':0'3(+(x, 1)) ⇔ s'(_gen_s':c':0'3(x))

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

They will be analysed ascendingly in the following order:
id_inc' < f'
f' = g'

Proved the following rewrite lemma:
id_inc'(_gen_s':c':0'3(_n5)) → _gen_s':c':0'3(_n5), rt ∈ Ω(1 + n5)

Induction Base:
id_inc'(_gen_s':c':0'3(0)) →RΩ(1)
0'

Induction Step:
id_inc'(_gen_s':c':0'3(+(_\$n6, 1))) →RΩ(1)
s'(id_inc'(_gen_s':c':0'3(_\$n6))) →IH
s'(_gen_s':c':0'3(_\$n6))

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

Rules:
f'(s'(x)) → f'(id_inc'(c'(x, x)))
f'(c'(s'(x), y)) → g'(c'(x, y))
g'(c'(s'(x), y)) → g'(c'(y, x))
g'(c'(x, s'(y))) → g'(c'(y, x))
g'(c'(x, x)) → f'(x)
id_inc'(c'(x, y)) → c'(id_inc'(x), id_inc'(y))
id_inc'(s'(x)) → s'(id_inc'(x))
id_inc'(0') → 0'
id_inc'(0') → s'(0')

Types:
f' :: s':c':0' → f':g'
s' :: s':c':0' → s':c':0'
id_inc' :: s':c':0' → s':c':0'
c' :: s':c':0' → s':c':0' → s':c':0'
g' :: s':c':0' → f':g'
0' :: s':c':0'
_hole_f':g'1 :: f':g'
_hole_s':c':0'2 :: s':c':0'
_gen_s':c':0'3 :: Nat → s':c':0'

Lemmas:
id_inc'(_gen_s':c':0'3(_n5)) → _gen_s':c':0'3(_n5), rt ∈ Ω(1 + n5)

Generator Equations:
_gen_s':c':0'3(0) ⇔ 0'
_gen_s':c':0'3(+(x, 1)) ⇔ s'(_gen_s':c':0'3(x))

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

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

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

Rules:
f'(s'(x)) → f'(id_inc'(c'(x, x)))
f'(c'(s'(x), y)) → g'(c'(x, y))
g'(c'(s'(x), y)) → g'(c'(y, x))
g'(c'(x, s'(y))) → g'(c'(y, x))
g'(c'(x, x)) → f'(x)
id_inc'(c'(x, y)) → c'(id_inc'(x), id_inc'(y))
id_inc'(s'(x)) → s'(id_inc'(x))
id_inc'(0') → 0'
id_inc'(0') → s'(0')

Types:
f' :: s':c':0' → f':g'
s' :: s':c':0' → s':c':0'
id_inc' :: s':c':0' → s':c':0'
c' :: s':c':0' → s':c':0' → s':c':0'
g' :: s':c':0' → f':g'
0' :: s':c':0'
_hole_f':g'1 :: f':g'
_hole_s':c':0'2 :: s':c':0'
_gen_s':c':0'3 :: Nat → s':c':0'

Lemmas:
id_inc'(_gen_s':c':0'3(_n5)) → _gen_s':c':0'3(_n5), rt ∈ Ω(1 + n5)

Generator Equations:
_gen_s':c':0'3(0) ⇔ 0'
_gen_s':c':0'3(+(x, 1)) ⇔ s'(_gen_s':c':0'3(x))

The following defined symbols remain to be analysed:
f'

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

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

Rules:
f'(s'(x)) → f'(id_inc'(c'(x, x)))
f'(c'(s'(x), y)) → g'(c'(x, y))
g'(c'(s'(x), y)) → g'(c'(y, x))
g'(c'(x, s'(y))) → g'(c'(y, x))
g'(c'(x, x)) → f'(x)
id_inc'(c'(x, y)) → c'(id_inc'(x), id_inc'(y))
id_inc'(s'(x)) → s'(id_inc'(x))
id_inc'(0') → 0'
id_inc'(0') → s'(0')

Types:
f' :: s':c':0' → f':g'
s' :: s':c':0' → s':c':0'
id_inc' :: s':c':0' → s':c':0'
c' :: s':c':0' → s':c':0' → s':c':0'
g' :: s':c':0' → f':g'
0' :: s':c':0'
_hole_f':g'1 :: f':g'
_hole_s':c':0'2 :: s':c':0'
_gen_s':c':0'3 :: Nat → s':c':0'

Lemmas:
id_inc'(_gen_s':c':0'3(_n5)) → _gen_s':c':0'3(_n5), rt ∈ Ω(1 + n5)

Generator Equations:
_gen_s':c':0'3(0) ⇔ 0'
_gen_s':c':0'3(+(x, 1)) ⇔ s'(_gen_s':c':0'3(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
id_inc'(_gen_s':c':0'3(_n5)) → _gen_s':c':0'3(_n5), rt ∈ Ω(1 + n5)