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), 554 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, 517 ms]
    (12) BOUNDS(1, n^1)
(13) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
(14) TRS for Loop Detection
    (15) DecreasingLoopProof [LOWER BOUND(ID), 31 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:

   IS_EMPTY(nil) -> c
   IS_EMPTY(cons(z0, z1)) -> c1
   HD(cons(z0, z1)) -> c2
   TL(cons(z0, z1)) -> c3
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0))
   IFAPPEND(z0, z1, true) -> c5
   IFAPPEND(z0, z1, false) -> c6(HD(z0))
   IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0))

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

   is_empty(nil) -> true
   is_empty(cons(z0, z1)) -> false
   hd(cons(z0, z1)) -> z0
   tl(cons(z0, z1)) -> z1
   append(z0, z1) -> ifappend(z0, z1, is_empty(z0))
   ifappend(z0, z1, true) -> z1
   ifappend(z0, z1, false) -> cons(hd(z0), append(tl(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:

   IS_EMPTY(nil) -> c
   IS_EMPTY(cons(z0, z1)) -> c1
   HD(cons(z0, z1)) -> c2
   TL(cons(z0, z1)) -> c3
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0))
   IFAPPEND(z0, z1, true) -> c5
   IFAPPEND(z0, z1, false) -> c6(HD(z0))
   IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0))

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

   is_empty(nil) -> true
   is_empty(cons(z0, z1)) -> false
   hd(cons(z0, z1)) -> z0
   tl(cons(z0, z1)) -> z1
   append(z0, z1) -> ifappend(z0, z1, is_empty(z0))
   ifappend(z0, z1, true) -> z1
   ifappend(z0, z1, false) -> cons(hd(z0), append(tl(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:

   IS_EMPTY(nil) -> c [1]
   IS_EMPTY(cons(z0, z1)) -> c1 [1]
   HD(cons(z0, z1)) -> c2 [1]
   TL(cons(z0, z1)) -> c3 [1]
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0)) [1]
   IFAPPEND(z0, z1, true) -> c5 [1]
   IFAPPEND(z0, z1, false) -> c6(HD(z0)) [1]
   IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0)) [1]
   is_empty(nil) -> true [0]
   is_empty(cons(z0, z1)) -> false [0]
   hd(cons(z0, z1)) -> z0 [0]
   tl(cons(z0, z1)) -> z1 [0]
   append(z0, z1) -> ifappend(z0, z1, is_empty(z0)) [0]
   ifappend(z0, z1, true) -> z1 [0]
   ifappend(z0, z1, false) -> cons(hd(z0), append(tl(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:

   IS_EMPTY(nil) -> c [1]
   IS_EMPTY(cons(z0, z1)) -> c1 [1]
   HD(cons(z0, z1)) -> c2 [1]
   TL(cons(z0, z1)) -> c3 [1]
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0)) [1]
   IFAPPEND(z0, z1, true) -> c5 [1]
   IFAPPEND(z0, z1, false) -> c6(HD(z0)) [1]
   IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0)) [1]
   is_empty(nil) -> true [0]
   is_empty(cons(z0, z1)) -> false [0]
   hd(cons(z0, z1)) -> z0 [0]
   tl(cons(z0, z1)) -> z1 [0]
   append(z0, z1) -> ifappend(z0, z1, is_empty(z0)) [0]
   ifappend(z0, z1, true) -> z1 [0]
   ifappend(z0, z1, false) -> cons(hd(z0), append(tl(z0), z1)) [0]

