WORST_CASE(Omega(n^1),?)
proof of /export/starexec/sandbox/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 503 ms]
(2) CpxRelTRS
(3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) SlicingProof [LOWER BOUND(ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 317 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 495 ms]
(14) BEST
    (15) proven lower bound
        (16) LowerBoundPropagationProof [FINISHED, 0 ms]
        (17) BOUNDS(n^1, INF)
    (18) typed CpxTrs


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

(0)
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(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: INNERMOST
----------------------------------------

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

(2)
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(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: INNERMOST
----------------------------------------

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

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


The TRS R consists of the following rules:

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

(5) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
eqEdge[Ite]/1
eqEdge[Ite]/2
eqEdge[Ite]/3
eqEdge[Ite]/4

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

(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(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)))
   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) -> False
   eqEdge[Ite](True) -> True

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

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

(8)
Obligation:
Innermost TRS:
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)))
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)
!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) -> False
eqEdge[Ite](True) -> True

Types:
getNodeFromEdge :: S:0' -> E -> S:0'
S :: S:0' -> S:0'
E :: S:0' -> S:0' -> E
via :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
Cons :: E -> Cons:Nil -> Cons:Nil
via[Ite] :: True:False -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
!EQ :: S:0' -> S:0' -> True:False
0' :: S:0'
member :: E -> Cons:Nil -> True:False
member[Ite] :: True:False -> E -> Cons:Nil -> True:False
eqEdge :: E -> E -> True:False
eqEdge[Ite] :: True:False -> True:False
and :: True:False -> True:False -> True:False
Nil :: Cons:Nil
notEmpty :: Cons:Nil -> True:False
True :: True:False
False :: True:False
reach :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
reach[Ite] :: True:False -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil
goal :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
via[Let] :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil -> Cons:Nil
hole_S:0'1_0 :: S:0'
hole_E2_0 :: E
hole_Cons:Nil3_0 :: Cons:Nil
hole_True:False4_0 :: True:False
gen_S:0'5_0 :: Nat -> S:0'
gen_Cons:Nil6_0 :: Nat -> Cons:Nil

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
via, !EQ, member, reach

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

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

(10)
Obligation:
Innermost TRS:
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)))
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)
!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) -> False
eqEdge[Ite](True) -> True

Types:
getNodeFromEdge :: S:0' -> E -> S:0'
S :: S:0' -> S:0'
E :: S:0' -> S:0' -> E
via :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
Cons :: E -> Cons:Nil -> Cons:Nil
via[Ite] :: True:False -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
!EQ :: S:0' -> S:0' -> True:False
0' :: S:0'
member :: E -> Cons:Nil -> True:False
member[Ite] :: True:False -> E -> Cons:Nil -> True:False
eqEdge :: E -> E -> True:False
eqEdge[Ite] :: True:False -> True:False
and :: True:False -> True:False -> True:False
Nil :: Cons:Nil
notEmpty :: Cons:Nil -> True:False
True :: True:False
False :: True:False
reach :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
reach[Ite] :: True:False -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil
goal :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
via[Let] :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil -> Cons:Nil
hole_S:0'1_0 :: S:0'
hole_E2_0 :: E
hole_Cons:Nil3_0 :: Cons:Nil
hole_True:False4_0 :: True:False
gen_S:0'5_0 :: Nat -> S:0'
gen_Cons:Nil6_0 :: Nat -> Cons:Nil


Generator Equations:
gen_S:0'5_0(0) <=> 0'
gen_S:0'5_0(+(x, 1)) <=> S(gen_S:0'5_0(x))
gen_Cons:Nil6_0(0) <=> Nil
gen_Cons:Nil6_0(+(x, 1)) <=> Cons(E(0', 0'), gen_Cons:Nil6_0(x))


The following defined symbols remain to be analysed:
!EQ, via, member, reach

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

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
!EQ(gen_S:0'5_0(n8_0), gen_S:0'5_0(+(1, n8_0))) -> False, rt in Omega(0)

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

