WORST_CASE(Omega(n^1),O(n^1))
proof of /export/starexec/sandbox2/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), 568 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, 1082 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:

   A__AND(true, z0) -> c(MARK(z0))
   A__AND(false, z0) -> c1
   A__AND(z0, z1) -> c2
   A__IF(true, z0, z1) -> c3(MARK(z0))
   A__IF(false, z0, z1) -> c4(MARK(z1))
   A__IF(z0, z1, z2) -> c5
   A__ADD(0, z0) -> c6(MARK(z0))
   A__ADD(s(z0), z1) -> c7
   A__ADD(z0, z1) -> c8
   A__FIRST(0, z0) -> c9
   A__FIRST(s(z0), cons(z1, z2)) -> c10
   A__FIRST(z0, z1) -> c11
   A__FROM(z0) -> c12
   A__FROM(z0) -> c13
   MARK(and(z0, z1)) -> c14(A__AND(mark(z0), z1), MARK(z0))
   MARK(if(z0, z1, z2)) -> c15(A__IF(mark(z0), z1, z2), MARK(z0))
   MARK(add(z0, z1)) -> c16(A__ADD(mark(z0), z1), MARK(z0))
   MARK(first(z0, z1)) -> c17(A__FIRST(mark(z0), mark(z1)), MARK(z0))
   MARK(first(z0, z1)) -> c18(A__FIRST(mark(z0), mark(z1)), MARK(z1))
   MARK(from(z0)) -> c19(A__FROM(z0))
   MARK(true) -> c20
   MARK(false) -> c21
   MARK(0) -> c22
   MARK(s(z0)) -> c23
   MARK(nil) -> c24
   MARK(cons(z0, z1)) -> c25

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

   a__and(true, z0) -> mark(z0)
   a__and(false, z0) -> false
   a__and(z0, z1) -> and(z0, z1)
   a__if(true, z0, z1) -> mark(z0)
   a__if(false, z0, z1) -> mark(z1)
   a__if(z0, z1, z2) -> if(z0, z1, z2)
   a__add(0, z0) -> mark(z0)
   a__add(s(z0), z1) -> s(add(z0, z1))
   a__add(z0, z1) -> add(z0, z1)
   a__first(0, z0) -> nil
   a__first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2))
   a__first(z0, z1) -> first(z0, z1)
   a__from(z0) -> cons(z0, from(s(z0)))
   a__from(z0) -> from(z0)
   mark(and(z0, z1)) -> a__and(mark(z0), z1)
   mark(if(z0, z1, z2)) -> a__if(mark(z0), z1, z2)
   mark(add(z0, z1)) -> a__add(mark(z0), z1)
   mark(first(z0, z1)) -> a__first(mark(z0), mark(z1))
   mark(from(z0)) -> a__from(z0)
   mark(true) -> true
   mark(false) -> false
   mark(0) -> 0
   mark(s(z0)) -> s(z0)
   mark(nil) -> nil
   mark(cons(z0, z1)) -> cons(z0, z1)

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:

   A__AND(true, z0) -> c(MARK(z0))
   A__AND(false, z0) -> c1
   A__AND(z0, z1) -> c2
   A__IF(true, z0, z1) -> c3(MARK(z0))
   A__IF(false, z0, z1) -> c4(MARK(z1))
   A__IF(z0, z1, z2) -> c5
   A__ADD(0, z0) -> c6(MARK(z0))
   A__ADD(s(z0), z1) -> c7
   A__ADD(z0, z1) -> c8
   A__FIRST(0, z0) -> c9
   A__FIRST(s(z0), cons(z1, z2)) -> c10
   A__FIRST(z0, z1) -> c11
   A__FROM(z0) -> c12
   A__FROM(z0) -> c13
   MARK(and(z0, z1)) -> c14(A__AND(mark(z0), z1), MARK(z0))
   MARK(if(z0, z1, z2)) -> c15(A__IF(mark(z0), z1, z2), MARK(z0))
   MARK(add(z0, z1)) -> c16(A__ADD(mark(z0), z1), MARK(z0))
   MARK(first(z0, z1)) -> c17(A__FIRST(mark(z0), mark(z1)), MARK(z0))
   MARK(first(z0, z1)) -> c18(A__FIRST(mark(z0), mark(z1)), MARK(z1))
   MARK(from(z0)) -> c19(A__FROM(z0))
   MARK(true) -> c20
   MARK(false) -> c21
   MARK(0) -> c22
   MARK(s(z0)) -> c23
   MARK(nil) -> c24
   MARK(cons(z0, z1)) -> c25

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

   a__and(true, z0) -> mark(z0)
   a__and(false, z0) -> false
   a__and(z0, z1) -> and(z0, z1)
   a__if(true, z0, z1) -> mark(z0)
   a__if(false, z0, z1) -> mark(z1)
   a__if(z0, z1, z2) -> if(z0, z1, z2)
   a__add(0, z0) -> mark(z0)
   a__add(s(z0), z1) -> s(add(z0, z1))
   a__add(z0, z1) -> add(z0, z1)
   a__first(0, z0) -> nil
   a__first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2))
   a__first(z0, z1) -> first(z0, z1)
   a__from(z0) -> cons(z0, from(s(z0)))
   a__from(z0) -> from(z0)
   mark(and(z0, z1)) -> a__and(mark(z0), z1)
   mark(if(z0, z1, z2)) -> a__if(mark(z0), z1, z2)
   mark(add(z0, z1)) -> a__add(mark(z0), z1)
   mark(first(z0, z1)) -> a__first(mark(z0), mark(z1))
   mark(from(z0)) -> a__from(z0)
   mark(true) -> true
   mark(false) -> false
   mark(0) -> 0
   mark(s(z0)) -> s(z0)
   mark(nil) -> nil
   mark(cons(z0, z1)) -> cons(z0, z1)

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:

   A__AND(true, z0) -> c(MARK(z0)) [1]
   A__AND(false, z0) -> c1 [1]
   A__AND(z0, z1) -> c2 [1]
   A__IF(true, z0, z1) -> c3(MARK(z0)) [1]
   A__IF(false, z0, z1) -> c4(MARK(z1)) [1]
   A__IF(z0, z1, z2) -> c5 [1]
   A__ADD(0, z0) -> c6(MARK(z0)) [1]
   A__ADD(s(z0), z1) -> c7 [1]
   A__ADD(z0, z1) -> c8 [1]
   A__FIRST(0, z0) -> c9 [1]
   A__FIRST(s(z0), cons(z1, z2)) -> c10 [1]
   A__FIRST(z0, z1) -> c11 [1]
   A__FROM(z0) -> c12 [1]
   A__FROM(z0) -> c13 [1]
   MARK(and(z0, z1)) -> c14(A__AND(mark(z0), z1), MARK(z0)) [1]
   MARK(if(z0, z1, z2)) -> c15(A__IF(mark(z0), z1, z2), MARK(z0)) [1]
   MARK(add(z0, z1)) -> c16(A__ADD(mark(z0), z1), MARK(z0)) [1]
   MARK(first(z0, z1)) -> c17(A__FIRST(mark(z0), mark(z1)), MARK(z0)) [1]
   MARK(first(z0, z1)) -> c18(A__FIRST(mark(z0), mark(z1)), MARK(z1)) [1]
   MARK(from(z0)) -> c19(A__FROM(z0)) [1]
   MARK(true) -> c20 [1]
   MARK(false) -> c21 [1]
   MARK(0) -> c22 [1]
   MARK(s(z0)) -> c23 [1]
   MARK(nil) -> c24 [1]
   MARK(cons(z0, z1)) -> c25 [1]
   a__and(true, z0) -> mark(z0) [0]
   a__and(false, z0) -> false [0]
   a__and(z0, z1) -> and(z0, z1) [0]
   a__if(true, z0, z1) -> mark(z0) [0]
   a__if(false, z0, z1) -> mark(z1) [0]
   a__if(z0, z1, z2) -> if(z0, z1, z2) [0]
   a__add(0, z0) -> mark(z0) [0]
   a__add(s(z0), z1) -> s(add(z0, z1)) [0]
   a__add(z0, z1) -> add(z0, z1) [0]
   a__first(0, z0) -> nil [0]
   a__first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2)) [0]
   a__first(z0, z1) -> first(z0, z1) [0]
   a__from(z0) -> cons(z0, from(s(z0))) [0]
   a__from(z0) -> from(z0) [0]
   mark(and(z0, z1)) -> a__and(mark(z0), z1) [0]
   mark(if(z0, z1, z2)) -> a__if(mark(z0), z1, z2) [0]
   mark(add(z0, z1)) -> a__add(mark(z0), z1) [0]
   mark(first(z0, z1)) -> a__first(mark(z0), mark(z1)) [0]
   mark(from(z0)) -> a__from(z0) [0]
   mark(true) -> true [0]
   mark(false) -> false [0]
   mark(0) -> 0 [0]
   mark(s(z0)) -> s(z0) [0]
   mark(nil) -> nil [0]
   mark(cons(z0, z1)) -> cons(z0, z1) [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:

   A__AND(true, z0) -> c(MARK(z0)) [1]
   A__AND(false, z0) -> c1 [1]
   A__AND(z0, z1) -> c2 [1]
   A__IF(true, z0, z1) -> c3(MARK(z0)) [1]
   A__IF(false, z0, z1) -> c4(MARK(z1)) [1]
   A__IF(z0, z1, z2) -> c5 [1]
   A__ADD(0, z0) -> c6(MARK(z0)) [1]
   A__ADD(s(z0), z1) -> c7 [1]
   A__ADD(z0, z1) -> c8 [1]
   A__FIRST(0, z0) -> c9 [1]
   A__FIRST(s(z0), cons(z1, z2)) -> c10 [1]
   A__FIRST(z0, z1) -> c11 [1]
   A__FROM(z0) -> c12 [1]
   A__FROM(z0) -> c13 [1]
   MARK(and(z0, z1)) -> c14(A__AND(mark(z0), z1), MARK(z0)) [1]
   MARK(if(z0, z1, z2)) -> c15(A__IF(mark(z0), z1, z2), MARK(z0)) [1]
   MARK(add(z0, z1)) -> c16(A__ADD(mark(z0), z1), MARK(z0)) [1]
   MARK(first(z0, z1)) -> c17(A__FIRST(mark(z0), mark(z1)), MARK(z0)) [1]
   MARK(first(z0, z1)) -> c18(A__FIRST(mark(z0), mark(z1)), MARK(z1)) [1]
   MARK(from(z0)) -> c19(A__FROM(z0)) [1]
   MARK(true) -> c20 [1]
   MARK(false) -> c21 [1]
   MARK(0) -> c22 [1]
   MARK(s(z0)) -> c23 [1]
   MARK(nil) -> c24 [1]
   MARK(cons(z0, z1)) -> c25 [1]
   a__and(true, z0) -> mark(z0) [0]
   a__and(false, z0) -> false [0]
   a__and(z0, z1) -> and(z0, z1) [0]
   a__if(true, z0, z1) -> mark(z0) [0]
   a__if(false, z0, z1) -> mark(z1) [0]
   a__if(z0, z1, z2) -> if(z0, z1, z2) [0]
   a__add(0, z0) -> mark(z0) [0]
   a__add(s(z0), z1) -> s(add(z0, z1)) [0]
   a__add(z0, z1) -> add(z0, z1) [0]
   a__first(0, z0) -> nil [0]
   a__first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2)) [0]
   a__first(z0, z1) -> first(z0, z1) [0]
   a__from(z0) -> cons(z0, from(s(z0))) [0]
   a__from(z0) -> from(z0) [0]
   mark(and(z0, z1)) -> a__and(mark(z0), z1) [0]
   mark(if(z0, z1, z2)) -> a__if(mark(z0), z1, z2) [0]
   mark(add(z0, z1)) -> a__add(mark(z0), z1) [0]
   mark(first(z0, z1)) -> a__first(mark(z0), mark(z1)) [0]
   mark(from(z0)) -> a__from(z0) [0]
   mark(true) -> true [0]
   mark(false) -> false [0]
   mark(0) -> 0 [0]
   mark(s(z0)) -> s(z0) [0]
   mark(nil) -> nil [0]
   mark(cons(z0, z1)) -> cons(z0, z1) [0]

