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)))
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)))
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)