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

0(#) → #
+(#, x) → x
+(x, #) → x
+(0(x), 0(y)) → 0(+(x, y))
+(0(x), 1(y)) → 1(+(x, y))
+(1(x), 0(y)) → 1(+(x, y))
+(0(x), j(y)) → j(+(x, y))
+(j(x), 0(y)) → j(+(x, y))
+(1(x), 1(y)) → j(+(+(x, y), 1(#)))
+(j(x), j(y)) → 1(+(+(x, y), j(#)))
+(1(x), j(y)) → 0(+(x, y))
+(j(x), 1(y)) → 0(+(x, y))
+(+(x, y), z) → +(x, +(y, z))
opp(#) → #
opp(0(x)) → 0(opp(x))
opp(1(x)) → j(opp(x))
opp(j(x)) → 1(opp(x))
-(x, y) → +(x, opp(y))
*(#, x) → #
*(0(x), y) → 0(*(x, y))
*(1(x), y) → +(0(*(x, y)), y)
*(j(x), y) → -(0(*(x, y)), y)
*(*(x, y), z) → *(x, *(y, z))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

0'(#') → #'
+'(#', x) → x
+'(x, #') → x
+'(0'(x), 0'(y)) → 0'(+'(x, y))
+'(0'(x), 1'(y)) → 1'(+'(x, y))
+'(1'(x), 0'(y)) → 1'(+'(x, y))
+'(0'(x), j'(y)) → j'(+'(x, y))
+'(j'(x), 0'(y)) → j'(+'(x, y))
+'(1'(x), 1'(y)) → j'(+'(+'(x, y), 1'(#')))
+'(j'(x), j'(y)) → 1'(+'(+'(x, y), j'(#')))
+'(1'(x), j'(y)) → 0'(+'(x, y))
+'(j'(x), 1'(y)) → 0'(+'(x, y))
+'(+'(x, y), z) → +'(x, +'(y, z))
opp'(#') → #'
opp'(0'(x)) → 0'(opp'(x))
opp'(1'(x)) → j'(opp'(x))
opp'(j'(x)) → 1'(opp'(x))
-'(x, y) → +'(x, opp'(y))
*'(#', x) → #'
*'(0'(x), y) → 0'(*'(x, y))
*'(1'(x), y) → +'(0'(*'(x, y)), y)
*'(j'(x), y) → -'(0'(*'(x, y)), y)
*'(*'(x, y), z) → *'(x, *'(y, z))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
0'(#') → #'
+'(#', x) → x
+'(x, #') → x
+'(0'(x), 0'(y)) → 0'(+'(x, y))
+'(0'(x), 1'(y)) → 1'(+'(x, y))
+'(1'(x), 0'(y)) → 1'(+'(x, y))
+'(0'(x), j'(y)) → j'(+'(x, y))
+'(j'(x), 0'(y)) → j'(+'(x, y))
+'(1'(x), 1'(y)) → j'(+'(+'(x, y), 1'(#')))
+'(j'(x), j'(y)) → 1'(+'(+'(x, y), j'(#')))
+'(1'(x), j'(y)) → 0'(+'(x, y))
+'(j'(x), 1'(y)) → 0'(+'(x, y))
+'(+'(x, y), z) → +'(x, +'(y, z))
opp'(#') → #'
opp'(0'(x)) → 0'(opp'(x))
opp'(1'(x)) → j'(opp'(x))
opp'(j'(x)) → 1'(opp'(x))
-'(x, y) → +'(x, opp'(y))
*'(#', x) → #'
*'(0'(x), y) → 0'(*'(x, y))
*'(1'(x), y) → +'(0'(*'(x, y)), y)
*'(j'(x), y) → -'(0'(*'(x, y)), y)
*'(*'(x, y), z) → *'(x, *'(y, z))

