WORST_CASE(Omega(n^1),?)
proof of input_ztjSUJ1gJY.trs
# AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 519 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 4 ms]
(4) CdtProblem
(5) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) CpxRelTRS
(9) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(10) typed CpxTrs
(11) OrderProof [LOWER BOUND(ID), 9 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 314 ms]
(14) typed CpxTrs
(15) RewriteLemmaProof [LOWER BOUND(ID), 167 ms]
(16) typed CpxTrs
(17) RewriteLemmaProof [LOWER BOUND(ID), 248 ms]
(18) typed CpxTrs
(19) RewriteLemmaProof [LOWER BOUND(ID), 1587 ms]
(20) BEST
    (21) proven lower bound
        (22) LowerBoundPropagationProof [FINISHED, 0 ms]
        (23) BOUNDS(n^1, INF)
    (24) typed CpxTrs


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

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


The TRS R consists of the following rules:

   getNodeFromEdge(S(S(x')), E(x, y)) -> y
   via(u, v, Cons(E(x, y), xs), edges) -> via[Ite](!EQ(u, x), u, v, Cons(E(x, y), xs), edges)
   getNodeFromEdge(S(0), E(x, y)) -> x
   member(x', Cons(x, xs)) -> member[Ite](eqEdge(x', x), x', Cons(x, xs))
   getNodeFromEdge(0, E(x, y)) -> x
   eqEdge(E(e11, e12), E(e21, e22)) -> eqEdge[Ite](and(!EQ(e11, e21), !EQ(e12, e22)), e21, e22, e11, e12)
   via(u, v, Nil, edges) -> Nil
   notEmpty(Cons(x, xs)) -> True
   notEmpty(Nil) -> False
   member(x, Nil) -> False
   reach(u, v, edges) -> reach[Ite](member(E(u, v), edges), u, v, edges)
   goal(u, v, edges) -> reach(u, v, edges)

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

   !EQ(S(x), S(y)) -> !EQ(x, y)
   !EQ(0, S(y)) -> False
   !EQ(S(x), 0) -> False
   !EQ(0, 0) -> True
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   via[Ite](True, u, v, Cons(E(x, y), xs), edges) -> via[Let](u, v, Cons(E(x, y), xs), edges, reach(y, v, edges))
   via[Let](u, v, Cons(x, xs), edges, Nil) -> via(u, v, xs, edges)
   via[Let](u, v, Cons(x, xs), edges, Cons(x', xs')) -> Cons(x, Cons(x', xs'))
   via[Ite](False, u, v, Cons(x, xs), edges) -> via(u, v, xs, edges)
   member[Ite](False, x', Cons(x, xs)) -> member(x', xs)
   reach[Ite](False, u, v, edges) -> via(u, v, edges, edges)
   reach[Ite](True, u, v, edges) -> Cons(E(u, v), Nil)
   member[Ite](True, x, xs) -> True
   eqEdge[Ite](False, e21, e22, e11, e12) -> False
   eqEdge[Ite](True, e21, e22, e11, e12) -> True

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

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


The TRS R consists of the following rules:

   getNodeFromEdge(S(S(x')), E(x, y)) -> y
   via(u, v, Cons(E(x, y), xs), edges) -> via[Ite](!EQ(u, x), u, v, Cons(E(x, y), xs), edges)
   getNodeFromEdge(S(0), E(x, y)) -> x
   member(x', Cons(x, xs)) -> member[Ite](eqEdge(x', x), x', Cons(x, xs))
   getNodeFromEdge(0, E(x, y)) -> x
   eqEdge(E(e11, e12), E(e21, e22)) -> eqEdge[Ite](and(!EQ(e11, e21), !EQ(e12, e22)), e21, e22, e11, e12)
   via(u, v, Nil, edges) -> Nil
   notEmpty(Cons(x, xs)) -> True
   notEmpty(Nil) -> False
   member(x, Nil) -> False
   reach(u, v, edges) -> reach[Ite](member(E(u, v), edges), u, v, edges)
   goal(u, v, edges) -> reach(u, v, edges)

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

   !EQ(S(x), S(y)) -> !EQ(x, y)
   !EQ(0, S(y)) -> False
   !EQ(S(x), 0) -> False
   !EQ(0, 0) -> True
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   via[Ite](True, u, v, Cons(E(x, y), xs), edges) -> via[Let](u, v, Cons(E(x, y), xs), edges, reach(y, v, edges))
   via[Let](u, v, Cons(x, xs), edges, Nil) -> via(u, v, xs, edges)
   via[Let](u, v, Cons(x, xs), edges, Cons(x', xs')) -> Cons(x, Cons(x', xs'))
   via[Ite](False, u, v, Cons(x, xs), edges) -> via(u, v, xs, edges)
   member[Ite](False, x', Cons(x, xs)) -> member(x', xs)
   reach[Ite](False, u, v, edges) -> via(u, v, edges, edges)
   reach[Ite](True, u, v, edges) -> Cons(E(u, v), Nil)
   member[Ite](True, x, xs) -> True
   eqEdge[Ite](False, e21, e22, e11, e12) -> False
   eqEdge[Ite](True, e21, e22, e11, e12) -> True

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0, S(z0)) -> False
   !EQ(S(z0), 0) -> False
   !EQ(0, 0) -> True
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   via[Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) -> via[Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5))
   via[Ite](False, z0, z1, Cons(z2, z3), z4) -> via(z0, z1, z3, z4)
   via[Let](z0, z1, Cons(z2, z3), z4, Nil) -> via(z0, z1, z3, z4)
   via[Let](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> Cons(z2, Cons(z5, z6))
   member[Ite](False, z0, Cons(z1, z2)) -> member(z0, z2)
   member[Ite](True, z0, z1) -> True
   reach[Ite](False, z0, z1, z2) -> via(z0, z1, z2, z2)
   reach[Ite](True, z0, z1, z2) -> Cons(E(z0, z1), Nil)
   eqEdge[Ite](False, z0, z1, z2, z3) -> False
   eqEdge[Ite](True, z0, z1, z2, z3) -> True
   getNodeFromEdge(S(S(z0)), E(z1, z2)) -> z2
   getNodeFromEdge(S(0), E(z0, z1)) -> z0
   getNodeFromEdge(0, E(z0, z1)) -> z0
   via(z0, z1, Cons(E(z2, z3), z4), z5) -> via[Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5)
   via(z0, z1, Nil, z2) -> Nil
   member(z0, Cons(z1, z2)) -> member[Ite](eqEdge(z0, z1), z0, Cons(z1, z2))
   member(z0, Nil) -> False
   eqEdge(E(z0, z1), E(z2, z3)) -> eqEdge[Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1)
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   reach(z0, z1, z2) -> reach[Ite](member(E(z0, z1), z2), z0, z1, z2)
   goal(z0, z1, z2) -> reach(z0, z1, z2)
Tuples:
   !EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
   !EQ'(0, S(z0)) -> c1
   !EQ'(S(z0), 0) -> c2
   !EQ'(0, 0) -> c3
   AND(False, False) -> c4
   AND(True, False) -> c5
   AND(False, True) -> c6
   AND(True, True) -> c7
   VIA[ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) -> c8(VIA[LET](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)), REACH(z3, z1, z5))
   VIA[ITE](False, z0, z1, Cons(z2, z3), z4) -> c9(VIA(z0, z1, z3, z4))
   VIA[LET](z0, z1, Cons(z2, z3), z4, Nil) -> c10(VIA(z0, z1, z3, z4))
   VIA[LET](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> c11
   MEMBER[ITE](False, z0, Cons(z1, z2)) -> c12(MEMBER(z0, z2))
   MEMBER[ITE](True, z0, z1) -> c13
   REACH[ITE](False, z0, z1, z2) -> c14(VIA(z0, z1, z2, z2))
   REACH[ITE](True, z0, z1, z2) -> c15
   EQEDGE[ITE](False, z0, z1, z2, z3) -> c16
   EQEDGE[ITE](True, z0, z1, z2, z3) -> c17
   GETNODEFROMEDGE(S(S(z0)), E(z1, z2)) -> c18
   GETNODEFROMEDGE(S(0), E(z0, z1)) -> c19
   GETNODEFROMEDGE(0, E(z0, z1)) -> c20
   VIA(z0, z1, Cons(E(z2, z3), z4), z5) -> c21(VIA[ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2))
   VIA(z0, z1, Nil, z2) -> c22
   MEMBER(z0, Cons(z1, z2)) -> c23(MEMBER[ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1))
   MEMBER(z0, Nil) -> c24
   EQEDGE(E(z0, z1), E(z2, z3)) -> c25(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z0, z2))
   EQEDGE(E(z0, z1), E(z2, z3)) -> c26(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z1, z3))
   NOTEMPTY(Cons(z0, z1)) -> c27
   NOTEMPTY(Nil) -> c28
   REACH(z0, z1, z2) -> c29(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2))
   GOAL(z0, z1, z2) -> c30(REACH(z0, z1, z2))
S tuples:
   GETNODEFROMEDGE(S(S(z0)), E(z1, z2)) -> c18
   GETNODEFROMEDGE(S(0), E(z0, z1)) -> c19
   GETNODEFROMEDGE(0, E(z0, z1)) -> c20
   VIA(z0, z1, Cons(E(z2, z3), z4), z5) -> c21(VIA[ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2))
   VIA(z0, z1, Nil, z2) -> c22
   MEMBER(z0, Cons(z1, z2)) -> c23(MEMBER[ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1))
   MEMBER(z0, Nil) -> c24
   EQEDGE(E(z0, z1), E(z2, z3)) -> c25(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z0, z2))
   EQEDGE(E(z0, z1), E(z2, z3)) -> c26(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z1, z3))
   NOTEMPTY(Cons(z0, z1)) -> c27
   NOTEMPTY(Nil) -> c28
   REACH(z0, z1, z2) -> c29(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2))
   GOAL(z0, z1, z2) -> c30(REACH(z0, z1, z2))
K tuples:none
Defined Rule Symbols:   getNodeFromEdge_2, via_4, member_2, eqEdge_2, notEmpty_1, reach_3, goal_3, !EQ_2, and_2, via[Ite]_5, via[Let]_5, member[Ite]_3, reach[Ite]_4, eqEdge[Ite]_5

Defined Pair Symbols:   !EQ'_2, AND_2, VIA[ITE]_5, VIA[LET]_5, MEMBER[ITE]_3, REACH[ITE]_4, EQEDGE[ITE]_5, GETNODEFROMEDGE_2, VIA_4, MEMBER_2, EQEDGE_2, NOTEMPTY_1, REACH_3, GOAL_3

