WORST_CASE(Omega(n^1),?)
proof of input_OFA5xe3ngI.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 61 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 39 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 425 ms]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 43 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 39 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 99 ms]
        (22) typed CpxTrs


----------------------------------------

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).


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))
   isEmpty(empty) -> true
   isEmpty(edge(x, y, i)) -> false
   from(edge(x, y, i)) -> x
   to(edge(x, y, i)) -> y
   rest(edge(x, y, i)) -> i
   rest(empty) -> empty
   reach(x, y, i, h) -> if1(eq(x, y), isEmpty(i), eq(x, from(i)), eq(y, to(i)), x, y, i, h)
   if1(true, b1, b2, b3, x, y, i, h) -> true
   if1(false, b1, b2, b3, x, y, i, h) -> if2(b1, b2, b3, x, y, i, h)
   if2(true, b2, b3, x, y, i, h) -> false
   if2(false, b2, b3, x, y, i, h) -> if3(b2, b3, x, y, i, h)
   if3(false, b3, x, y, i, h) -> reach(x, y, rest(i), edge(from(i), to(i), h))
   if3(true, b3, x, y, i, h) -> if4(b3, x, y, i, h)
   if4(true, x, y, i, h) -> true
   if4(false, x, y, i, h) -> or(reach(x, y, rest(i), h), reach(to(i), y, union(rest(i), h), empty))

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   eq(0, 0) -> true
   eq(0, s(z0)) -> false
   eq(s(z0), 0) -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   or(true, z0) -> true
   or(false, z0) -> z0
   union(empty, z0) -> z0
   union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
   isEmpty(empty) -> true
   isEmpty(edge(z0, z1, z2)) -> false
   from(edge(z0, z1, z2)) -> z0
   to(edge(z0, z1, z2)) -> z1
   rest(edge(z0, z1, z2)) -> z2
   rest(empty) -> empty
   reach(z0, z1, z2, z3) -> if1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3)
   if1(true, z0, z1, z2, z3, z4, z5, z6) -> true
   if1(false, z0, z1, z2, z3, z4, z5, z6) -> if2(z0, z1, z2, z3, z4, z5, z6)
   if2(true, z0, z1, z2, z3, z4, z5) -> false
   if2(false, z0, z1, z2, z3, z4, z5) -> if3(z0, z1, z2, z3, z4, z5)
   if3(false, z0, z1, z2, z3, z4) -> reach(z1, z2, rest(z3), edge(from(z3), to(z3), z4))
   if3(true, z0, z1, z2, z3, z4) -> if4(z0, z1, z2, z3, z4)
   if4(true, z0, z1, z2, z3) -> true
   if4(false, z0, z1, z2, z3) -> or(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty))
Tuples:
   EQ(0, 0) -> c
   EQ(0, s(z0)) -> c1
   EQ(s(z0), 0) -> c2
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   OR(true, z0) -> c4
   OR(false, z0) -> c5
   UNION(empty, z0) -> c6
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   ISEMPTY(empty) -> c8
   ISEMPTY(edge(z0, z1, z2)) -> c9
   FROM(edge(z0, z1, z2)) -> c10
   TO(edge(z0, z1, z2)) -> c11
   REST(edge(z0, z1, z2)) -> c12
   REST(empty) -> c13
   REACH(z0, z1, z2, z3) -> c14(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, z1))
   REACH(z0, z1, z2, z3) -> c15(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), ISEMPTY(z2))
   REACH(z0, z1, z2, z3) -> c16(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, from(z2)), FROM(z2))
   REACH(z0, z1, z2, z3) -> c17(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z1, to(z2)), TO(z2))
   IF1(true, z0, z1, z2, z3, z4, z5, z6) -> c18
   IF1(false, z0, z1, z2, z3, z4, z5, z6) -> c19(IF2(z0, z1, z2, z3, z4, z5, z6))
   IF2(true, z0, z1, z2, z3, z4, z5) -> c20
   IF2(false, z0, z1, z2, z3, z4, z5) -> c21(IF3(z0, z1, z2, z3, z4, z5))
   IF3(false, z0, z1, z2, z3, z4) -> c22(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), REST(z3))
   IF3(false, z0, z1, z2, z3, z4) -> c23(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), FROM(z3))
   IF3(false, z0, z1, z2, z3, z4) -> c24(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), TO(z3))
   IF3(true, z0, z1, z2, z3, z4) -> c25(IF4(z0, z1, z2, z3, z4))
   IF4(true, z0, z1, z2, z3) -> c26
   IF4(false, z0, z1, z2, z3) -> c27(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(z0, z1, rest(z2), z3), REST(z2))
   IF4(false, z0, z1, z2, z3) -> c28(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), TO(z2))
   IF4(false, z0, z1, z2, z3) -> c29(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), UNION(rest(z2), z3), REST(z2))
S tuples:
   EQ(0, 0) -> c
   EQ(0, s(z0)) -> c1
   EQ(s(z0), 0) -> c2
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   OR(true, z0) -> c4
   OR(false, z0) -> c5
   UNION(empty, z0) -> c6
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   ISEMPTY(empty) -> c8
   ISEMPTY(edge(z0, z1, z2)) -> c9
   FROM(edge(z0, z1, z2)) -> c10
   TO(edge(z0, z1, z2)) -> c11
   REST(edge(z0, z1, z2)) -> c12
   REST(empty) -> c13
   REACH(z0, z1, z2, z3) -> c14(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, z1))
   REACH(z0, z1, z2, z3) -> c15(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), ISEMPTY(z2))
   REACH(z0, z1, z2, z3) -> c16(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, from(z2)), FROM(z2))
   REACH(z0, z1, z2, z3) -> c17(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z1, to(z2)), TO(z2))
   IF1(true, z0, z1, z2, z3, z4, z5, z6) -> c18
   IF1(false, z0, z1, z2, z3, z4, z5, z6) -> c19(IF2(z0, z1, z2, z3, z4, z5, z6))
   IF2(true, z0, z1, z2, z3, z4, z5) -> c20
   IF2(false, z0, z1, z2, z3, z4, z5) -> c21(IF3(z0, z1, z2, z3, z4, z5))
   IF3(false, z0, z1, z2, z3, z4) -> c22(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), REST(z3))
   IF3(false, z0, z1, z2, z3, z4) -> c23(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), FROM(z3))
   IF3(false, z0, z1, z2, z3, z4) -> c24(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), TO(z3))
   IF3(true, z0, z1, z2, z3, z4) -> c25(IF4(z0, z1, z2, z3, z4))
   IF4(true, z0, z1, z2, z3) -> c26
   IF4(false, z0, z1, z2, z3) -> c27(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(z0, z1, rest(z2), z3), REST(z2))
   IF4(false, z0, z1, z2, z3) -> c28(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), TO(z2))
   IF4(false, z0, z1, z2, z3) -> c29(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), UNION(rest(z2), z3), REST(z2))
K tuples:none
Defined Rule Symbols:   eq_2, or_2, union_2, isEmpty_1, from_1, to_1, rest_1, reach_4, if1_8, if2_7, if3_6, if4_5

Defined Pair Symbols:   EQ_2, OR_2, UNION_2, ISEMPTY_1, FROM_1, TO_1, REST_1, REACH_4, IF1_8, IF2_7, IF3_6, IF4_5

Compound Symbols:   c, c1, c2, c3_1, c4, c5, c6, c7_1, c8, c9, c10, c11, c12, c13, c14_2, c15_2, c16_3, c17_3, c18, c19_1, c20, c21_1, c22_2, c23_2, c24_2, c25_1, c26, c27_3, c28_3, c29_4


----------------------------------------

(3) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

(4)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   EQ(0, 0) -> c
   EQ(0, s(z0)) -> c1
   EQ(s(z0), 0) -> c2
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   OR(true, z0) -> c4
   OR(false, z0) -> c5
   UNION(empty, z0) -> c6
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   ISEMPTY(empty) -> c8
   ISEMPTY(edge(z0, z1, z2)) -> c9
   FROM(edge(z0, z1, z2)) -> c10
   TO(edge(z0, z1, z2)) -> c11
   REST(edge(z0, z1, z2)) -> c12
   REST(empty) -> c13
   REACH(z0, z1, z2, z3) -> c14(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, z1))
   REACH(z0, z1, z2, z3) -> c15(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), ISEMPTY(z2))
   REACH(z0, z1, z2, z3) -> c16(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, from(z2)), FROM(z2))
   REACH(z0, z1, z2, z3) -> c17(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z1, to(z2)), TO(z2))
   IF1(true, z0, z1, z2, z3, z4, z5, z6) -> c18
   IF1(false, z0, z1, z2, z3, z4, z5, z6) -> c19(IF2(z0, z1, z2, z3, z4, z5, z6))
   IF2(true, z0, z1, z2, z3, z4, z5) -> c20
   IF2(false, z0, z1, z2, z3, z4, z5) -> c21(IF3(z0, z1, z2, z3, z4, z5))
   IF3(false, z0, z1, z2, z3, z4) -> c22(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), REST(z3))
   IF3(false, z0, z1, z2, z3, z4) -> c23(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), FROM(z3))
   IF3(false, z0, z1, z2, z3, z4) -> c24(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), TO(z3))
   IF3(true, z0, z1, z2, z3, z4) -> c25(IF4(z0, z1, z2, z3, z4))
   IF4(true, z0, z1, z2, z3) -> c26
   IF4(false, z0, z1, z2, z3) -> c27(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(z0, z1, rest(z2), z3), REST(z2))
   IF4(false, z0, z1, z2, z3) -> c28(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), TO(z2))
   IF4(false, z0, z1, z2, z3) -> c29(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), UNION(rest(z2), z3), REST(z2))