Types:
0' :: #':1':j' → #':1':j'
#' :: #':1':j'
+' :: #':1':j' → #':1':j' → #':1':j'
1' :: #':1':j' → #':1':j'
j' :: #':1':j' → #':1':j'
opp' :: #':1':j' → #':1':j'
-' :: #':1':j' → #':1':j' → #':1':j'
*' :: #':1':j' → #':1':j' → #':1':j'
_hole_#':1':j'1 :: #':1':j'
_gen_#':1':j'2 :: Nat → #':1':j'

Heuristically decided to analyse the following defined symbols:
+', opp', *'

They will be analysed ascendingly in the following order:
+' < *'

Rules:
0'(#') → #'
+'(#', x) → x
+'(x, #') → x
+'(0'(x), 0'(y)) → 0'(+'(x, y))
+'(0'(x), 1'(y)) → 1'(+'(x, y))
+'(1'(x), 0'(y)) → 1'(+'(x, y))
+'(0'(x), j'(y)) → j'(+'(x, y))
+'(j'(x), 0'(y)) → j'(+'(x, y))
+'(1'(x), 1'(y)) → j'(+'(+'(x, y), 1'(#')))
+'(j'(x), j'(y)) → 1'(+'(+'(x, y), j'(#')))
+'(1'(x), j'(y)) → 0'(+'(x, y))
+'(j'(x), 1'(y)) → 0'(+'(x, y))
+'(+'(x, y), z) → +'(x, +'(y, z))
opp'(#') → #'
opp'(0'(x)) → 0'(opp'(x))
opp'(1'(x)) → j'(opp'(x))
opp'(j'(x)) → 1'(opp'(x))
-'(x, y) → +'(x, opp'(y))
*'(#', x) → #'
*'(0'(x), y) → 0'(*'(x, y))
*'(1'(x), y) → +'(0'(*'(x, y)), y)
*'(j'(x), y) → -'(0'(*'(x, y)), y)
*'(*'(x, y), z) → *'(x, *'(y, z))

Types:
0' :: #':1':j' → #':1':j'
#' :: #':1':j'
+' :: #':1':j' → #':1':j' → #':1':j'
1' :: #':1':j' → #':1':j'
j' :: #':1':j' → #':1':j'
opp' :: #':1':j' → #':1':j'
-' :: #':1':j' → #':1':j' → #':1':j'
*' :: #':1':j' → #':1':j' → #':1':j'
_hole_#':1':j'1 :: #':1':j'
_gen_#':1':j'2 :: Nat → #':1':j'

Generator Equations:
_gen_#':1':j'2(0) ⇔ #'
_gen_#':1':j'2(+(x, 1)) ⇔ 1'(_gen_#':1':j'2(x))

The following defined symbols remain to be analysed:
+', opp', *'

They will be analysed ascendingly in the following order:
+' < *'

Proved the following rewrite lemma:
+'(_gen_#':1':j'2(+(1, _n4)), _gen_#':1':j'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)

Induction Base:
+'(_gen_#':1':j'2(+(1, 0)), _gen_#':1':j'2(+(1, 0)))

Induction Step:
+'(_gen_#':1':j'2(+(1, +(_\$n5, 1))), _gen_#':1':j'2(+(1, +(_\$n5, 1)))) →RΩ(1)
j'(+'(+'(_gen_#':1':j'2(+(1, _\$n5)), _gen_#':1':j'2(+(1, _\$n5))), 1'(#'))) →IH
j'(+'(_*3, 1'(#')))

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