The TRS has the following type information:
A__AND :: true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil -> c:c1:c2
true :: true:false:0:s:cons:and:if:add:first:from:nil
c :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25 -> c:c1:c2
MARK :: true:false:0:s:cons:and:if:add:first:from:nil -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25
false :: true:false:0:s:cons:and:if:add:first:from:nil
c1 :: c:c1:c2
c2 :: c:c1:c2
A__IF :: true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil -> c3:c4:c5
c3 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25 -> c3:c4:c5
c4 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25 -> c3:c4:c5
c5 :: c3:c4:c5
A__ADD :: true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil -> c6:c7:c8
0 :: true:false:0:s:cons:and:if:add:first:from:nil
c6 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25 -> c6:c7:c8
s :: true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil
c7 :: c6:c7:c8
c8 :: c6:c7:c8
A__FIRST :: true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil -> c9:c10:c11
c9 :: c9:c10:c11
cons :: true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil
c10 :: c9:c10:c11
c11 :: c9:c10:c11
A__FROM :: true:false:0:s:cons:and:if:add:first:from:nil -> c12:c13
c12 :: c12:c13
c13 :: c12:c13
and :: true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil
c14 :: c:c1:c2 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25
mark :: true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil
if :: true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil
c15 :: c3:c4:c5 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25
add :: true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil
c16 :: c6:c7:c8 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25
first :: true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil
c17 :: c9:c10:c11 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25
c18 :: c9:c10:c11 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25
from :: true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil
c19 :: c12:c13 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25
c20 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25
c21 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25
c22 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25
c23 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25
nil :: true:false:0:s:cons:and:if:add:first:from:nil
c24 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25
c25 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25
a__and :: true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil
a__if :: true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil
a__add :: true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil
a__first :: true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil
a__from :: true:false:0:s:cons:and:if:add:first:from:nil -> true:false:0:s:cons:and:if:add:first:from:nil

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:

   a__and(v0, v1) -> null_a__and [0]
   a__if(v0, v1, v2) -> null_a__if [0]
   a__add(v0, v1) -> null_a__add [0]
   a__first(v0, v1) -> null_a__first [0]
   a__from(v0) -> null_a__from [0]
   mark(v0) -> null_mark [0]
   MARK(v0) -> null_MARK [0]