The (relative) TRS S consists of the following rules:

   eq(0, 0) -> true
   eq(0, s(z0)) -> false
   eq(s(z0), 0) -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   or(true, z0) -> true
   or(false, z0) -> z0
   union(empty, z0) -> z0
   union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
   isEmpty(empty) -> true
   isEmpty(edge(z0, z1, z2)) -> false
   from(edge(z0, z1, z2)) -> z0
   to(edge(z0, z1, z2)) -> z1
   rest(edge(z0, z1, z2)) -> z2
   rest(empty) -> empty
   reach(z0, z1, z2, z3) -> if1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3)
   if1(true, z0, z1, z2, z3, z4, z5, z6) -> true
   if1(false, z0, z1, z2, z3, z4, z5, z6) -> if2(z0, z1, z2, z3, z4, z5, z6)
   if2(true, z0, z1, z2, z3, z4, z5) -> false
   if2(false, z0, z1, z2, z3, z4, z5) -> if3(z0, z1, z2, z3, z4, z5)
   if3(false, z0, z1, z2, z3, z4) -> reach(z1, z2, rest(z3), edge(from(z3), to(z3), z4))
   if3(true, z0, z1, z2, z3, z4) -> if4(z0, z1, z2, z3, z4)
   if4(true, z0, z1, z2, z3) -> true
   if4(false, z0, z1, z2, z3) -> or(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty))

Rewrite Strategy: INNERMOST
----------------------------------------

(5) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

(6)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   EQ(0', 0') -> c
   EQ(0', s(z0)) -> c1
   EQ(s(z0), 0') -> c2
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   OR(true, z0) -> c4
   OR(false, z0) -> c5
   UNION(empty, z0) -> c6
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   ISEMPTY(empty) -> c8
   ISEMPTY(edge(z0, z1, z2)) -> c9
   FROM(edge(z0, z1, z2)) -> c10
   TO(edge(z0, z1, z2)) -> c11
   REST(edge(z0, z1, z2)) -> c12
   REST(empty) -> c13
   REACH(z0, z1, z2, z3) -> c14(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, z1))
   REACH(z0, z1, z2, z3) -> c15(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), ISEMPTY(z2))
   REACH(z0, z1, z2, z3) -> c16(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, from(z2)), FROM(z2))
   REACH(z0, z1, z2, z3) -> c17(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z1, to(z2)), TO(z2))
   IF1(true, z0, z1, z2, z3, z4, z5, z6) -> c18
   IF1(false, z0, z1, z2, z3, z4, z5, z6) -> c19(IF2(z0, z1, z2, z3, z4, z5, z6))
   IF2(true, z0, z1, z2, z3, z4, z5) -> c20
   IF2(false, z0, z1, z2, z3, z4, z5) -> c21(IF3(z0, z1, z2, z3, z4, z5))
   IF3(false, z0, z1, z2, z3, z4) -> c22(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), REST(z3))
   IF3(false, z0, z1, z2, z3, z4) -> c23(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), FROM(z3))
   IF3(false, z0, z1, z2, z3, z4) -> c24(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), TO(z3))
   IF3(true, z0, z1, z2, z3, z4) -> c25(IF4(z0, z1, z2, z3, z4))
   IF4(true, z0, z1, z2, z3) -> c26
   IF4(false, z0, z1, z2, z3) -> c27(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(z0, z1, rest(z2), z3), REST(z2))
   IF4(false, z0, z1, z2, z3) -> c28(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), TO(z2))
   IF4(false, z0, z1, z2, z3) -> c29(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), UNION(rest(z2), z3), REST(z2))

The (relative) TRS S consists of the following rules:

   eq(0', 0') -> true
   eq(0', s(z0)) -> false
   eq(s(z0), 0') -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   or(true, z0) -> true
   or(false, z0) -> z0
   union(empty, z0) -> z0
   union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
   isEmpty(empty) -> true
   isEmpty(edge(z0, z1, z2)) -> false
   from(edge(z0, z1, z2)) -> z0
   to(edge(z0, z1, z2)) -> z1
   rest(edge(z0, z1, z2)) -> z2
   rest(empty) -> empty
   reach(z0, z1, z2, z3) -> if1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3)
   if1(true, z0, z1, z2, z3, z4, z5, z6) -> true
   if1(false, z0, z1, z2, z3, z4, z5, z6) -> if2(z0, z1, z2, z3, z4, z5, z6)
   if2(true, z0, z1, z2, z3, z4, z5) -> false
   if2(false, z0, z1, z2, z3, z4, z5) -> if3(z0, z1, z2, z3, z4, z5)
   if3(false, z0, z1, z2, z3, z4) -> reach(z1, z2, rest(z3), edge(from(z3), to(z3), z4))
   if3(true, z0, z1, z2, z3, z4) -> if4(z0, z1, z2, z3, z4)
   if4(true, z0, z1, z2, z3) -> true
   if4(false, z0, z1, z2, z3) -> or(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty))

