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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 550 ms]
(2) CpxRelTRS
(3) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxWeightedTrs
    (5) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CpxTypedWeightedTrs
    (7) CompletionProof [UPPER BOUND(ID), 0 ms]
    (8) CpxTypedWeightedCompleteTrs
    (9) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
    (10) CpxRNTS
    (11) CompleteCoflocoProof [FINISHED, 1155 ms]
    (12) BOUNDS(1, n^1)
(13) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
(14) TRS for Loop Detection
    (15) DecreasingLoopProof [LOWER BOUND(ID), 0 ms]
    (16) BEST
        (17) proven lower bound
            (18) LowerBoundPropagationProof [FINISHED, 0 ms]
            (19) BOUNDS(n^1, INF)
        (20) TRS for Loop Detection


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

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


The TRS R consists of the following rules:

   LT0(Nil, Cons(z0, z1)) -> c4
   LT0(Cons(z0, z1), Cons(z2, z3)) -> c5(LT0(z1, z3))
   LT0(z0, Nil) -> c6
   G(z0, Nil) -> c7
   G(z0, Cons(z1, z2)) -> c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
   F(z0, Nil) -> c9
   F(z0, Cons(z1, z2)) -> c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
   NOTEMPTY(Cons(z0, z1)) -> c11
   NOTEMPTY(Nil) -> c12
   NUMBER4(z0) -> c13
   GOAL(z0, z1) -> c14(F(z0, z1))
   GOAL(z0, z1) -> c15(G(z0, z1))

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

   G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c(G(z1, Cons(Cons(Nil, Nil), z2)))
   G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c1(G(z0, z2))
   F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c2(F(z1, Cons(Cons(Nil, Nil), z2)))
   F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c3(F(z0, z2))
   g[Ite][False][Ite](False, Cons(z0, z1), z2) -> g(z1, Cons(Cons(Nil, Nil), z2))
   g[Ite][False][Ite](True, z0, Cons(z1, z2)) -> g(z0, z2)
   f[Ite][False][Ite](False, Cons(z0, z1), z2) -> f(z1, Cons(Cons(Nil, Nil), z2))
   f[Ite][False][Ite](True, z0, Cons(z1, z2)) -> f(z0, z2)
   lt0(Nil, Cons(z0, z1)) -> True
   lt0(Cons(z0, z1), Cons(z2, z3)) -> lt0(z1, z3)
   lt0(z0, Nil) -> False
   g(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
   g(z0, Cons(z1, z2)) -> g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
   f(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
   f(z0, Cons(z1, z2)) -> f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   number4(z0) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
   goal(z0, z1) -> Cons(f(z0, z1), Cons(g(z0, z1), Nil))

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, n^1).


The TRS R consists of the following rules:

   LT0(Nil, Cons(z0, z1)) -> c4
   LT0(Cons(z0, z1), Cons(z2, z3)) -> c5(LT0(z1, z3))
   LT0(z0, Nil) -> c6
   G(z0, Nil) -> c7
   G(z0, Cons(z1, z2)) -> c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
   F(z0, Nil) -> c9
   F(z0, Cons(z1, z2)) -> c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
   NOTEMPTY(Cons(z0, z1)) -> c11
   NOTEMPTY(Nil) -> c12
   NUMBER4(z0) -> c13
   GOAL(z0, z1) -> c14(F(z0, z1))
   GOAL(z0, z1) -> c15(G(z0, z1))

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

   G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c(G(z1, Cons(Cons(Nil, Nil), z2)))
   G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c1(G(z0, z2))
   F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c2(F(z1, Cons(Cons(Nil, Nil), z2)))
   F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c3(F(z0, z2))
   g[Ite][False][Ite](False, Cons(z0, z1), z2) -> g(z1, Cons(Cons(Nil, Nil), z2))
   g[Ite][False][Ite](True, z0, Cons(z1, z2)) -> g(z0, z2)
   f[Ite][False][Ite](False, Cons(z0, z1), z2) -> f(z1, Cons(Cons(Nil, Nil), z2))
   f[Ite][False][Ite](True, z0, Cons(z1, z2)) -> f(z0, z2)
   lt0(Nil, Cons(z0, z1)) -> True
   lt0(Cons(z0, z1), Cons(z2, z3)) -> lt0(z1, z3)
   lt0(z0, Nil) -> False
   g(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
   g(z0, Cons(z1, z2)) -> g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
   f(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
   f(z0, Cons(z1, z2)) -> f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   number4(z0) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
   goal(z0, z1) -> Cons(f(z0, z1), Cons(g(z0, z1), Nil))

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

(3) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID))
Transformed relative TRS to weighted TRS
----------------------------------------

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


The TRS R consists of the following rules:

   LT0(Nil, Cons(z0, z1)) -> c4 [1]
   LT0(Cons(z0, z1), Cons(z2, z3)) -> c5(LT0(z1, z3)) [1]
   LT0(z0, Nil) -> c6 [1]
   G(z0, Nil) -> c7 [1]
   G(z0, Cons(z1, z2)) -> c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) [1]
   F(z0, Nil) -> c9 [1]
   F(z0, Cons(z1, z2)) -> c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) [1]
   NOTEMPTY(Cons(z0, z1)) -> c11 [1]
   NOTEMPTY(Nil) -> c12 [1]
   NUMBER4(z0) -> c13 [1]
   GOAL(z0, z1) -> c14(F(z0, z1)) [1]
   GOAL(z0, z1) -> c15(G(z0, z1)) [1]
   G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c(G(z1, Cons(Cons(Nil, Nil), z2))) [0]
   G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c1(G(z0, z2)) [0]
   F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c2(F(z1, Cons(Cons(Nil, Nil), z2))) [0]
   F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c3(F(z0, z2)) [0]
   g[Ite][False][Ite](False, Cons(z0, z1), z2) -> g(z1, Cons(Cons(Nil, Nil), z2)) [0]
   g[Ite][False][Ite](True, z0, Cons(z1, z2)) -> g(z0, z2) [0]
   f[Ite][False][Ite](False, Cons(z0, z1), z2) -> f(z1, Cons(Cons(Nil, Nil), z2)) [0]
   f[Ite][False][Ite](True, z0, Cons(z1, z2)) -> f(z0, z2) [0]
   lt0(Nil, Cons(z0, z1)) -> True [0]
   lt0(Cons(z0, z1), Cons(z2, z3)) -> lt0(z1, z3) [0]
   lt0(z0, Nil) -> False [0]
   g(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) [0]
   g(z0, Cons(z1, z2)) -> g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) [0]
   f(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) [0]
   f(z0, Cons(z1, z2)) -> f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) [0]
   notEmpty(Cons(z0, z1)) -> True [0]
   notEmpty(Nil) -> False [0]
   number4(z0) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) [0]
   goal(z0, z1) -> Cons(f(z0, z1), Cons(g(z0, z1), Nil)) [0]

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

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

(6)
Obligation:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   LT0(Nil, Cons(z0, z1)) -> c4 [1]
   LT0(Cons(z0, z1), Cons(z2, z3)) -> c5(LT0(z1, z3)) [1]
   LT0(z0, Nil) -> c6 [1]
   G(z0, Nil) -> c7 [1]
   G(z0, Cons(z1, z2)) -> c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) [1]
   F(z0, Nil) -> c9 [1]
   F(z0, Cons(z1, z2)) -> c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) [1]
   NOTEMPTY(Cons(z0, z1)) -> c11 [1]
   NOTEMPTY(Nil) -> c12 [1]
   NUMBER4(z0) -> c13 [1]
   GOAL(z0, z1) -> c14(F(z0, z1)) [1]
   GOAL(z0, z1) -> c15(G(z0, z1)) [1]
   G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c(G(z1, Cons(Cons(Nil, Nil), z2))) [0]
   G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c1(G(z0, z2)) [0]
   F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c2(F(z1, Cons(Cons(Nil, Nil), z2))) [0]
   F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c3(F(z0, z2)) [0]
   g[Ite][False][Ite](False, Cons(z0, z1), z2) -> g(z1, Cons(Cons(Nil, Nil), z2)) [0]
   g[Ite][False][Ite](True, z0, Cons(z1, z2)) -> g(z0, z2) [0]
   f[Ite][False][Ite](False, Cons(z0, z1), z2) -> f(z1, Cons(Cons(Nil, Nil), z2)) [0]
   f[Ite][False][Ite](True, z0, Cons(z1, z2)) -> f(z0, z2) [0]
   lt0(Nil, Cons(z0, z1)) -> True [0]
   lt0(Cons(z0, z1), Cons(z2, z3)) -> lt0(z1, z3) [0]
   lt0(z0, Nil) -> False [0]
   g(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) [0]
   g(z0, Cons(z1, z2)) -> g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) [0]
   f(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) [0]
   f(z0, Cons(z1, z2)) -> f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) [0]
   notEmpty(Cons(z0, z1)) -> True [0]
   notEmpty(Nil) -> False [0]
   number4(z0) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) [0]
   goal(z0, z1) -> Cons(f(z0, z1), Cons(g(z0, z1), Nil)) [0]

