WORST_CASE(Omega(n^1),O(n^2))
proof of input_HlHD7uZx8f.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, n^2).

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
    (3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (4) CdtProblem
    (5) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 103 ms]
    (10) CdtProblem
    (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 30 ms]
    (12) CdtProblem
    (13) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 182 ms]
    (14) CdtProblem
    (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 162 ms]
    (16) CdtProblem
    (17) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 135 ms]
    (18) CdtProblem
    (19) CdtKnowledgeProof [FINISHED, 0 ms]
    (20) BOUNDS(1, 1)
(21) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(22) CdtProblem
    (23) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (24) CpxRelTRS
    (25) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (26) CpxRelTRS
    (27) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (28) typed CpxTrs
    (29) OrderProof [LOWER BOUND(ID), 0 ms]
    (30) typed CpxTrs
    (31) RewriteLemmaProof [LOWER BOUND(ID), 430 ms]
    (32) BEST
        (33) proven lower bound
            (34) LowerBoundPropagationProof [FINISHED, 0 ms]
            (35) BOUNDS(n^1, INF)
        (36) typed CpxTrs
            (37) RewriteLemmaProof [LOWER BOUND(ID), 72 ms]
            (38) typed CpxTrs
            (39) RewriteLemmaProof [LOWER BOUND(ID), 69 ms]
            (40) typed CpxTrs
            (41) RewriteLemmaProof [LOWER BOUND(ID), 62 ms]
            (42) typed CpxTrs


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

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


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

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

(1) CpxTrsToCdtProof (UPPER BOUND(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))
   reach(z0, z1, empty, z2) -> false
   reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5)
   if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5)
   if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5))
   if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true
   if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), 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))
   REACH(z0, z1, empty, z2) -> c8
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
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))
   REACH(z0, z1, empty, z2) -> c8
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
K tuples:none
Defined Rule Symbols:   eq_2, or_2, union_2, reach_4, if_reach_1_5, if_reach_2_5

Defined Pair Symbols:   EQ_2, OR_2, UNION_2, REACH_4, IF_REACH_1_5, IF_REACH_2_5

Compound Symbols:   c, c1, c2, c3_1, c4, c5, c6, c7_1, c8, c9_2, c10_2, c11_1, c12, c13_2, c14_3


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

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 8 trailing nodes:
   OR(false, z0) -> c5
   EQ(0, s(z0)) -> c1
   UNION(empty, z0) -> c6
   IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12
   EQ(0, 0) -> c
   REACH(z0, z1, empty, z2) -> c8
   OR(true, z0) -> c4
   EQ(s(z0), 0) -> c2

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

(4)
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))
   reach(z0, z1, empty, z2) -> false
   reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5)
   if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5)
   if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5))
   if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true
   if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty))
Tuples:
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
S tuples:
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
K tuples:none
Defined Rule Symbols:   eq_2, or_2, union_2, reach_4, if_reach_1_5, if_reach_2_5

Defined Pair Symbols:   EQ_2, UNION_2, REACH_4, IF_REACH_1_5, IF_REACH_2_5

Compound Symbols:   c3_1, c7_1, c9_2, c10_2, c11_1, c13_2, c14_3


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

(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 2 trailing tuple parts
----------------------------------------

(6)
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))
   reach(z0, z1, empty, z2) -> false
   reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5)
   if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5)
   if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5))
   if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true
   if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty))
Tuples:
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
S tuples:
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
K tuples:none
Defined Rule Symbols:   eq_2, or_2, union_2, reach_4, if_reach_1_5, if_reach_2_5

Defined Pair Symbols:   EQ_2, UNION_2, REACH_4, IF_REACH_1_5, IF_REACH_2_5

Compound Symbols:   c3_1, c7_1, c9_2, c10_2, c11_1, c13_1, c14_2


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

(7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   or(true, z0) -> true
   or(false, z0) -> z0
   reach(z0, z1, empty, z2) -> false
   reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5)
   if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5)
   if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5))
   if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true
   if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty))

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

(8)
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)
   union(empty, z0) -> z0
   union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
Tuples:
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
S tuples:
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
K tuples:none
Defined Rule Symbols:   eq_2, union_2

Defined Pair Symbols:   EQ_2, UNION_2, REACH_4, IF_REACH_1_5, IF_REACH_2_5