Induction Step:
!EQ(gen_S:0'5_0(+(n8_0, 1)), gen_S:0'5_0(+(1, +(n8_0, 1)))) ->_R^Omega(0)
!EQ(gen_S:0'5_0(n8_0), gen_S:0'5_0(+(1, n8_0))) ->_IH
False

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

(12)
Obligation:
Innermost TRS:
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)))
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)
!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) -> False
eqEdge[Ite](True) -> True

Types:
getNodeFromEdge :: S:0' -> E -> S:0'
S :: S:0' -> S:0'
E :: S:0' -> S:0' -> E
via :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
Cons :: E -> Cons:Nil -> Cons:Nil
via[Ite] :: True:False -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
!EQ :: S:0' -> S:0' -> True:False
0' :: S:0'
member :: E -> Cons:Nil -> True:False
member[Ite] :: True:False -> E -> Cons:Nil -> True:False
eqEdge :: E -> E -> True:False
eqEdge[Ite] :: True:False -> True:False
and :: True:False -> True:False -> True:False
Nil :: Cons:Nil
notEmpty :: Cons:Nil -> True:False
True :: True:False
False :: True:False
reach :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
reach[Ite] :: True:False -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil
goal :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
via[Let] :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil -> Cons:Nil
hole_S:0'1_0 :: S:0'
hole_E2_0 :: E
hole_Cons:Nil3_0 :: Cons:Nil
hole_True:False4_0 :: True:False
gen_S:0'5_0 :: Nat -> S:0'
gen_Cons:Nil6_0 :: Nat -> Cons:Nil


Lemmas:
!EQ(gen_S:0'5_0(n8_0), gen_S:0'5_0(+(1, n8_0))) -> False, rt in Omega(0)


Generator Equations:
gen_S:0'5_0(0) <=> 0'
gen_S:0'5_0(+(x, 1)) <=> S(gen_S:0'5_0(x))
gen_Cons:Nil6_0(0) <=> Nil
gen_Cons:Nil6_0(+(x, 1)) <=> Cons(E(0', 0'), gen_Cons:Nil6_0(x))


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

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

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
via(gen_S:0'5_0(1), gen_S:0'5_0(b), gen_Cons:Nil6_0(n4119_0), gen_Cons:Nil6_0(d)) -> gen_Cons:Nil6_0(0), rt in Omega(1 + n4119_0)

Induction Base:
via(gen_S:0'5_0(1), gen_S:0'5_0(b), gen_Cons:Nil6_0(0), gen_Cons:Nil6_0(d)) ->_R^Omega(1)
Nil

Induction Step:
via(gen_S:0'5_0(1), gen_S:0'5_0(b), gen_Cons:Nil6_0(+(n4119_0, 1)), gen_Cons:Nil6_0(d)) ->_R^Omega(1)
via[Ite](!EQ(gen_S:0'5_0(1), 0'), gen_S:0'5_0(1), gen_S:0'5_0(b), Cons(E(0', 0'), gen_Cons:Nil6_0(n4119_0)), gen_Cons:Nil6_0(d)) ->_R^Omega(0)
via[Ite](False, gen_S:0'5_0(1), gen_S:0'5_0(b), Cons(E(0', 0'), gen_Cons:Nil6_0(n4119_0)), gen_Cons:Nil6_0(d)) ->_R^Omega(0)
via(gen_S:0'5_0(1), gen_S:0'5_0(b), gen_Cons:Nil6_0(n4119_0), gen_Cons:Nil6_0(d)) ->_IH
gen_Cons:Nil6_0(0)

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

(14)
Complex Obligation (BEST)

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

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

Innermost TRS:
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)))
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)
!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) -> False
eqEdge[Ite](True) -> True