Compound Symbols:   c_1, c1, c2, c3, c4, c5, c6, c7, c8_2, c9_1, c10_1, c11, c12_1, c13, c14_1, c15, c16, c17, c18, c19, c20, c21_2, c22, c23_2, c24, c25_3, c26_3, c27, c28, c29_2, c30_1


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

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

(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:

   GETNODEFROMEDGE(S(S(z0)), E(z1, z2)) -> c18
   GETNODEFROMEDGE(S(0), E(z0, z1)) -> c19
   GETNODEFROMEDGE(0, E(z0, z1)) -> c20
   VIA(z0, z1, Cons(E(z2, z3), z4), z5) -> c21(VIA[ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2))
   VIA(z0, z1, Nil, z2) -> c22
   MEMBER(z0, Cons(z1, z2)) -> c23(MEMBER[ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1))
   MEMBER(z0, Nil) -> c24
   EQEDGE(E(z0, z1), E(z2, z3)) -> c25(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z0, z2))
   EQEDGE(E(z0, z1), E(z2, z3)) -> c26(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z1, z3))
   NOTEMPTY(Cons(z0, z1)) -> c27
   NOTEMPTY(Nil) -> c28
   REACH(z0, z1, z2) -> c29(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2))
   GOAL(z0, z1, z2) -> c30(REACH(z0, z1, z2))

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

   !EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
   !EQ'(0, S(z0)) -> c1
   !EQ'(S(z0), 0) -> c2
   !EQ'(0, 0) -> c3
   AND(False, False) -> c4
   AND(True, False) -> c5
   AND(False, True) -> c6
   AND(True, True) -> c7
   VIA[ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) -> c8(VIA[LET](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)), REACH(z3, z1, z5))
   VIA[ITE](False, z0, z1, Cons(z2, z3), z4) -> c9(VIA(z0, z1, z3, z4))
   VIA[LET](z0, z1, Cons(z2, z3), z4, Nil) -> c10(VIA(z0, z1, z3, z4))
   VIA[LET](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> c11
   MEMBER[ITE](False, z0, Cons(z1, z2)) -> c12(MEMBER(z0, z2))
   MEMBER[ITE](True, z0, z1) -> c13
   REACH[ITE](False, z0, z1, z2) -> c14(VIA(z0, z1, z2, z2))
   REACH[ITE](True, z0, z1, z2) -> c15
   EQEDGE[ITE](False, z0, z1, z2, z3) -> c16
   EQEDGE[ITE](True, z0, z1, z2, z3) -> c17
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0, S(z0)) -> False
   !EQ(S(z0), 0) -> False
   !EQ(0, 0) -> True
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   via[Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) -> via[Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5))
   via[Ite](False, z0, z1, Cons(z2, z3), z4) -> via(z0, z1, z3, z4)
   via[Let](z0, z1, Cons(z2, z3), z4, Nil) -> via(z0, z1, z3, z4)
   via[Let](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> Cons(z2, Cons(z5, z6))
   member[Ite](False, z0, Cons(z1, z2)) -> member(z0, z2)
   member[Ite](True, z0, z1) -> True
   reach[Ite](False, z0, z1, z2) -> via(z0, z1, z2, z2)
   reach[Ite](True, z0, z1, z2) -> Cons(E(z0, z1), Nil)
   eqEdge[Ite](False, z0, z1, z2, z3) -> False
   eqEdge[Ite](True, z0, z1, z2, z3) -> True
   getNodeFromEdge(S(S(z0)), E(z1, z2)) -> z2
   getNodeFromEdge(S(0), E(z0, z1)) -> z0
   getNodeFromEdge(0, E(z0, z1)) -> z0
   via(z0, z1, Cons(E(z2, z3), z4), z5) -> via[Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5)
   via(z0, z1, Nil, z2) -> Nil
   member(z0, Cons(z1, z2)) -> member[Ite](eqEdge(z0, z1), z0, Cons(z1, z2))
   member(z0, Nil) -> False
   eqEdge(E(z0, z1), E(z2, z3)) -> eqEdge[Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1)
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   reach(z0, z1, z2) -> reach[Ite](member(E(z0, z1), z2), z0, z1, z2)
   goal(z0, z1, z2) -> reach(z0, z1, z2)

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

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

(8)
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:

   GETNODEFROMEDGE(S(S(z0)), E(z1, z2)) -> c18
   GETNODEFROMEDGE(S(0'), E(z0, z1)) -> c19
   GETNODEFROMEDGE(0', E(z0, z1)) -> c20
   VIA(z0, z1, Cons(E(z2, z3), z4), z5) -> c21(VIA[ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2))
   VIA(z0, z1, Nil, z2) -> c22
   MEMBER(z0, Cons(z1, z2)) -> c23(MEMBER[ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1))
   MEMBER(z0, Nil) -> c24
   EQEDGE(E(z0, z1), E(z2, z3)) -> c25(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z0, z2))
   EQEDGE(E(z0, z1), E(z2, z3)) -> c26(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z1, z3))
   NOTEMPTY(Cons(z0, z1)) -> c27
   NOTEMPTY(Nil) -> c28
   REACH(z0, z1, z2) -> c29(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2))
   GOAL(z0, z1, z2) -> c30(REACH(z0, z1, z2))

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

   !EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
   !EQ'(0', S(z0)) -> c1
   !EQ'(S(z0), 0') -> c2
   !EQ'(0', 0') -> c3
   AND(False, False) -> c4
   AND(True, False) -> c5
   AND(False, True) -> c6
   AND(True, True) -> c7
   VIA[ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) -> c8(VIA[LET](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)), REACH(z3, z1, z5))
   VIA[ITE](False, z0, z1, Cons(z2, z3), z4) -> c9(VIA(z0, z1, z3, z4))
   VIA[LET](z0, z1, Cons(z2, z3), z4, Nil) -> c10(VIA(z0, z1, z3, z4))
   VIA[LET](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> c11
   MEMBER[ITE](False, z0, Cons(z1, z2)) -> c12(MEMBER(z0, z2))
   MEMBER[ITE](True, z0, z1) -> c13
   REACH[ITE](False, z0, z1, z2) -> c14(VIA(z0, z1, z2, z2))
   REACH[ITE](True, z0, z1, z2) -> c15
   EQEDGE[ITE](False, z0, z1, z2, z3) -> c16
   EQEDGE[ITE](True, z0, z1, z2, z3) -> c17
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0', S(z0)) -> False
   !EQ(S(z0), 0') -> False
   !EQ(0', 0') -> True
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   via[Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) -> via[Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5))
   via[Ite](False, z0, z1, Cons(z2, z3), z4) -> via(z0, z1, z3, z4)
   via[Let](z0, z1, Cons(z2, z3), z4, Nil) -> via(z0, z1, z3, z4)
   via[Let](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> Cons(z2, Cons(z5, z6))
   member[Ite](False, z0, Cons(z1, z2)) -> member(z0, z2)
   member[Ite](True, z0, z1) -> True
   reach[Ite](False, z0, z1, z2) -> via(z0, z1, z2, z2)
   reach[Ite](True, z0, z1, z2) -> Cons(E(z0, z1), Nil)
   eqEdge[Ite](False, z0, z1, z2, z3) -> False
   eqEdge[Ite](True, z0, z1, z2, z3) -> True
   getNodeFromEdge(S(S(z0)), E(z1, z2)) -> z2
   getNodeFromEdge(S(0'), E(z0, z1)) -> z0
   getNodeFromEdge(0', E(z0, z1)) -> z0
   via(z0, z1, Cons(E(z2, z3), z4), z5) -> via[Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5)
   via(z0, z1, Nil, z2) -> Nil
   member(z0, Cons(z1, z2)) -> member[Ite](eqEdge(z0, z1), z0, Cons(z1, z2))
   member(z0, Nil) -> False
   eqEdge(E(z0, z1), E(z2, z3)) -> eqEdge[Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1)
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   reach(z0, z1, z2) -> reach[Ite](member(E(z0, z1), z2), z0, z1, z2)
   goal(z0, z1, z2) -> reach(z0, z1, z2)

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

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

(10)
Obligation:
Innermost TRS:
Rules:
GETNODEFROMEDGE(S(S(z0)), E(z1, z2)) -> c18
GETNODEFROMEDGE(S(0'), E(z0, z1)) -> c19
GETNODEFROMEDGE(0', E(z0, z1)) -> c20
VIA(z0, z1, Cons(E(z2, z3), z4), z5) -> c21(VIA[ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2))
VIA(z0, z1, Nil, z2) -> c22
MEMBER(z0, Cons(z1, z2)) -> c23(MEMBER[ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1))
MEMBER(z0, Nil) -> c24
EQEDGE(E(z0, z1), E(z2, z3)) -> c25(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z0, z2))
EQEDGE(E(z0, z1), E(z2, z3)) -> c26(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z1, z3))
NOTEMPTY(Cons(z0, z1)) -> c27
NOTEMPTY(Nil) -> c28
REACH(z0, z1, z2) -> c29(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2))
GOAL(z0, z1, z2) -> c30(REACH(z0, z1, z2))
!EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c1
!EQ'(S(z0), 0') -> c2
!EQ'(0', 0') -> c3
AND(False, False) -> c4
AND(True, False) -> c5
AND(False, True) -> c6
AND(True, True) -> c7
VIA[ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) -> c8(VIA[LET](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)), REACH(z3, z1, z5))
VIA[ITE](False, z0, z1, Cons(z2, z3), z4) -> c9(VIA(z0, z1, z3, z4))
VIA[LET](z0, z1, Cons(z2, z3), z4, Nil) -> c10(VIA(z0, z1, z3, z4))
VIA[LET](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> c11
MEMBER[ITE](False, z0, Cons(z1, z2)) -> c12(MEMBER(z0, z2))
MEMBER[ITE](True, z0, z1) -> c13
REACH[ITE](False, z0, z1, z2) -> c14(VIA(z0, z1, z2, z2))
REACH[ITE](True, z0, z1, z2) -> c15
EQEDGE[ITE](False, z0, z1, z2, z3) -> c16
EQEDGE[ITE](True, z0, z1, z2, z3) -> c17
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
via[Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) -> via[Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5))
via[Ite](False, z0, z1, Cons(z2, z3), z4) -> via(z0, z1, z3, z4)
via[Let](z0, z1, Cons(z2, z3), z4, Nil) -> via(z0, z1, z3, z4)
via[Let](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> Cons(z2, Cons(z5, z6))
member[Ite](False, z0, Cons(z1, z2)) -> member(z0, z2)
member[Ite](True, z0, z1) -> True
reach[Ite](False, z0, z1, z2) -> via(z0, z1, z2, z2)
reach[Ite](True, z0, z1, z2) -> Cons(E(z0, z1), Nil)
eqEdge[Ite](False, z0, z1, z2, z3) -> False
eqEdge[Ite](True, z0, z1, z2, z3) -> True
getNodeFromEdge(S(S(z0)), E(z1, z2)) -> z2
getNodeFromEdge(S(0'), E(z0, z1)) -> z0
getNodeFromEdge(0', E(z0, z1)) -> z0
via(z0, z1, Cons(E(z2, z3), z4), z5) -> via[Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5)
via(z0, z1, Nil, z2) -> Nil
member(z0, Cons(z1, z2)) -> member[Ite](eqEdge(z0, z1), z0, Cons(z1, z2))
member(z0, Nil) -> False
eqEdge(E(z0, z1), E(z2, z3)) -> eqEdge[Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1)
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
reach(z0, z1, z2) -> reach[Ite](member(E(z0, z1), z2), z0, z1, z2)
goal(z0, z1, z2) -> reach(z0, z1, z2)

Types:
GETNODEFROMEDGE :: S:0' -> E -> c18:c19:c20
S :: S:0' -> S:0'
E :: S:0' -> S:0' -> E
c18 :: c18:c19:c20
0' :: S:0'
c19 :: c18:c19:c20
c20 :: c18:c19:c20
VIA :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> c21:c22
Cons :: E -> Cons:Nil -> Cons:Nil
c21 :: c8:c9 -> c:c1:c2:c3 -> c21:c22
VIA[ITE] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> c8:c9
!EQ :: S:0' -> S:0' -> False:True
!EQ' :: S:0' -> S:0' -> c:c1:c2:c3
Nil :: Cons:Nil
c22 :: c21:c22
MEMBER :: E -> Cons:Nil -> c23:c24
c23 :: c12:c13 -> c25:c26 -> c23:c24
MEMBER[ITE] :: False:True -> E -> Cons:Nil -> c12:c13
eqEdge :: E -> E -> False:True
EQEDGE :: E -> E -> c25:c26
c24 :: c23:c24
c25 :: c16:c17 -> c4:c5:c6:c7 -> c:c1:c2:c3 -> c25:c26
EQEDGE[ITE] :: False:True -> S:0' -> S:0' -> S:0' -> S:0' -> c16:c17
and :: False:True -> False:True -> False:True
AND :: False:True -> False:True -> c4:c5:c6:c7
c26 :: c16:c17 -> c4:c5:c6:c7 -> c:c1:c2:c3 -> c25:c26
NOTEMPTY :: Cons:Nil -> c27:c28
c27 :: c27:c28
c28 :: c27:c28
REACH :: S:0' -> S:0' -> Cons:Nil -> c29
c29 :: c14:c15 -> c23:c24 -> c29
REACH[ITE] :: False:True -> S:0' -> S:0' -> Cons:Nil -> c14:c15
member :: E -> Cons:Nil -> False:True
GOAL :: S:0' -> S:0' -> Cons:Nil -> c30
c30 :: c29 -> c30
c :: c:c1:c2:c3 -> c:c1:c2:c3
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
False :: False:True
c4 :: c4:c5:c6:c7
True :: False:True
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
c8 :: c10:c11 -> c29 -> c8:c9
VIA[LET] :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil -> c10:c11
reach :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
c9 :: c21:c22 -> c8:c9
c10 :: c21:c22 -> c10:c11
c11 :: c10:c11
c12 :: c23:c24 -> c12:c13
c13 :: c12:c13
c14 :: c21:c22 -> c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
via[Ite] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
via[Let] :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil -> Cons:Nil
via :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
member[Ite] :: False:True -> E -> Cons:Nil -> False:True
reach[Ite] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil
eqEdge[Ite] :: False:True -> S:0' -> S:0' -> S:0' -> S:0' -> False:True
getNodeFromEdge :: S:0' -> E -> S:0'
notEmpty :: Cons:Nil -> False:True
goal :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
hole_c18:c19:c201_31 :: c18:c19:c20
hole_S:0'2_31 :: S:0'
hole_E3_31 :: E
hole_c21:c224_31 :: c21:c22
hole_Cons:Nil5_31 :: Cons:Nil
hole_c8:c96_31 :: c8:c9
hole_c:c1:c2:c37_31 :: c:c1:c2:c3
hole_False:True8_31 :: False:True
hole_c23:c249_31 :: c23:c24
hole_c12:c1310_31 :: c12:c13
hole_c25:c2611_31 :: c25:c26
hole_c16:c1712_31 :: c16:c17
hole_c4:c5:c6:c713_31 :: c4:c5:c6:c7
hole_c27:c2814_31 :: c27:c28
hole_c2915_31 :: c29
hole_c14:c1516_31 :: c14:c15
hole_c3017_31 :: c30
hole_c10:c1118_31 :: c10:c11
gen_S:0'19_31 :: Nat -> S:0'
gen_Cons:Nil20_31 :: Nat -> Cons:Nil
gen_c:c1:c2:c321_31 :: Nat -> c:c1:c2:c3

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

(11) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
VIA, !EQ, !EQ', MEMBER, REACH, member, reach, via

They will be analysed ascendingly in the following order:
!EQ < VIA
!EQ' < VIA
VIA = REACH
reach < VIA
!EQ < via
MEMBER < REACH
member < REACH
member < reach
reach = via

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

(12)
Obligation:
Innermost TRS:
Rules:
GETNODEFROMEDGE(S(S(z0)), E(z1, z2)) -> c18
GETNODEFROMEDGE(S(0'), E(z0, z1)) -> c19
GETNODEFROMEDGE(0', E(z0, z1)) -> c20
VIA(z0, z1, Cons(E(z2, z3), z4), z5) -> c21(VIA[ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2))
VIA(z0, z1, Nil, z2) -> c22
MEMBER(z0, Cons(z1, z2)) -> c23(MEMBER[ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1))
MEMBER(z0, Nil) -> c24
EQEDGE(E(z0, z1), E(z2, z3)) -> c25(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z0, z2))
EQEDGE(E(z0, z1), E(z2, z3)) -> c26(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z1, z3))
NOTEMPTY(Cons(z0, z1)) -> c27
NOTEMPTY(Nil) -> c28
REACH(z0, z1, z2) -> c29(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2))
GOAL(z0, z1, z2) -> c30(REACH(z0, z1, z2))
!EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c1
!EQ'(S(z0), 0') -> c2
!EQ'(0', 0') -> c3
AND(False, False) -> c4
AND(True, False) -> c5
AND(False, True) -> c6
AND(True, True) -> c7
VIA[ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) -> c8(VIA[LET](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)), REACH(z3, z1, z5))
VIA[ITE](False, z0, z1, Cons(z2, z3), z4) -> c9(VIA(z0, z1, z3, z4))
VIA[LET](z0, z1, Cons(z2, z3), z4, Nil) -> c10(VIA(z0, z1, z3, z4))
VIA[LET](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> c11
MEMBER[ITE](False, z0, Cons(z1, z2)) -> c12(MEMBER(z0, z2))
MEMBER[ITE](True, z0, z1) -> c13
REACH[ITE](False, z0, z1, z2) -> c14(VIA(z0, z1, z2, z2))
REACH[ITE](True, z0, z1, z2) -> c15
EQEDGE[ITE](False, z0, z1, z2, z3) -> c16
EQEDGE[ITE](True, z0, z1, z2, z3) -> c17
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
via[Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) -> via[Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5))
via[Ite](False, z0, z1, Cons(z2, z3), z4) -> via(z0, z1, z3, z4)
via[Let](z0, z1, Cons(z2, z3), z4, Nil) -> via(z0, z1, z3, z4)
via[Let](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> Cons(z2, Cons(z5, z6))
member[Ite](False, z0, Cons(z1, z2)) -> member(z0, z2)
member[Ite](True, z0, z1) -> True
reach[Ite](False, z0, z1, z2) -> via(z0, z1, z2, z2)
reach[Ite](True, z0, z1, z2) -> Cons(E(z0, z1), Nil)
eqEdge[Ite](False, z0, z1, z2, z3) -> False
eqEdge[Ite](True, z0, z1, z2, z3) -> True
getNodeFromEdge(S(S(z0)), E(z1, z2)) -> z2
getNodeFromEdge(S(0'), E(z0, z1)) -> z0
getNodeFromEdge(0', E(z0, z1)) -> z0
via(z0, z1, Cons(E(z2, z3), z4), z5) -> via[Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5)
via(z0, z1, Nil, z2) -> Nil
member(z0, Cons(z1, z2)) -> member[Ite](eqEdge(z0, z1), z0, Cons(z1, z2))
member(z0, Nil) -> False
eqEdge(E(z0, z1), E(z2, z3)) -> eqEdge[Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1)
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
reach(z0, z1, z2) -> reach[Ite](member(E(z0, z1), z2), z0, z1, z2)
goal(z0, z1, z2) -> reach(z0, z1, z2)

Types:
GETNODEFROMEDGE :: S:0' -> E -> c18:c19:c20
S :: S:0' -> S:0'
E :: S:0' -> S:0' -> E
c18 :: c18:c19:c20
0' :: S:0'
c19 :: c18:c19:c20
c20 :: c18:c19:c20
VIA :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> c21:c22
Cons :: E -> Cons:Nil -> Cons:Nil
c21 :: c8:c9 -> c:c1:c2:c3 -> c21:c22
VIA[ITE] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> c8:c9
!EQ :: S:0' -> S:0' -> False:True
!EQ' :: S:0' -> S:0' -> c:c1:c2:c3
Nil :: Cons:Nil
c22 :: c21:c22
MEMBER :: E -> Cons:Nil -> c23:c24
c23 :: c12:c13 -> c25:c26 -> c23:c24
MEMBER[ITE] :: False:True -> E -> Cons:Nil -> c12:c13
eqEdge :: E -> E -> False:True
EQEDGE :: E -> E -> c25:c26
c24 :: c23:c24
c25 :: c16:c17 -> c4:c5:c6:c7 -> c:c1:c2:c3 -> c25:c26
EQEDGE[ITE] :: False:True -> S:0' -> S:0' -> S:0' -> S:0' -> c16:c17
and :: False:True -> False:True -> False:True
AND :: False:True -> False:True -> c4:c5:c6:c7
c26 :: c16:c17 -> c4:c5:c6:c7 -> c:c1:c2:c3 -> c25:c26
NOTEMPTY :: Cons:Nil -> c27:c28
c27 :: c27:c28
c28 :: c27:c28
REACH :: S:0' -> S:0' -> Cons:Nil -> c29
c29 :: c14:c15 -> c23:c24 -> c29
REACH[ITE] :: False:True -> S:0' -> S:0' -> Cons:Nil -> c14:c15
member :: E -> Cons:Nil -> False:True
GOAL :: S:0' -> S:0' -> Cons:Nil -> c30
c30 :: c29 -> c30
c :: c:c1:c2:c3 -> c:c1:c2:c3
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
False :: False:True
c4 :: c4:c5:c6:c7
True :: False:True
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
c8 :: c10:c11 -> c29 -> c8:c9
VIA[LET] :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil -> c10:c11
reach :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
c9 :: c21:c22 -> c8:c9
c10 :: c21:c22 -> c10:c11
c11 :: c10:c11
c12 :: c23:c24 -> c12:c13
c13 :: c12:c13
c14 :: c21:c22 -> c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
via[Ite] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
via[Let] :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil -> Cons:Nil
via :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
member[Ite] :: False:True -> E -> Cons:Nil -> False:True
reach[Ite] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil
eqEdge[Ite] :: False:True -> S:0' -> S:0' -> S:0' -> S:0' -> False:True
getNodeFromEdge :: S:0' -> E -> S:0'
notEmpty :: Cons:Nil -> False:True
goal :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
hole_c18:c19:c201_31 :: c18:c19:c20
hole_S:0'2_31 :: S:0'
hole_E3_31 :: E
hole_c21:c224_31 :: c21:c22
hole_Cons:Nil5_31 :: Cons:Nil
hole_c8:c96_31 :: c8:c9
hole_c:c1:c2:c37_31 :: c:c1:c2:c3
hole_False:True8_31 :: False:True
hole_c23:c249_31 :: c23:c24
hole_c12:c1310_31 :: c12:c13
hole_c25:c2611_31 :: c25:c26
hole_c16:c1712_31 :: c16:c17
hole_c4:c5:c6:c713_31 :: c4:c5:c6:c7
hole_c27:c2814_31 :: c27:c28
hole_c2915_31 :: c29
hole_c14:c1516_31 :: c14:c15
hole_c3017_31 :: c30
hole_c10:c1118_31 :: c10:c11
gen_S:0'19_31 :: Nat -> S:0'
gen_Cons:Nil20_31 :: Nat -> Cons:Nil
gen_c:c1:c2:c321_31 :: Nat -> c:c1:c2:c3


Generator Equations:
gen_S:0'19_31(0) <=> 0'
gen_S:0'19_31(+(x, 1)) <=> S(gen_S:0'19_31(x))
gen_Cons:Nil20_31(0) <=> Nil
gen_Cons:Nil20_31(+(x, 1)) <=> Cons(E(0', 0'), gen_Cons:Nil20_31(x))
gen_c:c1:c2:c321_31(0) <=> c1
gen_c:c1:c2:c321_31(+(x, 1)) <=> c(gen_c:c1:c2:c321_31(x))


The following defined symbols remain to be analysed:
!EQ, VIA, !EQ', MEMBER, REACH, member, reach, via

They will be analysed ascendingly in the following order:
!EQ < VIA
!EQ' < VIA
VIA = REACH
reach < VIA
!EQ < via
MEMBER < REACH
member < REACH
member < reach
reach = via

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
!EQ(gen_S:0'19_31(n23_31), gen_S:0'19_31(+(1, n23_31))) -> False, rt in Omega(0)

Induction Base:
!EQ(gen_S:0'19_31(0), gen_S:0'19_31(+(1, 0))) ->_R^Omega(0)
False

Induction Step:
!EQ(gen_S:0'19_31(+(n23_31, 1)), gen_S:0'19_31(+(1, +(n23_31, 1)))) ->_R^Omega(0)
!EQ(gen_S:0'19_31(n23_31), gen_S:0'19_31(+(1, n23_31))) ->_IH
False

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

(14)
Obligation:
Innermost TRS:
Rules:
GETNODEFROMEDGE(S(S(z0)), E(z1, z2)) -> c18
GETNODEFROMEDGE(S(0'), E(z0, z1)) -> c19
GETNODEFROMEDGE(0', E(z0, z1)) -> c20
VIA(z0, z1, Cons(E(z2, z3), z4), z5) -> c21(VIA[ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2))
VIA(z0, z1, Nil, z2) -> c22
MEMBER(z0, Cons(z1, z2)) -> c23(MEMBER[ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1))
MEMBER(z0, Nil) -> c24
EQEDGE(E(z0, z1), E(z2, z3)) -> c25(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z0, z2))
EQEDGE(E(z0, z1), E(z2, z3)) -> c26(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z1, z3))
NOTEMPTY(Cons(z0, z1)) -> c27
NOTEMPTY(Nil) -> c28
REACH(z0, z1, z2) -> c29(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2))
GOAL(z0, z1, z2) -> c30(REACH(z0, z1, z2))
!EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c1
!EQ'(S(z0), 0') -> c2
!EQ'(0', 0') -> c3
AND(False, False) -> c4
AND(True, False) -> c5
AND(False, True) -> c6
AND(True, True) -> c7
VIA[ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) -> c8(VIA[LET](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)), REACH(z3, z1, z5))
VIA[ITE](False, z0, z1, Cons(z2, z3), z4) -> c9(VIA(z0, z1, z3, z4))
VIA[LET](z0, z1, Cons(z2, z3), z4, Nil) -> c10(VIA(z0, z1, z3, z4))
VIA[LET](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> c11
MEMBER[ITE](False, z0, Cons(z1, z2)) -> c12(MEMBER(z0, z2))
MEMBER[ITE](True, z0, z1) -> c13
REACH[ITE](False, z0, z1, z2) -> c14(VIA(z0, z1, z2, z2))
REACH[ITE](True, z0, z1, z2) -> c15
EQEDGE[ITE](False, z0, z1, z2, z3) -> c16
EQEDGE[ITE](True, z0, z1, z2, z3) -> c17
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
via[Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) -> via[Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5))
via[Ite](False, z0, z1, Cons(z2, z3), z4) -> via(z0, z1, z3, z4)
via[Let](z0, z1, Cons(z2, z3), z4, Nil) -> via(z0, z1, z3, z4)
via[Let](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> Cons(z2, Cons(z5, z6))
member[Ite](False, z0, Cons(z1, z2)) -> member(z0, z2)
member[Ite](True, z0, z1) -> True
reach[Ite](False, z0, z1, z2) -> via(z0, z1, z2, z2)
reach[Ite](True, z0, z1, z2) -> Cons(E(z0, z1), Nil)
eqEdge[Ite](False, z0, z1, z2, z3) -> False
eqEdge[Ite](True, z0, z1, z2, z3) -> True
getNodeFromEdge(S(S(z0)), E(z1, z2)) -> z2
getNodeFromEdge(S(0'), E(z0, z1)) -> z0
getNodeFromEdge(0', E(z0, z1)) -> z0
via(z0, z1, Cons(E(z2, z3), z4), z5) -> via[Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5)
via(z0, z1, Nil, z2) -> Nil
member(z0, Cons(z1, z2)) -> member[Ite](eqEdge(z0, z1), z0, Cons(z1, z2))
member(z0, Nil) -> False
eqEdge(E(z0, z1), E(z2, z3)) -> eqEdge[Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1)
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
reach(z0, z1, z2) -> reach[Ite](member(E(z0, z1), z2), z0, z1, z2)
goal(z0, z1, z2) -> reach(z0, z1, z2)

Types:
GETNODEFROMEDGE :: S:0' -> E -> c18:c19:c20
S :: S:0' -> S:0'
E :: S:0' -> S:0' -> E
c18 :: c18:c19:c20
0' :: S:0'
c19 :: c18:c19:c20
c20 :: c18:c19:c20
VIA :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> c21:c22
Cons :: E -> Cons:Nil -> Cons:Nil
c21 :: c8:c9 -> c:c1:c2:c3 -> c21:c22
VIA[ITE] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> c8:c9
!EQ :: S:0' -> S:0' -> False:True
!EQ' :: S:0' -> S:0' -> c:c1:c2:c3
Nil :: Cons:Nil
c22 :: c21:c22
MEMBER :: E -> Cons:Nil -> c23:c24
c23 :: c12:c13 -> c25:c26 -> c23:c24
MEMBER[ITE] :: False:True -> E -> Cons:Nil -> c12:c13
eqEdge :: E -> E -> False:True
EQEDGE :: E -> E -> c25:c26
c24 :: c23:c24
c25 :: c16:c17 -> c4:c5:c6:c7 -> c:c1:c2:c3 -> c25:c26
EQEDGE[ITE] :: False:True -> S:0' -> S:0' -> S:0' -> S:0' -> c16:c17
and :: False:True -> False:True -> False:True
AND :: False:True -> False:True -> c4:c5:c6:c7
c26 :: c16:c17 -> c4:c5:c6:c7 -> c:c1:c2:c3 -> c25:c26
NOTEMPTY :: Cons:Nil -> c27:c28
c27 :: c27:c28
c28 :: c27:c28
REACH :: S:0' -> S:0' -> Cons:Nil -> c29
c29 :: c14:c15 -> c23:c24 -> c29
REACH[ITE] :: False:True -> S:0' -> S:0' -> Cons:Nil -> c14:c15
member :: E -> Cons:Nil -> False:True
GOAL :: S:0' -> S:0' -> Cons:Nil -> c30
c30 :: c29 -> c30
c :: c:c1:c2:c3 -> c:c1:c2:c3
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
False :: False:True
c4 :: c4:c5:c6:c7
True :: False:True
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
c8 :: c10:c11 -> c29 -> c8:c9
VIA[LET] :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil -> c10:c11
reach :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
c9 :: c21:c22 -> c8:c9
c10 :: c21:c22 -> c10:c11
c11 :: c10:c11
c12 :: c23:c24 -> c12:c13
c13 :: c12:c13
c14 :: c21:c22 -> c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
via[Ite] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
via[Let] :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil -> Cons:Nil
via :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
member[Ite] :: False:True -> E -> Cons:Nil -> False:True
reach[Ite] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil
eqEdge[Ite] :: False:True -> S:0' -> S:0' -> S:0' -> S:0' -> False:True
getNodeFromEdge :: S:0' -> E -> S:0'
notEmpty :: Cons:Nil -> False:True
goal :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
hole_c18:c19:c201_31 :: c18:c19:c20
hole_S:0'2_31 :: S:0'
hole_E3_31 :: E
hole_c21:c224_31 :: c21:c22
hole_Cons:Nil5_31 :: Cons:Nil
hole_c8:c96_31 :: c8:c9
hole_c:c1:c2:c37_31 :: c:c1:c2:c3
hole_False:True8_31 :: False:True
hole_c23:c249_31 :: c23:c24
hole_c12:c1310_31 :: c12:c13
hole_c25:c2611_31 :: c25:c26
hole_c16:c1712_31 :: c16:c17
hole_c4:c5:c6:c713_31 :: c4:c5:c6:c7
hole_c27:c2814_31 :: c27:c28
hole_c2915_31 :: c29
hole_c14:c1516_31 :: c14:c15
hole_c3017_31 :: c30
hole_c10:c1118_31 :: c10:c11
gen_S:0'19_31 :: Nat -> S:0'
gen_Cons:Nil20_31 :: Nat -> Cons:Nil
gen_c:c1:c2:c321_31 :: Nat -> c:c1:c2:c3


Lemmas:
!EQ(gen_S:0'19_31(n23_31), gen_S:0'19_31(+(1, n23_31))) -> False, rt in Omega(0)


Generator Equations:
gen_S:0'19_31(0) <=> 0'
gen_S:0'19_31(+(x, 1)) <=> S(gen_S:0'19_31(x))
gen_Cons:Nil20_31(0) <=> Nil
gen_Cons:Nil20_31(+(x, 1)) <=> Cons(E(0', 0'), gen_Cons:Nil20_31(x))
gen_c:c1:c2:c321_31(0) <=> c1
gen_c:c1:c2:c321_31(+(x, 1)) <=> c(gen_c:c1:c2:c321_31(x))


The following defined symbols remain to be analysed:
!EQ', VIA, MEMBER, REACH, member, reach, via

They will be analysed ascendingly in the following order:
!EQ' < VIA
VIA = REACH
reach < VIA
MEMBER < REACH
member < REACH
member < reach
reach = via

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

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
!EQ'(gen_S:0'19_31(n596_31), gen_S:0'19_31(+(1, n596_31))) -> gen_c:c1:c2:c321_31(n596_31), rt in Omega(0)

Induction Base:
!EQ'(gen_S:0'19_31(0), gen_S:0'19_31(+(1, 0))) ->_R^Omega(0)
c1

Induction Step:
!EQ'(gen_S:0'19_31(+(n596_31, 1)), gen_S:0'19_31(+(1, +(n596_31, 1)))) ->_R^Omega(0)
c(!EQ'(gen_S:0'19_31(n596_31), gen_S:0'19_31(+(1, n596_31)))) ->_IH
c(gen_c:c1:c2:c321_31(c597_31))

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

(16)
Obligation:
Innermost TRS:
Rules:
GETNODEFROMEDGE(S(S(z0)), E(z1, z2)) -> c18
GETNODEFROMEDGE(S(0'), E(z0, z1)) -> c19
GETNODEFROMEDGE(0', E(z0, z1)) -> c20
VIA(z0, z1, Cons(E(z2, z3), z4), z5) -> c21(VIA[ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2))
VIA(z0, z1, Nil, z2) -> c22
MEMBER(z0, Cons(z1, z2)) -> c23(MEMBER[ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1))
MEMBER(z0, Nil) -> c24
EQEDGE(E(z0, z1), E(z2, z3)) -> c25(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z0, z2))
EQEDGE(E(z0, z1), E(z2, z3)) -> c26(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z1, z3))
NOTEMPTY(Cons(z0, z1)) -> c27
NOTEMPTY(Nil) -> c28
REACH(z0, z1, z2) -> c29(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2))
GOAL(z0, z1, z2) -> c30(REACH(z0, z1, z2))
!EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c1
!EQ'(S(z0), 0') -> c2
!EQ'(0', 0') -> c3
AND(False, False) -> c4
AND(True, False) -> c5
AND(False, True) -> c6
AND(True, True) -> c7
VIA[ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) -> c8(VIA[LET](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)), REACH(z3, z1, z5))
VIA[ITE](False, z0, z1, Cons(z2, z3), z4) -> c9(VIA(z0, z1, z3, z4))
VIA[LET](z0, z1, Cons(z2, z3), z4, Nil) -> c10(VIA(z0, z1, z3, z4))
VIA[LET](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> c11
MEMBER[ITE](False, z0, Cons(z1, z2)) -> c12(MEMBER(z0, z2))
MEMBER[ITE](True, z0, z1) -> c13
REACH[ITE](False, z0, z1, z2) -> c14(VIA(z0, z1, z2, z2))
REACH[ITE](True, z0, z1, z2) -> c15
EQEDGE[ITE](False, z0, z1, z2, z3) -> c16
EQEDGE[ITE](True, z0, z1, z2, z3) -> c17
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
via[Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) -> via[Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5))
via[Ite](False, z0, z1, Cons(z2, z3), z4) -> via(z0, z1, z3, z4)
via[Let](z0, z1, Cons(z2, z3), z4, Nil) -> via(z0, z1, z3, z4)
via[Let](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> Cons(z2, Cons(z5, z6))
member[Ite](False, z0, Cons(z1, z2)) -> member(z0, z2)
member[Ite](True, z0, z1) -> True
reach[Ite](False, z0, z1, z2) -> via(z0, z1, z2, z2)
reach[Ite](True, z0, z1, z2) -> Cons(E(z0, z1), Nil)
eqEdge[Ite](False, z0, z1, z2, z3) -> False
eqEdge[Ite](True, z0, z1, z2, z3) -> True
getNodeFromEdge(S(S(z0)), E(z1, z2)) -> z2
getNodeFromEdge(S(0'), E(z0, z1)) -> z0
getNodeFromEdge(0', E(z0, z1)) -> z0
via(z0, z1, Cons(E(z2, z3), z4), z5) -> via[Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5)
via(z0, z1, Nil, z2) -> Nil
member(z0, Cons(z1, z2)) -> member[Ite](eqEdge(z0, z1), z0, Cons(z1, z2))
member(z0, Nil) -> False
eqEdge(E(z0, z1), E(z2, z3)) -> eqEdge[Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1)
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
reach(z0, z1, z2) -> reach[Ite](member(E(z0, z1), z2), z0, z1, z2)
goal(z0, z1, z2) -> reach(z0, z1, z2)

Types:
GETNODEFROMEDGE :: S:0' -> E -> c18:c19:c20
S :: S:0' -> S:0'
E :: S:0' -> S:0' -> E
c18 :: c18:c19:c20
0' :: S:0'
c19 :: c18:c19:c20
c20 :: c18:c19:c20
VIA :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> c21:c22
Cons :: E -> Cons:Nil -> Cons:Nil
c21 :: c8:c9 -> c:c1:c2:c3 -> c21:c22
VIA[ITE] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> c8:c9
!EQ :: S:0' -> S:0' -> False:True
!EQ' :: S:0' -> S:0' -> c:c1:c2:c3
Nil :: Cons:Nil
c22 :: c21:c22
MEMBER :: E -> Cons:Nil -> c23:c24
c23 :: c12:c13 -> c25:c26 -> c23:c24
MEMBER[ITE] :: False:True -> E -> Cons:Nil -> c12:c13
eqEdge :: E -> E -> False:True
EQEDGE :: E -> E -> c25:c26
c24 :: c23:c24
c25 :: c16:c17 -> c4:c5:c6:c7 -> c:c1:c2:c3 -> c25:c26
EQEDGE[ITE] :: False:True -> S:0' -> S:0' -> S:0' -> S:0' -> c16:c17
and :: False:True -> False:True -> False:True
AND :: False:True -> False:True -> c4:c5:c6:c7
c26 :: c16:c17 -> c4:c5:c6:c7 -> c:c1:c2:c3 -> c25:c26
NOTEMPTY :: Cons:Nil -> c27:c28
c27 :: c27:c28
c28 :: c27:c28
REACH :: S:0' -> S:0' -> Cons:Nil -> c29
c29 :: c14:c15 -> c23:c24 -> c29
REACH[ITE] :: False:True -> S:0' -> S:0' -> Cons:Nil -> c14:c15
member :: E -> Cons:Nil -> False:True
GOAL :: S:0' -> S:0' -> Cons:Nil -> c30
c30 :: c29 -> c30
c :: c:c1:c2:c3 -> c:c1:c2:c3
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
False :: False:True
c4 :: c4:c5:c6:c7
True :: False:True
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
c8 :: c10:c11 -> c29 -> c8:c9
VIA[LET] :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil -> c10:c11
reach :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
c9 :: c21:c22 -> c8:c9
c10 :: c21:c22 -> c10:c11
c11 :: c10:c11
c12 :: c23:c24 -> c12:c13
c13 :: c12:c13
c14 :: c21:c22 -> c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
via[Ite] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
via[Let] :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil -> Cons:Nil
via :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
member[Ite] :: False:True -> E -> Cons:Nil -> False:True
reach[Ite] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil
eqEdge[Ite] :: False:True -> S:0' -> S:0' -> S:0' -> S:0' -> False:True
getNodeFromEdge :: S:0' -> E -> S:0'
notEmpty :: Cons:Nil -> False:True
goal :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
hole_c18:c19:c201_31 :: c18:c19:c20
hole_S:0'2_31 :: S:0'
hole_E3_31 :: E
hole_c21:c224_31 :: c21:c22
hole_Cons:Nil5_31 :: Cons:Nil
hole_c8:c96_31 :: c8:c9
hole_c:c1:c2:c37_31 :: c:c1:c2:c3
hole_False:True8_31 :: False:True
hole_c23:c249_31 :: c23:c24
hole_c12:c1310_31 :: c12:c13
hole_c25:c2611_31 :: c25:c26
hole_c16:c1712_31 :: c16:c17
hole_c4:c5:c6:c713_31 :: c4:c5:c6:c7
hole_c27:c2814_31 :: c27:c28
hole_c2915_31 :: c29
hole_c14:c1516_31 :: c14:c15
hole_c3017_31 :: c30
hole_c10:c1118_31 :: c10:c11
gen_S:0'19_31 :: Nat -> S:0'
gen_Cons:Nil20_31 :: Nat -> Cons:Nil
gen_c:c1:c2:c321_31 :: Nat -> c:c1:c2:c3


Lemmas:
!EQ(gen_S:0'19_31(n23_31), gen_S:0'19_31(+(1, n23_31))) -> False, rt in Omega(0)
!EQ'(gen_S:0'19_31(n596_31), gen_S:0'19_31(+(1, n596_31))) -> gen_c:c1:c2:c321_31(n596_31), rt in Omega(0)


Generator Equations:
gen_S:0'19_31(0) <=> 0'
gen_S:0'19_31(+(x, 1)) <=> S(gen_S:0'19_31(x))
gen_Cons:Nil20_31(0) <=> Nil
gen_Cons:Nil20_31(+(x, 1)) <=> Cons(E(0', 0'), gen_Cons:Nil20_31(x))
gen_c:c1:c2:c321_31(0) <=> c1
gen_c:c1:c2:c321_31(+(x, 1)) <=> c(gen_c:c1:c2:c321_31(x))


The following defined symbols remain to be analysed:
MEMBER, VIA, REACH, member, reach, via

They will be analysed ascendingly in the following order:
VIA = REACH
reach < VIA
MEMBER < REACH
member < REACH
member < reach
reach = via

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
via(gen_S:0'19_31(1), gen_S:0'19_31(b), gen_Cons:Nil20_31(n2678_31), gen_Cons:Nil20_31(d)) -> gen_Cons:Nil20_31(0), rt in Omega(0)

Induction Base:
via(gen_S:0'19_31(1), gen_S:0'19_31(b), gen_Cons:Nil20_31(0), gen_Cons:Nil20_31(d)) ->_R^Omega(0)
Nil

Induction Step:
via(gen_S:0'19_31(1), gen_S:0'19_31(b), gen_Cons:Nil20_31(+(n2678_31, 1)), gen_Cons:Nil20_31(d)) ->_R^Omega(0)
via[Ite](!EQ(gen_S:0'19_31(1), 0'), gen_S:0'19_31(1), gen_S:0'19_31(b), Cons(E(0', 0'), gen_Cons:Nil20_31(n2678_31)), gen_Cons:Nil20_31(d)) ->_R^Omega(0)
via[Ite](False, gen_S:0'19_31(1), gen_S:0'19_31(b), Cons(E(0', 0'), gen_Cons:Nil20_31(n2678_31)), gen_Cons:Nil20_31(d)) ->_R^Omega(0)
via(gen_S:0'19_31(1), gen_S:0'19_31(b), gen_Cons:Nil20_31(n2678_31), gen_Cons:Nil20_31(d)) ->_IH
gen_Cons:Nil20_31(0)

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

(18)
Obligation:
Innermost TRS:
Rules:
GETNODEFROMEDGE(S(S(z0)), E(z1, z2)) -> c18
GETNODEFROMEDGE(S(0'), E(z0, z1)) -> c19
GETNODEFROMEDGE(0', E(z0, z1)) -> c20
VIA(z0, z1, Cons(E(z2, z3), z4), z5) -> c21(VIA[ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2))
VIA(z0, z1, Nil, z2) -> c22
MEMBER(z0, Cons(z1, z2)) -> c23(MEMBER[ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1))
MEMBER(z0, Nil) -> c24
EQEDGE(E(z0, z1), E(z2, z3)) -> c25(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z0, z2))
EQEDGE(E(z0, z1), E(z2, z3)) -> c26(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z1, z3))
NOTEMPTY(Cons(z0, z1)) -> c27
NOTEMPTY(Nil) -> c28
REACH(z0, z1, z2) -> c29(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2))
GOAL(z0, z1, z2) -> c30(REACH(z0, z1, z2))
!EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c1
!EQ'(S(z0), 0') -> c2
!EQ'(0', 0') -> c3
AND(False, False) -> c4
AND(True, False) -> c5
AND(False, True) -> c6
AND(True, True) -> c7
VIA[ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) -> c8(VIA[LET](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)), REACH(z3, z1, z5))
VIA[ITE](False, z0, z1, Cons(z2, z3), z4) -> c9(VIA(z0, z1, z3, z4))
VIA[LET](z0, z1, Cons(z2, z3), z4, Nil) -> c10(VIA(z0, z1, z3, z4))
VIA[LET](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> c11
MEMBER[ITE](False, z0, Cons(z1, z2)) -> c12(MEMBER(z0, z2))
MEMBER[ITE](True, z0, z1) -> c13
REACH[ITE](False, z0, z1, z2) -> c14(VIA(z0, z1, z2, z2))
REACH[ITE](True, z0, z1, z2) -> c15
EQEDGE[ITE](False, z0, z1, z2, z3) -> c16
EQEDGE[ITE](True, z0, z1, z2, z3) -> c17
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
via[Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) -> via[Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5))
via[Ite](False, z0, z1, Cons(z2, z3), z4) -> via(z0, z1, z3, z4)
via[Let](z0, z1, Cons(z2, z3), z4, Nil) -> via(z0, z1, z3, z4)
via[Let](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> Cons(z2, Cons(z5, z6))
member[Ite](False, z0, Cons(z1, z2)) -> member(z0, z2)
member[Ite](True, z0, z1) -> True
reach[Ite](False, z0, z1, z2) -> via(z0, z1, z2, z2)
reach[Ite](True, z0, z1, z2) -> Cons(E(z0, z1), Nil)
eqEdge[Ite](False, z0, z1, z2, z3) -> False
eqEdge[Ite](True, z0, z1, z2, z3) -> True
getNodeFromEdge(S(S(z0)), E(z1, z2)) -> z2
getNodeFromEdge(S(0'), E(z0, z1)) -> z0
getNodeFromEdge(0', E(z0, z1)) -> z0
via(z0, z1, Cons(E(z2, z3), z4), z5) -> via[Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5)
via(z0, z1, Nil, z2) -> Nil
member(z0, Cons(z1, z2)) -> member[Ite](eqEdge(z0, z1), z0, Cons(z1, z2))
member(z0, Nil) -> False
eqEdge(E(z0, z1), E(z2, z3)) -> eqEdge[Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1)
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
reach(z0, z1, z2) -> reach[Ite](member(E(z0, z1), z2), z0, z1, z2)
goal(z0, z1, z2) -> reach(z0, z1, z2)

Types:
GETNODEFROMEDGE :: S:0' -> E -> c18:c19:c20
S :: S:0' -> S:0'
E :: S:0' -> S:0' -> E
c18 :: c18:c19:c20
0' :: S:0'
c19 :: c18:c19:c20
c20 :: c18:c19:c20
VIA :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> c21:c22
Cons :: E -> Cons:Nil -> Cons:Nil
c21 :: c8:c9 -> c:c1:c2:c3 -> c21:c22
VIA[ITE] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> c8:c9
!EQ :: S:0' -> S:0' -> False:True
!EQ' :: S:0' -> S:0' -> c:c1:c2:c3
Nil :: Cons:Nil
c22 :: c21:c22
MEMBER :: E -> Cons:Nil -> c23:c24
c23 :: c12:c13 -> c25:c26 -> c23:c24
MEMBER[ITE] :: False:True -> E -> Cons:Nil -> c12:c13
eqEdge :: E -> E -> False:True
EQEDGE :: E -> E -> c25:c26
c24 :: c23:c24
c25 :: c16:c17 -> c4:c5:c6:c7 -> c:c1:c2:c3 -> c25:c26
EQEDGE[ITE] :: False:True -> S:0' -> S:0' -> S:0' -> S:0' -> c16:c17
and :: False:True -> False:True -> False:True
AND :: False:True -> False:True -> c4:c5:c6:c7
c26 :: c16:c17 -> c4:c5:c6:c7 -> c:c1:c2:c3 -> c25:c26
NOTEMPTY :: Cons:Nil -> c27:c28
c27 :: c27:c28
c28 :: c27:c28
REACH :: S:0' -> S:0' -> Cons:Nil -> c29
c29 :: c14:c15 -> c23:c24 -> c29
REACH[ITE] :: False:True -> S:0' -> S:0' -> Cons:Nil -> c14:c15
member :: E -> Cons:Nil -> False:True
GOAL :: S:0' -> S:0' -> Cons:Nil -> c30
c30 :: c29 -> c30
c :: c:c1:c2:c3 -> c:c1:c2:c3
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
False :: False:True
c4 :: c4:c5:c6:c7
True :: False:True
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
c8 :: c10:c11 -> c29 -> c8:c9
VIA[LET] :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil -> c10:c11
reach :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
c9 :: c21:c22 -> c8:c9
c10 :: c21:c22 -> c10:c11
c11 :: c10:c11
c12 :: c23:c24 -> c12:c13
c13 :: c12:c13
c14 :: c21:c22 -> c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
via[Ite] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
via[Let] :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil -> Cons:Nil
via :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
member[Ite] :: False:True -> E -> Cons:Nil -> False:True
reach[Ite] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil
eqEdge[Ite] :: False:True -> S:0' -> S:0' -> S:0' -> S:0' -> False:True
getNodeFromEdge :: S:0' -> E -> S:0'
notEmpty :: Cons:Nil -> False:True
goal :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
hole_c18:c19:c201_31 :: c18:c19:c20
hole_S:0'2_31 :: S:0'
hole_E3_31 :: E
hole_c21:c224_31 :: c21:c22
hole_Cons:Nil5_31 :: Cons:Nil
hole_c8:c96_31 :: c8:c9
hole_c:c1:c2:c37_31 :: c:c1:c2:c3
hole_False:True8_31 :: False:True
hole_c23:c249_31 :: c23:c24
hole_c12:c1310_31 :: c12:c13
hole_c25:c2611_31 :: c25:c26
hole_c16:c1712_31 :: c16:c17
hole_c4:c5:c6:c713_31 :: c4:c5:c6:c7
hole_c27:c2814_31 :: c27:c28
hole_c2915_31 :: c29
hole_c14:c1516_31 :: c14:c15
hole_c3017_31 :: c30
hole_c10:c1118_31 :: c10:c11
gen_S:0'19_31 :: Nat -> S:0'
gen_Cons:Nil20_31 :: Nat -> Cons:Nil
gen_c:c1:c2:c321_31 :: Nat -> c:c1:c2:c3


Lemmas:
!EQ(gen_S:0'19_31(n23_31), gen_S:0'19_31(+(1, n23_31))) -> False, rt in Omega(0)
!EQ'(gen_S:0'19_31(n596_31), gen_S:0'19_31(+(1, n596_31))) -> gen_c:c1:c2:c321_31(n596_31), rt in Omega(0)
via(gen_S:0'19_31(1), gen_S:0'19_31(b), gen_Cons:Nil20_31(n2678_31), gen_Cons:Nil20_31(d)) -> gen_Cons:Nil20_31(0), rt in Omega(0)


Generator Equations:
gen_S:0'19_31(0) <=> 0'
gen_S:0'19_31(+(x, 1)) <=> S(gen_S:0'19_31(x))
gen_Cons:Nil20_31(0) <=> Nil
gen_Cons:Nil20_31(+(x, 1)) <=> Cons(E(0', 0'), gen_Cons:Nil20_31(x))
gen_c:c1:c2:c321_31(0) <=> c1
gen_c:c1:c2:c321_31(+(x, 1)) <=> c(gen_c:c1:c2:c321_31(x))


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

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

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
VIA(gen_S:0'19_31(1), gen_S:0'19_31(b), gen_Cons:Nil20_31(+(1, n13024_31)), gen_Cons:Nil20_31(d)) -> *22_31, rt in Omega(n13024_31)

Induction Base:
VIA(gen_S:0'19_31(1), gen_S:0'19_31(b), gen_Cons:Nil20_31(+(1, 0)), gen_Cons:Nil20_31(d))

Induction Step:
VIA(gen_S:0'19_31(1), gen_S:0'19_31(b), gen_Cons:Nil20_31(+(1, +(n13024_31, 1))), gen_Cons:Nil20_31(d)) ->_R^Omega(1)
c21(VIA[ITE](!EQ(gen_S:0'19_31(1), 0'), gen_S:0'19_31(1), gen_S:0'19_31(b), Cons(E(0', 0'), gen_Cons:Nil20_31(+(1, n13024_31))), gen_Cons:Nil20_31(d)), !EQ'(gen_S:0'19_31(1), 0')) ->_R^Omega(0)
c21(VIA[ITE](False, gen_S:0'19_31(1), gen_S:0'19_31(b), Cons(E(0', 0'), gen_Cons:Nil20_31(+(1, n13024_31))), gen_Cons:Nil20_31(d)), !EQ'(gen_S:0'19_31(1), 0')) ->_R^Omega(0)
c21(c9(VIA(gen_S:0'19_31(1), gen_S:0'19_31(b), gen_Cons:Nil20_31(+(1, n13024_31)), gen_Cons:Nil20_31(d))), !EQ'(gen_S:0'19_31(1), 0')) ->_IH
c21(c9(*22_31), !EQ'(gen_S:0'19_31(1), 0')) ->_R^Omega(0)
c21(c9(*22_31), c2)

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

(20)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
GETNODEFROMEDGE(S(S(z0)), E(z1, z2)) -> c18
GETNODEFROMEDGE(S(0'), E(z0, z1)) -> c19
GETNODEFROMEDGE(0', E(z0, z1)) -> c20
VIA(z0, z1, Cons(E(z2, z3), z4), z5) -> c21(VIA[ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2))
VIA(z0, z1, Nil, z2) -> c22
MEMBER(z0, Cons(z1, z2)) -> c23(MEMBER[ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1))
MEMBER(z0, Nil) -> c24
EQEDGE(E(z0, z1), E(z2, z3)) -> c25(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z0, z2))
EQEDGE(E(z0, z1), E(z2, z3)) -> c26(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z1, z3))
NOTEMPTY(Cons(z0, z1)) -> c27
NOTEMPTY(Nil) -> c28
REACH(z0, z1, z2) -> c29(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2))
GOAL(z0, z1, z2) -> c30(REACH(z0, z1, z2))
!EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c1
!EQ'(S(z0), 0') -> c2
!EQ'(0', 0') -> c3
AND(False, False) -> c4
AND(True, False) -> c5
AND(False, True) -> c6
AND(True, True) -> c7
VIA[ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) -> c8(VIA[LET](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)), REACH(z3, z1, z5))
VIA[ITE](False, z0, z1, Cons(z2, z3), z4) -> c9(VIA(z0, z1, z3, z4))
VIA[LET](z0, z1, Cons(z2, z3), z4, Nil) -> c10(VIA(z0, z1, z3, z4))
VIA[LET](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> c11
MEMBER[ITE](False, z0, Cons(z1, z2)) -> c12(MEMBER(z0, z2))
MEMBER[ITE](True, z0, z1) -> c13
REACH[ITE](False, z0, z1, z2) -> c14(VIA(z0, z1, z2, z2))
REACH[ITE](True, z0, z1, z2) -> c15
EQEDGE[ITE](False, z0, z1, z2, z3) -> c16
EQEDGE[ITE](True, z0, z1, z2, z3) -> c17
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
via[Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) -> via[Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5))
via[Ite](False, z0, z1, Cons(z2, z3), z4) -> via(z0, z1, z3, z4)
via[Let](z0, z1, Cons(z2, z3), z4, Nil) -> via(z0, z1, z3, z4)
via[Let](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> Cons(z2, Cons(z5, z6))
member[Ite](False, z0, Cons(z1, z2)) -> member(z0, z2)
member[Ite](True, z0, z1) -> True
reach[Ite](False, z0, z1, z2) -> via(z0, z1, z2, z2)
reach[Ite](True, z0, z1, z2) -> Cons(E(z0, z1), Nil)
eqEdge[Ite](False, z0, z1, z2, z3) -> False
eqEdge[Ite](True, z0, z1, z2, z3) -> True
getNodeFromEdge(S(S(z0)), E(z1, z2)) -> z2
getNodeFromEdge(S(0'), E(z0, z1)) -> z0
getNodeFromEdge(0', E(z0, z1)) -> z0
via(z0, z1, Cons(E(z2, z3), z4), z5) -> via[Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5)
via(z0, z1, Nil, z2) -> Nil
member(z0, Cons(z1, z2)) -> member[Ite](eqEdge(z0, z1), z0, Cons(z1, z2))
member(z0, Nil) -> False
eqEdge(E(z0, z1), E(z2, z3)) -> eqEdge[Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1)
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
reach(z0, z1, z2) -> reach[Ite](member(E(z0, z1), z2), z0, z1, z2)
goal(z0, z1, z2) -> reach(z0, z1, z2)

Types:
GETNODEFROMEDGE :: S:0' -> E -> c18:c19:c20
S :: S:0' -> S:0'
E :: S:0' -> S:0' -> E
c18 :: c18:c19:c20
0' :: S:0'
c19 :: c18:c19:c20
c20 :: c18:c19:c20
VIA :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> c21:c22
Cons :: E -> Cons:Nil -> Cons:Nil
c21 :: c8:c9 -> c:c1:c2:c3 -> c21:c22
VIA[ITE] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> c8:c9
!EQ :: S:0' -> S:0' -> False:True
!EQ' :: S:0' -> S:0' -> c:c1:c2:c3
Nil :: Cons:Nil
c22 :: c21:c22
MEMBER :: E -> Cons:Nil -> c23:c24
c23 :: c12:c13 -> c25:c26 -> c23:c24
MEMBER[ITE] :: False:True -> E -> Cons:Nil -> c12:c13
eqEdge :: E -> E -> False:True
EQEDGE :: E -> E -> c25:c26
c24 :: c23:c24
c25 :: c16:c17 -> c4:c5:c6:c7 -> c:c1:c2:c3 -> c25:c26
EQEDGE[ITE] :: False:True -> S:0' -> S:0' -> S:0' -> S:0' -> c16:c17
and :: False:True -> False:True -> False:True
AND :: False:True -> False:True -> c4:c5:c6:c7
c26 :: c16:c17 -> c4:c5:c6:c7 -> c:c1:c2:c3 -> c25:c26
NOTEMPTY :: Cons:Nil -> c27:c28
c27 :: c27:c28
c28 :: c27:c28
REACH :: S:0' -> S:0' -> Cons:Nil -> c29
c29 :: c14:c15 -> c23:c24 -> c29
REACH[ITE] :: False:True -> S:0' -> S:0' -> Cons:Nil -> c14:c15
member :: E -> Cons:Nil -> False:True
GOAL :: S:0' -> S:0' -> Cons:Nil -> c30
c30 :: c29 -> c30
c :: c:c1:c2:c3 -> c:c1:c2:c3
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
False :: False:True
c4 :: c4:c5:c6:c7
True :: False:True
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
c8 :: c10:c11 -> c29 -> c8:c9
VIA[LET] :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil -> c10:c11
reach :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
c9 :: c21:c22 -> c8:c9
c10 :: c21:c22 -> c10:c11
c11 :: c10:c11
c12 :: c23:c24 -> c12:c13
c13 :: c12:c13
c14 :: c21:c22 -> c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
via[Ite] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
via[Let] :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil -> Cons:Nil
via :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
member[Ite] :: False:True -> E -> Cons:Nil -> False:True
reach[Ite] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil
eqEdge[Ite] :: False:True -> S:0' -> S:0' -> S:0' -> S:0' -> False:True
getNodeFromEdge :: S:0' -> E -> S:0'
notEmpty :: Cons:Nil -> False:True
goal :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
hole_c18:c19:c201_31 :: c18:c19:c20
hole_S:0'2_31 :: S:0'
hole_E3_31 :: E
hole_c21:c224_31 :: c21:c22
hole_Cons:Nil5_31 :: Cons:Nil
hole_c8:c96_31 :: c8:c9
hole_c:c1:c2:c37_31 :: c:c1:c2:c3
hole_False:True8_31 :: False:True
hole_c23:c249_31 :: c23:c24
hole_c12:c1310_31 :: c12:c13
hole_c25:c2611_31 :: c25:c26
hole_c16:c1712_31 :: c16:c17
hole_c4:c5:c6:c713_31 :: c4:c5:c6:c7
hole_c27:c2814_31 :: c27:c28
hole_c2915_31 :: c29
hole_c14:c1516_31 :: c14:c15
hole_c3017_31 :: c30
hole_c10:c1118_31 :: c10:c11
gen_S:0'19_31 :: Nat -> S:0'
gen_Cons:Nil20_31 :: Nat -> Cons:Nil
gen_c:c1:c2:c321_31 :: Nat -> c:c1:c2:c3


Lemmas:
!EQ(gen_S:0'19_31(n23_31), gen_S:0'19_31(+(1, n23_31))) -> False, rt in Omega(0)
!EQ'(gen_S:0'19_31(n596_31), gen_S:0'19_31(+(1, n596_31))) -> gen_c:c1:c2:c321_31(n596_31), rt in Omega(0)
via(gen_S:0'19_31(1), gen_S:0'19_31(b), gen_Cons:Nil20_31(n2678_31), gen_Cons:Nil20_31(d)) -> gen_Cons:Nil20_31(0), rt in Omega(0)


Generator Equations:
gen_S:0'19_31(0) <=> 0'
gen_S:0'19_31(+(x, 1)) <=> S(gen_S:0'19_31(x))
gen_Cons:Nil20_31(0) <=> Nil
gen_Cons:Nil20_31(+(x, 1)) <=> Cons(E(0', 0'), gen_Cons:Nil20_31(x))
gen_c:c1:c2:c321_31(0) <=> c1
gen_c:c1:c2:c321_31(+(x, 1)) <=> c(gen_c:c1:c2:c321_31(x))


The following defined symbols remain to be analysed:
VIA

They will be analysed ascendingly in the following order:
VIA = REACH

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

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

(23)
BOUNDS(n^1, INF)

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

(24)
Obligation:
Innermost TRS:
Rules:
GETNODEFROMEDGE(S(S(z0)), E(z1, z2)) -> c18
GETNODEFROMEDGE(S(0'), E(z0, z1)) -> c19
GETNODEFROMEDGE(0', E(z0, z1)) -> c20
VIA(z0, z1, Cons(E(z2, z3), z4), z5) -> c21(VIA[ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2))
VIA(z0, z1, Nil, z2) -> c22
MEMBER(z0, Cons(z1, z2)) -> c23(MEMBER[ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1))
MEMBER(z0, Nil) -> c24
EQEDGE(E(z0, z1), E(z2, z3)) -> c25(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z0, z2))
EQEDGE(E(z0, z1), E(z2, z3)) -> c26(EQEDGE[ITE](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z1, z3))
NOTEMPTY(Cons(z0, z1)) -> c27
NOTEMPTY(Nil) -> c28
REACH(z0, z1, z2) -> c29(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2))
GOAL(z0, z1, z2) -> c30(REACH(z0, z1, z2))
!EQ'(S(z0), S(z1)) -> c(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c1
!EQ'(S(z0), 0') -> c2
!EQ'(0', 0') -> c3
AND(False, False) -> c4
AND(True, False) -> c5
AND(False, True) -> c6
AND(True, True) -> c7
VIA[ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) -> c8(VIA[LET](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)), REACH(z3, z1, z5))
VIA[ITE](False, z0, z1, Cons(z2, z3), z4) -> c9(VIA(z0, z1, z3, z4))
VIA[LET](z0, z1, Cons(z2, z3), z4, Nil) -> c10(VIA(z0, z1, z3, z4))
VIA[LET](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> c11
MEMBER[ITE](False, z0, Cons(z1, z2)) -> c12(MEMBER(z0, z2))
MEMBER[ITE](True, z0, z1) -> c13
REACH[ITE](False, z0, z1, z2) -> c14(VIA(z0, z1, z2, z2))
REACH[ITE](True, z0, z1, z2) -> c15
EQEDGE[ITE](False, z0, z1, z2, z3) -> c16
EQEDGE[ITE](True, z0, z1, z2, z3) -> c17
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
via[Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) -> via[Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5))
via[Ite](False, z0, z1, Cons(z2, z3), z4) -> via(z0, z1, z3, z4)
via[Let](z0, z1, Cons(z2, z3), z4, Nil) -> via(z0, z1, z3, z4)
via[Let](z0, z1, Cons(z2, z3), z4, Cons(z5, z6)) -> Cons(z2, Cons(z5, z6))
member[Ite](False, z0, Cons(z1, z2)) -> member(z0, z2)
member[Ite](True, z0, z1) -> True
reach[Ite](False, z0, z1, z2) -> via(z0, z1, z2, z2)
reach[Ite](True, z0, z1, z2) -> Cons(E(z0, z1), Nil)
eqEdge[Ite](False, z0, z1, z2, z3) -> False
eqEdge[Ite](True, z0, z1, z2, z3) -> True
getNodeFromEdge(S(S(z0)), E(z1, z2)) -> z2
getNodeFromEdge(S(0'), E(z0, z1)) -> z0
getNodeFromEdge(0', E(z0, z1)) -> z0
via(z0, z1, Cons(E(z2, z3), z4), z5) -> via[Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5)
via(z0, z1, Nil, z2) -> Nil
member(z0, Cons(z1, z2)) -> member[Ite](eqEdge(z0, z1), z0, Cons(z1, z2))
member(z0, Nil) -> False
eqEdge(E(z0, z1), E(z2, z3)) -> eqEdge[Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1)
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
reach(z0, z1, z2) -> reach[Ite](member(E(z0, z1), z2), z0, z1, z2)
goal(z0, z1, z2) -> reach(z0, z1, z2)

Types:
GETNODEFROMEDGE :: S:0' -> E -> c18:c19:c20
S :: S:0' -> S:0'
E :: S:0' -> S:0' -> E
c18 :: c18:c19:c20
0' :: S:0'
c19 :: c18:c19:c20
c20 :: c18:c19:c20
VIA :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> c21:c22
Cons :: E -> Cons:Nil -> Cons:Nil
c21 :: c8:c9 -> c:c1:c2:c3 -> c21:c22
VIA[ITE] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> c8:c9
!EQ :: S:0' -> S:0' -> False:True
!EQ' :: S:0' -> S:0' -> c:c1:c2:c3
Nil :: Cons:Nil
c22 :: c21:c22
MEMBER :: E -> Cons:Nil -> c23:c24
c23 :: c12:c13 -> c25:c26 -> c23:c24
MEMBER[ITE] :: False:True -> E -> Cons:Nil -> c12:c13
eqEdge :: E -> E -> False:True
EQEDGE :: E -> E -> c25:c26
c24 :: c23:c24
c25 :: c16:c17 -> c4:c5:c6:c7 -> c:c1:c2:c3 -> c25:c26
EQEDGE[ITE] :: False:True -> S:0' -> S:0' -> S:0' -> S:0' -> c16:c17
and :: False:True -> False:True -> False:True
AND :: False:True -> False:True -> c4:c5:c6:c7
c26 :: c16:c17 -> c4:c5:c6:c7 -> c:c1:c2:c3 -> c25:c26
NOTEMPTY :: Cons:Nil -> c27:c28
c27 :: c27:c28
c28 :: c27:c28
REACH :: S:0' -> S:0' -> Cons:Nil -> c29
c29 :: c14:c15 -> c23:c24 -> c29
REACH[ITE] :: False:True -> S:0' -> S:0' -> Cons:Nil -> c14:c15
member :: E -> Cons:Nil -> False:True
GOAL :: S:0' -> S:0' -> Cons:Nil -> c30
c30 :: c29 -> c30
c :: c:c1:c2:c3 -> c:c1:c2:c3
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
False :: False:True
c4 :: c4:c5:c6:c7
True :: False:True
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
c8 :: c10:c11 -> c29 -> c8:c9
VIA[LET] :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil -> c10:c11
reach :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
c9 :: c21:c22 -> c8:c9
c10 :: c21:c22 -> c10:c11
c11 :: c10:c11
c12 :: c23:c24 -> c12:c13
c13 :: c12:c13
c14 :: c21:c22 -> c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
via[Ite] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
via[Let] :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil -> Cons:Nil
via :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
member[Ite] :: False:True -> E -> Cons:Nil -> False:True
reach[Ite] :: False:True -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil
eqEdge[Ite] :: False:True -> S:0' -> S:0' -> S:0' -> S:0' -> False:True
getNodeFromEdge :: S:0' -> E -> S:0'
notEmpty :: Cons:Nil -> False:True
goal :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
hole_c18:c19:c201_31 :: c18:c19:c20
hole_S:0'2_31 :: S:0'
hole_E3_31 :: E
hole_c21:c224_31 :: c21:c22
hole_Cons:Nil5_31 :: Cons:Nil
hole_c8:c96_31 :: c8:c9
hole_c:c1:c2:c37_31 :: c:c1:c2:c3
hole_False:True8_31 :: False:True
hole_c23:c249_31 :: c23:c24
hole_c12:c1310_31 :: c12:c13
hole_c25:c2611_31 :: c25:c26
hole_c16:c1712_31 :: c16:c17
hole_c4:c5:c6:c713_31 :: c4:c5:c6:c7
hole_c27:c2814_31 :: c27:c28
hole_c2915_31 :: c29
hole_c14:c1516_31 :: c14:c15
hole_c3017_31 :: c30
hole_c10:c1118_31 :: c10:c11
gen_S:0'19_31 :: Nat -> S:0'
gen_Cons:Nil20_31 :: Nat -> Cons:Nil
gen_c:c1:c2:c321_31 :: Nat -> c:c1:c2:c3


Lemmas:
!EQ(gen_S:0'19_31(n23_31), gen_S:0'19_31(+(1, n23_31))) -> False, rt in Omega(0)
!EQ'(gen_S:0'19_31(n596_31), gen_S:0'19_31(+(1, n596_31))) -> gen_c:c1:c2:c321_31(n596_31), rt in Omega(0)
via(gen_S:0'19_31(1), gen_S:0'19_31(b), gen_Cons:Nil20_31(n2678_31), gen_Cons:Nil20_31(d)) -> gen_Cons:Nil20_31(0), rt in Omega(0)
VIA(gen_S:0'19_31(1), gen_S:0'19_31(b), gen_Cons:Nil20_31(+(1, n13024_31)), gen_Cons:Nil20_31(d)) -> *22_31, rt in Omega(n13024_31)


Generator Equations:
gen_S:0'19_31(0) <=> 0'
gen_S:0'19_31(+(x, 1)) <=> S(gen_S:0'19_31(x))
gen_Cons:Nil20_31(0) <=> Nil
gen_Cons:Nil20_31(+(x, 1)) <=> Cons(E(0', 0'), gen_Cons:Nil20_31(x))
gen_c:c1:c2:c321_31(0) <=> c1
gen_c:c1:c2:c321_31(+(x, 1)) <=> c(gen_c:c1:c2:c321_31(x))


The following defined symbols remain to be analysed:
REACH

They will be analysed ascendingly in the following order:
VIA = REACH