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

eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
or(true, y) → true
or(false, y) → y
union(empty, h) → h
union(edge(x, y, i), h) → edge(x, y, union(i, h))
reach(x, y, empty, h) → false
reach(x, y, edge(u, v, i), h) → if_reach_1(eq(x, u), x, y, edge(u, v, i), h)
if_reach_1(true, x, y, edge(u, v, i), h) → if_reach_2(eq(y, v), x, y, edge(u, v, i), h)
if_reach_2(true, x, y, edge(u, v, i), h) → true
if_reach_2(false, x, y, edge(u, v, i), h) → or(reach(x, y, i, h), reach(v, y, union(i, h), empty))
if_reach_1(false, x, y, edge(u, v, i), h) → reach(x, y, i, edge(u, v, h))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

eq'(0', 0') → true'
eq'(0', s'(x)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
or'(true', y) → true'
or'(false', y) → y
union'(empty', h) → h
union'(edge'(x, y, i), h) → edge'(x, y, union'(i, h))
reach'(x, y, empty', h) → false'
reach'(x, y, edge'(u, v, i), h) → if_reach_1'(eq'(x, u), x, y, edge'(u, v, i), h)
if_reach_1'(true', x, y, edge'(u, v, i), h) → if_reach_2'(eq'(y, v), x, y, edge'(u, v, i), h)
if_reach_2'(true', x, y, edge'(u, v, i), h) → true'
if_reach_2'(false', x, y, edge'(u, v, i), h) → or'(reach'(x, y, i, h), reach'(v, y, union'(i, h), empty'))
if_reach_1'(false', x, y, edge'(u, v, i), h) → reach'(x, y, i, edge'(u, v, h))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
eq'(0', 0') → true'
eq'(0', s'(x)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
or'(true', y) → true'
or'(false', y) → y
union'(empty', h) → h
union'(edge'(x, y, i), h) → edge'(x, y, union'(i, h))
reach'(x, y, empty', h) → false'
reach'(x, y, edge'(u, v, i), h) → if_reach_1'(eq'(x, u), x, y, edge'(u, v, i), h)
if_reach_1'(true', x, y, edge'(u, v, i), h) → if_reach_2'(eq'(y, v), x, y, edge'(u, v, i), h)
if_reach_2'(true', x, y, edge'(u, v, i), h) → true'
if_reach_2'(false', x, y, edge'(u, v, i), h) → or'(reach'(x, y, i, h), reach'(v, y, union'(i, h), empty'))
if_reach_1'(false', x, y, edge'(u, v, i), h) → reach'(x, y, i, edge'(u, v, h))

Types:
eq' :: 0':s' → 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
or' :: true':false' → true':false' → true':false'
union' :: empty':edge' → empty':edge' → empty':edge'
empty' :: empty':edge'
edge' :: 0':s' → 0':s' → empty':edge' → empty':edge'
reach' :: 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if_reach_1' :: true':false' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if_reach_2' :: true':false' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
_hole_true':false'1 :: true':false'
_hole_0':s'2 :: 0':s'
_hole_empty':edge'3 :: empty':edge'
_gen_0':s'4 :: Nat → 0':s'
_gen_empty':edge'5 :: Nat → empty':edge'

Heuristically decided to analyse the following defined symbols:
eq', union', reach'

They will be analysed ascendingly in the following order:
eq' < reach'
union' < reach'

Rules:
eq'(0', 0') → true'
eq'(0', s'(x)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
or'(true', y) → true'
or'(false', y) → y
union'(empty', h) → h
union'(edge'(x, y, i), h) → edge'(x, y, union'(i, h))
reach'(x, y, empty', h) → false'
reach'(x, y, edge'(u, v, i), h) → if_reach_1'(eq'(x, u), x, y, edge'(u, v, i), h)
if_reach_1'(true', x, y, edge'(u, v, i), h) → if_reach_2'(eq'(y, v), x, y, edge'(u, v, i), h)
if_reach_2'(true', x, y, edge'(u, v, i), h) → true'
if_reach_2'(false', x, y, edge'(u, v, i), h) → or'(reach'(x, y, i, h), reach'(v, y, union'(i, h), empty'))
if_reach_1'(false', x, y, edge'(u, v, i), h) → reach'(x, y, i, edge'(u, v, h))

Types:
eq' :: 0':s' → 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
or' :: true':false' → true':false' → true':false'
union' :: empty':edge' → empty':edge' → empty':edge'
empty' :: empty':edge'
edge' :: 0':s' → 0':s' → empty':edge' → empty':edge'
reach' :: 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if_reach_1' :: true':false' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if_reach_2' :: true':false' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
_hole_true':false'1 :: true':false'
_hole_0':s'2 :: 0':s'
_hole_empty':edge'3 :: empty':edge'
_gen_0':s'4 :: Nat → 0':s'
_gen_empty':edge'5 :: Nat → empty':edge'

Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_empty':edge'5(0) ⇔ empty'
_gen_empty':edge'5(+(x, 1)) ⇔ edge'(0', 0', _gen_empty':edge'5(x))

The following defined symbols remain to be analysed:
eq', union', reach'

They will be analysed ascendingly in the following order:
eq' < reach'
union' < reach'

Proved the following rewrite lemma:
eq'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → true', rt ∈ Ω(1 + n7)

Induction Base:
eq'(_gen_0':s'4(0), _gen_0':s'4(0)) →RΩ(1)
true'

Induction Step:
eq'(_gen_0':s'4(+(_\$n8, 1)), _gen_0':s'4(+(_\$n8, 1))) →RΩ(1)
eq'(_gen_0':s'4(_\$n8), _gen_0':s'4(_\$n8)) →IH
true'

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

Rules:
eq'(0', 0') → true'
eq'(0', s'(x)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
or'(true', y) → true'
or'(false', y) → y
union'(empty', h) → h
union'(edge'(x, y, i), h) → edge'(x, y, union'(i, h))
reach'(x, y, empty', h) → false'
reach'(x, y, edge'(u, v, i), h) → if_reach_1'(eq'(x, u), x, y, edge'(u, v, i), h)
if_reach_1'(true', x, y, edge'(u, v, i), h) → if_reach_2'(eq'(y, v), x, y, edge'(u, v, i), h)
if_reach_2'(true', x, y, edge'(u, v, i), h) → true'
if_reach_2'(false', x, y, edge'(u, v, i), h) → or'(reach'(x, y, i, h), reach'(v, y, union'(i, h), empty'))
if_reach_1'(false', x, y, edge'(u, v, i), h) → reach'(x, y, i, edge'(u, v, h))

Types:
eq' :: 0':s' → 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
or' :: true':false' → true':false' → true':false'
union' :: empty':edge' → empty':edge' → empty':edge'
empty' :: empty':edge'
edge' :: 0':s' → 0':s' → empty':edge' → empty':edge'
reach' :: 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if_reach_1' :: true':false' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if_reach_2' :: true':false' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
_hole_true':false'1 :: true':false'
_hole_0':s'2 :: 0':s'
_hole_empty':edge'3 :: empty':edge'
_gen_0':s'4 :: Nat → 0':s'
_gen_empty':edge'5 :: Nat → empty':edge'

Lemmas:
eq'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → true', rt ∈ Ω(1 + n7)

Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_empty':edge'5(0) ⇔ empty'
_gen_empty':edge'5(+(x, 1)) ⇔ edge'(0', 0', _gen_empty':edge'5(x))

The following defined symbols remain to be analysed:
union', reach'

They will be analysed ascendingly in the following order:
union' < reach'

Proved the following rewrite lemma:
union'(_gen_empty':edge'5(_n1239), _gen_empty':edge'5(b)) → _gen_empty':edge'5(+(_n1239, b)), rt ∈ Ω(1 + n1239)

Induction Base:
union'(_gen_empty':edge'5(0), _gen_empty':edge'5(b)) →RΩ(1)
_gen_empty':edge'5(b)

Induction Step:
union'(_gen_empty':edge'5(+(_\$n1240, 1)), _gen_empty':edge'5(_b1478)) →RΩ(1)
edge'(0', 0', union'(_gen_empty':edge'5(_\$n1240), _gen_empty':edge'5(_b1478))) →IH
edge'(0', 0', _gen_empty':edge'5(+(_\$n1240, _b1478)))

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

