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

f(S(x'), S(x)) → h(g(x', S(x)), f(S(S(x')), x))
h(0, S(x)) → h(0, x)
h(0, 0) → 0
g(S(x), S(x')) → h(f(S(x), S(x')), g(x, S(S(x'))))
g(S(x), 0) → 0
f(S(x), 0) → 0
h(S(x), x2) → h(x, x2)
g(0, x2) → 0
f(0, x2) → 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'), S'(x)) → h'(g'(x', S'(x)), f'(S'(S'(x')), x))
h'(0', S'(x)) → h'(0', x)
h'(0', 0') → 0'
g'(S'(x), S'(x')) → h'(f'(S'(x), S'(x')), g'(x, S'(S'(x'))))
g'(S'(x), 0') → 0'
f'(S'(x), 0') → 0'
h'(S'(x), x2) → h'(x, x2)
g'(0', x2) → 0'
f'(0', x2) → 0'

Rewrite Strategy: INNERMOST

Infered types.

Rules:
f'(S'(x'), S'(x)) → h'(g'(x', S'(x)), f'(S'(S'(x')), x))
h'(0', S'(x)) → h'(0', x)
h'(0', 0') → 0'
g'(S'(x), S'(x')) → h'(f'(S'(x), S'(x')), g'(x, S'(S'(x'))))
g'(S'(x), 0') → 0'
f'(S'(x), 0') → 0'
h'(S'(x), x2) → h'(x, x2)
g'(0', x2) → 0'
f'(0', x2) → 0'

Types:
f' :: S':0' → S':0' → S':0'
S' :: S':0' → S':0'
h' :: S':0' → S':0' → S':0'
g' :: S':0' → S':0' → S':0'
0' :: S':0'
_hole_S':0'1 :: S':0'
_gen_S':0'2 :: Nat → S':0'

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

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

Rules:
f'(S'(x'), S'(x)) → h'(g'(x', S'(x)), f'(S'(S'(x')), x))
h'(0', S'(x)) → h'(0', x)
h'(0', 0') → 0'
g'(S'(x), S'(x')) → h'(f'(S'(x), S'(x')), g'(x, S'(S'(x'))))
g'(S'(x), 0') → 0'
f'(S'(x), 0') → 0'
h'(S'(x), x2) → h'(x, x2)
g'(0', x2) → 0'
f'(0', x2) → 0'

Types:
f' :: S':0' → S':0' → S':0'
S' :: S':0' → S':0'
h' :: S':0' → S':0' → S':0'
g' :: S':0' → S':0' → S':0'
0' :: S':0'
_hole_S':0'1 :: S':0'
_gen_S':0'2 :: Nat → S':0'

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

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

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

Proved the following rewrite lemma:
h'(_gen_S':0'2(0), _gen_S':0'2(_n4)) → _gen_S':0'2(0), rt ∈ Ω(1 + n4)

Induction Base:
h'(_gen_S':0'2(0), _gen_S':0'2(0)) →RΩ(1)
0'

Induction Step:
h'(_gen_S':0'2(0), _gen_S':0'2(+(_$n5, 1))) →RΩ(1)
h'(0', _gen_S':0'2(_$n5)) →IH
_gen_S':0'2(0)

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