And the following fresh constants:    null_a__and, null_a__if, null_a__add, null_a__first, null_a__from, null_mark, null_MARK

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

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

   A__AND(true, z0) -> c(MARK(z0)) [1]
   A__AND(false, z0) -> c1 [1]
   A__AND(z0, z1) -> c2 [1]
   A__IF(true, z0, z1) -> c3(MARK(z0)) [1]
   A__IF(false, z0, z1) -> c4(MARK(z1)) [1]
   A__IF(z0, z1, z2) -> c5 [1]
   A__ADD(0, z0) -> c6(MARK(z0)) [1]
   A__ADD(s(z0), z1) -> c7 [1]
   A__ADD(z0, z1) -> c8 [1]
   A__FIRST(0, z0) -> c9 [1]
   A__FIRST(s(z0), cons(z1, z2)) -> c10 [1]
   A__FIRST(z0, z1) -> c11 [1]
   A__FROM(z0) -> c12 [1]
   A__FROM(z0) -> c13 [1]
   MARK(and(z0, z1)) -> c14(A__AND(mark(z0), z1), MARK(z0)) [1]
   MARK(if(z0, z1, z2)) -> c15(A__IF(mark(z0), z1, z2), MARK(z0)) [1]
   MARK(add(z0, z1)) -> c16(A__ADD(mark(z0), z1), MARK(z0)) [1]
   MARK(first(z0, z1)) -> c17(A__FIRST(mark(z0), mark(z1)), MARK(z0)) [1]
   MARK(first(z0, z1)) -> c18(A__FIRST(mark(z0), mark(z1)), MARK(z1)) [1]
   MARK(from(z0)) -> c19(A__FROM(z0)) [1]
   MARK(true) -> c20 [1]
   MARK(false) -> c21 [1]
   MARK(0) -> c22 [1]
   MARK(s(z0)) -> c23 [1]
   MARK(nil) -> c24 [1]
   MARK(cons(z0, z1)) -> c25 [1]
   a__and(true, z0) -> mark(z0) [0]
   a__and(false, z0) -> false [0]
   a__and(z0, z1) -> and(z0, z1) [0]
   a__if(true, z0, z1) -> mark(z0) [0]
   a__if(false, z0, z1) -> mark(z1) [0]
   a__if(z0, z1, z2) -> if(z0, z1, z2) [0]
   a__add(0, z0) -> mark(z0) [0]
   a__add(s(z0), z1) -> s(add(z0, z1)) [0]
   a__add(z0, z1) -> add(z0, z1) [0]
   a__first(0, z0) -> nil [0]
   a__first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2)) [0]
   a__first(z0, z1) -> first(z0, z1) [0]
   a__from(z0) -> cons(z0, from(s(z0))) [0]
   a__from(z0) -> from(z0) [0]
   mark(and(z0, z1)) -> a__and(mark(z0), z1) [0]
   mark(if(z0, z1, z2)) -> a__if(mark(z0), z1, z2) [0]
   mark(add(z0, z1)) -> a__add(mark(z0), z1) [0]
   mark(first(z0, z1)) -> a__first(mark(z0), mark(z1)) [0]
   mark(from(z0)) -> a__from(z0) [0]
   mark(true) -> true [0]
   mark(false) -> false [0]
   mark(0) -> 0 [0]
   mark(s(z0)) -> s(z0) [0]
   mark(nil) -> nil [0]
   mark(cons(z0, z1)) -> cons(z0, z1) [0]
   a__and(v0, v1) -> null_a__and [0]
   a__if(v0, v1, v2) -> null_a__if [0]
   a__add(v0, v1) -> null_a__add [0]
   a__first(v0, v1) -> null_a__first [0]
   a__from(v0) -> null_a__from [0]
   mark(v0) -> null_mark [0]
   MARK(v0) -> null_MARK [0]