Compound Symbols:   c3_1, c7_1, c9_2, c10_2, c11_1, c13_1, c14_2


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

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
We considered the (Usable) Rules:
   union(empty, z0) -> z0
   union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
And the Tuples:
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(0) = 0
   POL(EQ(x_1, x_2)) = 0
   POL(IF_REACH_1(x_1, x_2, x_3, x_4, x_5)) = [2]x_4 + [2]x_5
   POL(IF_REACH_2(x_1, x_2, x_3, x_4, x_5)) = [2]x_4 + [2]x_5
   POL(REACH(x_1, x_2, x_3, x_4)) = [2]x_3 + [2]x_4
   POL(UNION(x_1, x_2)) = 0
   POL(c10(x_1, x_2)) = x_1 + x_2
   POL(c11(x_1)) = x_1
   POL(c13(x_1)) = x_1
   POL(c14(x_1, x_2)) = x_1 + x_2
   POL(c3(x_1)) = x_1
   POL(c7(x_1)) = x_1
   POL(c9(x_1, x_2)) = x_1 + x_2
   POL(edge(x_1, x_2, x_3)) = [2] + x_3
   POL(empty) = 0
   POL(eq(x_1, x_2)) = 0
   POL(false) = 0
   POL(s(x_1)) = x_1
   POL(true) = [3]
   POL(union(x_1, x_2)) = x_1 + x_2

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

(10)
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)
   union(empty, z0) -> z0
   union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
Tuples:
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
S tuples:
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
K tuples:
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
Defined Rule Symbols:   eq_2, union_2

Defined Pair Symbols:   EQ_2, UNION_2, REACH_4, IF_REACH_1_5, IF_REACH_2_5

Compound Symbols:   c3_1, c7_1, c9_2, c10_2, c11_1, c13_1, c14_2


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

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
We considered the (Usable) Rules:
   union(empty, z0) -> z0
   union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
And the Tuples:
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(0) = 0
   POL(EQ(x_1, x_2)) = 0
   POL(IF_REACH_1(x_1, x_2, x_3, x_4, x_5)) = [1] + x_4 + x_5
   POL(IF_REACH_2(x_1, x_2, x_3, x_4, x_5)) = x_4 + x_5
   POL(REACH(x_1, x_2, x_3, x_4)) = [1] + x_3 + x_4
   POL(UNION(x_1, x_2)) = 0
   POL(c10(x_1, x_2)) = x_1 + x_2
   POL(c11(x_1)) = x_1
   POL(c13(x_1)) = x_1
   POL(c14(x_1, x_2)) = x_1 + x_2
   POL(c3(x_1)) = x_1
   POL(c7(x_1)) = x_1
   POL(c9(x_1, x_2)) = x_1 + x_2
   POL(edge(x_1, x_2, x_3)) = [2] + x_3
   POL(empty) = [1]
   POL(eq(x_1, x_2)) = 0
   POL(false) = 0
   POL(s(x_1)) = x_1
   POL(true) = [3]
   POL(union(x_1, x_2)) = x_1 + x_2

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

(12)
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)
   union(empty, z0) -> z0
   union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
Tuples:
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
S tuples:
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
K tuples:
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
Defined Rule Symbols:   eq_2, union_2

Defined Pair Symbols:   EQ_2, UNION_2, REACH_4, IF_REACH_1_5, IF_REACH_2_5

Compound Symbols:   c3_1, c7_1, c9_2, c10_2, c11_1, c13_1, c14_2


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

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
We considered the (Usable) Rules:
   union(empty, z0) -> z0
   union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
And the Tuples:
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(0) = 0
   POL(EQ(x_1, x_2)) = 0
   POL(IF_REACH_1(x_1, x_2, x_3, x_4, x_5)) = x_5^2 + [2]x_4*x_5 + x_4^2 + x_2*x_4
   POL(IF_REACH_2(x_1, x_2, x_3, x_4, x_5)) = x_5^2 + [2]x_4*x_5 + x_4^2 + x_2*x_4
   POL(REACH(x_1, x_2, x_3, x_4)) = x_4^2 + [2]x_3*x_4 + x_1*x_3 + x_3^2
   POL(UNION(x_1, x_2)) = x_1
   POL(c10(x_1, x_2)) = x_1 + x_2
   POL(c11(x_1)) = x_1
   POL(c13(x_1)) = x_1
   POL(c14(x_1, x_2)) = x_1 + x_2
   POL(c3(x_1)) = x_1
   POL(c7(x_1)) = x_1
   POL(c9(x_1, x_2)) = x_1 + x_2
   POL(edge(x_1, x_2, x_3)) = [1] + x_2 + x_3
   POL(empty) = 0
   POL(eq(x_1, x_2)) = 0
   POL(false) = 0
   POL(s(x_1)) = 0
   POL(true) = 0
   POL(union(x_1, x_2)) = x_1 + x_2

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