Rules:
f'(S'(x'), S'(x)) → h'(g'(x', S'(x)), f'(S'(S'(x')), x))
h'(0', S'(x)) → h'(0', x)
h'(0', 0') → 0'
g'(S'(x), S'(x')) → h'(f'(S'(x), S'(x')), g'(x, S'(S'(x'))))
g'(S'(x), 0') → 0'
f'(S'(x), 0') → 0'
h'(S'(x), x2) → h'(x, x2)
g'(0', x2) → 0'
f'(0', x2) → 0'

Types:
f' :: S':0' → S':0' → S':0'
S' :: S':0' → S':0'
h' :: S':0' → S':0' → S':0'
g' :: S':0' → S':0' → S':0'
0' :: S':0'
_hole_S':0'1 :: S':0'
_gen_S':0'2 :: Nat → S':0'

Lemmas:
h'(_gen_S':0'2(0), _gen_S':0'2(_n4)) → _gen_S':0'2(0), rt ∈ Ω(1 + n4)

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

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

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

Proved the following rewrite lemma:
g'(_gen_S':0'2(+(1, _n627)), _gen_S':0'2(1)) → _*3, rt ∈ Ω(n627)

Induction Base:
g'(_gen_S':0'2(+(1, 0)), _gen_S':0'2(1))

Induction Step:
g'(_gen_S':0'2(+(1, +(_$n628, 1))), _gen_S':0'2(1)) →RΩ(1)
h'(f'(S'(_gen_S':0'2(+(1, _$n628))), S'(_gen_S':0'2(0))), g'(_gen_S':0'2(+(1, _$n628)), S'(S'(_gen_S':0'2(0))))) →RΩ(1)
h'(h'(g'(_gen_S':0'2(+(1, _$n628)), S'(_gen_S':0'2(0))), f'(S'(S'(_gen_S':0'2(+(1, _$n628)))), _gen_S':0'2(0))), g'(_gen_S':0'2(+(1, _$n628)), S'(S'(_gen_S':0'2(0))))) →IH
h'(h'(_*3, f'(S'(S'(_gen_S':0'2(+(1, _$n628)))), _gen_S':0'2(0))), g'(_gen_S':0'2(+(1, _$n628)), S'(S'(_gen_S':0'2(0))))) →RΩ(1)
h'(h'(_*3, 0'), g'(_gen_S':0'2(+(1, _$n628)), S'(S'(_gen_S':0'2(0))))) →RΩ(1)
h'(h'(_*3, 0'), h'(f'(S'(_gen_S':0'2(_$n628)), S'(S'(_gen_S':0'2(0)))), g'(_gen_S':0'2(_$n628), S'(S'(S'(_gen_S':0'2(0))))))) →RΩ(1)
h'(h'(_*3, 0'), h'(h'(g'(_gen_S':0'2(_$n628), S'(S'(_gen_S':0'2(0)))), f'(S'(S'(_gen_S':0'2(_$n628))), S'(_gen_S':0'2(0)))), g'(_gen_S':0'2(_$n628), S'(S'(S'(_gen_S':0'2(0)))))))

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

