WORST_CASE(Omega(n^1),O(n^1))
proof of input_ICBPtBhwvk.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
    (3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (4) CdtProblem
    (5) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CpxTRS
    (9) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CpxWeightedTrs
    (11) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) CpxTypedWeightedTrs
    (13) CompletionProof [UPPER BOUND(ID), 0 ms]
    (14) CpxTypedWeightedCompleteTrs
    (15) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
    (16) CpxRNTS
    (17) CompleteCoflocoProof [FINISHED, 83 ms]
    (18) BOUNDS(1, n^1)
(19) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(20) CdtProblem
    (21) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (22) CpxRelTRS
    (23) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (24) CpxRelTRS
    (25) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (26) typed CpxTrs
    (27) OrderProof [LOWER BOUND(ID), 18 ms]
    (28) typed CpxTrs
    (29) RewriteLemmaProof [LOWER BOUND(ID), 873 ms]
    (30) BEST
        (31) proven lower bound
            (32) LowerBoundPropagationProof [FINISHED, 0 ms]
            (33) BOUNDS(n^1, INF)
        (34) typed CpxTrs
            (35) RewriteLemmaProof [LOWER BOUND(ID), 9 ms]
            (36) BOUNDS(1, INF)


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

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


The TRS R consists of the following rules:

   is_empty(nil) -> true
   is_empty(cons(x, l)) -> false
   hd(cons(x, l)) -> x
   tl(cons(x, l)) -> l
   append(l1, l2) -> ifappend(l1, l2, l1)
   ifappend(l1, l2, nil) -> l2
   ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2))

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

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, z0)
   ifappend(z0, z1, nil) -> z1
   ifappend(z0, z1, cons(z2, z3)) -> cons(z2, append(z3, z1))
Tuples:
   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, z0))
   IFAPPEND(z0, z1, nil) -> c5
   IFAPPEND(z0, z1, cons(z2, z3)) -> c6(APPEND(z3, z1))
S tuples:
   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, z0))
   IFAPPEND(z0, z1, nil) -> c5
   IFAPPEND(z0, z1, cons(z2, z3)) -> c6(APPEND(z3, z1))
K tuples:none
Defined Rule Symbols:   is_empty_1, hd_1, tl_1, append_2, ifappend_3

Defined Pair Symbols:   IS_EMPTY_1, HD_1, TL_1, APPEND_2, IFAPPEND_3

Compound Symbols:   c, c1, c2, c3, c4_1, c5, c6_1


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

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 5 trailing nodes:
   IS_EMPTY(nil) -> c
   IS_EMPTY(cons(z0, z1)) -> c1
   TL(cons(z0, z1)) -> c3
   HD(cons(z0, z1)) -> c2
   IFAPPEND(z0, z1, nil) -> c5

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

(4)
Obligation:
Complexity Dependency Tuples Problem

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, z0)
   ifappend(z0, z1, nil) -> z1
   ifappend(z0, z1, cons(z2, z3)) -> cons(z2, append(z3, z1))
Tuples:
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, z0))
   IFAPPEND(z0, z1, cons(z2, z3)) -> c6(APPEND(z3, z1))
S tuples:
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, z0))
   IFAPPEND(z0, z1, cons(z2, z3)) -> c6(APPEND(z3, z1))
K tuples:none
Defined Rule Symbols:   is_empty_1, hd_1, tl_1, append_2, ifappend_3

Defined Pair Symbols:   APPEND_2, IFAPPEND_3

Compound Symbols:   c4_1, c6_1


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

(5) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   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, z0)
   ifappend(z0, z1, nil) -> z1
   ifappend(z0, z1, cons(z2, z3)) -> cons(z2, append(z3, z1))

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, z0))
   IFAPPEND(z0, z1, cons(z2, z3)) -> c6(APPEND(z3, z1))
S tuples:
   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, z0))
   IFAPPEND(z0, z1, cons(z2, z3)) -> c6(APPEND(z3, z1))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:   APPEND_2, IFAPPEND_3

Compound Symbols:   c4_1, c6_1


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

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

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


The TRS R consists of the following rules:

   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, z0))
   IFAPPEND(z0, z1, cons(z2, z3)) -> c6(APPEND(z3, z1))