(14)
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)
   union(empty, z0) -> z0
   union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
Tuples:
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
S tuples:
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
K tuples:
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
Defined Rule Symbols:   eq_2, union_2

Defined Pair Symbols:   EQ_2, UNION_2, REACH_4, IF_REACH_1_5, IF_REACH_2_5

Compound Symbols:   c3_1, c7_1, c9_2, c10_2, c11_1, c13_1, c14_2


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

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
We considered the (Usable) Rules:
   union(empty, z0) -> z0
   union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
And the Tuples:
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(0) = 0
   POL(EQ(x_1, x_2)) = [2]x_1
   POL(IF_REACH_1(x_1, x_2, x_3, x_4, x_5)) = [2]x_3 + x_5^2 + [2]x_4*x_5 + [2]x_3*x_5 + x_4^2 + [2]x_3*x_4 + [2]x_2*x_4
   POL(IF_REACH_2(x_1, x_2, x_3, x_4, x_5)) = x_5^2 + [2]x_4*x_5 + [2]x_3*x_5 + x_4^2 + [2]x_3*x_4 + [2]x_2*x_4
   POL(REACH(x_1, x_2, x_3, x_4)) = [2]x_1 + [2]x_2 + x_4^2 + [2]x_3*x_4 + [2]x_2*x_4 + [2]x_1*x_3 + x_3^2 + [2]x_2*x_3
   POL(UNION(x_1, x_2)) = 0
   POL(c10(x_1, x_2)) = x_1 + x_2
   POL(c11(x_1)) = x_1
   POL(c13(x_1)) = x_1
   POL(c14(x_1, x_2)) = x_1 + x_2
   POL(c3(x_1)) = x_1
   POL(c7(x_1)) = x_1
   POL(c9(x_1, x_2)) = x_1 + x_2
   POL(edge(x_1, x_2, x_3)) = [1] + x_2 + x_3
   POL(empty) = 0
   POL(eq(x_1, x_2)) = 0
   POL(false) = 0
   POL(s(x_1)) = [1] + x_1
   POL(true) = 0
   POL(union(x_1, x_2)) = x_1 + x_2

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

(16)
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)
   union(empty, z0) -> z0
   union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
Tuples:
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
S tuples:
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
K tuples:
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
Defined Rule Symbols:   eq_2, union_2

Defined Pair Symbols:   EQ_2, UNION_2, REACH_4, IF_REACH_1_5, IF_REACH_2_5

Compound Symbols:   c3_1, c7_1, c9_2, c10_2, c11_1, c13_1, c14_2


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

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
We considered the (Usable) Rules:
   union(empty, z0) -> z0
   union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
And the Tuples:
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(0) = 0
   POL(EQ(x_1, x_2)) = 0
   POL(IF_REACH_1(x_1, x_2, x_3, x_4, x_5)) = [2]x_4 + x_5^2 + [2]x_4*x_5 + x_4^2 + x_2*x_4
   POL(IF_REACH_2(x_1, x_2, x_3, x_4, x_5)) = x_5^2 + [2]x_4*x_5 + x_4^2 + x_2*x_4
   POL(REACH(x_1, x_2, x_3, x_4)) = [2]x_3 + x_4^2 + [2]x_3*x_4 + x_1*x_3 + x_3^2
   POL(UNION(x_1, x_2)) = 0
   POL(c10(x_1, x_2)) = x_1 + x_2
   POL(c11(x_1)) = x_1
   POL(c13(x_1)) = x_1
   POL(c14(x_1, x_2)) = x_1 + x_2
   POL(c3(x_1)) = x_1
   POL(c7(x_1)) = x_1
   POL(c9(x_1, x_2)) = x_1 + x_2
   POL(edge(x_1, x_2, x_3)) = [2] + x_2 + x_3
   POL(empty) = 0
   POL(eq(x_1, x_2)) = 0
   POL(false) = 0
   POL(s(x_1)) = 0
   POL(true) = 0
   POL(union(x_1, x_2)) = x_1 + x_2

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