Rules:
0'(#') → #'
+'(#', x) → x
+'(x, #') → x
+'(0'(x), 0'(y)) → 0'(+'(x, y))
+'(0'(x), 1'(y)) → 1'(+'(x, y))
+'(1'(x), 0'(y)) → 1'(+'(x, y))
+'(0'(x), j'(y)) → j'(+'(x, y))
+'(j'(x), 0'(y)) → j'(+'(x, y))
+'(1'(x), 1'(y)) → j'(+'(+'(x, y), 1'(#')))
+'(j'(x), j'(y)) → 1'(+'(+'(x, y), j'(#')))
+'(1'(x), j'(y)) → 0'(+'(x, y))
+'(j'(x), 1'(y)) → 0'(+'(x, y))
+'(+'(x, y), z) → +'(x, +'(y, z))
opp'(#') → #'
opp'(0'(x)) → 0'(opp'(x))
opp'(1'(x)) → j'(opp'(x))
opp'(j'(x)) → 1'(opp'(x))
-'(x, y) → +'(x, opp'(y))
*'(#', x) → #'
*'(0'(x), y) → 0'(*'(x, y))
*'(1'(x), y) → +'(0'(*'(x, y)), y)
*'(j'(x), y) → -'(0'(*'(x, y)), y)
*'(*'(x, y), z) → *'(x, *'(y, z))

Types:
0' :: #':1':j' → #':1':j'
#' :: #':1':j'
+' :: #':1':j' → #':1':j' → #':1':j'
1' :: #':1':j' → #':1':j'
j' :: #':1':j' → #':1':j'
opp' :: #':1':j' → #':1':j'
-' :: #':1':j' → #':1':j' → #':1':j'
*' :: #':1':j' → #':1':j' → #':1':j'
_hole_#':1':j'1 :: #':1':j'
_gen_#':1':j'2 :: Nat → #':1':j'

Lemmas:
+'(_gen_#':1':j'2(+(1, _n4)), _gen_#':1':j'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)

Generator Equations:
_gen_#':1':j'2(0) ⇔ #'
_gen_#':1':j'2(+(x, 1)) ⇔ 1'(_gen_#':1':j'2(x))

The following defined symbols remain to be analysed:
opp', *'

Proved the following rewrite lemma:
opp'(_gen_#':1':j'2(+(1, _n4134615))) → _*3, rt ∈ Ω(n4134615)

Induction Base:
opp'(_gen_#':1':j'2(+(1, 0)))

Induction Step:
opp'(_gen_#':1':j'2(+(1, +(_\$n4134616, 1)))) →RΩ(1)
j'(opp'(_gen_#':1':j'2(+(1, _\$n4134616)))) →IH
j'(_*3)

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

Rules:
0'(#') → #'
+'(#', x) → x
+'(x, #') → x
+'(0'(x), 0'(y)) → 0'(+'(x, y))
+'(0'(x), 1'(y)) → 1'(+'(x, y))
+'(1'(x), 0'(y)) → 1'(+'(x, y))
+'(0'(x), j'(y)) → j'(+'(x, y))
+'(j'(x), 0'(y)) → j'(+'(x, y))
+'(1'(x), 1'(y)) → j'(+'(+'(x, y), 1'(#')))
+'(j'(x), j'(y)) → 1'(+'(+'(x, y), j'(#')))
+'(1'(x), j'(y)) → 0'(+'(x, y))
+'(j'(x), 1'(y)) → 0'(+'(x, y))
+'(+'(x, y), z) → +'(x, +'(y, z))
opp'(#') → #'
opp'(0'(x)) → 0'(opp'(x))
opp'(1'(x)) → j'(opp'(x))
opp'(j'(x)) → 1'(opp'(x))
-'(x, y) → +'(x, opp'(y))
*'(#', x) → #'
*'(0'(x), y) → 0'(*'(x, y))
*'(1'(x), y) → +'(0'(*'(x, y)), y)
*'(j'(x), y) → -'(0'(*'(x, y)), y)
*'(*'(x, y), z) → *'(x, *'(y, z))

Types:
0' :: #':1':j' → #':1':j'
#' :: #':1':j'
+' :: #':1':j' → #':1':j' → #':1':j'
1' :: #':1':j' → #':1':j'
j' :: #':1':j' → #':1':j'
opp' :: #':1':j' → #':1':j'
-' :: #':1':j' → #':1':j' → #':1':j'
*' :: #':1':j' → #':1':j' → #':1':j'
_hole_#':1':j'1 :: #':1':j'
_gen_#':1':j'2 :: Nat → #':1':j'