The TRS has the following type information:
A__AND :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> c:c1:c2
true :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
c :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK -> c:c1:c2
MARK :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK
false :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
c1 :: c:c1:c2
c2 :: c:c1:c2
A__IF :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> c3:c4:c5
c3 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK -> c3:c4:c5
c4 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK -> c3:c4:c5
c5 :: c3:c4:c5
A__ADD :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> c6:c7:c8
0 :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
c6 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK -> c6:c7:c8
s :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
c7 :: c6:c7:c8
c8 :: c6:c7:c8
A__FIRST :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> c9:c10:c11
c9 :: c9:c10:c11
cons :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
c10 :: c9:c10:c11
c11 :: c9:c10:c11
A__FROM :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> c12:c13
c12 :: c12:c13
c13 :: c12:c13
and :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
c14 :: c:c1:c2 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK
mark :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
if :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
c15 :: c3:c4:c5 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK
add :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
c16 :: c6:c7:c8 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK
first :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
c17 :: c9:c10:c11 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK
c18 :: c9:c10:c11 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK
from :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
c19 :: c12:c13 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK
c20 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK
c21 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK
c22 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK
c23 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK
nil :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
c24 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK
c25 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK
a__and :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
a__if :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
a__add :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
a__first :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
a__from :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
null_a__and :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
null_a__if :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
null_a__add :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
null_a__first :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
null_a__from :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
null_mark :: true:false:0:s:cons:and:if:add:first:from:nil:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark
null_MARK :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23:c24:c25:null_MARK

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:

   true => 3
   false => 1
   c1 => 0
   c2 => 1
   c5 => 0
   0 => 0
   c7 => 0
   c8 => 1
   c9 => 2
   c10 => 0
   c11 => 1
   c12 => 0
   c13 => 1
   c20 => 0
   c21 => 1
   c22 => 2
   c23 => 3
   nil => 2
   c24 => 4
   c25 => 5
   null_a__and => 0
   null_a__if => 0
   null_a__add => 0
   null_a__first => 0
   null_a__from => 0
   null_mark => 0
   null_MARK => 0

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

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

   A__ADD(z, z') -{ 1 }-> 1 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   A__ADD(z, z') -{ 1 }-> 0 :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   A__ADD(z, z') -{ 1 }-> 1 + MARK(z0) :|: z0 >= 0, z = 0, z' = z0
   A__AND(z, z') -{ 1 }-> 1 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   A__AND(z, z') -{ 1 }-> 0 :|: z = 1, z0 >= 0, z' = z0
   A__AND(z, z') -{ 1 }-> 1 + MARK(z0) :|: z = 3, z0 >= 0, z' = z0
   A__FIRST(z, z') -{ 1 }-> 2 :|: z0 >= 0, z = 0, z' = z0
   A__FIRST(z, z') -{ 1 }-> 1 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   A__FIRST(z, z') -{ 1 }-> 0 :|: z1 >= 0, z' = 1 + z1 + z2, z = 1 + z0, z0 >= 0, z2 >= 0
   A__FROM(z) -{ 1 }-> 1 :|: z = z0, z0 >= 0
   A__FROM(z) -{ 1 }-> 0 :|: z = z0, z0 >= 0
   A__IF(z, z', z'') -{ 1 }-> 0 :|: z'' = z2, z = z0, z1 >= 0, z' = z1, z0 >= 0, z2 >= 0
   A__IF(z, z', z'') -{ 1 }-> 1 + MARK(z0) :|: z = 3, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   A__IF(z, z', z'') -{ 1 }-> 1 + MARK(z1) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1
   MARK(z) -{ 1 }-> 5 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MARK(z) -{ 1 }-> 4 :|: z = 2
   MARK(z) -{ 1 }-> 3 :|: z = 1 + z0, z0 >= 0
   MARK(z) -{ 1 }-> 2 :|: z = 0
   MARK(z) -{ 1 }-> 1 :|: z = 1
   MARK(z) -{ 1 }-> 0 :|: z = 3
   MARK(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   MARK(z) -{ 1 }-> 1 + A__FROM(z0) :|: z = 1 + z0, z0 >= 0
   MARK(z) -{ 1 }-> 1 + A__IF(mark(z0), z1, z2) + MARK(z0) :|: z1 >= 0, z = 1 + z0 + z1 + z2, z0 >= 0, z2 >= 0
   MARK(z) -{ 1 }-> 1 + A__FIRST(mark(z0), mark(z1)) + MARK(z0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MARK(z) -{ 1 }-> 1 + A__FIRST(mark(z0), mark(z1)) + MARK(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MARK(z) -{ 1 }-> 1 + A__AND(mark(z0), z1) + MARK(z0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MARK(z) -{ 1 }-> 1 + A__ADD(mark(z0), z1) + MARK(z0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   a__add(z, z') -{ 0 }-> mark(z0) :|: z0 >= 0, z = 0, z' = z0
   a__add(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   a__add(z, z') -{ 0 }-> 1 + (1 + z0 + z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0
   a__add(z, z') -{ 0 }-> 1 + z0 + z1 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   a__and(z, z') -{ 0 }-> mark(z0) :|: z = 3, z0 >= 0, z' = z0
   a__and(z, z') -{ 0 }-> 1 :|: z = 1, z0 >= 0, z' = z0
   a__and(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   a__and(z, z') -{ 0 }-> 1 + z0 + z1 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   a__first(z, z') -{ 0 }-> 2 :|: z0 >= 0, z = 0, z' = z0
   a__first(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   a__first(z, z') -{ 0 }-> 1 + z0 + z1 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   a__first(z, z') -{ 0 }-> 1 + z1 + (1 + z0 + z2) :|: z1 >= 0, z' = 1 + z1 + z2, z = 1 + z0, z0 >= 0, z2 >= 0
   a__from(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   a__from(z) -{ 0 }-> 1 + z0 :|: z = z0, z0 >= 0
   a__from(z) -{ 0 }-> 1 + z0 + (1 + (1 + z0)) :|: z = z0, z0 >= 0
   a__if(z, z', z'') -{ 0 }-> mark(z0) :|: z = 3, z1 >= 0, z0 >= 0, z' = z0, z'' = z1
   a__if(z, z', z'') -{ 0 }-> mark(z1) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1
   a__if(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   a__if(z, z', z'') -{ 0 }-> 1 + z0 + z1 + z2 :|: z'' = z2, z = z0, z1 >= 0, z' = z1, z0 >= 0, z2 >= 0
   mark(z) -{ 0 }-> a__if(mark(z0), z1, z2) :|: z1 >= 0, z = 1 + z0 + z1 + z2, z0 >= 0, z2 >= 0
   mark(z) -{ 0 }-> a__from(z0) :|: z = 1 + z0, z0 >= 0
   mark(z) -{ 0 }-> a__first(mark(z0), mark(z1)) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   mark(z) -{ 0 }-> a__and(mark(z0), z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   mark(z) -{ 0 }-> a__add(mark(z0), z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   mark(z) -{ 0 }-> 3 :|: z = 3
   mark(z) -{ 0 }-> 2 :|: z = 2
   mark(z) -{ 0 }-> 1 :|: z = 1
   mark(z) -{ 0 }-> 0 :|: z = 0
   mark(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   mark(z) -{ 0 }-> 1 + z0 :|: z = 1 + z0, z0 >= 0
   mark(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1

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, V7),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V7),0,[fun2(V1, V, V7, Out)],[V1 >= 0,V >= 0,V7 >= 0]).
eq(start(V1, V, V7),0,[fun3(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V7),0,[fun4(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V7),0,[fun5(V1, Out)],[V1 >= 0]).
eq(start(V1, V, V7),0,[fun1(V1, Out)],[V1 >= 0]).
eq(start(V1, V, V7),0,[fun6(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V7),0,[fun7(V1, V, V7, Out)],[V1 >= 0,V >= 0,V7 >= 0]).
eq(start(V1, V, V7),0,[fun8(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V7),0,[fun9(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V7),0,[fun10(V1, Out)],[V1 >= 0]).
eq(start(V1, V, V7),0,[mark(V1, Out)],[V1 >= 0]).
eq(fun(V1, V, Out),1,[fun1(V2, Ret1)],[Out = 1 + Ret1,V1 = 3,V2 >= 0,V = V2]).
eq(fun(V1, V, Out),1,[],[Out = 0,V1 = 1,V3 >= 0,V = V3]).
eq(fun(V1, V, Out),1,[],[Out = 1,V1 = V5,V4 >= 0,V = V4,V5 >= 0]).
eq(fun2(V1, V, V7, Out),1,[fun1(V6, Ret11)],[Out = 1 + Ret11,V1 = 3,V8 >= 0,V6 >= 0,V = V6,V7 = V8]).
eq(fun2(V1, V, V7, Out),1,[fun1(V10, Ret12)],[Out = 1 + Ret12,V10 >= 0,V1 = 1,V9 >= 0,V = V9,V7 = V10]).
eq(fun2(V1, V, V7, Out),1,[],[Out = 0,V7 = V13,V1 = V11,V12 >= 0,V = V12,V11 >= 0,V13 >= 0]).
eq(fun3(V1, V, Out),1,[fun1(V14, Ret13)],[Out = 1 + Ret13,V14 >= 0,V1 = 0,V = V14]).
eq(fun3(V1, V, Out),1,[],[Out = 0,V15 >= 0,V1 = 1 + V16,V = V15,V16 >= 0]).
eq(fun3(V1, V, Out),1,[],[Out = 1,V1 = V18,V17 >= 0,V = V17,V18 >= 0]).
eq(fun4(V1, V, Out),1,[],[Out = 2,V19 >= 0,V1 = 0,V = V19]).
eq(fun4(V1, V, Out),1,[],[Out = 0,V20 >= 0,V = 1 + V20 + V21,V1 = 1 + V22,V22 >= 0,V21 >= 0]).
eq(fun4(V1, V, Out),1,[],[Out = 1,V1 = V24,V23 >= 0,V = V23,V24 >= 0]).
eq(fun5(V1, Out),1,[],[Out = 0,V1 = V25,V25 >= 0]).
eq(fun5(V1, Out),1,[],[Out = 1,V1 = V26,V26 >= 0]).
eq(fun1(V1, Out),1,[mark(V27, Ret010),fun(Ret010, V28, Ret01),fun1(V27, Ret14)],[Out = 1 + Ret01 + Ret14,V28 >= 0,V27 >= 0,V1 = 1 + V27 + V28]).
eq(fun1(V1, Out),1,[mark(V31, Ret0101),fun2(Ret0101, V30, V29, Ret011),fun1(V31, Ret15)],[Out = 1 + Ret011 + Ret15,V30 >= 0,V1 = 1 + V29 + V30 + V31,V31 >= 0,V29 >= 0]).
eq(fun1(V1, Out),1,[mark(V33, Ret0102),fun3(Ret0102, V32, Ret012),fun1(V33, Ret16)],[Out = 1 + Ret012 + Ret16,V32 >= 0,V33 >= 0,V1 = 1 + V32 + V33]).
eq(fun1(V1, Out),1,[mark(V35, Ret0103),mark(V34, Ret0111),fun4(Ret0103, Ret0111, Ret013),fun1(V35, Ret17)],[Out = 1 + Ret013 + Ret17,V34 >= 0,V35 >= 0,V1 = 1 + V34 + V35]).
eq(fun1(V1, Out),1,[mark(V37, Ret0104),mark(V36, Ret0112),fun4(Ret0104, Ret0112, Ret014),fun1(V36, Ret18)],[Out = 1 + Ret014 + Ret18,V36 >= 0,V37 >= 0,V1 = 1 + V36 + V37]).
eq(fun1(V1, Out),1,[fun5(V38, Ret19)],[Out = 1 + Ret19,V1 = 1 + V38,V38 >= 0]).
eq(fun1(V1, Out),1,[],[Out = 0,V1 = 3]).
eq(fun1(V1, Out),1,[],[Out = 1,V1 = 1]).
eq(fun1(V1, Out),1,[],[Out = 2,V1 = 0]).
eq(fun1(V1, Out),1,[],[Out = 3,V1 = 1 + V39,V39 >= 0]).
eq(fun1(V1, Out),1,[],[Out = 4,V1 = 2]).
eq(fun1(V1, Out),1,[],[Out = 5,V41 >= 0,V40 >= 0,V1 = 1 + V40 + V41]).
eq(fun6(V1, V, Out),0,[mark(V42, Ret)],[Out = Ret,V1 = 3,V42 >= 0,V = V42]).
eq(fun6(V1, V, Out),0,[],[Out = 1,V1 = 1,V43 >= 0,V = V43]).
eq(fun6(V1, V, Out),0,[],[Out = 1 + V44 + V45,V1 = V44,V45 >= 0,V = V45,V44 >= 0]).
eq(fun7(V1, V, V7, Out),0,[mark(V47, Ret2)],[Out = Ret2,V1 = 3,V46 >= 0,V47 >= 0,V = V47,V7 = V46]).
eq(fun7(V1, V, V7, Out),0,[mark(V48, Ret3)],[Out = Ret3,V48 >= 0,V1 = 1,V49 >= 0,V = V49,V7 = V48]).
eq(fun7(V1, V, V7, Out),0,[],[Out = 1 + V50 + V51 + V52,V7 = V50,V1 = V51,V52 >= 0,V = V52,V51 >= 0,V50 >= 0]).
eq(fun8(V1, V, Out),0,[mark(V53, Ret4)],[Out = Ret4,V53 >= 0,V1 = 0,V = V53]).
eq(fun8(V1, V, Out),0,[],[Out = 2 + V54 + V55,V55 >= 0,V1 = 1 + V54,V = V55,V54 >= 0]).
eq(fun8(V1, V, Out),0,[],[Out = 1 + V56 + V57,V1 = V56,V57 >= 0,V = V57,V56 >= 0]).
eq(fun9(V1, V, Out),0,[],[Out = 2,V58 >= 0,V1 = 0,V = V58]).
eq(fun9(V1, V, Out),0,[],[Out = 2 + V59 + V60 + V61,V59 >= 0,V = 1 + V59 + V61,V1 = 1 + V60,V60 >= 0,V61 >= 0]).
eq(fun9(V1, V, Out),0,[],[Out = 1 + V62 + V63,V1 = V62,V63 >= 0,V = V63,V62 >= 0]).
eq(fun10(V1, Out),0,[],[Out = 3 + 2*V64,V1 = V64,V64 >= 0]).
eq(fun10(V1, Out),0,[],[Out = 1 + V65,V1 = V65,V65 >= 0]).
eq(mark(V1, Out),0,[mark(V67, Ret0),fun6(Ret0, V66, Ret5)],[Out = Ret5,V66 >= 0,V67 >= 0,V1 = 1 + V66 + V67]).
eq(mark(V1, Out),0,[mark(V70, Ret02),fun7(Ret02, V69, V68, Ret6)],[Out = Ret6,V69 >= 0,V1 = 1 + V68 + V69 + V70,V70 >= 0,V68 >= 0]).
eq(mark(V1, Out),0,[mark(V71, Ret03),fun8(Ret03, V72, Ret7)],[Out = Ret7,V72 >= 0,V71 >= 0,V1 = 1 + V71 + V72]).
eq(mark(V1, Out),0,[mark(V73, Ret04),mark(V74, Ret110),fun9(Ret04, Ret110, Ret8)],[Out = Ret8,V74 >= 0,V73 >= 0,V1 = 1 + V73 + V74]).
eq(mark(V1, Out),0,[fun10(V75, Ret9)],[Out = Ret9,V1 = 1 + V75,V75 >= 0]).
eq(mark(V1, Out),0,[],[Out = 3,V1 = 3]).
eq(mark(V1, Out),0,[],[Out = 1,V1 = 1]).
eq(mark(V1, Out),0,[],[Out = 0,V1 = 0]).
eq(mark(V1, Out),0,[],[Out = 1 + V76,V1 = 1 + V76,V76 >= 0]).
eq(mark(V1, Out),0,[],[Out = 2,V1 = 2]).
eq(mark(V1, Out),0,[],[Out = 1 + V77 + V78,V78 >= 0,V77 >= 0,V1 = 1 + V77 + V78]).
eq(fun6(V1, V, Out),0,[],[Out = 0,V80 >= 0,V79 >= 0,V1 = V80,V = V79]).
eq(fun7(V1, V, V7, Out),0,[],[Out = 0,V82 >= 0,V7 = V83,V81 >= 0,V1 = V82,V = V81,V83 >= 0]).
eq(fun8(V1, V, Out),0,[],[Out = 0,V85 >= 0,V84 >= 0,V1 = V85,V = V84]).
eq(fun9(V1, V, Out),0,[],[Out = 0,V86 >= 0,V87 >= 0,V1 = V86,V = V87]).
eq(fun10(V1, Out),0,[],[Out = 0,V88 >= 0,V1 = V88]).
eq(mark(V1, Out),0,[],[Out = 0,V89 >= 0,V1 = V89]).
eq(fun1(V1, Out),0,[],[Out = 0,V90 >= 0,V1 = V90]).
input_output_vars(fun(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun2(V1,V,V7,Out),[V1,V,V7],[Out]).
input_output_vars(fun3(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun4(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun5(V1,Out),[V1],[Out]).
input_output_vars(fun1(V1,Out),[V1],[Out]).
input_output_vars(fun6(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun7(V1,V,V7,Out),[V1,V,V7],[Out]).
input_output_vars(fun8(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun9(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun10(V1,Out),[V1],[Out]).
input_output_vars(mark(V1,Out),[V1],[Out]).


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

#### Computed strongly connected components 
0. non_recursive  : [fun4/3]
1. non_recursive  : [fun5/2]
2. non_recursive  : [fun10/2]
3. non_recursive  : [fun9/3]
4. recursive [non_tail,multiple] : [fun6/3,fun7/4,fun8/3,mark/2]
5. recursive [multiple] : [fun/3,fun1/2,fun2/4,fun3/3]
6. non_recursive  : [start/3]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into fun4/3
1. SCC is partially evaluated into fun5/2
2. SCC is partially evaluated into fun10/2
3. SCC is partially evaluated into fun9/3
4. SCC is partially evaluated into mark/2
5. SCC is partially evaluated into fun1/2
6. SCC is partially evaluated into start/3

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

### Specialization of cost equations fun4/3 
* CE 43 is refined into CE [53] 
* CE 42 is refined into CE [54] 
* CE 41 is refined into CE [55] 


### Cost equations --> "Loop" of fun4/3 
* CEs [53] --> Loop 33 
* CEs [54] --> Loop 34 
* CEs [55] --> Loop 35 

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

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


### Specialization of cost equations fun5/2 
* CE 45 is refined into CE [56] 
* CE 44 is refined into CE [57] 


### Cost equations --> "Loop" of fun5/2 
* CEs [56] --> Loop 36 
* CEs [57] --> Loop 37 

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

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


### Specialization of cost equations fun10/2 
* CE 50 is refined into CE [58] 
* CE 51 is refined into CE [59] 
* CE 52 is refined into CE [60] 


### Cost equations --> "Loop" of fun10/2 
* CEs [58] --> Loop 38 
* CEs [59] --> Loop 39 
* CEs [60] --> Loop 40 

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

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


### Specialization of cost equations fun9/3 
* CE 47 is refined into CE [61] 
* CE 48 is refined into CE [62] 
* CE 49 is refined into CE [63] 
* CE 46 is refined into CE [64] 


### Cost equations --> "Loop" of fun9/3 
* CEs [61] --> Loop 41 
* CEs [62] --> Loop 42 
* CEs [63] --> Loop 43 
* CEs [64] --> Loop 44 

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

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


### Specialization of cost equations mark/2 
* CE 37 is refined into CE [65,66,67] 
* CE 38 is refined into CE [68] 
* CE 39 is refined into CE [69] 
* CE 40 is refined into CE [70] 
* CE 33 is refined into CE [71] 
* CE 34 is refined into CE [72] 
* CE 35 is refined into CE [73] 
* CE 36 is refined into CE [74,75,76,77] 
* CE 31 is refined into CE [78] 
* CE 32 is refined into CE [79] 
* CE 30 is refined into CE [80] 


### Cost equations --> "Loop" of mark/2 
* CEs [78] --> Loop 45 
* CEs [79] --> Loop 46 
* CEs [80] --> Loop 47 
* CEs [77] --> Loop 48 
* CEs [76] --> Loop 49 
* CEs [71] --> Loop 50 
* CEs [72] --> Loop 51 
* CEs [73] --> Loop 52 
* CEs [74] --> Loop 53 
* CEs [75] --> Loop 54 
* CEs [67] --> Loop 55 
* CEs [66,68,69] --> Loop 56 
* CEs [65,70] --> Loop 57 

### Ranking functions of CR mark(V1,Out) 
* RF of phase [45,46,47,48,49,50,51,52,53,54]: [V1]

#### Partial ranking functions of CR mark(V1,Out) 
* Partial RF of phase [45,46,47,48,49,50,51,52,53,54]:
  - RF of loop [45:1,46:1,47:1,48:1,48:2,49:1,49:2,50:1,50:2,51:1,51:2,52:1,52:2,53:1,53:2,54:1,54:2]:
    V1


### Specialization of cost equations fun1/2 
* CE 28 is refined into CE [81] 
* CE 26 is refined into CE [82] 
* CE 23 is refined into CE [83] 
* CE 29 is refined into CE [84] 
* CE 27 is refined into CE [85] 
* CE 22 is refined into CE [86,87] 
* CE 24 is refined into CE [88] 
* CE 25 is refined into CE [89] 
* CE 15 is refined into CE [90,91,92] 
* CE 16 is refined into CE [93,94,95] 
* CE 20 is refined into CE [96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114] 
* CE 21 is refined into CE [115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133] 
* CE 17 is refined into CE [134,135] 
* CE 18 is refined into CE [136] 
* CE 19 is refined into CE [137,138] 


### Cost equations --> "Loop" of fun1/2 
* CEs [134,135] --> Loop 58 
* CEs [136,137,138] --> Loop 59 
* CEs [96,98,100,102,104,107,115,117,119,121,123,126] --> Loop 60 
* CEs [90,91,92,97,99,101,103,106,109,110,112,114,116,118,120,122,125,128,129,131,133] --> Loop 61 
* CEs [93,94,95,105,108,111,113,124,127,130,132] --> Loop 62 
* CEs [81] --> Loop 63 
* CEs [82] --> Loop 64 
* CEs [87] --> Loop 65 
* CEs [83,84] --> Loop 66 
* CEs [85] --> Loop 67 
* CEs [86,88] --> Loop 68 
* CEs [89] --> Loop 69 

### Ranking functions of CR fun1(V1,Out) 
* RF of phase [58,59,60,61,62]: [V1]

#### Partial ranking functions of CR fun1(V1,Out) 
* Partial RF of phase [58,59,60,61,62]:
  - RF of loop [58:1,58:2,60:1,61:1,62:1]:
    V1
  - RF of loop [59:1,59:2]:
    V1-1


### Specialization of cost equations start/3 
* CE 4 is refined into CE [139,140,141,142,143,144,145] 
* CE 6 is refined into CE [146,147,148] 
* CE 3 is refined into CE [149,150,151,152,153,154,155] 
* CE 7 is refined into CE [156,157,158] 
* CE 1 is refined into CE [159] 
* CE 2 is refined into CE [160,161,162,163,164,165,166] 
* CE 5 is refined into CE [167] 
* CE 8 is refined into CE [168,169,170] 
* CE 9 is refined into CE [171,172,173] 
* CE 10 is refined into CE [174,175] 
* CE 11 is refined into CE [176,177,178,179,180,181,182] 
* CE 12 is refined into CE [183,184,185,186] 
* CE 13 is refined into CE [187,188,189] 
* CE 14 is refined into CE [190,191,192] 


### Cost equations --> "Loop" of start/3 
* CEs [139,140,141,142,143,144,145,146,147,148] --> Loop 70 
* CEs [149,150,151,152,153,154,155,156,157,158] --> Loop 71 
* CEs [159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192] --> Loop 72 

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

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


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

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

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

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


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

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


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

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

* Chain [38]: 0
  with precondition: [2*V1+3=Out,V1>=0] 


#### Cost of chains of fun9(V1,V,Out):
* Chain [44]: 0
  with precondition: [V1=0,Out=2,V>=0] 

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

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

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


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

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

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

* Chain [multiple([45,46,47,48,49,50,51,52,53,54],[[57],[56],[55]])]: 0
  with precondition: [V1>=1,Out>=0,5*V1>=2*Out+1,2*V1+1>=Out] 


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

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

* Chain [67]: 1
  with precondition: [V1=2,Out=4] 

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

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

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

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

* Chain [multiple([58,59,60,61,62],[[69],[68],[67],[66],[65],[64],[63]])]: 2*it(58)+2*it(59)+6*it(60)+4*it([63])+2*it([66])+1*it([67])+2*it([68])+0
  Such that:it([67]) =< V1/3+1/3
aux(16) =< V1
aux(17) =< V1+1
aux(18) =< 2*V1+1
aux(19) =< V1/2+1/2
aux(20) =< 2/3*V1
it(60) =< aux(16)
it([63]) =< aux(16)
it([67]) =< aux(16)
it([68]) =< aux(16)
it([66]) =< aux(17)
it([67]) =< aux(17)
it([68]) =< aux(17)
it(58) =< aux(18)
it(59) =< aux(18)
it(60) =< aux(18)
it([63]) =< aux(18)
it([66]) =< aux(18)
it([67]) =< aux(18)
it([68]) =< aux(18)
it([63]) =< aux(19)
it([67]) =< aux(19)
it([68]) =< aux(19)
it(59) =< aux(20)
it([67]) =< aux(20)
it(59) =< it([66])*(1/3)+it([66])*(1/3)+aux(20)
it([67]) =< it([66])*(1/3)+it([66])*(1/3)+aux(20)

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


#### Cost of chains of start(V1,V,V7):
* Chain [72]: 1*s(17)+6*s(19)+4*s(20)+2*s(21)+2*s(22)+2*s(23)+2*s(24)+1*s(29)+6*s(31)+4*s(32)+2*s(33)+2*s(34)+2*s(35)+2*s(36)+3
  Such that:s(25) =< V1
s(26) =< V1+1
s(27) =< 2*V1+1
s(28) =< V1/2+1/2
s(29) =< V1/3+1/3
s(30) =< 2/3*V1
s(13) =< V
s(14) =< V+1
s(15) =< 2*V+1
s(16) =< V/2+1/2
s(17) =< V/3+1/3
s(18) =< 2/3*V
s(31) =< s(25)
s(32) =< s(25)
s(29) =< s(25)
s(33) =< s(25)
s(34) =< s(26)
s(29) =< s(26)
s(33) =< s(26)
s(35) =< s(27)
s(36) =< s(27)
s(31) =< s(27)
s(32) =< s(27)
s(34) =< s(27)
s(29) =< s(27)
s(33) =< s(27)
s(32) =< s(28)
s(29) =< s(28)
s(33) =< s(28)
s(36) =< s(30)
s(29) =< s(30)
s(36) =< s(34)*(1/3)+s(34)*(1/3)+s(30)
s(29) =< s(34)*(1/3)+s(34)*(1/3)+s(30)
s(19) =< s(13)
s(20) =< s(13)
s(17) =< s(13)
s(21) =< s(13)
s(22) =< s(14)
s(17) =< s(14)
s(21) =< s(14)
s(23) =< s(15)
s(24) =< s(15)
s(19) =< s(15)
s(20) =< s(15)
s(22) =< s(15)
s(17) =< s(15)
s(21) =< s(15)
s(20) =< s(16)
s(17) =< s(16)
s(21) =< s(16)
s(24) =< s(18)
s(17) =< s(18)
s(24) =< s(22)*(1/3)+s(22)*(1/3)+s(18)
s(17) =< s(22)*(1/3)+s(22)*(1/3)+s(18)

  with precondition: [V1>=0] 

* Chain [71]: 1*s(41)+6*s(43)+4*s(44)+2*s(45)+2*s(46)+2*s(47)+2*s(48)+3
  Such that:s(37) =< V7
s(38) =< V7+1
s(39) =< 2*V7+1
s(40) =< V7/2+1/2
s(41) =< V7/3+1/3
s(42) =< 2/3*V7
s(43) =< s(37)
s(44) =< s(37)
s(41) =< s(37)
s(45) =< s(37)
s(46) =< s(38)
s(41) =< s(38)
s(45) =< s(38)
s(47) =< s(39)
s(48) =< s(39)
s(43) =< s(39)
s(44) =< s(39)
s(46) =< s(39)
s(41) =< s(39)
s(45) =< s(39)
s(44) =< s(40)
s(41) =< s(40)
s(45) =< s(40)
s(48) =< s(42)
s(41) =< s(42)
s(48) =< s(46)*(1/3)+s(46)*(1/3)+s(42)
s(41) =< s(46)*(1/3)+s(46)*(1/3)+s(42)

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

* Chain [70]: 1*s(53)+6*s(55)+4*s(56)+2*s(57)+2*s(58)+2*s(59)+2*s(60)+3
  Such that:s(49) =< V
s(50) =< V+1
s(51) =< 2*V+1
s(52) =< V/2+1/2
s(53) =< V/3+1/3
s(54) =< 2/3*V
s(55) =< s(49)
s(56) =< s(49)
s(53) =< s(49)
s(57) =< s(49)
s(58) =< s(50)
s(53) =< s(50)
s(57) =< s(50)
s(59) =< s(51)
s(60) =< s(51)
s(55) =< s(51)
s(56) =< s(51)
s(58) =< s(51)
s(53) =< s(51)
s(57) =< s(51)
s(56) =< s(52)
s(53) =< s(52)
s(57) =< s(52)
s(60) =< s(54)
s(53) =< s(54)
s(60) =< s(58)*(1/3)+s(58)*(1/3)+s(54)
s(53) =< s(58)*(1/3)+s(58)*(1/3)+s(54)

  with precondition: [V1=3,V>=0] 


Closed-form bounds of start(V1,V,V7): 
-------------------------------------
* Chain [72] with precondition: [V1>=0] 
    - Upper bound: V1/3+1/3+(12*V1+3+nat(V)*12+(2*V1+2)+nat(V+1)*2+(8*V1+4)+nat(2*V+1)*4)+nat(V/3+1/3) 
    - Complexity: n 
* Chain [71] with precondition: [V1=1,V>=0,V7>=0] 
    - Upper bound: 67/3*V7+28/3 
    - Complexity: n 
* Chain [70] with precondition: [V1=3,V>=0] 
    - Upper bound: 67/3*V+28/3 
    - Complexity: n 

### Maximum cost of start(V1,V,V7): max([nat(V7+1)*2+nat(V7)*12+nat(2*V7+1)*4+nat(V7/3+1/3),nat(V+1)*2+nat(V)*12+nat(2*V+1)*4+nat(V/3+1/3)+(67/3*V1+19/3)])+3 
Asymptotic class: n 
* Total analysis performed in 963 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:

   A__AND(true, z0) -> c(MARK(z0))
   A__AND(false, z0) -> c1
   A__AND(z0, z1) -> c2
   A__IF(true, z0, z1) -> c3(MARK(z0))
   A__IF(false, z0, z1) -> c4(MARK(z1))
   A__IF(z0, z1, z2) -> c5
   A__ADD(0, z0) -> c6(MARK(z0))
   A__ADD(s(z0), z1) -> c7
   A__ADD(z0, z1) -> c8
   A__FIRST(0, z0) -> c9
   A__FIRST(s(z0), cons(z1, z2)) -> c10
   A__FIRST(z0, z1) -> c11
   A__FROM(z0) -> c12
   A__FROM(z0) -> c13
   MARK(and(z0, z1)) -> c14(A__AND(mark(z0), z1), MARK(z0))
   MARK(if(z0, z1, z2)) -> c15(A__IF(mark(z0), z1, z2), MARK(z0))
   MARK(add(z0, z1)) -> c16(A__ADD(mark(z0), z1), MARK(z0))
   MARK(first(z0, z1)) -> c17(A__FIRST(mark(z0), mark(z1)), MARK(z0))
   MARK(first(z0, z1)) -> c18(A__FIRST(mark(z0), mark(z1)), MARK(z1))
   MARK(from(z0)) -> c19(A__FROM(z0))
   MARK(true) -> c20
   MARK(false) -> c21
   MARK(0) -> c22
   MARK(s(z0)) -> c23
   MARK(nil) -> c24
   MARK(cons(z0, z1)) -> c25

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

   a__and(true, z0) -> mark(z0)
   a__and(false, z0) -> false
   a__and(z0, z1) -> and(z0, z1)
   a__if(true, z0, z1) -> mark(z0)
   a__if(false, z0, z1) -> mark(z1)
   a__if(z0, z1, z2) -> if(z0, z1, z2)
   a__add(0, z0) -> mark(z0)
   a__add(s(z0), z1) -> s(add(z0, z1))
   a__add(z0, z1) -> add(z0, z1)
   a__first(0, z0) -> nil
   a__first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2))
   a__first(z0, z1) -> first(z0, z1)
   a__from(z0) -> cons(z0, from(s(z0)))
   a__from(z0) -> from(z0)
   mark(and(z0, z1)) -> a__and(mark(z0), z1)
   mark(if(z0, z1, z2)) -> a__if(mark(z0), z1, z2)
   mark(add(z0, z1)) -> a__add(mark(z0), z1)
   mark(first(z0, z1)) -> a__first(mark(z0), mark(z1))
   mark(from(z0)) -> a__from(z0)
   mark(true) -> true
   mark(false) -> false
   mark(0) -> 0
   mark(s(z0)) -> s(z0)
   mark(nil) -> nil
   mark(cons(z0, z1)) -> cons(z0, z1)

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

MARK(first(z0, z1)) ->^+ c17(A__FIRST(mark(z0), mark(z1)), MARK(z0))

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

The pumping substitution is [z0 / first(z0, z1)].

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:

   A__AND(true, z0) -> c(MARK(z0))
   A__AND(false, z0) -> c1
   A__AND(z0, z1) -> c2
   A__IF(true, z0, z1) -> c3(MARK(z0))
   A__IF(false, z0, z1) -> c4(MARK(z1))
   A__IF(z0, z1, z2) -> c5
   A__ADD(0, z0) -> c6(MARK(z0))
   A__ADD(s(z0), z1) -> c7
   A__ADD(z0, z1) -> c8
   A__FIRST(0, z0) -> c9
   A__FIRST(s(z0), cons(z1, z2)) -> c10
   A__FIRST(z0, z1) -> c11
   A__FROM(z0) -> c12
   A__FROM(z0) -> c13
   MARK(and(z0, z1)) -> c14(A__AND(mark(z0), z1), MARK(z0))
   MARK(if(z0, z1, z2)) -> c15(A__IF(mark(z0), z1, z2), MARK(z0))
   MARK(add(z0, z1)) -> c16(A__ADD(mark(z0), z1), MARK(z0))
   MARK(first(z0, z1)) -> c17(A__FIRST(mark(z0), mark(z1)), MARK(z0))
   MARK(first(z0, z1)) -> c18(A__FIRST(mark(z0), mark(z1)), MARK(z1))
   MARK(from(z0)) -> c19(A__FROM(z0))
   MARK(true) -> c20
   MARK(false) -> c21
   MARK(0) -> c22
   MARK(s(z0)) -> c23
   MARK(nil) -> c24
   MARK(cons(z0, z1)) -> c25

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

   a__and(true, z0) -> mark(z0)
   a__and(false, z0) -> false
   a__and(z0, z1) -> and(z0, z1)
   a__if(true, z0, z1) -> mark(z0)
   a__if(false, z0, z1) -> mark(z1)
   a__if(z0, z1, z2) -> if(z0, z1, z2)
   a__add(0, z0) -> mark(z0)
   a__add(s(z0), z1) -> s(add(z0, z1))
   a__add(z0, z1) -> add(z0, z1)
   a__first(0, z0) -> nil
   a__first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2))
   a__first(z0, z1) -> first(z0, z1)
   a__from(z0) -> cons(z0, from(s(z0)))
   a__from(z0) -> from(z0)
   mark(and(z0, z1)) -> a__and(mark(z0), z1)
   mark(if(z0, z1, z2)) -> a__if(mark(z0), z1, z2)
   mark(add(z0, z1)) -> a__add(mark(z0), z1)
   mark(first(z0, z1)) -> a__first(mark(z0), mark(z1))
   mark(from(z0)) -> a__from(z0)
   mark(true) -> true
   mark(false) -> false
   mark(0) -> 0
   mark(s(z0)) -> s(z0)
   mark(nil) -> nil
   mark(cons(z0, z1)) -> cons(z0, z1)

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:

   A__AND(true, z0) -> c(MARK(z0))
   A__AND(false, z0) -> c1
   A__AND(z0, z1) -> c2
   A__IF(true, z0, z1) -> c3(MARK(z0))
   A__IF(false, z0, z1) -> c4(MARK(z1))
   A__IF(z0, z1, z2) -> c5
   A__ADD(0, z0) -> c6(MARK(z0))
   A__ADD(s(z0), z1) -> c7
   A__ADD(z0, z1) -> c8
   A__FIRST(0, z0) -> c9
   A__FIRST(s(z0), cons(z1, z2)) -> c10
   A__FIRST(z0, z1) -> c11
   A__FROM(z0) -> c12
   A__FROM(z0) -> c13
   MARK(and(z0, z1)) -> c14(A__AND(mark(z0), z1), MARK(z0))
   MARK(if(z0, z1, z2)) -> c15(A__IF(mark(z0), z1, z2), MARK(z0))
   MARK(add(z0, z1)) -> c16(A__ADD(mark(z0), z1), MARK(z0))
   MARK(first(z0, z1)) -> c17(A__FIRST(mark(z0), mark(z1)), MARK(z0))
   MARK(first(z0, z1)) -> c18(A__FIRST(mark(z0), mark(z1)), MARK(z1))
   MARK(from(z0)) -> c19(A__FROM(z0))
   MARK(true) -> c20
   MARK(false) -> c21
   MARK(0) -> c22
   MARK(s(z0)) -> c23
   MARK(nil) -> c24
   MARK(cons(z0, z1)) -> c25

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

   a__and(true, z0) -> mark(z0)
   a__and(false, z0) -> false
   a__and(z0, z1) -> and(z0, z1)
   a__if(true, z0, z1) -> mark(z0)
   a__if(false, z0, z1) -> mark(z1)
   a__if(z0, z1, z2) -> if(z0, z1, z2)
   a__add(0, z0) -> mark(z0)
   a__add(s(z0), z1) -> s(add(z0, z1))
   a__add(z0, z1) -> add(z0, z1)
   a__first(0, z0) -> nil
   a__first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2))
   a__first(z0, z1) -> first(z0, z1)
   a__from(z0) -> cons(z0, from(s(z0)))
   a__from(z0) -> from(z0)
   mark(and(z0, z1)) -> a__and(mark(z0), z1)
   mark(if(z0, z1, z2)) -> a__if(mark(z0), z1, z2)
   mark(add(z0, z1)) -> a__add(mark(z0), z1)
   mark(first(z0, z1)) -> a__first(mark(z0), mark(z1))
   mark(from(z0)) -> a__from(z0)
   mark(true) -> true
   mark(false) -> false
   mark(0) -> 0
   mark(s(z0)) -> s(z0)
   mark(nil) -> nil
   mark(cons(z0, z1)) -> cons(z0, z1)

Rewrite Strategy: INNERMOST