Rewrite Strategy: INNERMOST
----------------------------------------

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(8)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
OR(true, z0) -> c4
OR(false, z0) -> c5
UNION(empty, z0) -> c6
UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
ISEMPTY(empty) -> c8
ISEMPTY(edge(z0, z1, z2)) -> c9
FROM(edge(z0, z1, z2)) -> c10
TO(edge(z0, z1, z2)) -> c11
REST(edge(z0, z1, z2)) -> c12
REST(empty) -> c13
REACH(z0, z1, z2, z3) -> c14(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, z1))
REACH(z0, z1, z2, z3) -> c15(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), ISEMPTY(z2))
REACH(z0, z1, z2, z3) -> c16(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, from(z2)), FROM(z2))
REACH(z0, z1, z2, z3) -> c17(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z1, to(z2)), TO(z2))
IF1(true, z0, z1, z2, z3, z4, z5, z6) -> c18
IF1(false, z0, z1, z2, z3, z4, z5, z6) -> c19(IF2(z0, z1, z2, z3, z4, z5, z6))
IF2(true, z0, z1, z2, z3, z4, z5) -> c20
IF2(false, z0, z1, z2, z3, z4, z5) -> c21(IF3(z0, z1, z2, z3, z4, z5))
IF3(false, z0, z1, z2, z3, z4) -> c22(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), REST(z3))
IF3(false, z0, z1, z2, z3, z4) -> c23(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), FROM(z3))
IF3(false, z0, z1, z2, z3, z4) -> c24(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), TO(z3))
IF3(true, z0, z1, z2, z3, z4) -> c25(IF4(z0, z1, z2, z3, z4))
IF4(true, z0, z1, z2, z3) -> c26
IF4(false, z0, z1, z2, z3) -> c27(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(z0, z1, rest(z2), z3), REST(z2))
IF4(false, z0, z1, z2, z3) -> c28(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), TO(z2))
IF4(false, z0, z1, z2, z3) -> c29(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), UNION(rest(z2), z3), REST(z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
union(empty, z0) -> z0
union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
isEmpty(empty) -> true
isEmpty(edge(z0, z1, z2)) -> false
from(edge(z0, z1, z2)) -> z0
to(edge(z0, z1, z2)) -> z1
rest(edge(z0, z1, z2)) -> z2
rest(empty) -> empty
reach(z0, z1, z2, z3) -> if1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3)
if1(true, z0, z1, z2, z3, z4, z5, z6) -> true
if1(false, z0, z1, z2, z3, z4, z5, z6) -> if2(z0, z1, z2, z3, z4, z5, z6)
if2(true, z0, z1, z2, z3, z4, z5) -> false
if2(false, z0, z1, z2, z3, z4, z5) -> if3(z0, z1, z2, z3, z4, z5)
if3(false, z0, z1, z2, z3, z4) -> reach(z1, z2, rest(z3), edge(from(z3), to(z3), z4))
if3(true, z0, z1, z2, z3, z4) -> if4(z0, z1, z2, z3, z4)
if4(true, z0, z1, z2, z3) -> true
if4(false, z0, z1, z2, z3) -> or(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty))

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
OR :: true:false -> true:false -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
UNION :: empty:edge -> empty:edge -> c6:c7
empty :: empty:edge
c6 :: c6:c7
edge :: 0':s -> 0':s -> empty:edge -> empty:edge
c7 :: c6:c7 -> c6:c7
ISEMPTY :: empty:edge -> c8:c9
c8 :: c8:c9
c9 :: c8:c9
FROM :: empty:edge -> c10
c10 :: c10
TO :: empty:edge -> c11
c11 :: c11
REST :: empty:edge -> c12:c13
c12 :: c12:c13
c13 :: c12:c13
REACH :: 0':s -> 0':s -> empty:edge -> empty:edge -> c14:c15:c16:c17
c14 :: c18:c19 -> c:c1:c2:c3 -> c14:c15:c16:c17
IF1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c18:c19
eq :: 0':s -> 0':s -> true:false
isEmpty :: empty:edge -> true:false
from :: empty:edge -> 0':s
to :: empty:edge -> 0':s
c15 :: c18:c19 -> c8:c9 -> c14:c15:c16:c17
c16 :: c18:c19 -> c:c1:c2:c3 -> c10 -> c14:c15:c16:c17
c17 :: c18:c19 -> c:c1:c2:c3 -> c11 -> c14:c15:c16:c17
c18 :: c18:c19
c19 :: c20:c21 -> c18:c19
IF2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c20:c21
c20 :: c20:c21
c21 :: c22:c23:c24:c25 -> c20:c21
IF3 :: true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c22:c23:c24:c25
c22 :: c14:c15:c16:c17 -> c12:c13 -> c22:c23:c24:c25
rest :: empty:edge -> empty:edge
c23 :: c14:c15:c16:c17 -> c10 -> c22:c23:c24:c25
c24 :: c14:c15:c16:c17 -> c11 -> c22:c23:c24:c25
c25 :: c26:c27:c28:c29 -> c22:c23:c24:c25
IF4 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c26:c27:c28:c29
c26 :: c26:c27:c28:c29
c27 :: c4:c5 -> c14:c15:c16:c17 -> c12:c13 -> c26:c27:c28:c29
reach :: 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
union :: empty:edge -> empty:edge -> empty:edge
c28 :: c4:c5 -> c14:c15:c16:c17 -> c11 -> c26:c27:c28:c29
c29 :: c4:c5 -> c14:c15:c16:c17 -> c6:c7 -> c12:c13 -> c26:c27:c28:c29
or :: true:false -> true:false -> true:false
if1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if3 :: true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if4 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
hole_c:c1:c2:c31_30 :: c:c1:c2:c3
hole_0':s2_30 :: 0':s
hole_c4:c53_30 :: c4:c5
hole_true:false4_30 :: true:false
hole_c6:c75_30 :: c6:c7
hole_empty:edge6_30 :: empty:edge
hole_c8:c97_30 :: c8:c9
hole_c108_30 :: c10
hole_c119_30 :: c11
hole_c12:c1310_30 :: c12:c13
hole_c14:c15:c16:c1711_30 :: c14:c15:c16:c17
hole_c18:c1912_30 :: c18:c19
hole_c20:c2113_30 :: c20:c21
hole_c22:c23:c24:c2514_30 :: c22:c23:c24:c25
hole_c26:c27:c28:c2915_30 :: c26:c27:c28:c29
gen_c:c1:c2:c316_30 :: Nat -> c:c1:c2:c3
gen_0':s17_30 :: Nat -> 0':s
gen_c6:c718_30 :: Nat -> c6:c7
gen_empty:edge19_30 :: Nat -> empty:edge

----------------------------------------

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
EQ, UNION, REACH, eq, reach, union

They will be analysed ascendingly in the following order:
EQ < REACH
UNION < REACH
eq < REACH
reach < REACH
union < REACH
eq < reach
union < reach

----------------------------------------

(10)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
OR(true, z0) -> c4
OR(false, z0) -> c5
UNION(empty, z0) -> c6
UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
ISEMPTY(empty) -> c8
ISEMPTY(edge(z0, z1, z2)) -> c9
FROM(edge(z0, z1, z2)) -> c10
TO(edge(z0, z1, z2)) -> c11
REST(edge(z0, z1, z2)) -> c12
REST(empty) -> c13
REACH(z0, z1, z2, z3) -> c14(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, z1))
REACH(z0, z1, z2, z3) -> c15(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), ISEMPTY(z2))
REACH(z0, z1, z2, z3) -> c16(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, from(z2)), FROM(z2))
REACH(z0, z1, z2, z3) -> c17(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z1, to(z2)), TO(z2))
IF1(true, z0, z1, z2, z3, z4, z5, z6) -> c18
IF1(false, z0, z1, z2, z3, z4, z5, z6) -> c19(IF2(z0, z1, z2, z3, z4, z5, z6))
IF2(true, z0, z1, z2, z3, z4, z5) -> c20
IF2(false, z0, z1, z2, z3, z4, z5) -> c21(IF3(z0, z1, z2, z3, z4, z5))
IF3(false, z0, z1, z2, z3, z4) -> c22(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), REST(z3))
IF3(false, z0, z1, z2, z3, z4) -> c23(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), FROM(z3))
IF3(false, z0, z1, z2, z3, z4) -> c24(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), TO(z3))
IF3(true, z0, z1, z2, z3, z4) -> c25(IF4(z0, z1, z2, z3, z4))
IF4(true, z0, z1, z2, z3) -> c26
IF4(false, z0, z1, z2, z3) -> c27(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(z0, z1, rest(z2), z3), REST(z2))
IF4(false, z0, z1, z2, z3) -> c28(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), TO(z2))
IF4(false, z0, z1, z2, z3) -> c29(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), UNION(rest(z2), z3), REST(z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
union(empty, z0) -> z0
union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
isEmpty(empty) -> true
isEmpty(edge(z0, z1, z2)) -> false
from(edge(z0, z1, z2)) -> z0
to(edge(z0, z1, z2)) -> z1
rest(edge(z0, z1, z2)) -> z2
rest(empty) -> empty
reach(z0, z1, z2, z3) -> if1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3)
if1(true, z0, z1, z2, z3, z4, z5, z6) -> true
if1(false, z0, z1, z2, z3, z4, z5, z6) -> if2(z0, z1, z2, z3, z4, z5, z6)
if2(true, z0, z1, z2, z3, z4, z5) -> false
if2(false, z0, z1, z2, z3, z4, z5) -> if3(z0, z1, z2, z3, z4, z5)
if3(false, z0, z1, z2, z3, z4) -> reach(z1, z2, rest(z3), edge(from(z3), to(z3), z4))
if3(true, z0, z1, z2, z3, z4) -> if4(z0, z1, z2, z3, z4)
if4(true, z0, z1, z2, z3) -> true
if4(false, z0, z1, z2, z3) -> or(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty))

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
OR :: true:false -> true:false -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
UNION :: empty:edge -> empty:edge -> c6:c7
empty :: empty:edge
c6 :: c6:c7
edge :: 0':s -> 0':s -> empty:edge -> empty:edge
c7 :: c6:c7 -> c6:c7
ISEMPTY :: empty:edge -> c8:c9
c8 :: c8:c9
c9 :: c8:c9
FROM :: empty:edge -> c10
c10 :: c10
TO :: empty:edge -> c11
c11 :: c11
REST :: empty:edge -> c12:c13
c12 :: c12:c13
c13 :: c12:c13
REACH :: 0':s -> 0':s -> empty:edge -> empty:edge -> c14:c15:c16:c17
c14 :: c18:c19 -> c:c1:c2:c3 -> c14:c15:c16:c17
IF1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c18:c19
eq :: 0':s -> 0':s -> true:false
isEmpty :: empty:edge -> true:false
from :: empty:edge -> 0':s
to :: empty:edge -> 0':s
c15 :: c18:c19 -> c8:c9 -> c14:c15:c16:c17
c16 :: c18:c19 -> c:c1:c2:c3 -> c10 -> c14:c15:c16:c17
c17 :: c18:c19 -> c:c1:c2:c3 -> c11 -> c14:c15:c16:c17
c18 :: c18:c19
c19 :: c20:c21 -> c18:c19
IF2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c20:c21
c20 :: c20:c21
c21 :: c22:c23:c24:c25 -> c20:c21
IF3 :: true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c22:c23:c24:c25
c22 :: c14:c15:c16:c17 -> c12:c13 -> c22:c23:c24:c25
rest :: empty:edge -> empty:edge
c23 :: c14:c15:c16:c17 -> c10 -> c22:c23:c24:c25
c24 :: c14:c15:c16:c17 -> c11 -> c22:c23:c24:c25
c25 :: c26:c27:c28:c29 -> c22:c23:c24:c25
IF4 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c26:c27:c28:c29
c26 :: c26:c27:c28:c29
c27 :: c4:c5 -> c14:c15:c16:c17 -> c12:c13 -> c26:c27:c28:c29
reach :: 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
union :: empty:edge -> empty:edge -> empty:edge
c28 :: c4:c5 -> c14:c15:c16:c17 -> c11 -> c26:c27:c28:c29
c29 :: c4:c5 -> c14:c15:c16:c17 -> c6:c7 -> c12:c13 -> c26:c27:c28:c29
or :: true:false -> true:false -> true:false
if1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if3 :: true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if4 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
hole_c:c1:c2:c31_30 :: c:c1:c2:c3
hole_0':s2_30 :: 0':s
hole_c4:c53_30 :: c4:c5
hole_true:false4_30 :: true:false
hole_c6:c75_30 :: c6:c7
hole_empty:edge6_30 :: empty:edge
hole_c8:c97_30 :: c8:c9
hole_c108_30 :: c10
hole_c119_30 :: c11
hole_c12:c1310_30 :: c12:c13
hole_c14:c15:c16:c1711_30 :: c14:c15:c16:c17
hole_c18:c1912_30 :: c18:c19
hole_c20:c2113_30 :: c20:c21
hole_c22:c23:c24:c2514_30 :: c22:c23:c24:c25
hole_c26:c27:c28:c2915_30 :: c26:c27:c28:c29
gen_c:c1:c2:c316_30 :: Nat -> c:c1:c2:c3
gen_0':s17_30 :: Nat -> 0':s
gen_c6:c718_30 :: Nat -> c6:c7
gen_empty:edge19_30 :: Nat -> empty:edge


