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
and(true, y) → y
and(false, y) → false
size(empty) → 0
size(edge(x, y, i)) → s(size(i))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
reachable(x, y, i) → reach(x, y, 0, i, i)
reach(x, y, c, i, j) → if1(eq(x, y), x, y, c, i, j)
if1(true, x, y, c, i, j) → true
if1(false, x, y, c, i, j) → if2(le(c, size(j)), x, y, c, i, j)
if2(false, x, y, c, i, j) → false
if2(true, x, y, c, empty, j) → false
if2(true, x, y, c, edge(u, v, i), j) → or(if2(true, x, y, c, i, j), and(eq(x, u), reach(v, y, s(c), j, j)))

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
and'(true', y) → y
and'(false', y) → false'
size'(empty') → 0'
size'(edge'(x, y, i)) → s'(size'(i))
le'(0', y) → true'
le'(s'(x), 0') → false'
le'(s'(x), s'(y)) → le'(x, y)
reachable'(x, y, i) → reach'(x, y, 0', i, i)
reach'(x, y, c, i, j) → if1'(eq'(x, y), x, y, c, i, j)
if1'(true', x, y, c, i, j) → true'
if1'(false', x, y, c, i, j) → if2'(le'(c, size'(j)), x, y, c, i, j)
if2'(false', x, y, c, i, j) → false'
if2'(true', x, y, c, empty', j) → false'
if2'(true', x, y, c, edge'(u, v, i), j) → or'(if2'(true', x, y, c, i, j), and'(eq'(x, u), reach'(v, y, s'(c), j, j)))

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
and'(true', y) → y
and'(false', y) → false'
size'(empty') → 0'
size'(edge'(x, y, i)) → s'(size'(i))
le'(0', y) → true'
le'(s'(x), 0') → false'
le'(s'(x), s'(y)) → le'(x, y)
reachable'(x, y, i) → reach'(x, y, 0', i, i)
reach'(x, y, c, i, j) → if1'(eq'(x, y), x, y, c, i, j)
if1'(true', x, y, c, i, j) → true'
if1'(false', x, y, c, i, j) → if2'(le'(c, size'(j)), x, y, c, i, j)
if2'(false', x, y, c, i, j) → false'
if2'(true', x, y, c, empty', j) → false'
if2'(true', x, y, c, edge'(u, v, i), j) → or'(if2'(true', x, y, c, i, j), and'(eq'(x, u), reach'(v, y, s'(c), j, j)))

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'
and' :: true':false' → true':false' → true':false'
size' :: empty':edge' → 0':s'
empty' :: empty':edge'
edge' :: 0':s' → 0':s' → empty':edge' → empty':edge'
le' :: 0':s' → 0':s' → true':false'
reachable' :: 0':s' → 0':s' → empty':edge' → true':false'
reach' :: 0':s' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if1' :: true':false' → 0':s' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if2' :: true':false' → 0':s' → 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', size', le', reach', if2'

They will be analysed ascendingly in the following order:
eq' < reach'
eq' < if2'
size' < reach'
le' < reach'
reach' = if2'

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
and'(true', y) → y
and'(false', y) → false'
size'(empty') → 0'
size'(edge'(x, y, i)) → s'(size'(i))
le'(0', y) → true'
le'(s'(x), 0') → false'
le'(s'(x), s'(y)) → le'(x, y)
reachable'(x, y, i) → reach'(x, y, 0', i, i)
reach'(x, y, c, i, j) → if1'(eq'(x, y), x, y, c, i, j)
if1'(true', x, y, c, i, j) → true'
if1'(false', x, y, c, i, j) → if2'(le'(c, size'(j)), x, y, c, i, j)
if2'(false', x, y, c, i, j) → false'
if2'(true', x, y, c, empty', j) → false'
if2'(true', x, y, c, edge'(u, v, i), j) → or'(if2'(true', x, y, c, i, j), and'(eq'(x, u), reach'(v, y, s'(c), j, j)))

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'
and' :: true':false' → true':false' → true':false'
size' :: empty':edge' → 0':s'
empty' :: empty':edge'
edge' :: 0':s' → 0':s' → empty':edge' → empty':edge'
le' :: 0':s' → 0':s' → true':false'
reachable' :: 0':s' → 0':s' → empty':edge' → true':false'
reach' :: 0':s' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if1' :: true':false' → 0':s' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if2' :: true':false' → 0':s' → 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', size', le', reach', if2'