Lemmas:
+'(_gen_#':1':j'2(+(1, _n4)), _gen_#':1':j'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
opp'(_gen_#':1':j'2(+(1, _n4134615))) → _*3, rt ∈ Ω(n4134615)

Generator Equations:
_gen_#':1':j'2(0) ⇔ #'
_gen_#':1':j'2(+(x, 1)) ⇔ 1'(_gen_#':1':j'2(x))

The following defined symbols remain to be analysed:
*'

Proved the following rewrite lemma:
*'(_gen_#':1':j'2(_n4136338), _gen_#':1':j'2(0)) → _gen_#':1':j'2(0), rt ∈ Ω(1 + n4136338)

Induction Base:
*'(_gen_#':1':j'2(0), _gen_#':1':j'2(0)) →RΩ(1)
#'

Induction Step:
*'(_gen_#':1':j'2(+(_\$n4136339, 1)), _gen_#':1':j'2(0)) →RΩ(1)
+'(0'(*'(_gen_#':1':j'2(_\$n4136339), _gen_#':1':j'2(0))), _gen_#':1':j'2(0)) →IH
+'(0'(_gen_#':1':j'2(0)), _gen_#':1':j'2(0)) →RΩ(1)
+'(#', _gen_#':1':j'2(0)) →RΩ(1)
_gen_#':1':j'2(0)

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

Rules:
0'(#') → #'
+'(#', x) → x
+'(x, #') → x
+'(0'(x), 0'(y)) → 0'(+'(x, y))
+'(0'(x), 1'(y)) → 1'(+'(x, y))
+'(1'(x), 0'(y)) → 1'(+'(x, y))
+'(0'(x), j'(y)) → j'(+'(x, y))
+'(j'(x), 0'(y)) → j'(+'(x, y))
+'(1'(x), 1'(y)) → j'(+'(+'(x, y), 1'(#')))
+'(j'(x), j'(y)) → 1'(+'(+'(x, y), j'(#')))
+'(1'(x), j'(y)) → 0'(+'(x, y))
+'(j'(x), 1'(y)) → 0'(+'(x, y))
+'(+'(x, y), z) → +'(x, +'(y, z))
opp'(#') → #'
opp'(0'(x)) → 0'(opp'(x))
opp'(1'(x)) → j'(opp'(x))
opp'(j'(x)) → 1'(opp'(x))
-'(x, y) → +'(x, opp'(y))
*'(#', x) → #'
*'(0'(x), y) → 0'(*'(x, y))
*'(1'(x), y) → +'(0'(*'(x, y)), y)
*'(j'(x), y) → -'(0'(*'(x, y)), y)
*'(*'(x, y), z) → *'(x, *'(y, z))

Types:
0' :: #':1':j' → #':1':j'
#' :: #':1':j'
+' :: #':1':j' → #':1':j' → #':1':j'
1' :: #':1':j' → #':1':j'
j' :: #':1':j' → #':1':j'
opp' :: #':1':j' → #':1':j'
-' :: #':1':j' → #':1':j' → #':1':j'
*' :: #':1':j' → #':1':j' → #':1':j'
_hole_#':1':j'1 :: #':1':j'
_gen_#':1':j'2 :: Nat → #':1':j'

Lemmas:
+'(_gen_#':1':j'2(+(1, _n4)), _gen_#':1':j'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
opp'(_gen_#':1':j'2(+(1, _n4134615))) → _*3, rt ∈ Ω(n4134615)
*'(_gen_#':1':j'2(_n4136338), _gen_#':1':j'2(0)) → _gen_#':1':j'2(0), rt ∈ Ω(1 + n4136338)

Generator Equations:
_gen_#':1':j'2(0) ⇔ #'
_gen_#':1':j'2(+(x, 1)) ⇔ 1'(_gen_#':1':j'2(x))

No more defined symbols left to analyse.

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