Generator Equations:
gen_c:c1:c2:c316_30(0) <=> c
gen_c:c1:c2:c316_30(+(x, 1)) <=> c3(gen_c:c1:c2:c316_30(x))
gen_0':s17_30(0) <=> 0'
gen_0':s17_30(+(x, 1)) <=> s(gen_0':s17_30(x))
gen_c6:c718_30(0) <=> c6
gen_c6:c718_30(+(x, 1)) <=> c7(gen_c6:c718_30(x))
gen_empty:edge19_30(0) <=> empty
gen_empty:edge19_30(+(x, 1)) <=> edge(0', 0', gen_empty:edge19_30(x))


The following defined symbols remain to be analysed:
EQ, UNION, REACH, eq, reach, union

They will be analysed ascendingly in the following order:
EQ < REACH
UNION < REACH
eq < REACH
reach < REACH
union < REACH
eq < reach
union < reach

----------------------------------------

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
EQ(gen_0':s17_30(n21_30), gen_0':s17_30(n21_30)) -> gen_c:c1:c2:c316_30(n21_30), rt in Omega(1 + n21_30)

Induction Base:
EQ(gen_0':s17_30(0), gen_0':s17_30(0)) ->_R^Omega(1)
c

Induction Step:
EQ(gen_0':s17_30(+(n21_30, 1)), gen_0':s17_30(+(n21_30, 1))) ->_R^Omega(1)
c3(EQ(gen_0':s17_30(n21_30), gen_0':s17_30(n21_30))) ->_IH
c3(gen_c:c1:c2:c316_30(c22_30))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(12)
Complex Obligation (BEST)

----------------------------------------

(13)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
OR(true, z0) -> c4
OR(false, z0) -> c5
UNION(empty, z0) -> c6
UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
ISEMPTY(empty) -> c8
ISEMPTY(edge(z0, z1, z2)) -> c9
FROM(edge(z0, z1, z2)) -> c10
TO(edge(z0, z1, z2)) -> c11
REST(edge(z0, z1, z2)) -> c12
REST(empty) -> c13
REACH(z0, z1, z2, z3) -> c14(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, z1))
REACH(z0, z1, z2, z3) -> c15(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), ISEMPTY(z2))
REACH(z0, z1, z2, z3) -> c16(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, from(z2)), FROM(z2))
REACH(z0, z1, z2, z3) -> c17(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z1, to(z2)), TO(z2))
IF1(true, z0, z1, z2, z3, z4, z5, z6) -> c18
IF1(false, z0, z1, z2, z3, z4, z5, z6) -> c19(IF2(z0, z1, z2, z3, z4, z5, z6))
IF2(true, z0, z1, z2, z3, z4, z5) -> c20
IF2(false, z0, z1, z2, z3, z4, z5) -> c21(IF3(z0, z1, z2, z3, z4, z5))
IF3(false, z0, z1, z2, z3, z4) -> c22(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), REST(z3))
IF3(false, z0, z1, z2, z3, z4) -> c23(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), FROM(z3))
IF3(false, z0, z1, z2, z3, z4) -> c24(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), TO(z3))
IF3(true, z0, z1, z2, z3, z4) -> c25(IF4(z0, z1, z2, z3, z4))
IF4(true, z0, z1, z2, z3) -> c26
IF4(false, z0, z1, z2, z3) -> c27(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(z0, z1, rest(z2), z3), REST(z2))
IF4(false, z0, z1, z2, z3) -> c28(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), TO(z2))
IF4(false, z0, z1, z2, z3) -> c29(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), UNION(rest(z2), z3), REST(z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
union(empty, z0) -> z0
union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
isEmpty(empty) -> true
isEmpty(edge(z0, z1, z2)) -> false
from(edge(z0, z1, z2)) -> z0
to(edge(z0, z1, z2)) -> z1
rest(edge(z0, z1, z2)) -> z2
rest(empty) -> empty
reach(z0, z1, z2, z3) -> if1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3)
if1(true, z0, z1, z2, z3, z4, z5, z6) -> true
if1(false, z0, z1, z2, z3, z4, z5, z6) -> if2(z0, z1, z2, z3, z4, z5, z6)
if2(true, z0, z1, z2, z3, z4, z5) -> false
if2(false, z0, z1, z2, z3, z4, z5) -> if3(z0, z1, z2, z3, z4, z5)
if3(false, z0, z1, z2, z3, z4) -> reach(z1, z2, rest(z3), edge(from(z3), to(z3), z4))
if3(true, z0, z1, z2, z3, z4) -> if4(z0, z1, z2, z3, z4)
if4(true, z0, z1, z2, z3) -> true
if4(false, z0, z1, z2, z3) -> or(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty))

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
OR :: true:false -> true:false -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
UNION :: empty:edge -> empty:edge -> c6:c7
empty :: empty:edge
c6 :: c6:c7
edge :: 0':s -> 0':s -> empty:edge -> empty:edge
c7 :: c6:c7 -> c6:c7
ISEMPTY :: empty:edge -> c8:c9
c8 :: c8:c9
c9 :: c8:c9
FROM :: empty:edge -> c10
c10 :: c10
TO :: empty:edge -> c11
c11 :: c11
REST :: empty:edge -> c12:c13
c12 :: c12:c13
c13 :: c12:c13
REACH :: 0':s -> 0':s -> empty:edge -> empty:edge -> c14:c15:c16:c17
c14 :: c18:c19 -> c:c1:c2:c3 -> c14:c15:c16:c17
IF1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c18:c19
eq :: 0':s -> 0':s -> true:false
isEmpty :: empty:edge -> true:false
from :: empty:edge -> 0':s
to :: empty:edge -> 0':s
c15 :: c18:c19 -> c8:c9 -> c14:c15:c16:c17
c16 :: c18:c19 -> c:c1:c2:c3 -> c10 -> c14:c15:c16:c17
c17 :: c18:c19 -> c:c1:c2:c3 -> c11 -> c14:c15:c16:c17
c18 :: c18:c19
c19 :: c20:c21 -> c18:c19
IF2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c20:c21
c20 :: c20:c21
c21 :: c22:c23:c24:c25 -> c20:c21
IF3 :: true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c22:c23:c24:c25
c22 :: c14:c15:c16:c17 -> c12:c13 -> c22:c23:c24:c25
rest :: empty:edge -> empty:edge
c23 :: c14:c15:c16:c17 -> c10 -> c22:c23:c24:c25
c24 :: c14:c15:c16:c17 -> c11 -> c22:c23:c24:c25
c25 :: c26:c27:c28:c29 -> c22:c23:c24:c25
IF4 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c26:c27:c28:c29
c26 :: c26:c27:c28:c29
c27 :: c4:c5 -> c14:c15:c16:c17 -> c12:c13 -> c26:c27:c28:c29
reach :: 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
union :: empty:edge -> empty:edge -> empty:edge
c28 :: c4:c5 -> c14:c15:c16:c17 -> c11 -> c26:c27:c28:c29
c29 :: c4:c5 -> c14:c15:c16:c17 -> c6:c7 -> c12:c13 -> c26:c27:c28:c29
or :: true:false -> true:false -> true:false
if1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if3 :: true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if4 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
hole_c:c1:c2:c31_30 :: c:c1:c2:c3
hole_0':s2_30 :: 0':s
hole_c4:c53_30 :: c4:c5
hole_true:false4_30 :: true:false
hole_c6:c75_30 :: c6:c7
hole_empty:edge6_30 :: empty:edge
hole_c8:c97_30 :: c8:c9
hole_c108_30 :: c10
hole_c119_30 :: c11
hole_c12:c1310_30 :: c12:c13
hole_c14:c15:c16:c1711_30 :: c14:c15:c16:c17
hole_c18:c1912_30 :: c18:c19
hole_c20:c2113_30 :: c20:c21
hole_c22:c23:c24:c2514_30 :: c22:c23:c24:c25
hole_c26:c27:c28:c2915_30 :: c26:c27:c28:c29
gen_c:c1:c2:c316_30 :: Nat -> c:c1:c2:c3
gen_0':s17_30 :: Nat -> 0':s
gen_c6:c718_30 :: Nat -> c6:c7
gen_empty:edge19_30 :: Nat -> empty:edge