Types:
getNodeFromEdge :: S:0' -> E -> S:0'
S :: S:0' -> S:0'
E :: S:0' -> S:0' -> E
via :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
Cons :: E -> Cons:Nil -> Cons:Nil
via[Ite] :: True:False -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
!EQ :: S:0' -> S:0' -> True:False
0' :: S:0'
member :: E -> Cons:Nil -> True:False
member[Ite] :: True:False -> E -> Cons:Nil -> True:False
eqEdge :: E -> E -> True:False
eqEdge[Ite] :: True:False -> True:False
and :: True:False -> True:False -> True:False
Nil :: Cons:Nil
notEmpty :: Cons:Nil -> True:False
True :: True:False
False :: True:False
reach :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
reach[Ite] :: True:False -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil
goal :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
via[Let] :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil -> Cons:Nil
hole_S:0'1_0 :: S:0'
hole_E2_0 :: E
hole_Cons:Nil3_0 :: Cons:Nil
hole_True:False4_0 :: True:False
gen_S:0'5_0 :: Nat -> S:0'
gen_Cons:Nil6_0 :: Nat -> Cons:Nil


Lemmas:
!EQ(gen_S:0'5_0(n8_0), gen_S:0'5_0(+(1, n8_0))) -> False, rt in Omega(0)


Generator Equations:
gen_S:0'5_0(0) <=> 0'
gen_S:0'5_0(+(x, 1)) <=> S(gen_S:0'5_0(x))
gen_Cons:Nil6_0(0) <=> Nil
gen_Cons:Nil6_0(+(x, 1)) <=> Cons(E(0', 0'), gen_Cons:Nil6_0(x))


The following defined symbols remain to be analysed:
via

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

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

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

(17)
BOUNDS(n^1, INF)

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

(18)
Obligation:
Innermost TRS:
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)))
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)
!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) -> False
eqEdge[Ite](True) -> True

Types:
getNodeFromEdge :: S:0' -> E -> S:0'
S :: S:0' -> S:0'
E :: S:0' -> S:0' -> E
via :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
Cons :: E -> Cons:Nil -> Cons:Nil
via[Ite] :: True:False -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil
!EQ :: S:0' -> S:0' -> True:False
0' :: S:0'
member :: E -> Cons:Nil -> True:False
member[Ite] :: True:False -> E -> Cons:Nil -> True:False
eqEdge :: E -> E -> True:False
eqEdge[Ite] :: True:False -> True:False
and :: True:False -> True:False -> True:False
Nil :: Cons:Nil
notEmpty :: Cons:Nil -> True:False
True :: True:False
False :: True:False
reach :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
reach[Ite] :: True:False -> S:0' -> S:0' -> Cons:Nil -> Cons:Nil
goal :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil
via[Let] :: S:0' -> S:0' -> Cons:Nil -> Cons:Nil -> Cons:Nil -> Cons:Nil
hole_S:0'1_0 :: S:0'
hole_E2_0 :: E
hole_Cons:Nil3_0 :: Cons:Nil
hole_True:False4_0 :: True:False
gen_S:0'5_0 :: Nat -> S:0'
gen_Cons:Nil6_0 :: Nat -> Cons:Nil


Lemmas:
!EQ(gen_S:0'5_0(n8_0), gen_S:0'5_0(+(1, n8_0))) -> False, rt in Omega(0)
via(gen_S:0'5_0(1), gen_S:0'5_0(b), gen_Cons:Nil6_0(n4119_0), gen_Cons:Nil6_0(d)) -> gen_Cons:Nil6_0(0), rt in Omega(1 + n4119_0)


Generator Equations:
gen_S:0'5_0(0) <=> 0'
gen_S:0'5_0(+(x, 1)) <=> S(gen_S:0'5_0(x))
gen_Cons:Nil6_0(0) <=> Nil
gen_Cons:Nil6_0(+(x, 1)) <=> Cons(E(0', 0'), gen_Cons:Nil6_0(x))


The following defined symbols remain to be analysed:
reach

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