The TRS has the following type information:
LT0 :: Nil:Cons -> Nil:Cons -> c4:c5:c6
Nil :: Nil:Cons
Cons :: Nil:Cons -> Nil:Cons -> Nil:Cons
c4 :: c4:c5:c6
c5 :: c4:c5:c6 -> c4:c5:c6
c6 :: c4:c5:c6
G :: Nil:Cons -> Nil:Cons -> c7:c8
c7 :: c7:c8
c8 :: c:c1 -> c4:c5:c6 -> c7:c8
G[ITE][FALSE][ITE] :: False:True -> Nil:Cons -> Nil:Cons -> c:c1
lt0 :: Nil:Cons -> Nil:Cons -> False:True
F :: Nil:Cons -> Nil:Cons -> c9:c10
c9 :: c9:c10
c10 :: c2:c3 -> c4:c5:c6 -> c9:c10
F[ITE][FALSE][ITE] :: False:True -> Nil:Cons -> Nil:Cons -> c2:c3
NOTEMPTY :: Nil:Cons -> c11:c12
c11 :: c11:c12
c12 :: c11:c12
NUMBER4 :: a -> c13
c13 :: c13
GOAL :: Nil:Cons -> Nil:Cons -> c14:c15
c14 :: c9:c10 -> c14:c15
c15 :: c7:c8 -> c14:c15
False :: False:True
c :: c7:c8 -> c:c1
True :: False:True
c1 :: c7:c8 -> c:c1
c2 :: c9:c10 -> c2:c3
c3 :: c9:c10 -> c2:c3
g[Ite][False][Ite] :: False:True -> Nil:Cons -> Nil:Cons -> Nil:Cons
g :: Nil:Cons -> Nil:Cons -> Nil:Cons
f[Ite][False][Ite] :: False:True -> Nil:Cons -> Nil:Cons -> Nil:Cons
f :: Nil:Cons -> Nil:Cons -> Nil:Cons
notEmpty :: Nil:Cons -> False:True
number4 :: b -> Nil:Cons
goal :: Nil:Cons -> Nil:Cons -> Nil:Cons

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

(7) CompletionProof (UPPER BOUND(ID))
The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

   G[ITE][FALSE][ITE](v0, v1, v2) -> null_G[ITE][FALSE][ITE] [0]
   F[ITE][FALSE][ITE](v0, v1, v2) -> null_F[ITE][FALSE][ITE] [0]
   g[Ite][False][Ite](v0, v1, v2) -> null_g[Ite][False][Ite] [0]
   f[Ite][False][Ite](v0, v1, v2) -> null_f[Ite][False][Ite] [0]
   lt0(v0, v1) -> null_lt0 [0]
   g(v0, v1) -> null_g [0]
   f(v0, v1) -> null_f [0]
   notEmpty(v0) -> null_notEmpty [0]
   number4(v0) -> null_number4 [0]
   goal(v0, v1) -> null_goal [0]
   LT0(v0, v1) -> null_LT0 [0]
   G(v0, v1) -> null_G [0]
   F(v0, v1) -> null_F [0]
   NOTEMPTY(v0) -> null_NOTEMPTY [0]

And the following fresh constants:    null_G[ITE][FALSE][ITE], null_F[ITE][FALSE][ITE], null_g[Ite][False][Ite], null_f[Ite][False][Ite], null_lt0, null_g, null_f, null_notEmpty, null_number4, null_goal, null_LT0, null_G, null_F, null_NOTEMPTY, const, const1, const2

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

(8)
Obligation:
Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   LT0(Nil, Cons(z0, z1)) -> c4 [1]
   LT0(Cons(z0, z1), Cons(z2, z3)) -> c5(LT0(z1, z3)) [1]
   LT0(z0, Nil) -> c6 [1]
   G(z0, Nil) -> c7 [1]
   G(z0, Cons(z1, z2)) -> c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) [1]
   F(z0, Nil) -> c9 [1]
   F(z0, Cons(z1, z2)) -> c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) [1]
   NOTEMPTY(Cons(z0, z1)) -> c11 [1]
   NOTEMPTY(Nil) -> c12 [1]
   NUMBER4(z0) -> c13 [1]
   GOAL(z0, z1) -> c14(F(z0, z1)) [1]
   GOAL(z0, z1) -> c15(G(z0, z1)) [1]
   G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c(G(z1, Cons(Cons(Nil, Nil), z2))) [0]
   G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c1(G(z0, z2)) [0]
   F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c2(F(z1, Cons(Cons(Nil, Nil), z2))) [0]
   F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c3(F(z0, z2)) [0]
   g[Ite][False][Ite](False, Cons(z0, z1), z2) -> g(z1, Cons(Cons(Nil, Nil), z2)) [0]
   g[Ite][False][Ite](True, z0, Cons(z1, z2)) -> g(z0, z2) [0]
   f[Ite][False][Ite](False, Cons(z0, z1), z2) -> f(z1, Cons(Cons(Nil, Nil), z2)) [0]
   f[Ite][False][Ite](True, z0, Cons(z1, z2)) -> f(z0, z2) [0]
   lt0(Nil, Cons(z0, z1)) -> True [0]
   lt0(Cons(z0, z1), Cons(z2, z3)) -> lt0(z1, z3) [0]
   lt0(z0, Nil) -> False [0]
   g(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) [0]
   g(z0, Cons(z1, z2)) -> g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) [0]
   f(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) [0]
   f(z0, Cons(z1, z2)) -> f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) [0]
   notEmpty(Cons(z0, z1)) -> True [0]
   notEmpty(Nil) -> False [0]
   number4(z0) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))) [0]
   goal(z0, z1) -> Cons(f(z0, z1), Cons(g(z0, z1), Nil)) [0]
   G[ITE][FALSE][ITE](v0, v1, v2) -> null_G[ITE][FALSE][ITE] [0]
   F[ITE][FALSE][ITE](v0, v1, v2) -> null_F[ITE][FALSE][ITE] [0]
   g[Ite][False][Ite](v0, v1, v2) -> null_g[Ite][False][Ite] [0]
   f[Ite][False][Ite](v0, v1, v2) -> null_f[Ite][False][Ite] [0]
   lt0(v0, v1) -> null_lt0 [0]
   g(v0, v1) -> null_g [0]
   f(v0, v1) -> null_f [0]
   notEmpty(v0) -> null_notEmpty [0]
   number4(v0) -> null_number4 [0]
   goal(v0, v1) -> null_goal [0]
   LT0(v0, v1) -> null_LT0 [0]
   G(v0, v1) -> null_G [0]
   F(v0, v1) -> null_F [0]
   NOTEMPTY(v0) -> null_NOTEMPTY [0]