S is empty.
Rewrite Strategy: INNERMOST
----------------------------------------

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

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

   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, z0)) [1]
   IFAPPEND(z0, z1, cons(z2, z3)) -> c6(APPEND(z3, z1)) [1]

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

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

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

   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, z0)) [1]
   IFAPPEND(z0, z1, cons(z2, z3)) -> c6(APPEND(z3, z1)) [1]

The TRS has the following type information:
APPEND :: cons -> a -> c4
c4 :: c6 -> c4
IFAPPEND :: cons -> a -> cons -> c6
cons :: b -> cons -> cons
c6 :: c4 -> c6

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

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

   IFAPPEND(v0, v1, v2) -> null_IFAPPEND [0]

And the following fresh constants:    null_IFAPPEND, const, const1, const2, const3

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

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

   APPEND(z0, z1) -> c4(IFAPPEND(z0, z1, z0)) [1]
   IFAPPEND(z0, z1, cons(z2, z3)) -> c6(APPEND(z3, z1)) [1]
   IFAPPEND(v0, v1, v2) -> null_IFAPPEND [0]

The TRS has the following type information:
APPEND :: cons -> a -> c4
c4 :: c6:null_IFAPPEND -> c4
IFAPPEND :: cons -> a -> cons -> c6:null_IFAPPEND
cons :: b -> cons -> cons
c6 :: c4 -> c6:null_IFAPPEND
null_IFAPPEND :: c6:null_IFAPPEND
const :: c4
const1 :: cons
const2 :: a
const3 :: b

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

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

   null_IFAPPEND => 0
   const => 0
   const1 => 0
   const2 => 0
   const3 => 0

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

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

   APPEND(z, z') -{ 1 }-> 1 + IFAPPEND(z0, z1, z0) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   IFAPPEND(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   IFAPPEND(z, z', z'') -{ 1 }-> 1 + APPEND(z3, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0, z'' = 1 + z2 + z3, z2 >= 0, z3 >= 0

Only complete derivations are relevant for the runtime complexity.

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

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

eq(start(V1, V, V4),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V4),0,[fun1(V1, V, V4, Out)],[V1 >= 0,V >= 0,V4 >= 0]).
eq(fun(V1, V, Out),1,[fun1(V3, V2, V3, Ret1)],[Out = 1 + Ret1,V1 = V3,V2 >= 0,V = V2,V3 >= 0]).
eq(fun1(V1, V, V4, Out),1,[fun(V7, V5, Ret11)],[Out = 1 + Ret11,V1 = V6,V5 >= 0,V = V5,V6 >= 0,V4 = 1 + V7 + V8,V8 >= 0,V7 >= 0]).
eq(fun1(V1, V, V4, Out),0,[],[Out = 0,V10 >= 0,V4 = V11,V9 >= 0,V1 = V10,V = V9,V11 >= 0]).
input_output_vars(fun(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun1(V1,V,V4,Out),[V1,V,V4],[Out]).


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

#### Computed strongly connected components 
0. recursive  : [fun/3,fun1/4]
1. non_recursive  : [start/3]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into fun/3
1. SCC is partially evaluated into start/3

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

### Specialization of cost equations fun/3 
* CE 5 is refined into CE [6] 
* CE 4 is refined into CE [7] 


### Cost equations --> "Loop" of fun/3 
* CEs [7] --> Loop 4 
* CEs [6] --> Loop 5 

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

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


### Specialization of cost equations start/3 
* CE 1 is refined into CE [8] 
* CE 2 is refined into CE [9,10] 
* CE 3 is refined into CE [11,12] 


### Cost equations --> "Loop" of start/3 
* CEs [8,9,10,11,12] --> Loop 6 

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

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


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

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

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

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


#### Cost of chains of start(V1,V,V4):
* Chain [6]: 2*s(1)+2*s(2)+2
  Such that:s(2) =< V1
s(1) =< V4

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


Closed-form bounds of start(V1,V,V4): 
-------------------------------------
* Chain [6] with precondition: [V1>=0,V>=0] 
    - Upper bound: 2*V1+2+nat(V4)*2 
    - Complexity: n 

### Maximum cost of start(V1,V,V4): 2*V1+2+nat(V4)*2 
Asymptotic class: n 
* Total analysis performed in 51 ms.


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

(18)
BOUNDS(1, n^1)

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

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

(20)
Obligation:
Complexity Dependency Tuples Problem

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, z0)
   ifappend(z0, z1, nil) -> z1
   ifappend(z0, z1, cons(z2, z3)) -> cons(z2, append(z3, z1))