(18)
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)
   union(empty, z0) -> z0
   union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3))
Tuples:
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
S tuples:
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
K tuples:
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3))
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
Defined Rule Symbols:   eq_2, union_2

Defined Pair Symbols:   EQ_2, UNION_2, REACH_4, IF_REACH_1_5, IF_REACH_2_5

Compound Symbols:   c3_1, c7_1, c9_2, c10_2, c11_1, c13_1, c14_2


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

(19) CdtKnowledgeProof (FINISHED)
The following tuples could be moved from S to K by knowledge propagation:
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   EQ(s(z0), s(z1)) -> c3(EQ(z0, z1))
Now S is empty
----------------------------------------

(20)
BOUNDS(1, 1)

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

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

(22)
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))
   reach(z0, z1, empty, z2) -> false
   reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5)
   if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5)
   if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5))
   if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true
   if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), 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))
   REACH(z0, z1, empty, z2) -> c8
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
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))
   REACH(z0, z1, empty, z2) -> c8
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
K tuples:none
Defined Rule Symbols:   eq_2, or_2, union_2, reach_4, if_reach_1_5, if_reach_2_5

Defined Pair Symbols:   EQ_2, OR_2, UNION_2, REACH_4, IF_REACH_1_5, IF_REACH_2_5

Compound Symbols:   c, c1, c2, c3_1, c4, c5, c6, c7_1, c8, c9_2, c10_2, c11_1, c12, c13_2, c14_3


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

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

(24)
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))
   REACH(z0, z1, empty, z2) -> c8
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))

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))
   reach(z0, z1, empty, z2) -> false
   reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5)
   if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5)
   if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5))
   if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true
   if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty))

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

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

(26)
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))
   REACH(z0, z1, empty, z2) -> c8
   REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
   IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
   IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
   IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5))
   IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))

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))
   reach(z0, z1, empty, z2) -> false
   reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5)
   if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5)
   if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5))
   if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true
   if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty))

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

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

(28)
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))
REACH(z0, z1, empty, z2) -> c8
REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12
IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5))
IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
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))
reach(z0, z1, empty, z2) -> false
reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5)
if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5)
if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5))
if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true
if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), 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
REACH :: 0':s -> 0':s -> empty:edge -> empty:edge -> c8:c9
c8 :: c8:c9
c9 :: c10:c11 -> c:c1:c2:c3 -> c8:c9
IF_REACH_1 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c10:c11
eq :: 0':s -> 0':s -> true:false
c10 :: c12:c13:c14 -> c:c1:c2:c3 -> c10:c11
IF_REACH_2 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c12:c13:c14
c11 :: c8:c9 -> c10:c11
c12 :: c12:c13:c14
c13 :: c4:c5 -> c8:c9 -> c12:c13:c14
reach :: 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
union :: empty:edge -> empty:edge -> empty:edge
c14 :: c4:c5 -> c8:c9 -> c6:c7 -> c12:c13:c14
or :: true:false -> true:false -> 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_c:c1:c2:c31_15 :: c:c1:c2:c3
hole_0':s2_15 :: 0':s
hole_c4:c53_15 :: c4:c5
hole_true:false4_15 :: true:false
hole_c6:c75_15 :: c6:c7
hole_empty:edge6_15 :: empty:edge
hole_c8:c97_15 :: c8:c9
hole_c10:c118_15 :: c10:c11
hole_c12:c13:c149_15 :: c12:c13:c14
gen_c:c1:c2:c310_15 :: Nat -> c:c1:c2:c3
gen_0':s11_15 :: Nat -> 0':s
gen_c6:c712_15 :: Nat -> c6:c7
gen_empty:edge13_15 :: Nat -> empty:edge

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

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

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