Rules:
eq'(0', 0') → true'
eq'(0', s'(x)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
or'(true', y) → true'
or'(false', y) → y
union'(empty', h) → h
union'(edge'(x, y, i), h) → edge'(x, y, union'(i, h))
reach'(x, y, empty', h) → false'
reach'(x, y, edge'(u, v, i), h) → if_reach_1'(eq'(x, u), x, y, edge'(u, v, i), h)
if_reach_1'(true', x, y, edge'(u, v, i), h) → if_reach_2'(eq'(y, v), x, y, edge'(u, v, i), h)
if_reach_2'(true', x, y, edge'(u, v, i), h) → true'
if_reach_2'(false', x, y, edge'(u, v, i), h) → or'(reach'(x, y, i, h), reach'(v, y, union'(i, h), empty'))
if_reach_1'(false', x, y, edge'(u, v, i), h) → reach'(x, y, i, edge'(u, v, h))

Types:
eq' :: 0':s' → 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
or' :: true':false' → true':false' → true':false'
union' :: empty':edge' → empty':edge' → empty':edge'
empty' :: empty':edge'
edge' :: 0':s' → 0':s' → empty':edge' → empty':edge'
reach' :: 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if_reach_1' :: true':false' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if_reach_2' :: true':false' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
_hole_true':false'1 :: true':false'
_hole_0':s'2 :: 0':s'
_hole_empty':edge'3 :: empty':edge'
_gen_0':s'4 :: Nat → 0':s'
_gen_empty':edge'5 :: Nat → empty':edge'

Lemmas:
eq'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → true', rt ∈ Ω(1 + n7)
union'(_gen_empty':edge'5(_n1239), _gen_empty':edge'5(b)) → _gen_empty':edge'5(+(_n1239, b)), rt ∈ Ω(1 + n1239)

Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_empty':edge'5(0) ⇔ empty'
_gen_empty':edge'5(+(x, 1)) ⇔ edge'(0', 0', _gen_empty':edge'5(x))

The following defined symbols remain to be analysed:
reach'

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

Rules:
eq'(0', 0') → true'
eq'(0', s'(x)) → false'
eq'(s'(x), 0') → false'
eq'(s'(x), s'(y)) → eq'(x, y)
or'(true', y) → true'
or'(false', y) → y
union'(empty', h) → h
union'(edge'(x, y, i), h) → edge'(x, y, union'(i, h))
reach'(x, y, empty', h) → false'
reach'(x, y, edge'(u, v, i), h) → if_reach_1'(eq'(x, u), x, y, edge'(u, v, i), h)
if_reach_1'(true', x, y, edge'(u, v, i), h) → if_reach_2'(eq'(y, v), x, y, edge'(u, v, i), h)
if_reach_2'(true', x, y, edge'(u, v, i), h) → true'
if_reach_2'(false', x, y, edge'(u, v, i), h) → or'(reach'(x, y, i, h), reach'(v, y, union'(i, h), empty'))
if_reach_1'(false', x, y, edge'(u, v, i), h) → reach'(x, y, i, edge'(u, v, h))

Types:
eq' :: 0':s' → 0':s' → true':false'
0' :: 0':s'
true' :: true':false'
s' :: 0':s' → 0':s'
false' :: true':false'
or' :: true':false' → true':false' → true':false'
union' :: empty':edge' → empty':edge' → empty':edge'
empty' :: empty':edge'
edge' :: 0':s' → 0':s' → empty':edge' → empty':edge'
reach' :: 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if_reach_1' :: true':false' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if_reach_2' :: true':false' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
_hole_true':false'1 :: true':false'
_hole_0':s'2 :: 0':s'
_hole_empty':edge'3 :: empty':edge'
_gen_0':s'4 :: Nat → 0':s'
_gen_empty':edge'5 :: Nat → empty':edge'

Lemmas:
eq'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → true', rt ∈ Ω(1 + n7)
union'(_gen_empty':edge'5(_n1239), _gen_empty':edge'5(b)) → _gen_empty':edge'5(+(_n1239, b)), rt ∈ Ω(1 + n1239)

Generator Equations:
_gen_0':s'4(0) ⇔ 0'
_gen_0':s'4(+(x, 1)) ⇔ s'(_gen_0':s'4(x))
_gen_empty':edge'5(0) ⇔ empty'
_gen_empty':edge'5(+(x, 1)) ⇔ edge'(0', 0', _gen_empty':edge'5(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
eq'(_gen_0':s'4(_n7), _gen_0':s'4(_n7)) → true', rt ∈ Ω(1 + n7)