Generator Equations:
gen_c:c1:c2:c316_30(0) <=> c
gen_c:c1:c2:c316_30(+(x, 1)) <=> c3(gen_c:c1:c2:c316_30(x))
gen_0':s17_30(0) <=> 0'
gen_0':s17_30(+(x, 1)) <=> s(gen_0':s17_30(x))
gen_c6:c718_30(0) <=> c6
gen_c6:c718_30(+(x, 1)) <=> c7(gen_c6:c718_30(x))
gen_empty:edge19_30(0) <=> empty
gen_empty:edge19_30(+(x, 1)) <=> edge(0', 0', gen_empty:edge19_30(x))


The following defined symbols remain to be analysed:
EQ, UNION, REACH, eq, reach, union

They will be analysed ascendingly in the following order:
EQ < REACH
UNION < REACH
eq < REACH
reach < REACH
union < REACH
eq < reach
union < reach

----------------------------------------

(14) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(15)
BOUNDS(n^1, INF)

----------------------------------------

(16)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
OR(true, z0) -> c4
OR(false, z0) -> c5
UNION(empty, z0) -> c6
UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
ISEMPTY(empty) -> c8
ISEMPTY(edge(z0, z1, z2)) -> c9
FROM(edge(z0, z1, z2)) -> c10
TO(edge(z0, z1, z2)) -> c11
REST(edge(z0, z1, z2)) -> c12
REST(empty) -> c13
REACH(z0, z1, z2, z3) -> c14(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, z1))
REACH(z0, z1, z2, z3) -> c15(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), ISEMPTY(z2))
REACH(z0, z1, z2, z3) -> c16(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, from(z2)), FROM(z2))
REACH(z0, z1, z2, z3) -> c17(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z1, to(z2)), TO(z2))
IF1(true, z0, z1, z2, z3, z4, z5, z6) -> c18
IF1(false, z0, z1, z2, z3, z4, z5, z6) -> c19(IF2(z0, z1, z2, z3, z4, z5, z6))
IF2(true, z0, z1, z2, z3, z4, z5) -> c20
IF2(false, z0, z1, z2, z3, z4, z5) -> c21(IF3(z0, z1, z2, z3, z4, z5))
IF3(false, z0, z1, z2, z3, z4) -> c22(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), REST(z3))
IF3(false, z0, z1, z2, z3, z4) -> c23(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), FROM(z3))
IF3(false, z0, z1, z2, z3, z4) -> c24(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), TO(z3))
IF3(true, z0, z1, z2, z3, z4) -> c25(IF4(z0, z1, z2, z3, z4))
IF4(true, z0, z1, z2, z3) -> c26
IF4(false, z0, z1, z2, z3) -> c27(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(z0, z1, rest(z2), z3), REST(z2))
IF4(false, z0, z1, z2, z3) -> c28(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), TO(z2))
IF4(false, z0, z1, z2, z3) -> c29(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), UNION(rest(z2), z3), REST(z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
union(empty, z0) -> z0
union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
isEmpty(empty) -> true
isEmpty(edge(z0, z1, z2)) -> false
from(edge(z0, z1, z2)) -> z0
to(edge(z0, z1, z2)) -> z1
rest(edge(z0, z1, z2)) -> z2
rest(empty) -> empty
reach(z0, z1, z2, z3) -> if1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3)
if1(true, z0, z1, z2, z3, z4, z5, z6) -> true
if1(false, z0, z1, z2, z3, z4, z5, z6) -> if2(z0, z1, z2, z3, z4, z5, z6)
if2(true, z0, z1, z2, z3, z4, z5) -> false
if2(false, z0, z1, z2, z3, z4, z5) -> if3(z0, z1, z2, z3, z4, z5)
if3(false, z0, z1, z2, z3, z4) -> reach(z1, z2, rest(z3), edge(from(z3), to(z3), z4))
if3(true, z0, z1, z2, z3, z4) -> if4(z0, z1, z2, z3, z4)
if4(true, z0, z1, z2, z3) -> true
if4(false, z0, z1, z2, z3) -> or(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty))

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
OR :: true:false -> true:false -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
UNION :: empty:edge -> empty:edge -> c6:c7
empty :: empty:edge
c6 :: c6:c7
edge :: 0':s -> 0':s -> empty:edge -> empty:edge
c7 :: c6:c7 -> c6:c7
ISEMPTY :: empty:edge -> c8:c9
c8 :: c8:c9
c9 :: c8:c9
FROM :: empty:edge -> c10
c10 :: c10
TO :: empty:edge -> c11
c11 :: c11
REST :: empty:edge -> c12:c13
c12 :: c12:c13
c13 :: c12:c13
REACH :: 0':s -> 0':s -> empty:edge -> empty:edge -> c14:c15:c16:c17
c14 :: c18:c19 -> c:c1:c2:c3 -> c14:c15:c16:c17
IF1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c18:c19
eq :: 0':s -> 0':s -> true:false
isEmpty :: empty:edge -> true:false
from :: empty:edge -> 0':s
to :: empty:edge -> 0':s
c15 :: c18:c19 -> c8:c9 -> c14:c15:c16:c17
c16 :: c18:c19 -> c:c1:c2:c3 -> c10 -> c14:c15:c16:c17
c17 :: c18:c19 -> c:c1:c2:c3 -> c11 -> c14:c15:c16:c17
c18 :: c18:c19
c19 :: c20:c21 -> c18:c19
IF2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c20:c21
c20 :: c20:c21
c21 :: c22:c23:c24:c25 -> c20:c21
IF3 :: true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c22:c23:c24:c25
c22 :: c14:c15:c16:c17 -> c12:c13 -> c22:c23:c24:c25
rest :: empty:edge -> empty:edge
c23 :: c14:c15:c16:c17 -> c10 -> c22:c23:c24:c25
c24 :: c14:c15:c16:c17 -> c11 -> c22:c23:c24:c25
c25 :: c26:c27:c28:c29 -> c22:c23:c24:c25
IF4 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c26:c27:c28:c29
c26 :: c26:c27:c28:c29
c27 :: c4:c5 -> c14:c15:c16:c17 -> c12:c13 -> c26:c27:c28:c29
reach :: 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
union :: empty:edge -> empty:edge -> empty:edge
c28 :: c4:c5 -> c14:c15:c16:c17 -> c11 -> c26:c27:c28:c29
c29 :: c4:c5 -> c14:c15:c16:c17 -> c6:c7 -> c12:c13 -> c26:c27:c28:c29
or :: true:false -> true:false -> true:false
if1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if3 :: true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if4 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
hole_c:c1:c2:c31_30 :: c:c1:c2:c3
hole_0':s2_30 :: 0':s
hole_c4:c53_30 :: c4:c5
hole_true:false4_30 :: true:false
hole_c6:c75_30 :: c6:c7
hole_empty:edge6_30 :: empty:edge
hole_c8:c97_30 :: c8:c9
hole_c108_30 :: c10
hole_c119_30 :: c11
hole_c12:c1310_30 :: c12:c13
hole_c14:c15:c16:c1711_30 :: c14:c15:c16:c17
hole_c18:c1912_30 :: c18:c19
hole_c20:c2113_30 :: c20:c21
hole_c22:c23:c24:c2514_30 :: c22:c23:c24:c25
hole_c26:c27:c28:c2915_30 :: c26:c27:c28:c29
gen_c:c1:c2:c316_30 :: Nat -> c:c1:c2:c3
gen_0':s17_30 :: Nat -> 0':s
gen_c6:c718_30 :: Nat -> c6:c7
gen_empty:edge19_30 :: Nat -> empty:edge


Lemmas:
EQ(gen_0':s17_30(n21_30), gen_0':s17_30(n21_30)) -> gen_c:c1:c2:c316_30(n21_30), rt in Omega(1 + n21_30)