(30)
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))
REACH(z0, z1, empty, z2) -> c8
REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12
IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5))
IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
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))
reach(z0, z1, empty, z2) -> false
reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5)
if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5)
if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5))
if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true
if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), 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
REACH :: 0':s -> 0':s -> empty:edge -> empty:edge -> c8:c9
c8 :: c8:c9
c9 :: c10:c11 -> c:c1:c2:c3 -> c8:c9
IF_REACH_1 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c10:c11
eq :: 0':s -> 0':s -> true:false
c10 :: c12:c13:c14 -> c:c1:c2:c3 -> c10:c11
IF_REACH_2 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c12:c13:c14
c11 :: c8:c9 -> c10:c11
c12 :: c12:c13:c14
c13 :: c4:c5 -> c8:c9 -> c12:c13:c14
reach :: 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
union :: empty:edge -> empty:edge -> empty:edge
c14 :: c4:c5 -> c8:c9 -> c6:c7 -> c12:c13:c14
or :: true:false -> true:false -> 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_c:c1:c2:c31_15 :: c:c1:c2:c3
hole_0':s2_15 :: 0':s
hole_c4:c53_15 :: c4:c5
hole_true:false4_15 :: true:false
hole_c6:c75_15 :: c6:c7
hole_empty:edge6_15 :: empty:edge
hole_c8:c97_15 :: c8:c9
hole_c10:c118_15 :: c10:c11
hole_c12:c13:c149_15 :: c12:c13:c14
gen_c:c1:c2:c310_15 :: Nat -> c:c1:c2:c3
gen_0':s11_15 :: Nat -> 0':s
gen_c6:c712_15 :: Nat -> c6:c7
gen_empty:edge13_15 :: Nat -> empty:edge


Generator Equations:
gen_c:c1:c2:c310_15(0) <=> c
gen_c:c1:c2:c310_15(+(x, 1)) <=> c3(gen_c:c1:c2:c310_15(x))
gen_0':s11_15(0) <=> 0'
gen_0':s11_15(+(x, 1)) <=> s(gen_0':s11_15(x))
gen_c6:c712_15(0) <=> c6
gen_c6:c712_15(+(x, 1)) <=> c7(gen_c6:c712_15(x))
gen_empty:edge13_15(0) <=> empty
gen_empty:edge13_15(+(x, 1)) <=> edge(0', 0', gen_empty:edge13_15(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

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

(31) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
EQ(gen_0':s11_15(n15_15), gen_0':s11_15(n15_15)) -> gen_c:c1:c2:c310_15(n15_15), rt in Omega(1 + n15_15)

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

Induction Step:
EQ(gen_0':s11_15(+(n15_15, 1)), gen_0':s11_15(+(n15_15, 1))) ->_R^Omega(1)
c3(EQ(gen_0':s11_15(n15_15), gen_0':s11_15(n15_15))) ->_IH
c3(gen_c:c1:c2:c310_15(c16_15))

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

(32)
Complex Obligation (BEST)

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

(33)
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))
REACH(z0, z1, empty, z2) -> c8
REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12
IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5))
IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
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))
reach(z0, z1, empty, z2) -> false
reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5)
if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5)
if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5))
if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true
if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), 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
REACH :: 0':s -> 0':s -> empty:edge -> empty:edge -> c8:c9
c8 :: c8:c9
c9 :: c10:c11 -> c:c1:c2:c3 -> c8:c9
IF_REACH_1 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c10:c11
eq :: 0':s -> 0':s -> true:false
c10 :: c12:c13:c14 -> c:c1:c2:c3 -> c10:c11
IF_REACH_2 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c12:c13:c14
c11 :: c8:c9 -> c10:c11
c12 :: c12:c13:c14
c13 :: c4:c5 -> c8:c9 -> c12:c13:c14
reach :: 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
union :: empty:edge -> empty:edge -> empty:edge
c14 :: c4:c5 -> c8:c9 -> c6:c7 -> c12:c13:c14
or :: true:false -> true:false -> 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_c:c1:c2:c31_15 :: c:c1:c2:c3
hole_0':s2_15 :: 0':s
hole_c4:c53_15 :: c4:c5
hole_true:false4_15 :: true:false
hole_c6:c75_15 :: c6:c7
hole_empty:edge6_15 :: empty:edge
hole_c8:c97_15 :: c8:c9
hole_c10:c118_15 :: c10:c11
hole_c12:c13:c149_15 :: c12:c13:c14
gen_c:c1:c2:c310_15 :: Nat -> c:c1:c2:c3
gen_0':s11_15 :: Nat -> 0':s
gen_c6:c712_15 :: Nat -> c6:c7
gen_empty:edge13_15 :: Nat -> empty:edge