The TRS has the following type information:
LT0 :: Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> c4:c5:c6:null_LT0
Nil :: Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal
Cons :: Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal
c4 :: c4:c5:c6:null_LT0
c5 :: c4:c5:c6:null_LT0 -> c4:c5:c6:null_LT0
c6 :: c4:c5:c6:null_LT0
G :: Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> c7:c8:null_G
c7 :: c7:c8:null_G
c8 :: c:c1:null_G[ITE][FALSE][ITE] -> c4:c5:c6:null_LT0 -> c7:c8:null_G
G[ITE][FALSE][ITE] :: False:True:null_lt0:null_notEmpty -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> c:c1:null_G[ITE][FALSE][ITE]
lt0 :: Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> False:True:null_lt0:null_notEmpty
F :: Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> c9:c10:null_F
c9 :: c9:c10:null_F
c10 :: c2:c3:null_F[ITE][FALSE][ITE] -> c4:c5:c6:null_LT0 -> c9:c10:null_F
F[ITE][FALSE][ITE] :: False:True:null_lt0:null_notEmpty -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> c2:c3:null_F[ITE][FALSE][ITE]
NOTEMPTY :: Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> c11:c12:null_NOTEMPTY
c11 :: c11:c12:null_NOTEMPTY
c12 :: c11:c12:null_NOTEMPTY
NUMBER4 :: a -> c13
c13 :: c13
GOAL :: Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> c14:c15
c14 :: c9:c10:null_F -> c14:c15
c15 :: c7:c8:null_G -> c14:c15
False :: False:True:null_lt0:null_notEmpty
c :: c7:c8:null_G -> c:c1:null_G[ITE][FALSE][ITE]
True :: False:True:null_lt0:null_notEmpty
c1 :: c7:c8:null_G -> c:c1:null_G[ITE][FALSE][ITE]
c2 :: c9:c10:null_F -> c2:c3:null_F[ITE][FALSE][ITE]
c3 :: c9:c10:null_F -> c2:c3:null_F[ITE][FALSE][ITE]
g[Ite][False][Ite] :: False:True:null_lt0:null_notEmpty -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal
g :: Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal
f[Ite][False][Ite] :: False:True:null_lt0:null_notEmpty -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal
f :: Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal
notEmpty :: Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> False:True:null_lt0:null_notEmpty
number4 :: b -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal
goal :: Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal -> Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal
null_G[ITE][FALSE][ITE] :: c:c1:null_G[ITE][FALSE][ITE]
null_F[ITE][FALSE][ITE] :: c2:c3:null_F[ITE][FALSE][ITE]
null_g[Ite][False][Ite] :: Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal
null_f[Ite][False][Ite] :: Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal
null_lt0 :: False:True:null_lt0:null_notEmpty
null_g :: Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal
null_f :: Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal
null_notEmpty :: False:True:null_lt0:null_notEmpty
null_number4 :: Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal
null_goal :: Nil:Cons:null_g[Ite][False][Ite]:null_f[Ite][False][Ite]:null_g:null_f:null_number4:null_goal
null_LT0 :: c4:c5:c6:null_LT0
null_G :: c7:c8:null_G
null_F :: c9:c10:null_F
null_NOTEMPTY :: c11:c12:null_NOTEMPTY
const :: a
const1 :: c14:c15
const2 :: b

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

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID))
Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

   Nil => 0
   c4 => 0
   c6 => 1
   c7 => 0
   c9 => 0
   c11 => 1
   c12 => 2
   c13 => 0
   False => 1
   True => 2
   null_G[ITE][FALSE][ITE] => 0
   null_F[ITE][FALSE][ITE] => 0
   null_g[Ite][False][Ite] => 0
   null_f[Ite][False][Ite] => 0
   null_lt0 => 0
   null_g => 0
   null_f => 0
   null_notEmpty => 0
   null_number4 => 0
   null_goal => 0
   null_LT0 => 0
   null_G => 0
   null_F => 0
   null_NOTEMPTY => 0
   const => 0
   const1 => 0
   const2 => 0

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