Generator Equations:
gen_c:c1:c2:c316_30(0) <=> c
gen_c:c1:c2:c316_30(+(x, 1)) <=> c3(gen_c:c1:c2:c316_30(x))
gen_0':s17_30(0) <=> 0'
gen_0':s17_30(+(x, 1)) <=> s(gen_0':s17_30(x))
gen_c6:c718_30(0) <=> c6
gen_c6:c718_30(+(x, 1)) <=> c7(gen_c6:c718_30(x))
gen_empty:edge19_30(0) <=> empty
gen_empty:edge19_30(+(x, 1)) <=> edge(0', 0', gen_empty:edge19_30(x))


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

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

----------------------------------------

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
UNION(gen_empty:edge19_30(n1111_30), gen_empty:edge19_30(b)) -> gen_c6:c718_30(n1111_30), rt in Omega(1 + n1111_30)

Induction Base:
UNION(gen_empty:edge19_30(0), gen_empty:edge19_30(b)) ->_R^Omega(1)
c6

Induction Step:
UNION(gen_empty:edge19_30(+(n1111_30, 1)), gen_empty:edge19_30(b)) ->_R^Omega(1)
c7(UNION(gen_empty:edge19_30(n1111_30), gen_empty:edge19_30(b))) ->_IH
c7(gen_c6:c718_30(c1112_30))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(18)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
OR(true, z0) -> c4
OR(false, z0) -> c5
UNION(empty, z0) -> c6
UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
ISEMPTY(empty) -> c8
ISEMPTY(edge(z0, z1, z2)) -> c9
FROM(edge(z0, z1, z2)) -> c10
TO(edge(z0, z1, z2)) -> c11
REST(edge(z0, z1, z2)) -> c12
REST(empty) -> c13
REACH(z0, z1, z2, z3) -> c14(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, z1))
REACH(z0, z1, z2, z3) -> c15(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), ISEMPTY(z2))
REACH(z0, z1, z2, z3) -> c16(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, from(z2)), FROM(z2))
REACH(z0, z1, z2, z3) -> c17(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z1, to(z2)), TO(z2))
IF1(true, z0, z1, z2, z3, z4, z5, z6) -> c18
IF1(false, z0, z1, z2, z3, z4, z5, z6) -> c19(IF2(z0, z1, z2, z3, z4, z5, z6))
IF2(true, z0, z1, z2, z3, z4, z5) -> c20
IF2(false, z0, z1, z2, z3, z4, z5) -> c21(IF3(z0, z1, z2, z3, z4, z5))
IF3(false, z0, z1, z2, z3, z4) -> c22(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), REST(z3))
IF3(false, z0, z1, z2, z3, z4) -> c23(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), FROM(z3))
IF3(false, z0, z1, z2, z3, z4) -> c24(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), TO(z3))
IF3(true, z0, z1, z2, z3, z4) -> c25(IF4(z0, z1, z2, z3, z4))
IF4(true, z0, z1, z2, z3) -> c26
IF4(false, z0, z1, z2, z3) -> c27(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(z0, z1, rest(z2), z3), REST(z2))
IF4(false, z0, z1, z2, z3) -> c28(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), TO(z2))
IF4(false, z0, z1, z2, z3) -> c29(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), UNION(rest(z2), z3), REST(z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
union(empty, z0) -> z0
union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
isEmpty(empty) -> true
isEmpty(edge(z0, z1, z2)) -> false
from(edge(z0, z1, z2)) -> z0
to(edge(z0, z1, z2)) -> z1
rest(edge(z0, z1, z2)) -> z2
rest(empty) -> empty
reach(z0, z1, z2, z3) -> if1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3)
if1(true, z0, z1, z2, z3, z4, z5, z6) -> true
if1(false, z0, z1, z2, z3, z4, z5, z6) -> if2(z0, z1, z2, z3, z4, z5, z6)
if2(true, z0, z1, z2, z3, z4, z5) -> false
if2(false, z0, z1, z2, z3, z4, z5) -> if3(z0, z1, z2, z3, z4, z5)
if3(false, z0, z1, z2, z3, z4) -> reach(z1, z2, rest(z3), edge(from(z3), to(z3), z4))
if3(true, z0, z1, z2, z3, z4) -> if4(z0, z1, z2, z3, z4)
if4(true, z0, z1, z2, z3) -> true
if4(false, z0, z1, z2, z3) -> or(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty))

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
OR :: true:false -> true:false -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
UNION :: empty:edge -> empty:edge -> c6:c7
empty :: empty:edge
c6 :: c6:c7
edge :: 0':s -> 0':s -> empty:edge -> empty:edge
c7 :: c6:c7 -> c6:c7
ISEMPTY :: empty:edge -> c8:c9
c8 :: c8:c9
c9 :: c8:c9
FROM :: empty:edge -> c10
c10 :: c10
TO :: empty:edge -> c11
c11 :: c11
REST :: empty:edge -> c12:c13
c12 :: c12:c13
c13 :: c12:c13
REACH :: 0':s -> 0':s -> empty:edge -> empty:edge -> c14:c15:c16:c17
c14 :: c18:c19 -> c:c1:c2:c3 -> c14:c15:c16:c17
IF1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c18:c19
eq :: 0':s -> 0':s -> true:false
isEmpty :: empty:edge -> true:false
from :: empty:edge -> 0':s
to :: empty:edge -> 0':s
c15 :: c18:c19 -> c8:c9 -> c14:c15:c16:c17
c16 :: c18:c19 -> c:c1:c2:c3 -> c10 -> c14:c15:c16:c17
c17 :: c18:c19 -> c:c1:c2:c3 -> c11 -> c14:c15:c16:c17
c18 :: c18:c19
c19 :: c20:c21 -> c18:c19
IF2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c20:c21
c20 :: c20:c21
c21 :: c22:c23:c24:c25 -> c20:c21
IF3 :: true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c22:c23:c24:c25
c22 :: c14:c15:c16:c17 -> c12:c13 -> c22:c23:c24:c25
rest :: empty:edge -> empty:edge
c23 :: c14:c15:c16:c17 -> c10 -> c22:c23:c24:c25
c24 :: c14:c15:c16:c17 -> c11 -> c22:c23:c24:c25
c25 :: c26:c27:c28:c29 -> c22:c23:c24:c25
IF4 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c26:c27:c28:c29
c26 :: c26:c27:c28:c29
c27 :: c4:c5 -> c14:c15:c16:c17 -> c12:c13 -> c26:c27:c28:c29
reach :: 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
union :: empty:edge -> empty:edge -> empty:edge
c28 :: c4:c5 -> c14:c15:c16:c17 -> c11 -> c26:c27:c28:c29
c29 :: c4:c5 -> c14:c15:c16:c17 -> c6:c7 -> c12:c13 -> c26:c27:c28:c29
or :: true:false -> true:false -> true:false
if1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if3 :: true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if4 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
hole_c:c1:c2:c31_30 :: c:c1:c2:c3
hole_0':s2_30 :: 0':s
hole_c4:c53_30 :: c4:c5
hole_true:false4_30 :: true:false
hole_c6:c75_30 :: c6:c7
hole_empty:edge6_30 :: empty:edge
hole_c8:c97_30 :: c8:c9
hole_c108_30 :: c10
hole_c119_30 :: c11
hole_c12:c1310_30 :: c12:c13
hole_c14:c15:c16:c1711_30 :: c14:c15:c16:c17
hole_c18:c1912_30 :: c18:c19
hole_c20:c2113_30 :: c20:c21
hole_c22:c23:c24:c2514_30 :: c22:c23:c24:c25
hole_c26:c27:c28:c2915_30 :: c26:c27:c28:c29
gen_c:c1:c2:c316_30 :: Nat -> c:c1:c2:c3
gen_0':s17_30 :: Nat -> 0':s
gen_c6:c718_30 :: Nat -> c6:c7
gen_empty:edge19_30 :: Nat -> empty:edge


Lemmas:
EQ(gen_0':s17_30(n21_30), gen_0':s17_30(n21_30)) -> gen_c:c1:c2:c316_30(n21_30), rt in Omega(1 + n21_30)
UNION(gen_empty:edge19_30(n1111_30), gen_empty:edge19_30(b)) -> gen_c6:c718_30(n1111_30), rt in Omega(1 + n1111_30)


Generator Equations:
gen_c:c1:c2:c316_30(0) <=> c
gen_c:c1:c2:c316_30(+(x, 1)) <=> c3(gen_c:c1:c2:c316_30(x))
gen_0':s17_30(0) <=> 0'
gen_0':s17_30(+(x, 1)) <=> s(gen_0':s17_30(x))
gen_c6:c718_30(0) <=> c6
gen_c6:c718_30(+(x, 1)) <=> c7(gen_c6:c718_30(x))
gen_empty:edge19_30(0) <=> empty
gen_empty:edge19_30(+(x, 1)) <=> edge(0', 0', gen_empty:edge19_30(x))


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

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

----------------------------------------

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
eq(gen_0':s17_30(n2178_30), gen_0':s17_30(n2178_30)) -> true, rt in Omega(0)