Generator Equations:
gen_c:c1:c2:c310_15(0) <=> c
gen_c:c1:c2:c310_15(+(x, 1)) <=> c3(gen_c:c1:c2:c310_15(x))
gen_0':s11_15(0) <=> 0'
gen_0':s11_15(+(x, 1)) <=> s(gen_0':s11_15(x))
gen_c6:c712_15(0) <=> c6
gen_c6:c712_15(+(x, 1)) <=> c7(gen_c6:c712_15(x))
gen_empty:edge13_15(0) <=> empty
gen_empty:edge13_15(+(x, 1)) <=> edge(0', 0', gen_empty:edge13_15(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

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

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

(35)
BOUNDS(n^1, INF)

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

(36)
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))
REACH(z0, z1, empty, z2) -> c8
REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12
IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5))
IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
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))
reach(z0, z1, empty, z2) -> false
reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5)
if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5)
if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5))
if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true
if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), 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
REACH :: 0':s -> 0':s -> empty:edge -> empty:edge -> c8:c9
c8 :: c8:c9
c9 :: c10:c11 -> c:c1:c2:c3 -> c8:c9
IF_REACH_1 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c10:c11
eq :: 0':s -> 0':s -> true:false
c10 :: c12:c13:c14 -> c:c1:c2:c3 -> c10:c11
IF_REACH_2 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c12:c13:c14
c11 :: c8:c9 -> c10:c11
c12 :: c12:c13:c14
c13 :: c4:c5 -> c8:c9 -> c12:c13:c14
reach :: 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
union :: empty:edge -> empty:edge -> empty:edge
c14 :: c4:c5 -> c8:c9 -> c6:c7 -> c12:c13:c14
or :: true:false -> true:false -> 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_c:c1:c2:c31_15 :: c:c1:c2:c3
hole_0':s2_15 :: 0':s
hole_c4:c53_15 :: c4:c5
hole_true:false4_15 :: true:false
hole_c6:c75_15 :: c6:c7
hole_empty:edge6_15 :: empty:edge
hole_c8:c97_15 :: c8:c9
hole_c10:c118_15 :: c10:c11
hole_c12:c13:c149_15 :: c12:c13:c14
gen_c:c1:c2:c310_15 :: Nat -> c:c1:c2:c3
gen_0':s11_15 :: Nat -> 0':s
gen_c6:c712_15 :: Nat -> c6:c7
gen_empty:edge13_15 :: Nat -> empty:edge


Lemmas:
EQ(gen_0':s11_15(n15_15), gen_0':s11_15(n15_15)) -> gen_c:c1:c2:c310_15(n15_15), rt in Omega(1 + n15_15)


Generator Equations:
gen_c:c1:c2:c310_15(0) <=> c
gen_c:c1:c2:c310_15(+(x, 1)) <=> c3(gen_c:c1:c2:c310_15(x))
gen_0':s11_15(0) <=> 0'
gen_0':s11_15(+(x, 1)) <=> s(gen_0':s11_15(x))
gen_c6:c712_15(0) <=> c6
gen_c6:c712_15(+(x, 1)) <=> c7(gen_c6:c712_15(x))
gen_empty:edge13_15(0) <=> empty
gen_empty:edge13_15(+(x, 1)) <=> edge(0', 0', gen_empty:edge13_15(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

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

(37) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
UNION(gen_empty:edge13_15(n925_15), gen_empty:edge13_15(b)) -> gen_c6:c712_15(n925_15), rt in Omega(1 + n925_15)

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

Induction Step:
UNION(gen_empty:edge13_15(+(n925_15, 1)), gen_empty:edge13_15(b)) ->_R^Omega(1)
c7(UNION(gen_empty:edge13_15(n925_15), gen_empty:edge13_15(b))) ->_IH
c7(gen_c6:c712_15(c926_15))

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

(38)
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))
REACH(z0, z1, empty, z2) -> c8
REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12
IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5))
IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
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))
reach(z0, z1, empty, z2) -> false
reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5)
if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5)
if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5))
if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true
if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), 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
REACH :: 0':s -> 0':s -> empty:edge -> empty:edge -> c8:c9
c8 :: c8:c9
c9 :: c10:c11 -> c:c1:c2:c3 -> c8:c9
IF_REACH_1 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c10:c11
eq :: 0':s -> 0':s -> true:false
c10 :: c12:c13:c14 -> c:c1:c2:c3 -> c10:c11
IF_REACH_2 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c12:c13:c14
c11 :: c8:c9 -> c10:c11
c12 :: c12:c13:c14
c13 :: c4:c5 -> c8:c9 -> c12:c13:c14
reach :: 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
union :: empty:edge -> empty:edge -> empty:edge
c14 :: c4:c5 -> c8:c9 -> c6:c7 -> c12:c13:c14
or :: true:false -> true:false -> 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_c:c1:c2:c31_15 :: c:c1:c2:c3
hole_0':s2_15 :: 0':s
hole_c4:c53_15 :: c4:c5
hole_true:false4_15 :: true:false
hole_c6:c75_15 :: c6:c7
hole_empty:edge6_15 :: empty:edge
hole_c8:c97_15 :: c8:c9
hole_c10:c118_15 :: c10:c11
hole_c12:c13:c149_15 :: c12:c13:c14
gen_c:c1:c2:c310_15 :: Nat -> c:c1:c2:c3
gen_0':s11_15 :: Nat -> 0':s
gen_c6:c712_15 :: Nat -> c6:c7
gen_empty:edge13_15 :: Nat -> empty:edge