Tuples:
   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, z0))
   IFAPPEND(z0, z1, nil) -> c5
   IFAPPEND(z0, z1, cons(z2, z3)) -> c6(APPEND(z3, z1))
S tuples:
   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, z0))
   IFAPPEND(z0, z1, nil) -> c5
   IFAPPEND(z0, z1, cons(z2, z3)) -> c6(APPEND(z3, z1))
K tuples:none
Defined Rule Symbols:   is_empty_1, hd_1, tl_1, append_2, ifappend_3

Defined Pair Symbols:   IS_EMPTY_1, HD_1, TL_1, APPEND_2, IFAPPEND_3

Compound Symbols:   c, c1, c2, c3, c4_1, c5, c6_1


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

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

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


The TRS R consists of the following rules:

   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, z0))
   IFAPPEND(z0, z1, nil) -> c5
   IFAPPEND(z0, z1, cons(z2, z3)) -> c6(APPEND(z3, z1))

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, z0)
   ifappend(z0, z1, nil) -> z1
   ifappend(z0, z1, cons(z2, z3)) -> cons(z2, append(z3, z1))

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

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

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


The TRS R consists of the following rules:

   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, z0))
   IFAPPEND(z0, z1, nil) -> c5
   IFAPPEND(z0, z1, cons(z2, z3)) -> c6(APPEND(z3, z1))

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, z0)
   ifappend(z0, z1, nil) -> z1
   ifappend(z0, z1, cons(z2, z3)) -> cons(z2, append(z3, z1))

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

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

(26)
Obligation:
Innermost TRS:
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, z0))
IFAPPEND(z0, z1, nil) -> c5
IFAPPEND(z0, z1, cons(z2, z3)) -> c6(APPEND(z3, z1))
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, z0)
ifappend(z0, z1, nil) -> z1
ifappend(z0, z1, cons(z2, z3)) -> cons(z2, append(z3, z1))

Types:
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 -> c4
IFAPPEND :: nil:cons -> a -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c4 -> c5:c6
is_empty :: nil:cons -> true:false
true :: true:false
false :: true:false
hd :: nil:cons -> hd
tl :: nil:cons -> nil:cons
append :: nil:cons -> nil:cons -> nil:cons
ifappend :: nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_7 :: c:c1
hole_nil:cons2_7 :: nil:cons
hole_hd3_7 :: hd
hole_c24_7 :: c2
hole_c35_7 :: c3
hole_c46_7 :: c4
hole_a7_7 :: a
hole_c5:c68_7 :: c5:c6
hole_true:false9_7 :: true:false
gen_nil:cons10_7 :: Nat -> nil:cons

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

(27) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
APPEND, append
----------------------------------------

(28)
Obligation:
Innermost TRS:
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, z0))
IFAPPEND(z0, z1, nil) -> c5
IFAPPEND(z0, z1, cons(z2, z3)) -> c6(APPEND(z3, z1))
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, z0)
ifappend(z0, z1, nil) -> z1
ifappend(z0, z1, cons(z2, z3)) -> cons(z2, append(z3, z1))

Types:
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 -> c4
IFAPPEND :: nil:cons -> a -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c4 -> c5:c6
is_empty :: nil:cons -> true:false
true :: true:false
false :: true:false
hd :: nil:cons -> hd
tl :: nil:cons -> nil:cons
append :: nil:cons -> nil:cons -> nil:cons
ifappend :: nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_7 :: c:c1
hole_nil:cons2_7 :: nil:cons
hole_hd3_7 :: hd
hole_c24_7 :: c2
hole_c35_7 :: c3
hole_c46_7 :: c4
hole_a7_7 :: a
hole_c5:c68_7 :: c5:c6
hole_true:false9_7 :: true:false
gen_nil:cons10_7 :: Nat -> nil:cons


Generator Equations:
gen_nil:cons10_7(0) <=> nil
gen_nil:cons10_7(+(x, 1)) <=> cons(hole_hd3_7, gen_nil:cons10_7(x))


The following defined symbols remain to be analysed:
APPEND, append
----------------------------------------

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APPEND(gen_nil:cons10_7(n12_7), hole_a7_7) -> *11_7, rt in Omega(n12_7)

Induction Base:
APPEND(gen_nil:cons10_7(0), hole_a7_7)

