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