(10)
Obligation:
Complexity RNTS consisting of the following rules:

   F(z, z') -{ 1 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   F(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   F(z, z') -{ 1 }-> 1 + F[ITE][FALSE][ITE](lt0(z0, 1 + 0 + 0), z0, 1 + z1 + z2) + LT0(z0, 1 + 0 + 0) :|: z = z0, z1 >= 0, z' = 1 + z1 + z2, z0 >= 0, z2 >= 0
   F[ITE][FALSE][ITE](z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   F[ITE][FALSE][ITE](z, z', z'') -{ 0 }-> 1 + F(z0, z2) :|: z = 2, z1 >= 0, z'' = 1 + z1 + z2, z0 >= 0, z' = z0, z2 >= 0
   F[ITE][FALSE][ITE](z, z', z'') -{ 0 }-> 1 + F(z1, 1 + (1 + 0 + 0) + z2) :|: z'' = z2, z' = 1 + z0 + z1, z1 >= 0, z = 1, z0 >= 0, z2 >= 0
   G(z, z') -{ 1 }-> 0 :|: z = z0, z0 >= 0, z' = 0
   G(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   G(z, z') -{ 1 }-> 1 + G[ITE][FALSE][ITE](lt0(z0, 1 + 0 + 0), z0, 1 + z1 + z2) + LT0(z0, 1 + 0 + 0) :|: z = z0, z1 >= 0, z' = 1 + z1 + z2, z0 >= 0, z2 >= 0
   GOAL(z, z') -{ 1 }-> 1 + G(z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   GOAL(z, z') -{ 1 }-> 1 + F(z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   G[ITE][FALSE][ITE](z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   G[ITE][FALSE][ITE](z, z', z'') -{ 0 }-> 1 + G(z0, z2) :|: z = 2, z1 >= 0, z'' = 1 + z1 + z2, z0 >= 0, z' = z0, z2 >= 0
   G[ITE][FALSE][ITE](z, z', z'') -{ 0 }-> 1 + G(z1, 1 + (1 + 0 + 0) + z2) :|: z'' = z2, z' = 1 + z0 + z1, z1 >= 0, z = 1, z0 >= 0, z2 >= 0
   LT0(z, z') -{ 1 }-> 1 :|: z = z0, z0 >= 0, z' = 0
   LT0(z, z') -{ 1 }-> 0 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   LT0(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   LT0(z, z') -{ 1 }-> 1 + LT0(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   NOTEMPTY(z) -{ 1 }-> 2 :|: z = 0
   NOTEMPTY(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   NOTEMPTY(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   NUMBER4(z) -{ 1 }-> 0 :|: z = z0, z0 >= 0
   f(z, z') -{ 0 }-> f[Ite][False][Ite](lt0(z0, 1 + 0 + 0), z0, 1 + z1 + z2) :|: z = z0, z1 >= 0, z' = 1 + z1 + z2, z0 >= 0, z2 >= 0
   f(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   f(z, z') -{ 0 }-> 1 + 0 + (1 + 0 + (1 + 0 + (1 + 0 + 0))) :|: z = z0, z0 >= 0, z' = 0
   f[Ite][False][Ite](z, z', z'') -{ 0 }-> f(z0, z2) :|: z = 2, z1 >= 0, z'' = 1 + z1 + z2, z0 >= 0, z' = z0, z2 >= 0
   f[Ite][False][Ite](z, z', z'') -{ 0 }-> f(z1, 1 + (1 + 0 + 0) + z2) :|: z'' = z2, z' = 1 + z0 + z1, z1 >= 0, z = 1, z0 >= 0, z2 >= 0
   f[Ite][False][Ite](z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   g(z, z') -{ 0 }-> g[Ite][False][Ite](lt0(z0, 1 + 0 + 0), z0, 1 + z1 + z2) :|: z = z0, z1 >= 0, z' = 1 + z1 + z2, z0 >= 0, z2 >= 0
   g(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   g(z, z') -{ 0 }-> 1 + 0 + (1 + 0 + (1 + 0 + (1 + 0 + 0))) :|: z = z0, z0 >= 0, z' = 0
   g[Ite][False][Ite](z, z', z'') -{ 0 }-> g(z0, z2) :|: z = 2, z1 >= 0, z'' = 1 + z1 + z2, z0 >= 0, z' = z0, z2 >= 0
   g[Ite][False][Ite](z, z', z'') -{ 0 }-> g(z1, 1 + (1 + 0 + 0) + z2) :|: z'' = z2, z' = 1 + z0 + z1, z1 >= 0, z = 1, z0 >= 0, z2 >= 0
   g[Ite][False][Ite](z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   goal(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   goal(z, z') -{ 0 }-> 1 + f(z0, z1) + (1 + g(z0, z1) + 0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   lt0(z, z') -{ 0 }-> lt0(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   lt0(z, z') -{ 0 }-> 2 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0
   lt0(z, z') -{ 0 }-> 1 :|: z = z0, z0 >= 0, z' = 0
   lt0(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   notEmpty(z) -{ 0 }-> 2 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   notEmpty(z) -{ 0 }-> 1 :|: z = 0
   notEmpty(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   number4(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   number4(z) -{ 0 }-> 1 + 0 + (1 + 0 + (1 + 0 + (1 + 0 + 0))) :|: z = z0, z0 >= 0

Only complete derivations are relevant for the runtime complexity.

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

(11) CompleteCoflocoProof (FINISHED)
Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V1, V, V25),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V25),0,[fun1(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V25),0,[fun3(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V25),0,[fun5(V1, Out)],[V1 >= 0]).
eq(start(V1, V, V25),0,[fun6(V1, Out)],[V1 >= 0]).
eq(start(V1, V, V25),0,[fun7(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V25),0,[fun2(V1, V, V25, Out)],[V1 >= 0,V >= 0,V25 >= 0]).
eq(start(V1, V, V25),0,[fun4(V1, V, V25, Out)],[V1 >= 0,V >= 0,V25 >= 0]).
eq(start(V1, V, V25),0,[fun8(V1, V, V25, Out)],[V1 >= 0,V >= 0,V25 >= 0]).
eq(start(V1, V, V25),0,[fun9(V1, V, V25, Out)],[V1 >= 0,V >= 0,V25 >= 0]).
eq(start(V1, V, V25),0,[lt0(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V25),0,[g(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V25),0,[f(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V25),0,[notEmpty(V1, Out)],[V1 >= 0]).
eq(start(V1, V, V25),0,[number4(V1, Out)],[V1 >= 0]).
eq(start(V1, V, V25),0,[goal(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(fun(V1, V, Out),1,[],[Out = 0,V = 1 + V2 + V3,V2 >= 0,V3 >= 0,V1 = 0]).
eq(fun(V1, V, Out),1,[fun(V4, V6, Ret1)],[Out = 1 + Ret1,V4 >= 0,V = 1 + V6 + V7,V5 >= 0,V1 = 1 + V4 + V5,V7 >= 0,V6 >= 0]).
eq(fun(V1, V, Out),1,[],[Out = 1,V1 = V8,V8 >= 0,V = 0]).
eq(fun1(V1, V, Out),1,[],[Out = 0,V1 = V9,V9 >= 0,V = 0]).
eq(fun1(V1, V, Out),1,[lt0(V10, 1 + 0 + 0, Ret010),fun2(Ret010, V10, 1 + V12 + V11, Ret01),fun(V10, 1 + 0 + 0, Ret11)],[Out = 1 + Ret01 + Ret11,V1 = V10,V12 >= 0,V = 1 + V11 + V12,V10 >= 0,V11 >= 0]).
eq(fun3(V1, V, Out),1,[],[Out = 0,V1 = V13,V13 >= 0,V = 0]).
eq(fun3(V1, V, Out),1,[lt0(V14, 1 + 0 + 0, Ret0101),fun4(Ret0101, V14, 1 + V16 + V15, Ret011),fun(V14, 1 + 0 + 0, Ret12)],[Out = 1 + Ret011 + Ret12,V1 = V14,V16 >= 0,V = 1 + V15 + V16,V14 >= 0,V15 >= 0]).
eq(fun5(V1, Out),1,[],[Out = 1,V17 >= 0,V18 >= 0,V1 = 1 + V17 + V18]).
eq(fun5(V1, Out),1,[],[Out = 2,V1 = 0]).
eq(fun6(V1, Out),1,[],[Out = 0,V1 = V19,V19 >= 0]).
eq(fun7(V1, V, Out),1,[fun3(V20, V21, Ret13)],[Out = 1 + Ret13,V1 = V20,V21 >= 0,V = V21,V20 >= 0]).
eq(fun7(V1, V, Out),1,[fun1(V23, V22, Ret14)],[Out = 1 + Ret14,V1 = V23,V22 >= 0,V = V22,V23 >= 0]).
eq(fun2(V1, V, V25, Out),0,[fun1(V24, 1 + (1 + 0 + 0) + V26, Ret15)],[Out = 1 + Ret15,V25 = V26,V = 1 + V24 + V27,V24 >= 0,V1 = 1,V27 >= 0,V26 >= 0]).
eq(fun2(V1, V, V25, Out),0,[fun1(V28, V29, Ret16)],[Out = 1 + Ret16,V1 = 2,V30 >= 0,V25 = 1 + V29 + V30,V28 >= 0,V = V28,V29 >= 0]).
eq(fun4(V1, V, V25, Out),0,[fun3(V33, 1 + (1 + 0 + 0) + V31, Ret17)],[Out = 1 + Ret17,V25 = V31,V = 1 + V32 + V33,V33 >= 0,V1 = 1,V32 >= 0,V31 >= 0]).
eq(fun4(V1, V, V25, Out),0,[fun3(V36, V34, Ret18)],[Out = 1 + Ret18,V1 = 2,V35 >= 0,V25 = 1 + V34 + V35,V36 >= 0,V = V36,V34 >= 0]).
eq(fun8(V1, V, V25, Out),0,[g(V38, 1 + (1 + 0 + 0) + V37, Ret)],[Out = Ret,V25 = V37,V = 1 + V38 + V39,V38 >= 0,V1 = 1,V39 >= 0,V37 >= 0]).
eq(fun8(V1, V, V25, Out),0,[g(V42, V40, Ret2)],[Out = Ret2,V1 = 2,V41 >= 0,V25 = 1 + V40 + V41,V42 >= 0,V = V42,V40 >= 0]).
eq(fun9(V1, V, V25, Out),0,[f(V45, 1 + (1 + 0 + 0) + V43, Ret3)],[Out = Ret3,V25 = V43,V = 1 + V44 + V45,V45 >= 0,V1 = 1,V44 >= 0,V43 >= 0]).
eq(fun9(V1, V, V25, Out),0,[f(V48, V46, Ret4)],[Out = Ret4,V1 = 2,V47 >= 0,V25 = 1 + V46 + V47,V48 >= 0,V = V48,V46 >= 0]).
eq(lt0(V1, V, Out),0,[],[Out = 2,V = 1 + V49 + V50,V50 >= 0,V49 >= 0,V1 = 0]).
eq(lt0(V1, V, Out),0,[lt0(V53, V54, Ret5)],[Out = Ret5,V53 >= 0,V = 1 + V52 + V54,V51 >= 0,V1 = 1 + V51 + V53,V52 >= 0,V54 >= 0]).
eq(lt0(V1, V, Out),0,[],[Out = 1,V1 = V55,V55 >= 0,V = 0]).
eq(g(V1, V, Out),0,[],[Out = 4,V1 = V56,V56 >= 0,V = 0]).
eq(g(V1, V, Out),0,[lt0(V57, 1 + 0 + 0, Ret0),fun8(Ret0, V57, 1 + V59 + V58, Ret6)],[Out = Ret6,V1 = V57,V59 >= 0,V = 1 + V58 + V59,V57 >= 0,V58 >= 0]).
eq(f(V1, V, Out),0,[],[Out = 4,V1 = V60,V60 >= 0,V = 0]).
eq(f(V1, V, Out),0,[lt0(V61, 1 + 0 + 0, Ret02),fun9(Ret02, V61, 1 + V63 + V62, Ret7)],[Out = Ret7,V1 = V61,V63 >= 0,V = 1 + V62 + V63,V61 >= 0,V62 >= 0]).
eq(notEmpty(V1, Out),0,[],[Out = 2,V64 >= 0,V65 >= 0,V1 = 1 + V64 + V65]).
eq(notEmpty(V1, Out),0,[],[Out = 1,V1 = 0]).
eq(number4(V1, Out),0,[],[Out = 4,V1 = V66,V66 >= 0]).
eq(goal(V1, V, Out),0,[f(V68, V67, Ret012),g(V68, V67, Ret101)],[Out = 2 + Ret012 + Ret101,V1 = V68,V67 >= 0,V = V67,V68 >= 0]).
eq(fun2(V1, V, V25, Out),0,[],[Out = 0,V70 >= 0,V25 = V71,V69 >= 0,V1 = V70,V = V69,V71 >= 0]).
eq(fun4(V1, V, V25, Out),0,[],[Out = 0,V74 >= 0,V25 = V72,V73 >= 0,V1 = V74,V = V73,V72 >= 0]).
eq(fun8(V1, V, V25, Out),0,[],[Out = 0,V77 >= 0,V25 = V75,V76 >= 0,V1 = V77,V = V76,V75 >= 0]).
eq(fun9(V1, V, V25, Out),0,[],[Out = 0,V78 >= 0,V25 = V79,V80 >= 0,V1 = V78,V = V80,V79 >= 0]).
eq(lt0(V1, V, Out),0,[],[Out = 0,V82 >= 0,V81 >= 0,V1 = V82,V = V81]).
eq(g(V1, V, Out),0,[],[Out = 0,V84 >= 0,V83 >= 0,V1 = V84,V = V83]).
eq(f(V1, V, Out),0,[],[Out = 0,V86 >= 0,V85 >= 0,V1 = V86,V = V85]).
eq(notEmpty(V1, Out),0,[],[Out = 0,V87 >= 0,V1 = V87]).
eq(number4(V1, Out),0,[],[Out = 0,V88 >= 0,V1 = V88]).
eq(goal(V1, V, Out),0,[],[Out = 0,V89 >= 0,V90 >= 0,V1 = V89,V = V90]).
eq(fun(V1, V, Out),0,[],[Out = 0,V92 >= 0,V91 >= 0,V1 = V92,V = V91]).
eq(fun1(V1, V, Out),0,[],[Out = 0,V94 >= 0,V93 >= 0,V1 = V94,V = V93]).
eq(fun3(V1, V, Out),0,[],[Out = 0,V96 >= 0,V95 >= 0,V1 = V96,V = V95]).
eq(fun5(V1, Out),0,[],[Out = 0,V97 >= 0,V1 = V97]).
input_output_vars(fun(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun1(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun3(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun5(V1,Out),[V1],[Out]).
input_output_vars(fun6(V1,Out),[V1],[Out]).
input_output_vars(fun7(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun2(V1,V,V25,Out),[V1,V,V25],[Out]).
input_output_vars(fun4(V1,V,V25,Out),[V1,V,V25],[Out]).
input_output_vars(fun8(V1,V,V25,Out),[V1,V,V25],[Out]).
input_output_vars(fun9(V1,V,V25,Out),[V1,V,V25],[Out]).
input_output_vars(lt0(V1,V,Out),[V1,V],[Out]).
input_output_vars(g(V1,V,Out),[V1,V],[Out]).
input_output_vars(f(V1,V,Out),[V1,V],[Out]).
input_output_vars(notEmpty(V1,Out),[V1],[Out]).
input_output_vars(number4(V1,Out),[V1],[Out]).
input_output_vars(goal(V1,V,Out),[V1,V],[Out]).


CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components 
0. recursive  : [lt0/3]
1. recursive  : [f/3,fun9/4]
2. recursive  : [fun/3]
3. recursive [non_tail] : [fun1/3,fun2/4]
4. recursive [non_tail] : [fun3/3,fun4/4]
5. non_recursive  : [fun5/2]
6. non_recursive  : [fun6/2]
7. non_recursive  : [fun7/3]
8. recursive  : [fun8/4,g/3]
9. non_recursive  : [goal/3]
10. non_recursive  : [notEmpty/2]
11. non_recursive  : [number4/2]
12. non_recursive  : [start/3]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into lt0/3
1. SCC is partially evaluated into f/3
2. SCC is partially evaluated into fun/3
3. SCC is partially evaluated into fun1/3
4. SCC is partially evaluated into fun3/3
5. SCC is partially evaluated into fun5/2
6. SCC is completely evaluated into other SCCs
7. SCC is partially evaluated into fun7/3
8. SCC is partially evaluated into g/3
9. SCC is partially evaluated into goal/3
10. SCC is partially evaluated into notEmpty/2
11. SCC is partially evaluated into number4/2
12. SCC is partially evaluated into start/3

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations lt0/3 
* CE 54 is refined into CE [62] 
* CE 53 is refined into CE [63] 
* CE 51 is refined into CE [64] 
* CE 52 is refined into CE [65] 


### Cost equations --> "Loop" of lt0/3 
* CEs [65] --> Loop 36 
* CEs [62] --> Loop 37 
* CEs [63] --> Loop 38 
* CEs [64] --> Loop 39 

### Ranking functions of CR lt0(V1,V,Out) 
* RF of phase [36]: [V,V1]

#### Partial ranking functions of CR lt0(V1,V,Out) 
* Partial RF of phase [36]:
  - RF of loop [36:1]:
    V
    V1


### Specialization of cost equations f/3 
* CE 37 is refined into CE [66,67,68] 
* CE 41 is refined into CE [69] 
* CE 40 is refined into CE [70] 
* CE 39 is refined into CE [71] 
* CE 38 is refined into CE [72] 


### Cost equations --> "Loop" of f/3 
* CEs [71] --> Loop 40 
* CEs [72] --> Loop 41 
* CEs [70] --> Loop 42 
* CEs [66,67,68,69] --> Loop 43 

### Ranking functions of CR f(V1,V,Out) 
* RF of phase [40]: [V1]
* RF of phase [41]: [V]

#### Partial ranking functions of CR f(V1,V,Out) 
* Partial RF of phase [40]:
  - RF of loop [40:1]:
    V1
* Partial RF of phase [41]:
  - RF of loop [41:1]:
    V


### Specialization of cost equations fun/3 
* CE 44 is refined into CE [73] 
* CE 42 is refined into CE [74] 
* CE 45 is refined into CE [75] 
* CE 43 is refined into CE [76] 


### Cost equations --> "Loop" of fun/3 
* CEs [76] --> Loop 44 
* CEs [73] --> Loop 45 
* CEs [74,75] --> Loop 46 

### Ranking functions of CR fun(V1,V,Out) 
* RF of phase [44]: [V,V1]

#### Partial ranking functions of CR fun(V1,V,Out) 
* Partial RF of phase [44]:
  - RF of loop [44:1]:
    V
    V1


### Specialization of cost equations fun1/3 
* CE 32 is refined into CE [77,78,79,80,81,82,83] 
* CE 35 is refined into CE [84] 
* CE 36 is refined into CE [85] 
* CE 34 is refined into CE [86,87,88] 
* CE 33 is refined into CE [89] 


### Cost equations --> "Loop" of fun1/3 
* CEs [88] --> Loop 47 
* CEs [87] --> Loop 48 
* CEs [86] --> Loop 49 
* CEs [89] --> Loop 50 
* CEs [80,83] --> Loop 51 
* CEs [79,82] --> Loop 52 
* CEs [84,85] --> Loop 53 
* CEs [77,78,81] --> Loop 54 

### Ranking functions of CR fun1(V1,V,Out) 
* RF of phase [47,48,49]: [V1]
* RF of phase [50]: [V]

#### Partial ranking functions of CR fun1(V1,V,Out) 
* Partial RF of phase [47,48,49]:
  - RF of loop [47:1,48:1,49:1]:
    V1
* Partial RF of phase [50]:
  - RF of loop [50:1]:
    V


### Specialization of cost equations fun3/3 
* CE 27 is refined into CE [90,91,92,93,94,95,96] 
* CE 30 is refined into CE [97] 
* CE 31 is refined into CE [98] 
* CE 29 is refined into CE [99,100,101] 
* CE 28 is refined into CE [102] 


### Cost equations --> "Loop" of fun3/3 
* CEs [101] --> Loop 55 
* CEs [100] --> Loop 56 
* CEs [99] --> Loop 57 
* CEs [102] --> Loop 58 
* CEs [93,96] --> Loop 59 
* CEs [92,95] --> Loop 60 
* CEs [97,98] --> Loop 61 
* CEs [90,91,94] --> Loop 62 

### Ranking functions of CR fun3(V1,V,Out) 
* RF of phase [55,56,57]: [V1]
* RF of phase [58]: [V]

#### Partial ranking functions of CR fun3(V1,V,Out) 
* Partial RF of phase [55,56,57]:
  - RF of loop [55:1,56:1,57:1]:
    V1
* Partial RF of phase [58]:
  - RF of loop [58:1]:
    V


### Specialization of cost equations fun5/2 
* CE 46 is refined into CE [103] 
* CE 48 is refined into CE [104] 
* CE 47 is refined into CE [105] 


### Cost equations --> "Loop" of fun5/2 
* CEs [103] --> Loop 63 
* CEs [104] --> Loop 64 
* CEs [105] --> Loop 65 

### Ranking functions of CR fun5(V1,Out) 

#### Partial ranking functions of CR fun5(V1,Out) 


### Specialization of cost equations fun7/3 
* CE 49 is refined into CE [106,107,108,109,110,111] 
* CE 50 is refined into CE [112,113,114,115,116,117] 


### Cost equations --> "Loop" of fun7/3 
* CEs [111,117] --> Loop 66 
* CEs [110,116] --> Loop 67 
* CEs [109,115] --> Loop 68 
* CEs [108,114] --> Loop 69 
* CEs [107,113] --> Loop 70 
* CEs [106,112] --> Loop 71 

### Ranking functions of CR fun7(V1,V,Out) 

#### Partial ranking functions of CR fun7(V1,V,Out) 


### Specialization of cost equations g/3 
* CE 22 is refined into CE [118,119,120] 
* CE 26 is refined into CE [121] 
* CE 25 is refined into CE [122] 
* CE 24 is refined into CE [123] 
* CE 23 is refined into CE [124] 


### Cost equations --> "Loop" of g/3 
* CEs [123] --> Loop 72 
* CEs [124] --> Loop 73 
* CEs [122] --> Loop 74 
* CEs [118,119,120,121] --> Loop 75 

### Ranking functions of CR g(V1,V,Out) 
* RF of phase [72]: [V1]
* RF of phase [73]: [V]

#### Partial ranking functions of CR g(V1,V,Out) 
* Partial RF of phase [72]:
  - RF of loop [72:1]:
    V1
* Partial RF of phase [73]:
  - RF of loop [73:1]:
    V


### Specialization of cost equations goal/3 
* CE 60 is refined into CE [125,126,127,128,129,130,131,132,133,134] 
* CE 61 is refined into CE [135] 


### Cost equations --> "Loop" of goal/3 
* CEs [134] --> Loop 76 
* CEs [128,133] --> Loop 77 
* CEs [125] --> Loop 78 
* CEs [135] --> Loop 79 
* CEs [132] --> Loop 80 
* CEs [127,131] --> Loop 81 
* CEs [130] --> Loop 82 
* CEs [126,129] --> Loop 83 

### Ranking functions of CR goal(V1,V,Out) 

#### Partial ranking functions of CR goal(V1,V,Out) 


### Specialization of cost equations notEmpty/2 
* CE 55 is refined into CE [136] 
* CE 57 is refined into CE [137] 
* CE 56 is refined into CE [138] 


### Cost equations --> "Loop" of notEmpty/2 
* CEs [136] --> Loop 84 
* CEs [137] --> Loop 85 
* CEs [138] --> Loop 86 

### Ranking functions of CR notEmpty(V1,Out) 

#### Partial ranking functions of CR notEmpty(V1,Out) 


### Specialization of cost equations number4/2 
* CE 58 is refined into CE [139] 
* CE 59 is refined into CE [140] 


### Cost equations --> "Loop" of number4/2 
* CEs [139] --> Loop 87 
* CEs [140] --> Loop 88 

### Ranking functions of CR number4(V1,Out) 

#### Partial ranking functions of CR number4(V1,Out) 


### Specialization of cost equations start/3 
* CE 2 is refined into CE [141,142,143,144] 
* CE 4 is refined into CE [145,146,147,148,149,150] 
* CE 6 is refined into CE [151,152,153,154,155,156] 
* CE 8 is refined into CE [157,158,159,160] 
* CE 1 is refined into CE [161] 
* CE 3 is refined into CE [162,163,164] 
* CE 5 is refined into CE [165,166,167,168,169,170] 
* CE 7 is refined into CE [171,172,173,174,175,176] 
* CE 9 is refined into CE [177,178,179] 
* CE 10 is refined into CE [180,181,182,183] 
* CE 11 is refined into CE [184,185,186,187,188,189] 
* CE 12 is refined into CE [190,191,192,193,194,195] 
* CE 13 is refined into CE [196,197,198] 
* CE 14 is refined into CE [199] 
* CE 15 is refined into CE [200,201,202,203,204,205] 
* CE 16 is refined into CE [206,207,208,209,210] 
* CE 17 is refined into CE [211,212,213,214] 
* CE 18 is refined into CE [215,216,217,218] 
* CE 19 is refined into CE [219,220,221] 
* CE 20 is refined into CE [222,223] 
* CE 21 is refined into CE [224,225,226,227,228,229,230,231] 


### Cost equations --> "Loop" of start/3 
* CEs [180,207,213,217,226,227] --> Loop 89 
* CEs [141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160] --> Loop 90 
* CEs [162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179] --> Loop 91 
* CEs [161,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,208,209,210,211,212,214,215,216,218,219,220,221,222,223,224,225,228,229,230,231] --> Loop 92 

### Ranking functions of CR start(V1,V,V25) 

#### Partial ranking functions of CR start(V1,V,V25) 


Computing Bounds
=====================================

#### Cost of chains of lt0(V1,V,Out):
* Chain [[36],39]: 0
  with precondition: [Out=2,V1>=1,V>=2] 

* Chain [[36],38]: 0
  with precondition: [Out=1,V1>=1,V>=1] 

* Chain [[36],37]: 0
  with precondition: [Out=0,V1>=1,V>=1] 

* Chain [39]: 0
  with precondition: [V1=0,Out=2,V>=1] 

* Chain [38]: 0
  with precondition: [V=0,Out=1,V1>=0] 

* Chain [37]: 0
  with precondition: [Out=0,V1>=0,V>=0] 


#### Cost of chains of f(V1,V,Out):
* Chain [[41],43]: 0
  with precondition: [V1=0,Out=0,V>=1] 

* Chain [[41],42]: 0
  with precondition: [V1=0,Out=4,V>=1] 

* Chain [[40],[41],43]: 0
  with precondition: [Out=0,V1>=1,V>=1] 

* Chain [[40],[41],42]: 0
  with precondition: [Out=4,V1>=1,V>=1] 

* Chain [[40],43]: 0
  with precondition: [Out=0,V1>=1,V>=1] 

* Chain [43]: 0
  with precondition: [Out=0,V1>=0,V>=0] 

* Chain [42]: 0
  with precondition: [V=0,Out=4,V1>=0] 


#### Cost of chains of fun(V1,V,Out):
* Chain [[44],46]: 1*it(44)+1
  Such that:it(44) =< V

  with precondition: [Out>=1,V1>=Out,V>=Out] 

* Chain [[44],45]: 1*it(44)+1
  Such that:it(44) =< V

  with precondition: [Out>=2,V1+1>=Out,V+1>=Out] 

* Chain [46]: 1
  with precondition: [Out=0,V1>=0,V>=0] 

* Chain [45]: 1
  with precondition: [V=0,Out=1,V1>=0] 


#### Cost of chains of fun1(V1,V,Out):
* Chain [[50],54]: 2*it(50)+2
  Such that:it(50) =< V

  with precondition: [V1=0,Out>=3,2*V>=Out+1] 

* Chain [[50],53]: 2*it(50)+1
  Such that:it(50) =< V

  with precondition: [V1=0,Out>=2,2*V>=Out] 

* Chain [[47,48,49],[50],54]: 8*it(47)+2*it(50)+2
  Such that:it(50) =< 2*V1+V
aux(5) =< V1
it(47) =< aux(5)

  with precondition: [V1>=1,V>=1,Out>=5,2*V+8*V1>=Out+1] 

* Chain [[47,48,49],[50],53]: 8*it(47)+2*it(50)+1
  Such that:it(50) =< 2*V1+V
aux(6) =< V1
it(47) =< aux(6)

  with precondition: [V1>=1,V>=1,Out>=4,2*V+8*V1>=Out] 

* Chain [[47,48,49],54]: 8*it(47)+2
  Such that:aux(7) =< V1
it(47) =< aux(7)

  with precondition: [V1>=1,V>=1,Out>=3,4*V1+1>=Out] 

* Chain [[47,48,49],53]: 8*it(47)+1
  Such that:aux(8) =< V1
it(47) =< aux(8)

  with precondition: [V1>=1,V>=1,Out>=2,4*V1>=Out] 

* Chain [[47,48,49],52]: 8*it(47)+4
  Such that:aux(10) =< V1
it(47) =< aux(10)

  with precondition: [V1>=2,V>=1,Out>=4,4*V1>=Out+2] 

* Chain [[47,48,49],51]: 8*it(47)+4
  Such that:aux(12) =< V1
it(47) =< aux(12)

  with precondition: [V1>=2,V>=1,Out>=5,4*V1>=Out+1] 

* Chain [54]: 2
  with precondition: [Out=1,V1>=0,V>=1] 

* Chain [53]: 1
  with precondition: [Out=0,V1>=0,V>=0] 

* Chain [52]: 4
  with precondition: [Out=2,V1>=1,V>=1] 

* Chain [51]: 4
  with precondition: [Out=3,V1>=1,V>=1] 


#### Cost of chains of fun3(V1,V,Out):
* Chain [[58],62]: 2*it(58)+2
  Such that:it(58) =< V

  with precondition: [V1=0,Out>=3,2*V>=Out+1] 

* Chain [[58],61]: 2*it(58)+1
  Such that:it(58) =< V

  with precondition: [V1=0,Out>=2,2*V>=Out] 

* Chain [[55,56,57],[58],62]: 8*it(55)+2*it(58)+2
  Such that:it(58) =< 2*V1+V
aux(21) =< V1
it(55) =< aux(21)

  with precondition: [V1>=1,V>=1,Out>=5,2*V+8*V1>=Out+1] 

* Chain [[55,56,57],[58],61]: 8*it(55)+2*it(58)+1
  Such that:it(58) =< 2*V1+V
aux(22) =< V1
it(55) =< aux(22)

  with precondition: [V1>=1,V>=1,Out>=4,2*V+8*V1>=Out] 

* Chain [[55,56,57],62]: 8*it(55)+2
  Such that:aux(23) =< V1
it(55) =< aux(23)

  with precondition: [V1>=1,V>=1,Out>=3,4*V1+1>=Out] 

* Chain [[55,56,57],61]: 8*it(55)+1
  Such that:aux(24) =< V1
it(55) =< aux(24)

  with precondition: [V1>=1,V>=1,Out>=2,4*V1>=Out] 

* Chain [[55,56,57],60]: 8*it(55)+4
  Such that:aux(26) =< V1
it(55) =< aux(26)

  with precondition: [V1>=2,V>=1,Out>=4,4*V1>=Out+2] 

* Chain [[55,56,57],59]: 8*it(55)+4
  Such that:aux(28) =< V1
it(55) =< aux(28)

  with precondition: [V1>=2,V>=1,Out>=5,4*V1>=Out+1] 

* Chain [62]: 2
  with precondition: [Out=1,V1>=0,V>=1] 

* Chain [61]: 1
  with precondition: [Out=0,V1>=0,V>=0] 

* Chain [60]: 4
  with precondition: [Out=2,V1>=1,V>=1] 

* Chain [59]: 4
  with precondition: [Out=3,V1>=1,V>=1] 


#### Cost of chains of fun5(V1,Out):
* Chain [65]: 1
  with precondition: [V1=0,Out=2] 

* Chain [64]: 0
  with precondition: [Out=0,V1>=0] 

* Chain [63]: 1
  with precondition: [Out=1,V1>=1] 


#### Cost of chains of fun7(V1,V,Out):
* Chain [71]: 8*s(54)+3
  Such that:aux(33) =< V
s(54) =< aux(33)

  with precondition: [V1=0,Out>=3,2*V+1>=Out] 

* Chain [70]: 2
  with precondition: [Out=1,V1>=0,V>=0] 

* Chain [69]: 3
  with precondition: [Out=2,V1>=0,V>=1] 

* Chain [68]: 48*s(58)+5
  Such that:aux(34) =< V1
s(58) =< aux(34)

  with precondition: [V1>=1,V>=1,Out>=3,4*V1+1>=Out] 

* Chain [67]: 16*s(62)+5
  Such that:aux(35) =< V1
s(62) =< aux(35)

  with precondition: [V1>=1,V>=1,Out>=4,4*V1+2>=Out] 

* Chain [66]: 8*s(67)+32*s(68)+3
  Such that:aux(36) =< V1
aux(37) =< 2*V1+V
s(67) =< aux(37)
s(68) =< aux(36)

  with precondition: [V1>=1,V>=1,Out>=5,2*V+8*V1+1>=Out] 


#### Cost of chains of g(V1,V,Out):
* Chain [[73],75]: 0
  with precondition: [V1=0,Out=0,V>=1] 

* Chain [[73],74]: 0
  with precondition: [V1=0,Out=4,V>=1] 

* Chain [[72],[73],75]: 0
  with precondition: [Out=0,V1>=1,V>=1] 

* Chain [[72],[73],74]: 0
  with precondition: [Out=4,V1>=1,V>=1] 

* Chain [[72],75]: 0
  with precondition: [Out=0,V1>=1,V>=1] 

* Chain [75]: 0
  with precondition: [Out=0,V1>=0,V>=0] 

* Chain [74]: 0
  with precondition: [V=0,Out=4,V1>=0] 


#### Cost of chains of goal(V1,V,Out):
* Chain [83]: 0
  with precondition: [V1=0,Out=6,V>=1] 

* Chain [82]: 0
  with precondition: [V1=0,Out=10,V>=1] 

* Chain [81]: 0
  with precondition: [V=0,Out=6,V1>=0] 

* Chain [80]: 0
  with precondition: [V=0,Out=10,V1>=0] 

* Chain [79]: 0
  with precondition: [Out=0,V1>=0,V>=0] 

* Chain [78]: 0
  with precondition: [Out=2,V1>=0,V>=0] 

* Chain [77]: 0
  with precondition: [Out=6,V1>=1,V>=1] 

* Chain [76]: 0
  with precondition: [Out=10,V1>=1,V>=1] 


#### Cost of chains of notEmpty(V1,Out):
* Chain [86]: 0
  with precondition: [V1=0,Out=1] 

* Chain [85]: 0
  with precondition: [Out=0,V1>=0] 

* Chain [84]: 0
  with precondition: [Out=2,V1>=1] 


#### Cost of chains of number4(V1,Out):
* Chain [88]: 0
  with precondition: [Out=0,V1>=0] 

* Chain [87]: 0
  with precondition: [Out=4,V1>=0] 


#### Cost of chains of start(V1,V,V25):
* Chain [92]: 18*s(73)+192*s(78)+16*s(83)+5
  Such that:aux(38) =< V1
aux(39) =< 2*V1+V
aux(40) =< V
s(73) =< aux(40)
s(78) =< aux(38)
s(83) =< aux(39)

  with precondition: [V1>=0] 

* Chain [91]: 8*s(106)+96*s(108)+8*s(113)+4
  Such that:aux(41) =< V
aux(42) =< 2*V+V25
aux(43) =< V25+2
s(108) =< aux(41)
s(113) =< aux(42)
s(106) =< aux(43)

  with precondition: [V1=1,V>=1,V25>=0] 

* Chain [90]: 8*s(126)+96*s(128)+8*s(133)+4
  Such that:aux(44) =< V
aux(45) =< 2*V+V25
aux(46) =< V25
s(128) =< aux(44)
s(133) =< aux(45)
s(126) =< aux(46)

  with precondition: [V1=2,V>=0,V25>=1] 

* Chain [89]: 1
  with precondition: [V=0,V1>=0] 


Closed-form bounds of start(V1,V,V25): 
-------------------------------------
* Chain [92] with precondition: [V1>=0] 
    - Upper bound: 192*V1+5+nat(V)*18+nat(2*V1+V)*16 
    - Complexity: n 
* Chain [91] with precondition: [V1=1,V>=1,V25>=0] 
    - Upper bound: 112*V+16*V25+20 
    - Complexity: n 
* Chain [90] with precondition: [V1=2,V>=0,V25>=1] 
    - Upper bound: 112*V+16*V25+4 
    - Complexity: n 
* Chain [89] with precondition: [V=0,V1>=0] 
    - Upper bound: 1 
    - Complexity: constant 

### Maximum cost of start(V1,V,V25): nat(V)*18+3+max([192*V1+1+nat(2*V1+V)*16,nat(2*V+V25)*8+nat(V)*78+max([nat(V25)*8,nat(V25+2)*8])])+1 
Asymptotic class: n 
* Total analysis performed in 1099 ms.


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

(12)
BOUNDS(1, n^1)

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

(13) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID))
Transformed a relative TRS into a decreasing-loop problem.
----------------------------------------

(14)
Obligation:
Analyzing the following TRS for decreasing loops:

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


The TRS R consists of the following rules:

   LT0(Nil, Cons(z0, z1)) -> c4
   LT0(Cons(z0, z1), Cons(z2, z3)) -> c5(LT0(z1, z3))
   LT0(z0, Nil) -> c6
   G(z0, Nil) -> c7
   G(z0, Cons(z1, z2)) -> c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
   F(z0, Nil) -> c9
   F(z0, Cons(z1, z2)) -> c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
   NOTEMPTY(Cons(z0, z1)) -> c11
   NOTEMPTY(Nil) -> c12
   NUMBER4(z0) -> c13
   GOAL(z0, z1) -> c14(F(z0, z1))
   GOAL(z0, z1) -> c15(G(z0, z1))

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

   G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c(G(z1, Cons(Cons(Nil, Nil), z2)))
   G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c1(G(z0, z2))
   F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c2(F(z1, Cons(Cons(Nil, Nil), z2)))
   F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c3(F(z0, z2))
   g[Ite][False][Ite](False, Cons(z0, z1), z2) -> g(z1, Cons(Cons(Nil, Nil), z2))
   g[Ite][False][Ite](True, z0, Cons(z1, z2)) -> g(z0, z2)
   f[Ite][False][Ite](False, Cons(z0, z1), z2) -> f(z1, Cons(Cons(Nil, Nil), z2))
   f[Ite][False][Ite](True, z0, Cons(z1, z2)) -> f(z0, z2)
   lt0(Nil, Cons(z0, z1)) -> True
   lt0(Cons(z0, z1), Cons(z2, z3)) -> lt0(z1, z3)
   lt0(z0, Nil) -> False
   g(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
   g(z0, Cons(z1, z2)) -> g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
   f(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
   f(z0, Cons(z1, z2)) -> f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   number4(z0) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
   goal(z0, z1) -> Cons(f(z0, z1), Cons(g(z0, z1), Nil))

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

(15) DecreasingLoopProof (LOWER BOUND(ID))
The following loop(s) give(s) rise to the lower bound Omega(n^1):

The rewrite sequence

LT0(Cons(z0, z1), Cons(z2, z3)) ->^+ c5(LT0(z1, z3))

gives rise to a decreasing loop by considering the right hand sides subterm at position [0].

The pumping substitution is [z1 / Cons(z0, z1), z3 / Cons(z2, z3)].

The result substitution is [ ].




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

(16)
Complex Obligation (BEST)

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

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

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


The TRS R consists of the following rules:

   LT0(Nil, Cons(z0, z1)) -> c4
   LT0(Cons(z0, z1), Cons(z2, z3)) -> c5(LT0(z1, z3))
   LT0(z0, Nil) -> c6
   G(z0, Nil) -> c7
   G(z0, Cons(z1, z2)) -> c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
   F(z0, Nil) -> c9
   F(z0, Cons(z1, z2)) -> c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
   NOTEMPTY(Cons(z0, z1)) -> c11
   NOTEMPTY(Nil) -> c12
   NUMBER4(z0) -> c13
   GOAL(z0, z1) -> c14(F(z0, z1))
   GOAL(z0, z1) -> c15(G(z0, z1))

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

   G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c(G(z1, Cons(Cons(Nil, Nil), z2)))
   G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c1(G(z0, z2))
   F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c2(F(z1, Cons(Cons(Nil, Nil), z2)))
   F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c3(F(z0, z2))
   g[Ite][False][Ite](False, Cons(z0, z1), z2) -> g(z1, Cons(Cons(Nil, Nil), z2))
   g[Ite][False][Ite](True, z0, Cons(z1, z2)) -> g(z0, z2)
   f[Ite][False][Ite](False, Cons(z0, z1), z2) -> f(z1, Cons(Cons(Nil, Nil), z2))
   f[Ite][False][Ite](True, z0, Cons(z1, z2)) -> f(z0, z2)
   lt0(Nil, Cons(z0, z1)) -> True
   lt0(Cons(z0, z1), Cons(z2, z3)) -> lt0(z1, z3)
   lt0(z0, Nil) -> False
   g(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
   g(z0, Cons(z1, z2)) -> g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
   f(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
   f(z0, Cons(z1, z2)) -> f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   number4(z0) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
   goal(z0, z1) -> Cons(f(z0, z1), Cons(g(z0, z1), Nil))

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

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

(19)
BOUNDS(n^1, INF)

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

(20)
Obligation:
Analyzing the following TRS for decreasing loops:

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


The TRS R consists of the following rules:

   LT0(Nil, Cons(z0, z1)) -> c4
   LT0(Cons(z0, z1), Cons(z2, z3)) -> c5(LT0(z1, z3))
   LT0(z0, Nil) -> c6
   G(z0, Nil) -> c7
   G(z0, Cons(z1, z2)) -> c8(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
   F(z0, Nil) -> c9
   F(z0, Cons(z1, z2)) -> c10(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
   NOTEMPTY(Cons(z0, z1)) -> c11
   NOTEMPTY(Nil) -> c12
   NUMBER4(z0) -> c13
   GOAL(z0, z1) -> c14(F(z0, z1))
   GOAL(z0, z1) -> c15(G(z0, z1))

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

   G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c(G(z1, Cons(Cons(Nil, Nil), z2)))
   G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c1(G(z0, z2))
   F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c2(F(z1, Cons(Cons(Nil, Nil), z2)))
   F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c3(F(z0, z2))
   g[Ite][False][Ite](False, Cons(z0, z1), z2) -> g(z1, Cons(Cons(Nil, Nil), z2))
   g[Ite][False][Ite](True, z0, Cons(z1, z2)) -> g(z0, z2)
   f[Ite][False][Ite](False, Cons(z0, z1), z2) -> f(z1, Cons(Cons(Nil, Nil), z2))
   f[Ite][False][Ite](True, z0, Cons(z1, z2)) -> f(z0, z2)
   lt0(Nil, Cons(z0, z1)) -> True
   lt0(Cons(z0, z1), Cons(z2, z3)) -> lt0(z1, z3)
   lt0(z0, Nil) -> False
   g(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
   g(z0, Cons(z1, z2)) -> g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
   f(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
   f(z0, Cons(z1, z2)) -> f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   number4(z0) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
   goal(z0, z1) -> Cons(f(z0, z1), Cons(g(z0, z1), Nil))

Rewrite Strategy: INNERMOST