Induction Step:
APPEND(gen_nil:cons10_7(+(n12_7, 1)), hole_a7_7) ->_R^Omega(1)
c4(IFAPPEND(gen_nil:cons10_7(+(n12_7, 1)), hole_a7_7, gen_nil:cons10_7(+(n12_7, 1)))) ->_R^Omega(1)
c4(c6(APPEND(gen_nil:cons10_7(n12_7), hole_a7_7))) ->_IH
c4(c6(*11_7))

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

(30)
Complex Obligation (BEST)

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

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

Innermost TRS:
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, z0))
IFAPPEND(z0, z1, nil) -> c5
IFAPPEND(z0, z1, cons(z2, z3)) -> c6(APPEND(z3, z1))
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, z0)
ifappend(z0, z1, nil) -> z1
ifappend(z0, z1, cons(z2, z3)) -> cons(z2, append(z3, z1))

Types:
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 -> c4
IFAPPEND :: nil:cons -> a -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c4 -> c5:c6
is_empty :: nil:cons -> true:false
true :: true:false
false :: true:false
hd :: nil:cons -> hd
tl :: nil:cons -> nil:cons
append :: nil:cons -> nil:cons -> nil:cons
ifappend :: nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_7 :: c:c1
hole_nil:cons2_7 :: nil:cons
hole_hd3_7 :: hd
hole_c24_7 :: c2
hole_c35_7 :: c3
hole_c46_7 :: c4
hole_a7_7 :: a
hole_c5:c68_7 :: c5:c6
hole_true:false9_7 :: true:false
gen_nil:cons10_7 :: Nat -> nil:cons


Generator Equations:
gen_nil:cons10_7(0) <=> nil
gen_nil:cons10_7(+(x, 1)) <=> cons(hole_hd3_7, gen_nil:cons10_7(x))


The following defined symbols remain to be analysed:
APPEND, append
----------------------------------------

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

(33)
BOUNDS(n^1, INF)

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

(34)
Obligation:
Innermost TRS:
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, z0))
IFAPPEND(z0, z1, nil) -> c5
IFAPPEND(z0, z1, cons(z2, z3)) -> c6(APPEND(z3, z1))
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, z0)
ifappend(z0, z1, nil) -> z1
ifappend(z0, z1, cons(z2, z3)) -> cons(z2, append(z3, z1))

Types:
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 -> c4
IFAPPEND :: nil:cons -> a -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c4 -> c5:c6
is_empty :: nil:cons -> true:false
true :: true:false
false :: true:false
hd :: nil:cons -> hd
tl :: nil:cons -> nil:cons
append :: nil:cons -> nil:cons -> nil:cons
ifappend :: nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_7 :: c:c1
hole_nil:cons2_7 :: nil:cons
hole_hd3_7 :: hd
hole_c24_7 :: c2
hole_c35_7 :: c3
hole_c46_7 :: c4
hole_a7_7 :: a
hole_c5:c68_7 :: c5:c6
hole_true:false9_7 :: true:false
gen_nil:cons10_7 :: Nat -> nil:cons


Lemmas:
APPEND(gen_nil:cons10_7(n12_7), hole_a7_7) -> *11_7, rt in Omega(n12_7)


Generator Equations:
gen_nil:cons10_7(0) <=> nil
gen_nil:cons10_7(+(x, 1)) <=> cons(hole_hd3_7, gen_nil:cons10_7(x))


The following defined symbols remain to be analysed:
append
----------------------------------------

(35) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
append(gen_nil:cons10_7(n508_7), gen_nil:cons10_7(b)) -> gen_nil:cons10_7(+(n508_7, b)), rt in Omega(0)

Induction Base:
append(gen_nil:cons10_7(0), gen_nil:cons10_7(b)) ->_R^Omega(0)
ifappend(gen_nil:cons10_7(0), gen_nil:cons10_7(b), gen_nil:cons10_7(0)) ->_R^Omega(0)
gen_nil:cons10_7(b)

Induction Step:
append(gen_nil:cons10_7(+(n508_7, 1)), gen_nil:cons10_7(b)) ->_R^Omega(0)
ifappend(gen_nil:cons10_7(+(n508_7, 1)), gen_nil:cons10_7(b), gen_nil:cons10_7(+(n508_7, 1))) ->_R^Omega(0)
cons(hole_hd3_7, append(gen_nil:cons10_7(n508_7), gen_nil:cons10_7(b))) ->_IH
cons(hole_hd3_7, gen_nil:cons10_7(+(b, c509_7)))

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

(36)
BOUNDS(1, INF)