Induction Base:
eq(gen_0':s17_30(0), gen_0':s17_30(0)) ->_R^Omega(0)
true

Induction Step:
eq(gen_0':s17_30(+(n2178_30, 1)), gen_0':s17_30(+(n2178_30, 1))) ->_R^Omega(0)
eq(gen_0':s17_30(n2178_30), gen_0':s17_30(n2178_30)) ->_IH
true

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(20)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
OR(true, z0) -> c4
OR(false, z0) -> c5
UNION(empty, z0) -> c6
UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
ISEMPTY(empty) -> c8
ISEMPTY(edge(z0, z1, z2)) -> c9
FROM(edge(z0, z1, z2)) -> c10
TO(edge(z0, z1, z2)) -> c11
REST(edge(z0, z1, z2)) -> c12
REST(empty) -> c13
REACH(z0, z1, z2, z3) -> c14(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, z1))
REACH(z0, z1, z2, z3) -> c15(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), ISEMPTY(z2))
REACH(z0, z1, z2, z3) -> c16(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, from(z2)), FROM(z2))
REACH(z0, z1, z2, z3) -> c17(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z1, to(z2)), TO(z2))
IF1(true, z0, z1, z2, z3, z4, z5, z6) -> c18
IF1(false, z0, z1, z2, z3, z4, z5, z6) -> c19(IF2(z0, z1, z2, z3, z4, z5, z6))
IF2(true, z0, z1, z2, z3, z4, z5) -> c20
IF2(false, z0, z1, z2, z3, z4, z5) -> c21(IF3(z0, z1, z2, z3, z4, z5))
IF3(false, z0, z1, z2, z3, z4) -> c22(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), REST(z3))
IF3(false, z0, z1, z2, z3, z4) -> c23(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), FROM(z3))
IF3(false, z0, z1, z2, z3, z4) -> c24(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), TO(z3))
IF3(true, z0, z1, z2, z3, z4) -> c25(IF4(z0, z1, z2, z3, z4))
IF4(true, z0, z1, z2, z3) -> c26
IF4(false, z0, z1, z2, z3) -> c27(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(z0, z1, rest(z2), z3), REST(z2))
IF4(false, z0, z1, z2, z3) -> c28(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), TO(z2))
IF4(false, z0, z1, z2, z3) -> c29(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), UNION(rest(z2), z3), REST(z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
union(empty, z0) -> z0
union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
isEmpty(empty) -> true
isEmpty(edge(z0, z1, z2)) -> false
from(edge(z0, z1, z2)) -> z0
to(edge(z0, z1, z2)) -> z1
rest(edge(z0, z1, z2)) -> z2
rest(empty) -> empty
reach(z0, z1, z2, z3) -> if1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3)
if1(true, z0, z1, z2, z3, z4, z5, z6) -> true
if1(false, z0, z1, z2, z3, z4, z5, z6) -> if2(z0, z1, z2, z3, z4, z5, z6)
if2(true, z0, z1, z2, z3, z4, z5) -> false
if2(false, z0, z1, z2, z3, z4, z5) -> if3(z0, z1, z2, z3, z4, z5)
if3(false, z0, z1, z2, z3, z4) -> reach(z1, z2, rest(z3), edge(from(z3), to(z3), z4))
if3(true, z0, z1, z2, z3, z4) -> if4(z0, z1, z2, z3, z4)
if4(true, z0, z1, z2, z3) -> true
if4(false, z0, z1, z2, z3) -> or(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty))

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
OR :: true:false -> true:false -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
UNION :: empty:edge -> empty:edge -> c6:c7
empty :: empty:edge
c6 :: c6:c7
edge :: 0':s -> 0':s -> empty:edge -> empty:edge
c7 :: c6:c7 -> c6:c7
ISEMPTY :: empty:edge -> c8:c9
c8 :: c8:c9
c9 :: c8:c9
FROM :: empty:edge -> c10
c10 :: c10
TO :: empty:edge -> c11
c11 :: c11
REST :: empty:edge -> c12:c13
c12 :: c12:c13
c13 :: c12:c13
REACH :: 0':s -> 0':s -> empty:edge -> empty:edge -> c14:c15:c16:c17
c14 :: c18:c19 -> c:c1:c2:c3 -> c14:c15:c16:c17
IF1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c18:c19
eq :: 0':s -> 0':s -> true:false
isEmpty :: empty:edge -> true:false
from :: empty:edge -> 0':s
to :: empty:edge -> 0':s
c15 :: c18:c19 -> c8:c9 -> c14:c15:c16:c17
c16 :: c18:c19 -> c:c1:c2:c3 -> c10 -> c14:c15:c16:c17
c17 :: c18:c19 -> c:c1:c2:c3 -> c11 -> c14:c15:c16:c17
c18 :: c18:c19
c19 :: c20:c21 -> c18:c19
IF2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c20:c21
c20 :: c20:c21
c21 :: c22:c23:c24:c25 -> c20:c21
IF3 :: true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c22:c23:c24:c25
c22 :: c14:c15:c16:c17 -> c12:c13 -> c22:c23:c24:c25
rest :: empty:edge -> empty:edge
c23 :: c14:c15:c16:c17 -> c10 -> c22:c23:c24:c25
c24 :: c14:c15:c16:c17 -> c11 -> c22:c23:c24:c25
c25 :: c26:c27:c28:c29 -> c22:c23:c24:c25
IF4 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c26:c27:c28:c29
c26 :: c26:c27:c28:c29
c27 :: c4:c5 -> c14:c15:c16:c17 -> c12:c13 -> c26:c27:c28:c29
reach :: 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
union :: empty:edge -> empty:edge -> empty:edge
c28 :: c4:c5 -> c14:c15:c16:c17 -> c11 -> c26:c27:c28:c29
c29 :: c4:c5 -> c14:c15:c16:c17 -> c6:c7 -> c12:c13 -> c26:c27:c28:c29
or :: true:false -> true:false -> true:false
if1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if3 :: true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if4 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
hole_c:c1:c2:c31_30 :: c:c1:c2:c3
hole_0':s2_30 :: 0':s
hole_c4:c53_30 :: c4:c5
hole_true:false4_30 :: true:false
hole_c6:c75_30 :: c6:c7
hole_empty:edge6_30 :: empty:edge
hole_c8:c97_30 :: c8:c9
hole_c108_30 :: c10
hole_c119_30 :: c11
hole_c12:c1310_30 :: c12:c13
hole_c14:c15:c16:c1711_30 :: c14:c15:c16:c17
hole_c18:c1912_30 :: c18:c19
hole_c20:c2113_30 :: c20:c21
hole_c22:c23:c24:c2514_30 :: c22:c23:c24:c25
hole_c26:c27:c28:c2915_30 :: c26:c27:c28:c29
gen_c:c1:c2:c316_30 :: Nat -> c:c1:c2:c3
gen_0':s17_30 :: Nat -> 0':s
gen_c6:c718_30 :: Nat -> c6:c7
gen_empty:edge19_30 :: Nat -> empty:edge


Lemmas:
EQ(gen_0':s17_30(n21_30), gen_0':s17_30(n21_30)) -> gen_c:c1:c2:c316_30(n21_30), rt in Omega(1 + n21_30)
UNION(gen_empty:edge19_30(n1111_30), gen_empty:edge19_30(b)) -> gen_c6:c718_30(n1111_30), rt in Omega(1 + n1111_30)
eq(gen_0':s17_30(n2178_30), gen_0':s17_30(n2178_30)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c316_30(0) <=> c
gen_c:c1:c2:c316_30(+(x, 1)) <=> c3(gen_c:c1:c2:c316_30(x))
gen_0':s17_30(0) <=> 0'
gen_0':s17_30(+(x, 1)) <=> s(gen_0':s17_30(x))
gen_c6:c718_30(0) <=> c6
gen_c6:c718_30(+(x, 1)) <=> c7(gen_c6:c718_30(x))
gen_empty:edge19_30(0) <=> empty
gen_empty:edge19_30(+(x, 1)) <=> edge(0', 0', gen_empty:edge19_30(x))


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

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

----------------------------------------

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
union(gen_empty:edge19_30(n2931_30), gen_empty:edge19_30(b)) -> gen_empty:edge19_30(+(n2931_30, b)), rt in Omega(0)

Induction Base:
union(gen_empty:edge19_30(0), gen_empty:edge19_30(b)) ->_R^Omega(0)
gen_empty:edge19_30(b)