Rules:
f'(S'(x'), S'(x)) → h'(g'(x', S'(x)), f'(S'(S'(x')), x))
h'(0', S'(x)) → h'(0', x)
h'(0', 0') → 0'
g'(S'(x), S'(x')) → h'(f'(S'(x), S'(x')), g'(x, S'(S'(x'))))
g'(S'(x), 0') → 0'
f'(S'(x), 0') → 0'
h'(S'(x), x2) → h'(x, x2)
g'(0', x2) → 0'
f'(0', x2) → 0'

Types:
f' :: S':0' → S':0' → S':0'
S' :: S':0' → S':0'
h' :: S':0' → S':0' → S':0'
g' :: S':0' → S':0' → S':0'
0' :: S':0'
_hole_S':0'1 :: S':0'
_gen_S':0'2 :: Nat → S':0'

Lemmas:
h'(_gen_S':0'2(0), _gen_S':0'2(_n4)) → _gen_S':0'2(0), rt ∈ Ω(1 + n4)
g'(_gen_S':0'2(+(1, _n627)), _gen_S':0'2(1)) → _*3, rt ∈ Ω(n627)

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

The following defined symbols remain to be analysed:
f'

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

Proved the following rewrite lemma:
f'(_gen_S':0'2(+(1, _n30596)), _gen_S':0'2(1)) → _*3, rt ∈ Ω(n30596)

Induction Base:
f'(_gen_S':0'2(+(1, 0)), _gen_S':0'2(1))

Induction Step:
f'(_gen_S':0'2(+(1, +(_$n30597, 1))), _gen_S':0'2(1)) →RΩ(1)
h'(g'(_gen_S':0'2(+(1, _$n30597)), S'(_gen_S':0'2(0))), f'(S'(S'(_gen_S':0'2(+(1, _$n30597)))), _gen_S':0'2(0))) →RΩ(1)
h'(h'(f'(S'(_gen_S':0'2(_$n30597)), S'(_gen_S':0'2(0))), g'(_gen_S':0'2(_$n30597), S'(S'(_gen_S':0'2(0))))), f'(S'(S'(_gen_S':0'2(+(1, _$n30597)))), _gen_S':0'2(0))) →IH
h'(h'(_*3, g'(_gen_S':0'2(_$n30597), S'(S'(_gen_S':0'2(0))))), f'(S'(S'(_gen_S':0'2(+(1, _$n30597)))), _gen_S':0'2(0)))

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

Rules:
f'(S'(x'), S'(x)) → h'(g'(x', S'(x)), f'(S'(S'(x')), x))
h'(0', S'(x)) → h'(0', x)
h'(0', 0') → 0'
g'(S'(x), S'(x')) → h'(f'(S'(x), S'(x')), g'(x, S'(S'(x'))))
g'(S'(x), 0') → 0'
f'(S'(x), 0') → 0'
h'(S'(x), x2) → h'(x, x2)
g'(0', x2) → 0'
f'(0', x2) → 0'

Types:
f' :: S':0' → S':0' → S':0'
S' :: S':0' → S':0'
h' :: S':0' → S':0' → S':0'
g' :: S':0' → S':0' → S':0'
0' :: S':0'
_hole_S':0'1 :: S':0'
_gen_S':0'2 :: Nat → S':0'

Lemmas:
h'(_gen_S':0'2(0), _gen_S':0'2(_n4)) → _gen_S':0'2(0), rt ∈ Ω(1 + n4)
g'(_gen_S':0'2(+(1, _n627)), _gen_S':0'2(1)) → _*3, rt ∈ Ω(n627)
f'(_gen_S':0'2(+(1, _n30596)), _gen_S':0'2(1)) → _*3, rt ∈ Ω(n30596)

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

The following defined symbols remain to be analysed:
g'

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

Proved the following rewrite lemma:
g'(_gen_S':0'2(+(1, _n98273)), _gen_S':0'2(1)) → _*3, rt ∈ Ω(n98273)

Induction Base:
g'(_gen_S':0'2(+(1, 0)), _gen_S':0'2(1))

Induction Step:
g'(_gen_S':0'2(+(1, +(_$n98274, 1))), _gen_S':0'2(1)) →RΩ(1)
h'(f'(S'(_gen_S':0'2(+(1, _$n98274))), S'(_gen_S':0'2(0))), g'(_gen_S':0'2(+(1, _$n98274)), S'(S'(_gen_S':0'2(0))))) →RΩ(1)
h'(h'(g'(_gen_S':0'2(+(1, _$n98274)), S'(_gen_S':0'2(0))), f'(S'(S'(_gen_S':0'2(+(1, _$n98274)))), _gen_S':0'2(0))), g'(_gen_S':0'2(+(1, _$n98274)), S'(S'(_gen_S':0'2(0))))) →IH
h'(h'(_*3, f'(S'(S'(_gen_S':0'2(+(1, _$n98274)))), _gen_S':0'2(0))), g'(_gen_S':0'2(+(1, _$n98274)), S'(S'(_gen_S':0'2(0))))) →RΩ(1)
h'(h'(_*3, 0'), g'(_gen_S':0'2(+(1, _$n98274)), S'(S'(_gen_S':0'2(0))))) →RΩ(1)
h'(h'(_*3, 0'), h'(f'(S'(_gen_S':0'2(_$n98274)), S'(S'(_gen_S':0'2(0)))), g'(_gen_S':0'2(_$n98274), S'(S'(S'(_gen_S':0'2(0))))))) →RΩ(1)
h'(h'(_*3, 0'), h'(h'(g'(_gen_S':0'2(_$n98274), S'(S'(_gen_S':0'2(0)))), f'(S'(S'(_gen_S':0'2(_$n98274))), S'(_gen_S':0'2(0)))), g'(_gen_S':0'2(_$n98274), S'(S'(S'(_gen_S':0'2(0)))))))

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

Rules:
f'(S'(x'), S'(x)) → h'(g'(x', S'(x)), f'(S'(S'(x')), x))
h'(0', S'(x)) → h'(0', x)
h'(0', 0') → 0'
g'(S'(x), S'(x')) → h'(f'(S'(x), S'(x')), g'(x, S'(S'(x'))))
g'(S'(x), 0') → 0'
f'(S'(x), 0') → 0'
h'(S'(x), x2) → h'(x, x2)
g'(0', x2) → 0'
f'(0', x2) → 0'

Types:
f' :: S':0' → S':0' → S':0'
S' :: S':0' → S':0'
h' :: S':0' → S':0' → S':0'
g' :: S':0' → S':0' → S':0'
0' :: S':0'
_hole_S':0'1 :: S':0'
_gen_S':0'2 :: Nat → S':0'

Lemmas:
h'(_gen_S':0'2(0), _gen_S':0'2(_n4)) → _gen_S':0'2(0), rt ∈ Ω(1 + n4)
g'(_gen_S':0'2(+(1, _n98273)), _gen_S':0'2(1)) → _*3, rt ∈ Ω(n98273)
f'(_gen_S':0'2(+(1, _n30596)), _gen_S':0'2(1)) → _*3, rt ∈ Ω(n30596)

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

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
h'(_gen_S':0'2(0), _gen_S':0'2(_n4)) → _gen_S':0'2(0), rt ∈ Ω(1 + n4)