The TRS has the following type information:
IS_EMPTY :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: hd -> nil:cons -> nil:cons
c1 :: c:c1
HD :: nil:cons -> c2
c2 :: c2
TL :: nil:cons -> c3
c3 :: c3
APPEND :: nil:cons -> a -> c4
c4 :: c5:c6:c7 -> c:c1 -> c4
IFAPPEND :: nil:cons -> a -> true:false -> c5:c6:c7
is_empty :: nil:cons -> true:false
true :: true:false
c5 :: c5:c6:c7
false :: true:false
c6 :: c2 -> c5:c6:c7
c7 :: c4 -> c3 -> c5:c6:c7
tl :: nil:cons -> nil:cons
hd :: nil:cons -> hd
append :: nil:cons -> nil:cons -> nil:cons
ifappend :: nil:cons -> nil:cons -> true:false -> 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:

   is_empty(v0) -> null_is_empty [0]
   hd(v0) -> null_hd [0]
   tl(v0) -> null_tl [0]
   append(v0, v1) -> null_append [0]
   ifappend(v0, v1, v2) -> null_ifappend [0]
   IS_EMPTY(v0) -> null_IS_EMPTY [0]
   HD(v0) -> null_HD [0]
   TL(v0) -> null_TL [0]
   IFAPPEND(v0, v1, v2) -> null_IFAPPEND [0]

And the following fresh constants:    null_is_empty, null_hd, null_tl, null_append, null_ifappend, null_IS_EMPTY, null_HD, null_TL, null_IFAPPEND, const, const1

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

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

   IS_EMPTY(nil) -> c [1]
   IS_EMPTY(cons(z0, z1)) -> c1 [1]
   HD(cons(z0, z1)) -> c2 [1]
   TL(cons(z0, z1)) -> c3 [1]
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0)) [1]
   IFAPPEND(z0, z1, true) -> c5 [1]
   IFAPPEND(z0, z1, false) -> c6(HD(z0)) [1]
   IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0)) [1]
   is_empty(nil) -> true [0]
   is_empty(cons(z0, z1)) -> false [0]
   hd(cons(z0, z1)) -> z0 [0]
   tl(cons(z0, z1)) -> z1 [0]
   append(z0, z1) -> ifappend(z0, z1, is_empty(z0)) [0]
   ifappend(z0, z1, true) -> z1 [0]
   ifappend(z0, z1, false) -> cons(hd(z0), append(tl(z0), z1)) [0]
   is_empty(v0) -> null_is_empty [0]
   hd(v0) -> null_hd [0]
   tl(v0) -> null_tl [0]
   append(v0, v1) -> null_append [0]
   ifappend(v0, v1, v2) -> null_ifappend [0]
   IS_EMPTY(v0) -> null_IS_EMPTY [0]
   HD(v0) -> null_HD [0]
   TL(v0) -> null_TL [0]
   IFAPPEND(v0, v1, v2) -> null_IFAPPEND [0]

