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

:(:(x, y), z) → :(x, :(y, z))
:(+(x, y), z) → +(:(x, z), :(y, z))
:(z, +(x, f(y))) → :(g(z, y), +(x, a))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


:'(:'(x, y), z) → :'(x, :'(y, z))
:'(+'(x, y), z) → +'(:'(x, z), :'(y, z))
:'(z, +'(x, f'(y))) → :'(g'(z, y), +'(x, a'))

Rewrite Strategy: INNERMOST

Sliced the following arguments:
f'/0
g'/0
g'/1

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


:'(:'(x, y), z) → :'(x, :'(y, z))
:'(+'(x, y), z) → +'(:'(x, z), :'(y, z))
:'(z, +'(x, f')) → :'(g', +'(x, a'))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
:'(:'(x, y), z) → :'(x, :'(y, z))
:'(+'(x, y), z) → +'(:'(x, z), :'(y, z))
:'(z, +'(x, f')) → :'(g', +'(x, a'))

Types:
:' :: +':f':g':a' → +':f':g':a' → +':f':g':a'
+' :: +':f':g':a' → +':f':g':a' → +':f':g':a'
f' :: +':f':g':a'
g' :: +':f':g':a'
a' :: +':f':g':a'
_hole_+':f':g':a'1 :: +':f':g':a'
_gen_+':f':g':a'2 :: Nat → +':f':g':a'

Heuristically decided to analyse the following defined symbols:
:'

Rules:
:'(:'(x, y), z) → :'(x, :'(y, z))
:'(+'(x, y), z) → +'(:'(x, z), :'(y, z))
:'(z, +'(x, f')) → :'(g', +'(x, a'))

Types:
:' :: +':f':g':a' → +':f':g':a' → +':f':g':a'
+' :: +':f':g':a' → +':f':g':a' → +':f':g':a'
f' :: +':f':g':a'
g' :: +':f':g':a'
a' :: +':f':g':a'
_hole_+':f':g':a'1 :: +':f':g':a'
_gen_+':f':g':a'2 :: Nat → +':f':g':a'

Generator Equations:
_gen_+':f':g':a'2(0) ⇔ f'
_gen_+':f':g':a'2(+(x, 1)) ⇔ +'(_gen_+':f':g':a'2(x), f')

The following defined symbols remain to be analysed:
:'

Proved the following rewrite lemma:
:'(_gen_+':f':g':a'2(+(1, _n4)), _gen_+':f':g':a'2(b)) → _*3, rt ∈ Ω(n4)

Induction Base:
:'(_gen_+':f':g':a'2(+(1, 0)), _gen_+':f':g':a'2(b))

Induction Step:
:'(_gen_+':f':g':a'2(+(1, +(_$n5, 1))), _gen_+':f':g':a'2(_b1059)) →RΩ(1)
+'(:'(_gen_+':f':g':a'2(+(1, _$n5)), _gen_+':f':g':a'2(_b1059)), :'(f', _gen_+':f':g':a'2(_b1059))) →IH
+'(_*3, :'(f', _gen_+':f':g':a'2(_b1059)))

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

Rules:
:'(:'(x, y), z) → :'(x, :'(y, z))
:'(+'(x, y), z) → +'(:'(x, z), :'(y, z))
:'(z, +'(x, f')) → :'(g', +'(x, a'))

Types:
:' :: +':f':g':a' → +':f':g':a' → +':f':g':a'
+' :: +':f':g':a' → +':f':g':a' → +':f':g':a'
f' :: +':f':g':a'
g' :: +':f':g':a'
a' :: +':f':g':a'
_hole_+':f':g':a'1 :: +':f':g':a'
_gen_+':f':g':a'2 :: Nat → +':f':g':a'

Lemmas:
:'(_gen_+':f':g':a'2(+(1, _n4)), _gen_+':f':g':a'2(b)) → _*3, rt ∈ Ω(n4)

Generator Equations:
_gen_+':f':g':a'2(0) ⇔ f'
_gen_+':f':g':a'2(+(x, 1)) ⇔ +'(_gen_+':f':g':a'2(x), f')

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
:'(_gen_+':f':g':a'2(+(1, _n4)), _gen_+':f':g':a'2(b)) → _*3, rt ∈ Ω(n4)