They will be analysed ascendingly in the following order:
eq' < reach'
eq' < if2'
size' < reach'
le' < reach'
reach' = if2'

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
and'(true', y) → y
and'(false', y) → false'
size'(empty') → 0'
size'(edge'(x, y, i)) → s'(size'(i))
le'(0', y) → true'
le'(s'(x), 0') → false'
le'(s'(x), s'(y)) → le'(x, y)
reachable'(x, y, i) → reach'(x, y, 0', i, i)
reach'(x, y, c, i, j) → if1'(eq'(x, y), x, y, c, i, j)
if1'(true', x, y, c, i, j) → true'
if1'(false', x, y, c, i, j) → if2'(le'(c, size'(j)), x, y, c, i, j)
if2'(false', x, y, c, i, j) → false'
if2'(true', x, y, c, empty', j) → false'
if2'(true', x, y, c, edge'(u, v, i), j) → or'(if2'(true', x, y, c, i, j), and'(eq'(x, u), reach'(v, y, s'(c), j, j)))

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'
and' :: true':false' → true':false' → true':false'
size' :: empty':edge' → 0':s'
empty' :: empty':edge'
edge' :: 0':s' → 0':s' → empty':edge' → empty':edge'
le' :: 0':s' → 0':s' → true':false'
reachable' :: 0':s' → 0':s' → empty':edge' → true':false'
reach' :: 0':s' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if1' :: true':false' → 0':s' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if2' :: true':false' → 0':s' → 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:
size', le', reach', if2'

They will be analysed ascendingly in the following order:
size' < reach'
le' < reach'
reach' = if2'

Proved the following rewrite lemma:
size'(_gen_empty':edge'5(_n1392)) → _gen_0':s'4(_n1392), rt ∈ Ω(1 + n1392)

Induction Base:
size'(_gen_empty':edge'5(0)) →RΩ(1)
0'

Induction Step:
size'(_gen_empty':edge'5(+(_\$n1393, 1))) →RΩ(1)
s'(size'(_gen_empty':edge'5(_\$n1393))) →IH
s'(_gen_0':s'4(_\$n1393))

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
and'(true', y) → y
and'(false', y) → false'
size'(empty') → 0'
size'(edge'(x, y, i)) → s'(size'(i))
le'(0', y) → true'
le'(s'(x), 0') → false'
le'(s'(x), s'(y)) → le'(x, y)
reachable'(x, y, i) → reach'(x, y, 0', i, i)
reach'(x, y, c, i, j) → if1'(eq'(x, y), x, y, c, i, j)
if1'(true', x, y, c, i, j) → true'
if1'(false', x, y, c, i, j) → if2'(le'(c, size'(j)), x, y, c, i, j)
if2'(false', x, y, c, i, j) → false'
if2'(true', x, y, c, empty', j) → false'
if2'(true', x, y, c, edge'(u, v, i), j) → or'(if2'(true', x, y, c, i, j), and'(eq'(x, u), reach'(v, y, s'(c), j, j)))

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'
and' :: true':false' → true':false' → true':false'
size' :: empty':edge' → 0':s'
empty' :: empty':edge'
edge' :: 0':s' → 0':s' → empty':edge' → empty':edge'
le' :: 0':s' → 0':s' → true':false'
reachable' :: 0':s' → 0':s' → empty':edge' → true':false'
reach' :: 0':s' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if1' :: true':false' → 0':s' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if2' :: true':false' → 0':s' → 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)
size'(_gen_empty':edge'5(_n1392)) → _gen_0':s'4(_n1392), rt ∈ Ω(1 + n1392)

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:
le', reach', if2'

They will be analysed ascendingly in the following order:
le' < reach'
reach' = if2'

Proved the following rewrite lemma:
le'(_gen_0':s'4(_n2331), _gen_0':s'4(_n2331)) → true', rt ∈ Ω(1 + n2331)

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