The TRS has the following type information:
IS_EMPTY :: nil:cons:null_tl:null_append:null_ifappend -> c:c1:null_IS_EMPTY
nil :: nil:cons:null_tl:null_append:null_ifappend
c :: c:c1:null_IS_EMPTY
cons :: null_hd -> nil:cons:null_tl:null_append:null_ifappend -> nil:cons:null_tl:null_append:null_ifappend
c1 :: c:c1:null_IS_EMPTY
HD :: nil:cons:null_tl:null_append:null_ifappend -> c2:null_HD
c2 :: c2:null_HD
TL :: nil:cons:null_tl:null_append:null_ifappend -> c3:null_TL
c3 :: c3:null_TL
APPEND :: nil:cons:null_tl:null_append:null_ifappend -> a -> c4
c4 :: c5:c6:c7:null_IFAPPEND -> c:c1:null_IS_EMPTY -> c4
IFAPPEND :: nil:cons:null_tl:null_append:null_ifappend -> a -> true:false:null_is_empty -> c5:c6:c7:null_IFAPPEND
is_empty :: nil:cons:null_tl:null_append:null_ifappend -> true:false:null_is_empty
true :: true:false:null_is_empty
c5 :: c5:c6:c7:null_IFAPPEND
false :: true:false:null_is_empty
c6 :: c2:null_HD -> c5:c6:c7:null_IFAPPEND
c7 :: c4 -> c3:null_TL -> c5:c6:c7:null_IFAPPEND
tl :: nil:cons:null_tl:null_append:null_ifappend -> nil:cons:null_tl:null_append:null_ifappend
hd :: nil:cons:null_tl:null_append:null_ifappend -> null_hd
append :: nil:cons:null_tl:null_append:null_ifappend -> nil:cons:null_tl:null_append:null_ifappend -> nil:cons:null_tl:null_append:null_ifappend
ifappend :: nil:cons:null_tl:null_append:null_ifappend -> nil:cons:null_tl:null_append:null_ifappend -> true:false:null_is_empty -> nil:cons:null_tl:null_append:null_ifappend
null_is_empty :: true:false:null_is_empty
null_hd :: null_hd
null_tl :: nil:cons:null_tl:null_append:null_ifappend
null_append :: nil:cons:null_tl:null_append:null_ifappend
null_ifappend :: nil:cons:null_tl:null_append:null_ifappend
null_IS_EMPTY :: c:c1:null_IS_EMPTY
null_HD :: c2:null_HD
null_TL :: c3:null_TL
null_IFAPPEND :: c5:c6:c7:null_IFAPPEND
const :: c4
const1 :: a

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
   c => 1
   c1 => 2
   c2 => 1
   c3 => 1
   true => 2
   c5 => 0
   false => 1
   null_is_empty => 0
   null_hd => 0
   null_tl => 0
   null_append => 0
   null_ifappend => 0
   null_IS_EMPTY => 0
   null_HD => 0
   null_TL => 0
   null_IFAPPEND => 0
   const => 0
   const1 => 0

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

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

   APPEND(z, z') -{ 1 }-> 1 + IFAPPEND(z0, z1, is_empty(z0)) + IS_EMPTY(z0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   HD(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   HD(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   IFAPPEND(z, z', z'') -{ 1 }-> 0 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 2
   IFAPPEND(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   IFAPPEND(z, z', z'') -{ 1 }-> 1 + HD(z0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 1
   IFAPPEND(z, z', z'') -{ 1 }-> 1 + APPEND(tl(z0), z1) + TL(z0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 1
   IS_EMPTY(z) -{ 1 }-> 2 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   IS_EMPTY(z) -{ 1 }-> 1 :|: z = 0
   IS_EMPTY(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   TL(z) -{ 1 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   TL(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   append(z, z') -{ 0 }-> ifappend(z0, z1, is_empty(z0)) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   append(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   hd(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   hd(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   ifappend(z, z', z'') -{ 0 }-> z1 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 2
   ifappend(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   ifappend(z, z', z'') -{ 0 }-> 1 + hd(z0) + append(tl(z0), z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 1
   is_empty(z) -{ 0 }-> 2 :|: z = 0
   is_empty(z) -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   is_empty(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   tl(z) -{ 0 }-> z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   tl(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0

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(V, V8, V12),0,[fun(V, Out)],[V >= 0]).
eq(start(V, V8, V12),0,[fun1(V, Out)],[V >= 0]).
eq(start(V, V8, V12),0,[fun2(V, Out)],[V >= 0]).
eq(start(V, V8, V12),0,[fun3(V, V8, Out)],[V >= 0,V8 >= 0]).
eq(start(V, V8, V12),0,[fun4(V, V8, V12, Out)],[V >= 0,V8 >= 0,V12 >= 0]).
eq(start(V, V8, V12),0,[fun5(V, Out)],[V >= 0]).
eq(start(V, V8, V12),0,[hd(V, Out)],[V >= 0]).
eq(start(V, V8, V12),0,[tl(V, Out)],[V >= 0]).
eq(start(V, V8, V12),0,[append(V, V8, Out)],[V >= 0,V8 >= 0]).
eq(start(V, V8, V12),0,[ifappend(V, V8, V12, Out)],[V >= 0,V8 >= 0,V12 >= 0]).
eq(fun(V, Out),1,[],[Out = 1,V = 0]).
eq(fun(V, Out),1,[],[Out = 2,V1 >= 0,V2 >= 0,V = 1 + V1 + V2]).
eq(fun1(V, Out),1,[],[Out = 1,V3 >= 0,V4 >= 0,V = 1 + V3 + V4]).
eq(fun2(V, Out),1,[],[Out = 1,V5 >= 0,V6 >= 0,V = 1 + V5 + V6]).
eq(fun3(V, V8, Out),1,[fun5(V7, Ret012),fun4(V7, V9, Ret012, Ret01),fun(V7, Ret1)],[Out = 1 + Ret01 + Ret1,V = V7,V9 >= 0,V8 = V9,V7 >= 0]).
eq(fun4(V, V8, V12, Out),1,[],[Out = 0,V = V11,V10 >= 0,V8 = V10,V11 >= 0,V12 = 2]).
eq(fun4(V, V8, V12, Out),1,[fun1(V14, Ret11)],[Out = 1 + Ret11,V = V14,V13 >= 0,V8 = V13,V14 >= 0,V12 = 1]).
eq(fun4(V, V8, V12, Out),1,[tl(V16, Ret010),fun3(Ret010, V15, Ret011),fun2(V16, Ret12)],[Out = 1 + Ret011 + Ret12,V = V16,V15 >= 0,V8 = V15,V16 >= 0,V12 = 1]).
eq(fun5(V, Out),0,[],[Out = 2,V = 0]).
eq(fun5(V, Out),0,[],[Out = 1,V17 >= 0,V18 >= 0,V = 1 + V17 + V18]).
eq(hd(V, Out),0,[],[Out = V20,V19 >= 0,V20 >= 0,V = 1 + V19 + V20]).
eq(tl(V, Out),0,[],[Out = V22,V22 >= 0,V21 >= 0,V = 1 + V21 + V22]).
eq(append(V, V8, Out),0,[fun5(V23, Ret2),ifappend(V23, V24, Ret2, Ret)],[Out = Ret,V = V23,V24 >= 0,V8 = V24,V23 >= 0]).
eq(ifappend(V, V8, V12, Out),0,[],[Out = V25,V = V26,V25 >= 0,V8 = V25,V26 >= 0,V12 = 2]).
eq(ifappend(V, V8, V12, Out),0,[hd(V27, Ret013),tl(V27, Ret10),append(Ret10, V28, Ret13)],[Out = 1 + Ret013 + Ret13,V = V27,V28 >= 0,V8 = V28,V27 >= 0,V12 = 1]).
eq(fun5(V, Out),0,[],[Out = 0,V29 >= 0,V = V29]).
eq(hd(V, Out),0,[],[Out = 0,V30 >= 0,V = V30]).
eq(tl(V, Out),0,[],[Out = 0,V31 >= 0,V = V31]).
eq(append(V, V8, Out),0,[],[Out = 0,V32 >= 0,V33 >= 0,V = V32,V8 = V33]).
eq(ifappend(V, V8, V12, Out),0,[],[Out = 0,V34 >= 0,V12 = V36,V35 >= 0,V = V34,V8 = V35,V36 >= 0]).
eq(fun(V, Out),0,[],[Out = 0,V37 >= 0,V = V37]).
eq(fun1(V, Out),0,[],[Out = 0,V38 >= 0,V = V38]).
eq(fun2(V, Out),0,[],[Out = 0,V39 >= 0,V = V39]).
eq(fun4(V, V8, V12, Out),0,[],[Out = 0,V40 >= 0,V12 = V41,V42 >= 0,V = V40,V8 = V42,V41 >= 0]).
input_output_vars(fun(V,Out),[V],[Out]).
input_output_vars(fun1(V,Out),[V],[Out]).
input_output_vars(fun2(V,Out),[V],[Out]).
input_output_vars(fun3(V,V8,Out),[V,V8],[Out]).
input_output_vars(fun4(V,V8,V12,Out),[V,V8,V12],[Out]).
input_output_vars(fun5(V,Out),[V],[Out]).
input_output_vars(hd(V,Out),[V],[Out]).
input_output_vars(tl(V,Out),[V],[Out]).
input_output_vars(append(V,V8,Out),[V,V8],[Out]).
input_output_vars(ifappend(V,V8,V12,Out),[V,V8,V12],[Out]).


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

#### Computed strongly connected components 
0. non_recursive  : [fun5/2]
1. non_recursive  : [hd/2]
2. non_recursive  : [tl/2]
3. recursive  : [append/3,ifappend/4]
4. non_recursive  : [fun/2]
5. non_recursive  : [fun1/2]
6. non_recursive  : [fun2/2]
7. recursive [non_tail] : [fun3/3,fun4/4]
8. non_recursive  : [start/3]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into fun5/2
1. SCC is partially evaluated into hd/2
2. SCC is partially evaluated into tl/2
3. SCC is partially evaluated into append/3
4. SCC is partially evaluated into fun/2
5. SCC is partially evaluated into fun1/2
6. SCC is partially evaluated into fun2/2
7. SCC is partially evaluated into fun3/3
8. SCC is partially evaluated into start/3

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

### Specialization of cost equations fun5/2 
* CE 34 is refined into CE [36] 
* CE 35 is refined into CE [37] 
* CE 33 is refined into CE [38] 


### Cost equations --> "Loop" of fun5/2 
* CEs [36] --> Loop 22 
* CEs [37] --> Loop 23 
* CEs [38] --> Loop 24 

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

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


### Specialization of cost equations hd/2 
* CE 24 is refined into CE [39] 
* CE 25 is refined into CE [40] 


### Cost equations --> "Loop" of hd/2 
* CEs [39] --> Loop 25 
* CEs [40] --> Loop 26 

### Ranking functions of CR hd(V,Out) 

#### Partial ranking functions of CR hd(V,Out) 


### Specialization of cost equations tl/2 
* CE 14 is refined into CE [41] 
* CE 15 is refined into CE [42] 


### Cost equations --> "Loop" of tl/2 
* CEs [41] --> Loop 27 
* CEs [42] --> Loop 28 

### Ranking functions of CR tl(V,Out) 

#### Partial ranking functions of CR tl(V,Out) 


### Specialization of cost equations append/3 
* CE 28 is refined into CE [43] 
* CE 26 is refined into CE [44,45,46] 
* CE 29 is refined into CE [47] 
* CE 27 is refined into CE [48,49,50,51] 


### Cost equations --> "Loop" of append/3 
* CEs [49] --> Loop 29 
* CEs [48,50,51] --> Loop 30 
* CEs [43] --> Loop 31 
* CEs [44,45,46,47] --> Loop 32 

### Ranking functions of CR append(V,V8,Out) 
* RF of phase [29,30]: [V]

#### Partial ranking functions of CR append(V,V8,Out) 
* Partial RF of phase [29,30]:
  - RF of loop [29:1,30:1]:
    V


### Specialization of cost equations fun/2 
* CE 31 is refined into CE [52] 
* CE 32 is refined into CE [53] 
* CE 30 is refined into CE [54] 


### Cost equations --> "Loop" of fun/2 
* CEs [52] --> Loop 33 
* CEs [53] --> Loop 34 
* CEs [54] --> Loop 35 

### Ranking functions of CR fun(V,Out) 

#### Partial ranking functions of CR fun(V,Out) 


### Specialization of cost equations fun1/2 
* CE 22 is refined into CE [55] 
* CE 23 is refined into CE [56] 


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

### Ranking functions of CR fun1(V,Out) 

#### Partial ranking functions of CR fun1(V,Out) 


### Specialization of cost equations fun2/2 
* CE 20 is refined into CE [57] 
* CE 21 is refined into CE [58] 


### Cost equations --> "Loop" of fun2/2 
* CEs [57] --> Loop 38 
* CEs [58] --> Loop 39 

### Ranking functions of CR fun2(V,Out) 

#### Partial ranking functions of CR fun2(V,Out) 


### Specialization of cost equations fun3/3 
* CE 16 is refined into CE [59,60,61,62,63,64,65] 
* CE 18 is refined into CE [66,67,68,69] 
* CE 19 is refined into CE [70,71] 
* CE 17 is refined into CE [72,73,74,75,76,77,78,79] 


### Cost equations --> "Loop" of fun3/3 
* CEs [75,79] --> Loop 40 
* CEs [73,77] --> Loop 41 
* CEs [74,78] --> Loop 42 
* CEs [72,76] --> Loop 43 
* CEs [69] --> Loop 44 
* CEs [67] --> Loop 45 
* CEs [63,65,68] --> Loop 46 
* CEs [66] --> Loop 47 
* CEs [59,61,70] --> Loop 48 
* CEs [60,62,64,71] --> Loop 49 

### Ranking functions of CR fun3(V,V8,Out) 
* RF of phase [40,41,42,43]: [V]

#### Partial ranking functions of CR fun3(V,V8,Out) 
* Partial RF of phase [40,41,42,43]:
  - RF of loop [40:1,41:1,42:1,43:1]:
    V


### Specialization of cost equations start/3 
* CE 4 is refined into CE [80] 
* CE 1 is refined into CE [81] 
* CE 2 is refined into CE [82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97] 
* CE 3 is refined into CE [98,99] 
* CE 5 is refined into CE [100,101,102,103,104,105,106,107,108,109] 
* CE 6 is refined into CE [110,111,112] 
* CE 7 is refined into CE [113,114] 
* CE 8 is refined into CE [115,116] 
* CE 9 is refined into CE [117,118,119,120,121,122] 
* CE 10 is refined into CE [123,124,125] 
* CE 11 is refined into CE [126,127] 
* CE 12 is refined into CE [128,129] 
* CE 13 is refined into CE [130,131,132] 


### Cost equations --> "Loop" of start/3 
* CEs [80] --> Loop 50 
* CEs [82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109] --> Loop 51 
* CEs [81,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132] --> Loop 52 

### Ranking functions of CR start(V,V8,V12) 

#### Partial ranking functions of CR start(V,V8,V12) 


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

#### Cost of chains of fun5(V,Out):
* Chain [24]: 0
  with precondition: [V=0,Out=2] 

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

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


#### Cost of chains of hd(V,Out):
* Chain [26]: 0
  with precondition: [Out=0,V>=0] 

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


#### Cost of chains of tl(V,Out):
* Chain [28]: 0
  with precondition: [Out=0,V>=0] 

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


#### Cost of chains of append(V,V8,Out):
* Chain [[29,30],32]: 0
  with precondition: [V>=1,V8>=0,Out>=1] 

* Chain [[29,30],31]: 0
  with precondition: [V>=1,V8>=0,Out>=V8+1] 

* Chain [32]: 0
  with precondition: [Out=0,V>=0,V8>=0] 

* Chain [31]: 0
  with precondition: [V=0,V8=Out,V8>=0] 


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

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

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


#### Cost of chains of fun1(V,Out):
* Chain [37]: 0
  with precondition: [Out=0,V>=0] 

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


#### Cost of chains of fun2(V,Out):
* Chain [39]: 0
  with precondition: [Out=0,V>=0] 

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


#### Cost of chains of fun3(V,V8,Out):
* Chain [[40,41,42,43],49]: 12*it(40)+2
  Such that:aux(5) =< V
it(40) =< aux(5)

  with precondition: [V>=1,V8>=0,Out>=3,5*V+1>=Out] 

* Chain [[40,41,42,43],48]: 12*it(40)+3
  Such that:aux(6) =< V
it(40) =< aux(6)

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

* Chain [[40,41,42,43],47]: 12*it(40)+2
  Such that:aux(7) =< V
it(40) =< aux(7)

  with precondition: [V>=2,V8>=0,Out>=4,5*V>=Out+3] 

* Chain [[40,41,42,43],46]: 12*it(40)+3
  Such that:aux(8) =< V
it(40) =< aux(8)

  with precondition: [V>=2,V8>=0,Out>=5,5*V>=Out+2] 

* Chain [[40,41,42,43],45]: 12*it(40)+3
  Such that:aux(9) =< V
it(40) =< aux(9)

  with precondition: [V>=2,V8>=0,Out>=6,5*V>=Out+1] 

* Chain [[40,41,42,43],44]: 12*it(40)+4
  Such that:aux(10) =< V
it(40) =< aux(10)

  with precondition: [V>=2,V8>=0,Out>=7,5*V>=Out] 

* Chain [49]: 2
  with precondition: [Out=1,V>=0,V8>=0] 

* Chain [48]: 3
  with precondition: [V=0,Out=2,V8>=0] 

* Chain [47]: 2
  with precondition: [Out=2,V>=1,V8>=0] 

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

* Chain [45]: 3
  with precondition: [Out=4,V>=1,V8>=0] 

* Chain [44]: 4
  with precondition: [Out=5,V>=1,V8>=0] 


#### Cost of chains of start(V,V8,V12):
* Chain [52]: 72*s(14)+4
  Such that:aux(12) =< V
s(14) =< aux(12)

  with precondition: [V>=0] 

* Chain [51]: 144*s(18)+6
  Such that:aux(13) =< V
s(18) =< aux(13)

  with precondition: [V12=1,V>=0,V8>=0] 

* Chain [50]: 1
  with precondition: [V12=2,V>=0,V8>=0] 


Closed-form bounds of start(V,V8,V12): 
-------------------------------------
* Chain [52] with precondition: [V>=0] 
    - Upper bound: 72*V+4 
    - Complexity: n 
* Chain [51] with precondition: [V12=1,V>=0,V8>=0] 
    - Upper bound: 144*V+6 
    - Complexity: n 
* Chain [50] with precondition: [V12=2,V>=0,V8>=0] 
    - Upper bound: 1 
    - Complexity: constant 

### Maximum cost of start(V,V8,V12): 144*V+6 
Asymptotic class: n 
* Total analysis performed in 492 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:

   IS_EMPTY(nil) -> c
   IS_EMPTY(cons(z0, z1)) -> c1
   HD(cons(z0, z1)) -> c2
   TL(cons(z0, z1)) -> c3
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0))
   IFAPPEND(z0, z1, true) -> c5
   IFAPPEND(z0, z1, false) -> c6(HD(z0))
   IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0))

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

   is_empty(nil) -> true
   is_empty(cons(z0, z1)) -> false
   hd(cons(z0, z1)) -> z0
   tl(cons(z0, z1)) -> z1
   append(z0, z1) -> ifappend(z0, z1, is_empty(z0))
   ifappend(z0, z1, true) -> z1
   ifappend(z0, z1, false) -> cons(hd(z0), append(tl(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

IFAPPEND(cons(z01_2, cons(z01_0, z12_0)), z1, false) ->^+ c7(c4(IFAPPEND(cons(z01_0, z12_0), z1, false), IS_EMPTY(cons(z01_0, z12_0))), TL(cons(z01_2, cons(z01_0, z12_0))))

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

The pumping substitution is [z12_0 / cons(z01_0, z12_0)].

The result substitution is [z01_2 / z01_0].




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

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

   IS_EMPTY(nil) -> c
   IS_EMPTY(cons(z0, z1)) -> c1
   HD(cons(z0, z1)) -> c2
   TL(cons(z0, z1)) -> c3
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0))
   IFAPPEND(z0, z1, true) -> c5
   IFAPPEND(z0, z1, false) -> c6(HD(z0))
   IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0))

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

   is_empty(nil) -> true
   is_empty(cons(z0, z1)) -> false
   hd(cons(z0, z1)) -> z0
   tl(cons(z0, z1)) -> z1
   append(z0, z1) -> ifappend(z0, z1, is_empty(z0))
   ifappend(z0, z1, true) -> z1
   ifappend(z0, z1, false) -> cons(hd(z0), append(tl(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:

   IS_EMPTY(nil) -> c
   IS_EMPTY(cons(z0, z1)) -> c1
   HD(cons(z0, z1)) -> c2
   TL(cons(z0, z1)) -> c3
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0))
   IFAPPEND(z0, z1, true) -> c5
   IFAPPEND(z0, z1, false) -> c6(HD(z0))
   IFAPPEND(z0, z1, false) -> c7(APPEND(tl(z0), z1), TL(z0))

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

   is_empty(nil) -> true
   is_empty(cons(z0, z1)) -> false
   hd(cons(z0, z1)) -> z0
   tl(cons(z0, z1)) -> z1
   append(z0, z1) -> ifappend(z0, z1, is_empty(z0))
   ifappend(z0, z1, true) -> z1
   ifappend(z0, z1, false) -> cons(hd(z0), append(tl(z0), z1))

Rewrite Strategy: INNERMOST