Induction Step:
union(gen_empty:edge19_30(+(n2931_30, 1)), gen_empty:edge19_30(b)) ->_R^Omega(0)
edge(0', 0', union(gen_empty:edge19_30(n2931_30), gen_empty:edge19_30(b))) ->_IH
edge(0', 0', gen_empty:edge19_30(+(b, c2932_30)))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(22)
Obligation:
Innermost TRS:
Rules:
EQ(0', 0') -> c
EQ(0', s(z0)) -> c1
EQ(s(z0), 0') -> c2
EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
OR(true, z0) -> c4
OR(false, z0) -> c5
UNION(empty, z0) -> c6
UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
ISEMPTY(empty) -> c8
ISEMPTY(edge(z0, z1, z2)) -> c9
FROM(edge(z0, z1, z2)) -> c10
TO(edge(z0, z1, z2)) -> c11
REST(edge(z0, z1, z2)) -> c12
REST(empty) -> c13
REACH(z0, z1, z2, z3) -> c14(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, z1))
REACH(z0, z1, z2, z3) -> c15(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), ISEMPTY(z2))
REACH(z0, z1, z2, z3) -> c16(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z0, from(z2)), FROM(z2))
REACH(z0, z1, z2, z3) -> c17(IF1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3), EQ(z1, to(z2)), TO(z2))
IF1(true, z0, z1, z2, z3, z4, z5, z6) -> c18
IF1(false, z0, z1, z2, z3, z4, z5, z6) -> c19(IF2(z0, z1, z2, z3, z4, z5, z6))
IF2(true, z0, z1, z2, z3, z4, z5) -> c20
IF2(false, z0, z1, z2, z3, z4, z5) -> c21(IF3(z0, z1, z2, z3, z4, z5))
IF3(false, z0, z1, z2, z3, z4) -> c22(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), REST(z3))
IF3(false, z0, z1, z2, z3, z4) -> c23(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), FROM(z3))
IF3(false, z0, z1, z2, z3, z4) -> c24(REACH(z1, z2, rest(z3), edge(from(z3), to(z3), z4)), TO(z3))
IF3(true, z0, z1, z2, z3, z4) -> c25(IF4(z0, z1, z2, z3, z4))
IF4(true, z0, z1, z2, z3) -> c26
IF4(false, z0, z1, z2, z3) -> c27(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(z0, z1, rest(z2), z3), REST(z2))
IF4(false, z0, z1, z2, z3) -> c28(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), TO(z2))
IF4(false, z0, z1, z2, z3) -> c29(OR(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty)), REACH(to(z2), z1, union(rest(z2), z3), empty), UNION(rest(z2), z3), REST(z2))
eq(0', 0') -> true
eq(0', s(z0)) -> false
eq(s(z0), 0') -> false
eq(s(z0), s(z1)) -> eq(z0, z1)
or(true, z0) -> true
or(false, z0) -> z0
union(empty, z0) -> z0
union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
isEmpty(empty) -> true
isEmpty(edge(z0, z1, z2)) -> false
from(edge(z0, z1, z2)) -> z0
to(edge(z0, z1, z2)) -> z1
rest(edge(z0, z1, z2)) -> z2
rest(empty) -> empty
reach(z0, z1, z2, z3) -> if1(eq(z0, z1), isEmpty(z2), eq(z0, from(z2)), eq(z1, to(z2)), z0, z1, z2, z3)
if1(true, z0, z1, z2, z3, z4, z5, z6) -> true
if1(false, z0, z1, z2, z3, z4, z5, z6) -> if2(z0, z1, z2, z3, z4, z5, z6)
if2(true, z0, z1, z2, z3, z4, z5) -> false
if2(false, z0, z1, z2, z3, z4, z5) -> if3(z0, z1, z2, z3, z4, z5)
if3(false, z0, z1, z2, z3, z4) -> reach(z1, z2, rest(z3), edge(from(z3), to(z3), z4))
if3(true, z0, z1, z2, z3, z4) -> if4(z0, z1, z2, z3, z4)
if4(true, z0, z1, z2, z3) -> true
if4(false, z0, z1, z2, z3) -> or(reach(z0, z1, rest(z2), z3), reach(to(z2), z1, union(rest(z2), z3), empty))

Types:
EQ :: 0':s -> 0':s -> c:c1:c2:c3
0' :: 0':s
c :: c:c1:c2:c3
s :: 0':s -> 0':s
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3 -> c:c1:c2:c3
OR :: true:false -> true:false -> c4:c5
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c4:c5
UNION :: empty:edge -> empty:edge -> c6:c7
empty :: empty:edge
c6 :: c6:c7
edge :: 0':s -> 0':s -> empty:edge -> empty:edge
c7 :: c6:c7 -> c6:c7
ISEMPTY :: empty:edge -> c8:c9
c8 :: c8:c9
c9 :: c8:c9
FROM :: empty:edge -> c10
c10 :: c10
TO :: empty:edge -> c11
c11 :: c11
REST :: empty:edge -> c12:c13
c12 :: c12:c13
c13 :: c12:c13
REACH :: 0':s -> 0':s -> empty:edge -> empty:edge -> c14:c15:c16:c17
c14 :: c18:c19 -> c:c1:c2:c3 -> c14:c15:c16:c17
IF1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c18:c19
eq :: 0':s -> 0':s -> true:false
isEmpty :: empty:edge -> true:false
from :: empty:edge -> 0':s
to :: empty:edge -> 0':s
c15 :: c18:c19 -> c8:c9 -> c14:c15:c16:c17
c16 :: c18:c19 -> c:c1:c2:c3 -> c10 -> c14:c15:c16:c17
c17 :: c18:c19 -> c:c1:c2:c3 -> c11 -> c14:c15:c16:c17
c18 :: c18:c19
c19 :: c20:c21 -> c18:c19
IF2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c20:c21
c20 :: c20:c21
c21 :: c22:c23:c24:c25 -> c20:c21
IF3 :: true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c22:c23:c24:c25
c22 :: c14:c15:c16:c17 -> c12:c13 -> c22:c23:c24:c25
rest :: empty:edge -> empty:edge
c23 :: c14:c15:c16:c17 -> c10 -> c22:c23:c24:c25
c24 :: c14:c15:c16:c17 -> c11 -> c22:c23:c24:c25
c25 :: c26:c27:c28:c29 -> c22:c23:c24:c25
IF4 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c26:c27:c28:c29
c26 :: c26:c27:c28:c29
c27 :: c4:c5 -> c14:c15:c16:c17 -> c12:c13 -> c26:c27:c28:c29
reach :: 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
union :: empty:edge -> empty:edge -> empty:edge
c28 :: c4:c5 -> c14:c15:c16:c17 -> c11 -> c26:c27:c28:c29
c29 :: c4:c5 -> c14:c15:c16:c17 -> c6:c7 -> c12:c13 -> c26:c27:c28:c29
or :: true:false -> true:false -> true:false
if1 :: true:false -> true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if2 :: true:false -> true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if3 :: true:false -> true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
if4 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
hole_c:c1:c2:c31_30 :: c:c1:c2:c3
hole_0':s2_30 :: 0':s
hole_c4:c53_30 :: c4:c5
hole_true:false4_30 :: true:false
hole_c6:c75_30 :: c6:c7
hole_empty:edge6_30 :: empty:edge
hole_c8:c97_30 :: c8:c9
hole_c108_30 :: c10
hole_c119_30 :: c11
hole_c12:c1310_30 :: c12:c13
hole_c14:c15:c16:c1711_30 :: c14:c15:c16:c17
hole_c18:c1912_30 :: c18:c19
hole_c20:c2113_30 :: c20:c21
hole_c22:c23:c24:c2514_30 :: c22:c23:c24:c25
hole_c26:c27:c28:c2915_30 :: c26:c27:c28:c29
gen_c:c1:c2:c316_30 :: Nat -> c:c1:c2:c3
gen_0':s17_30 :: Nat -> 0':s
gen_c6:c718_30 :: Nat -> c6:c7
gen_empty:edge19_30 :: Nat -> empty:edge


Lemmas:
EQ(gen_0':s17_30(n21_30), gen_0':s17_30(n21_30)) -> gen_c:c1:c2:c316_30(n21_30), rt in Omega(1 + n21_30)
UNION(gen_empty:edge19_30(n1111_30), gen_empty:edge19_30(b)) -> gen_c6:c718_30(n1111_30), rt in Omega(1 + n1111_30)
eq(gen_0':s17_30(n2178_30), gen_0':s17_30(n2178_30)) -> true, rt in Omega(0)
union(gen_empty:edge19_30(n2931_30), gen_empty:edge19_30(b)) -> gen_empty:edge19_30(+(n2931_30, b)), rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c316_30(0) <=> c
gen_c:c1:c2:c316_30(+(x, 1)) <=> c3(gen_c:c1:c2:c316_30(x))
gen_0':s17_30(0) <=> 0'
gen_0':s17_30(+(x, 1)) <=> s(gen_0':s17_30(x))
gen_c6:c718_30(0) <=> c6
gen_c6:c718_30(+(x, 1)) <=> c7(gen_c6:c718_30(x))
gen_empty:edge19_30(0) <=> empty
gen_empty:edge19_30(+(x, 1)) <=> edge(0', 0', gen_empty:edge19_30(x))


The following defined symbols remain to be analysed:
reach, REACH

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