Induction Step:
le'(_gen_0':s'4(+(_\$n2332, 1)), _gen_0':s'4(+(_\$n2332, 1))) →RΩ(1)
le'(_gen_0':s'4(_\$n2332), _gen_0':s'4(_\$n2332)) →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
and'(true', y) → y
and'(false', y) → false'
size'(empty') → 0'
size'(edge'(x, y, i)) → s'(size'(i))
le'(0', y) → true'
le'(s'(x), 0') → false'
le'(s'(x), s'(y)) → le'(x, y)
reachable'(x, y, i) → reach'(x, y, 0', i, i)
reach'(x, y, c, i, j) → if1'(eq'(x, y), x, y, c, i, j)
if1'(true', x, y, c, i, j) → true'
if1'(false', x, y, c, i, j) → if2'(le'(c, size'(j)), x, y, c, i, j)
if2'(false', x, y, c, i, j) → false'
if2'(true', x, y, c, empty', j) → false'
if2'(true', x, y, c, edge'(u, v, i), j) → or'(if2'(true', x, y, c, i, j), and'(eq'(x, u), reach'(v, y, s'(c), j, j)))

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'
and' :: true':false' → true':false' → true':false'
size' :: empty':edge' → 0':s'
empty' :: empty':edge'
edge' :: 0':s' → 0':s' → empty':edge' → empty':edge'
le' :: 0':s' → 0':s' → true':false'
reachable' :: 0':s' → 0':s' → empty':edge' → true':false'
reach' :: 0':s' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if1' :: true':false' → 0':s' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if2' :: true':false' → 0':s' → 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)
size'(_gen_empty':edge'5(_n1392)) → _gen_0':s'4(_n1392), rt ∈ Ω(1 + n1392)
le'(_gen_0':s'4(_n2331), _gen_0':s'4(_n2331)) → true', rt ∈ Ω(1 + n2331)

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:
if2', reach'

They will be analysed ascendingly in the following order:
reach' = if2'

Proved the following rewrite lemma:
if2'(true', _gen_0':s'4(0), _gen_0':s'4(0), _gen_0':s'4(c), _gen_empty':edge'5(_n3661), _gen_empty':edge'5(e)) → _*6, rt ∈ Ω(n3661)

Induction Base:
if2'(true', _gen_0':s'4(0), _gen_0':s'4(0), _gen_0':s'4(c), _gen_empty':edge'5(0), _gen_empty':edge'5(e))