Lemmas:
EQ(gen_0':s11_15(n15_15), gen_0':s11_15(n15_15)) -> gen_c:c1:c2:c310_15(n15_15), rt in Omega(1 + n15_15)
UNION(gen_empty:edge13_15(n925_15), gen_empty:edge13_15(b)) -> gen_c6:c712_15(n925_15), rt in Omega(1 + n925_15)


Generator Equations:
gen_c:c1:c2:c310_15(0) <=> c
gen_c:c1:c2:c310_15(+(x, 1)) <=> c3(gen_c:c1:c2:c310_15(x))
gen_0':s11_15(0) <=> 0'
gen_0':s11_15(+(x, 1)) <=> s(gen_0':s11_15(x))
gen_c6:c712_15(0) <=> c6
gen_c6:c712_15(+(x, 1)) <=> c7(gen_c6:c712_15(x))
gen_empty:edge13_15(0) <=> empty
gen_empty:edge13_15(+(x, 1)) <=> edge(0', 0', gen_empty:edge13_15(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

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

(39) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
eq(gen_0':s11_15(n1668_15), gen_0':s11_15(n1668_15)) -> true, rt in Omega(0)

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

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

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

(40)
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))
REACH(z0, z1, empty, z2) -> c8
REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12
IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5))
IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
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))
reach(z0, z1, empty, z2) -> false
reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5)
if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5)
if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5))
if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true
if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), 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
REACH :: 0':s -> 0':s -> empty:edge -> empty:edge -> c8:c9
c8 :: c8:c9
c9 :: c10:c11 -> c:c1:c2:c3 -> c8:c9
IF_REACH_1 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c10:c11
eq :: 0':s -> 0':s -> true:false
c10 :: c12:c13:c14 -> c:c1:c2:c3 -> c10:c11
IF_REACH_2 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c12:c13:c14
c11 :: c8:c9 -> c10:c11
c12 :: c12:c13:c14
c13 :: c4:c5 -> c8:c9 -> c12:c13:c14
reach :: 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
union :: empty:edge -> empty:edge -> empty:edge
c14 :: c4:c5 -> c8:c9 -> c6:c7 -> c12:c13:c14
or :: true:false -> true:false -> 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_c:c1:c2:c31_15 :: c:c1:c2:c3
hole_0':s2_15 :: 0':s
hole_c4:c53_15 :: c4:c5
hole_true:false4_15 :: true:false
hole_c6:c75_15 :: c6:c7
hole_empty:edge6_15 :: empty:edge
hole_c8:c97_15 :: c8:c9
hole_c10:c118_15 :: c10:c11
hole_c12:c13:c149_15 :: c12:c13:c14
gen_c:c1:c2:c310_15 :: Nat -> c:c1:c2:c3
gen_0':s11_15 :: Nat -> 0':s
gen_c6:c712_15 :: Nat -> c6:c7
gen_empty:edge13_15 :: Nat -> empty:edge


Lemmas:
EQ(gen_0':s11_15(n15_15), gen_0':s11_15(n15_15)) -> gen_c:c1:c2:c310_15(n15_15), rt in Omega(1 + n15_15)
UNION(gen_empty:edge13_15(n925_15), gen_empty:edge13_15(b)) -> gen_c6:c712_15(n925_15), rt in Omega(1 + n925_15)
eq(gen_0':s11_15(n1668_15), gen_0':s11_15(n1668_15)) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c310_15(0) <=> c
gen_c:c1:c2:c310_15(+(x, 1)) <=> c3(gen_c:c1:c2:c310_15(x))
gen_0':s11_15(0) <=> 0'
gen_0':s11_15(+(x, 1)) <=> s(gen_0':s11_15(x))
gen_c6:c712_15(0) <=> c6
gen_c6:c712_15(+(x, 1)) <=> c7(gen_c6:c712_15(x))
gen_empty:edge13_15(0) <=> empty
gen_empty:edge13_15(+(x, 1)) <=> edge(0', 0', gen_empty:edge13_15(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

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

(41) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
union(gen_empty:edge13_15(n2265_15), gen_empty:edge13_15(b)) -> gen_empty:edge13_15(+(n2265_15, b)), rt in Omega(0)

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

Induction Step:
union(gen_empty:edge13_15(+(n2265_15, 1)), gen_empty:edge13_15(b)) ->_R^Omega(0)
edge(0', 0', union(gen_empty:edge13_15(n2265_15), gen_empty:edge13_15(b))) ->_IH
edge(0', 0', gen_empty:edge13_15(+(b, c2266_15)))

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

(42)
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))
REACH(z0, z1, empty, z2) -> c8
REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2))
IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3))
IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5)))
IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12
IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5))
IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5))
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))
reach(z0, z1, empty, z2) -> false
reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5)
if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5)
if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5))
if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true
if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), 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
REACH :: 0':s -> 0':s -> empty:edge -> empty:edge -> c8:c9
c8 :: c8:c9
c9 :: c10:c11 -> c:c1:c2:c3 -> c8:c9
IF_REACH_1 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c10:c11
eq :: 0':s -> 0':s -> true:false
c10 :: c12:c13:c14 -> c:c1:c2:c3 -> c10:c11
IF_REACH_2 :: true:false -> 0':s -> 0':s -> empty:edge -> empty:edge -> c12:c13:c14
c11 :: c8:c9 -> c10:c11
c12 :: c12:c13:c14
c13 :: c4:c5 -> c8:c9 -> c12:c13:c14
reach :: 0':s -> 0':s -> empty:edge -> empty:edge -> true:false
union :: empty:edge -> empty:edge -> empty:edge
c14 :: c4:c5 -> c8:c9 -> c6:c7 -> c12:c13:c14
or :: true:false -> true:false -> 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_c:c1:c2:c31_15 :: c:c1:c2:c3
hole_0':s2_15 :: 0':s
hole_c4:c53_15 :: c4:c5
hole_true:false4_15 :: true:false
hole_c6:c75_15 :: c6:c7
hole_empty:edge6_15 :: empty:edge
hole_c8:c97_15 :: c8:c9
hole_c10:c118_15 :: c10:c11
hole_c12:c13:c149_15 :: c12:c13:c14
gen_c:c1:c2:c310_15 :: Nat -> c:c1:c2:c3
gen_0':s11_15 :: Nat -> 0':s
gen_c6:c712_15 :: Nat -> c6:c7
gen_empty:edge13_15 :: Nat -> empty:edge


Lemmas:
EQ(gen_0':s11_15(n15_15), gen_0':s11_15(n15_15)) -> gen_c:c1:c2:c310_15(n15_15), rt in Omega(1 + n15_15)
UNION(gen_empty:edge13_15(n925_15), gen_empty:edge13_15(b)) -> gen_c6:c712_15(n925_15), rt in Omega(1 + n925_15)
eq(gen_0':s11_15(n1668_15), gen_0':s11_15(n1668_15)) -> true, rt in Omega(0)
union(gen_empty:edge13_15(n2265_15), gen_empty:edge13_15(b)) -> gen_empty:edge13_15(+(n2265_15, b)), rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c310_15(0) <=> c
gen_c:c1:c2:c310_15(+(x, 1)) <=> c3(gen_c:c1:c2:c310_15(x))
gen_0':s11_15(0) <=> 0'
gen_0':s11_15(+(x, 1)) <=> s(gen_0':s11_15(x))
gen_c6:c712_15(0) <=> c6
gen_c6:c712_15(+(x, 1)) <=> c7(gen_c6:c712_15(x))
gen_empty:edge13_15(0) <=> empty
gen_empty:edge13_15(+(x, 1)) <=> edge(0', 0', gen_empty:edge13_15(x))


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

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