Induction Step:
if2'(true', _gen_0':s'4(0), _gen_0':s'4(0), _gen_0':s'4(_c19052), _gen_empty':edge'5(+(_\$n3662, 1)), _gen_empty':edge'5(_e19053)) →RΩ(1)
or'(if2'(true', _gen_0':s'4(0), _gen_0':s'4(0), _gen_0':s'4(_c19052), _gen_empty':edge'5(_\$n3662), _gen_empty':edge'5(_e19053)), and'(eq'(_gen_0':s'4(0), 0'), reach'(0', _gen_0':s'4(0), s'(_gen_0':s'4(_c19052)), _gen_empty':edge'5(_e19053), _gen_empty':edge'5(_e19053)))) →IH
or'(_*6, and'(eq'(_gen_0':s'4(0), 0'), reach'(0', _gen_0':s'4(0), s'(_gen_0':s'4(_c19052)), _gen_empty':edge'5(_e19053), _gen_empty':edge'5(_e19053)))) →LΩ(1)
or'(_*6, and'(true', reach'(0', _gen_0':s'4(0), s'(_gen_0':s'4(_c19052)), _gen_empty':edge'5(_e19053), _gen_empty':edge'5(_e19053)))) →RΩ(1)
or'(_*6, and'(true', if1'(eq'(0', _gen_0':s'4(0)), 0', _gen_0':s'4(0), s'(_gen_0':s'4(_c19052)), _gen_empty':edge'5(_e19053), _gen_empty':edge'5(_e19053)))) →LΩ(1)
or'(_*6, and'(true', if1'(true', 0', _gen_0':s'4(0), s'(_gen_0':s'4(_c19052)), _gen_empty':edge'5(_e19053), _gen_empty':edge'5(_e19053)))) →RΩ(1)
or'(_*6, and'(true', true')) →RΩ(1)
or'(_*6, 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
and'(true', y) → y
and'(false', y) → false'
size'(empty') → 0'
size'(edge'(x, y, i)) → s'(size'(i))
le'(0', y) → true'
le'(s'(x), 0') → false'
le'(s'(x), s'(y)) → le'(x, y)
reachable'(x, y, i) → reach'(x, y, 0', i, i)
reach'(x, y, c, i, j) → if1'(eq'(x, y), x, y, c, i, j)
if1'(true', x, y, c, i, j) → true'
if1'(false', x, y, c, i, j) → if2'(le'(c, size'(j)), x, y, c, i, j)
if2'(false', x, y, c, i, j) → false'
if2'(true', x, y, c, empty', j) → false'
if2'(true', x, y, c, edge'(u, v, i), j) → or'(if2'(true', x, y, c, i, j), and'(eq'(x, u), reach'(v, y, s'(c), j, j)))

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'
and' :: true':false' → true':false' → true':false'
size' :: empty':edge' → 0':s'
empty' :: empty':edge'
edge' :: 0':s' → 0':s' → empty':edge' → empty':edge'
le' :: 0':s' → 0':s' → true':false'
reachable' :: 0':s' → 0':s' → empty':edge' → true':false'
reach' :: 0':s' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if1' :: true':false' → 0':s' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if2' :: true':false' → 0':s' → 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)
size'(_gen_empty':edge'5(_n1392)) → _gen_0':s'4(_n1392), rt ∈ Ω(1 + n1392)
le'(_gen_0':s'4(_n2331), _gen_0':s'4(_n2331)) → true', rt ∈ Ω(1 + n2331)
if2'(true', _gen_0':s'4(0), _gen_0':s'4(0), _gen_0':s'4(c), _gen_empty':edge'5(_n3661), _gen_empty':edge'5(e)) → _*6, rt ∈ Ω(n3661)

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'

They will be analysed ascendingly in the following order:
reach' = if2'

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
and'(true', y) → y
and'(false', y) → false'
size'(empty') → 0'
size'(edge'(x, y, i)) → s'(size'(i))
le'(0', y) → true'
le'(s'(x), 0') → false'
le'(s'(x), s'(y)) → le'(x, y)
reachable'(x, y, i) → reach'(x, y, 0', i, i)
reach'(x, y, c, i, j) → if1'(eq'(x, y), x, y, c, i, j)
if1'(true', x, y, c, i, j) → true'
if1'(false', x, y, c, i, j) → if2'(le'(c, size'(j)), x, y, c, i, j)
if2'(false', x, y, c, i, j) → false'
if2'(true', x, y, c, empty', j) → false'
if2'(true', x, y, c, edge'(u, v, i), j) → or'(if2'(true', x, y, c, i, j), and'(eq'(x, u), reach'(v, y, s'(c), j, j)))

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'
and' :: true':false' → true':false' → true':false'
size' :: empty':edge' → 0':s'
empty' :: empty':edge'
edge' :: 0':s' → 0':s' → empty':edge' → empty':edge'
le' :: 0':s' → 0':s' → true':false'
reachable' :: 0':s' → 0':s' → empty':edge' → true':false'
reach' :: 0':s' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if1' :: true':false' → 0':s' → 0':s' → 0':s' → empty':edge' → empty':edge' → true':false'
if2' :: true':false' → 0':s' → 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)
size'(_gen_empty':edge'5(_n1392)) → _gen_0':s'4(_n1392), rt ∈ Ω(1 + n1392)
le'(_gen_0':s'4(_n2331), _gen_0':s'4(_n2331)) → true', rt ∈ Ω(1 + n2331)
if2'(true', _gen_0':s'4(0), _gen_0':s'4(0), _gen_0':s'4(c), _gen_empty':edge'5(_n3661), _gen_empty':edge'5(e)) → _*6, rt ∈ Ω(n3661)

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)