WORST_CASE(Omega(n^1),O(n^1))
proof of input_UYre3CNRdC.trs
# AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 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) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CpxTRS
    (11) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
    (12) CpxTRS
    (13) CpxTrsMatchBoundsTAProof [FINISHED, 30 ms]
    (14) BOUNDS(1, n^1)
(15) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(16) CdtProblem
    (17) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (18) CpxRelTRS
    (19) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (20) CpxRelTRS
    (21) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (22) typed CpxTrs
    (23) OrderProof [LOWER BOUND(ID), 9 ms]
    (24) typed CpxTrs
    (25) RewriteLemmaProof [LOWER BOUND(ID), 5551 ms]
    (26) typed CpxTrs
    (27) RewriteLemmaProof [LOWER BOUND(ID), 6091 ms]
    (28) BEST
        (29) proven lower bound
            (30) LowerBoundPropagationProof [FINISHED, 0 ms]
            (31) BOUNDS(n^1, INF)
        (32) typed CpxTrs
            (33) RewriteLemmaProof [LOWER BOUND(ID), 23 ms]
            (34) 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:

   merge(nil, y) -> y
   merge(x, nil) -> x
   merge(.(x, y), .(u, v)) -> if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
   ++(nil, y) -> y
   ++(.(x, y), z) -> .(x, ++(y, z))
   if(true, x, y) -> x
   if(false, x, y) -> x

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:
   merge(nil, z0) -> z0
   merge(z0, nil) -> z0
   merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3)))
   ++(nil, z0) -> z0
   ++(.(z0, z1), z2) -> .(z0, ++(z1, z2))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z0
Tuples:
   MERGE(nil, z0) -> c
   MERGE(z0, nil) -> c1
   MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3)))
   MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3))
   ++'(nil, z0) -> c4
   ++'(.(z0, z1), z2) -> c5(++'(z1, z2))
   IF(true, z0, z1) -> c6
   IF(false, z0, z1) -> c7
S tuples:
   MERGE(nil, z0) -> c
   MERGE(z0, nil) -> c1
   MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3)))
   MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3))
   ++'(nil, z0) -> c4
   ++'(.(z0, z1), z2) -> c5(++'(z1, z2))
   IF(true, z0, z1) -> c6
   IF(false, z0, z1) -> c7
K tuples:none
Defined Rule Symbols:   merge_2, ++_2, if_3

Defined Pair Symbols:   MERGE_2, ++'_2, IF_3

Compound Symbols:   c, c1, c2_2, c3_2, c4, c5_1, c6, c7


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

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 5 trailing nodes:
   IF(false, z0, z1) -> c7
   IF(true, z0, z1) -> c6
   MERGE(z0, nil) -> c1
   MERGE(nil, z0) -> c
   ++'(nil, z0) -> c4

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   merge(nil, z0) -> z0
   merge(z0, nil) -> z0
   merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3)))
   ++(nil, z0) -> z0
   ++(.(z0, z1), z2) -> .(z0, ++(z1, z2))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z0
Tuples:
   MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3)))
   MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3))
   ++'(.(z0, z1), z2) -> c5(++'(z1, z2))
S tuples:
   MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3)))
   MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3))
   ++'(.(z0, z1), z2) -> c5(++'(z1, z2))
K tuples:none
Defined Rule Symbols:   merge_2, ++_2, if_3

Defined Pair Symbols:   MERGE_2, ++'_2

Compound Symbols:   c2_2, c3_2, c5_1


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

(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 2 trailing tuple parts
----------------------------------------

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   merge(nil, z0) -> z0
   merge(z0, nil) -> z0
   merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3)))
   ++(nil, z0) -> z0
   ++(.(z0, z1), z2) -> .(z0, ++(z1, z2))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z0
Tuples:
   ++'(.(z0, z1), z2) -> c5(++'(z1, z2))
   MERGE(.(z0, z1), .(z2, z3)) -> c2(MERGE(z1, .(z2, z3)))
   MERGE(.(z0, z1), .(z2, z3)) -> c3(MERGE(.(z0, z1), z3))
S tuples:
   ++'(.(z0, z1), z2) -> c5(++'(z1, z2))
   MERGE(.(z0, z1), .(z2, z3)) -> c2(MERGE(z1, .(z2, z3)))
   MERGE(.(z0, z1), .(z2, z3)) -> c3(MERGE(.(z0, z1), z3))
K tuples:none
Defined Rule Symbols:   merge_2, ++_2, if_3

Defined Pair Symbols:   ++'_2, MERGE_2

Compound Symbols:   c5_1, c2_1, c3_1


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

(7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   merge(nil, z0) -> z0
   merge(z0, nil) -> z0
   merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3)))
   ++(nil, z0) -> z0
   ++(.(z0, z1), z2) -> .(z0, ++(z1, z2))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z0

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:none
Tuples:
   ++'(.(z0, z1), z2) -> c5(++'(z1, z2))
   MERGE(.(z0, z1), .(z2, z3)) -> c2(MERGE(z1, .(z2, z3)))
   MERGE(.(z0, z1), .(z2, z3)) -> c3(MERGE(.(z0, z1), z3))
S tuples:
   ++'(.(z0, z1), z2) -> c5(++'(z1, z2))
   MERGE(.(z0, z1), .(z2, z3)) -> c2(MERGE(z1, .(z2, z3)))
   MERGE(.(z0, z1), .(z2, z3)) -> c3(MERGE(.(z0, z1), z3))
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:   ++'_2, MERGE_2

Compound Symbols:   c5_1, c2_1, c3_1


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

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

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

   ++'(.(z0, z1), z2) -> c5(++'(z1, z2))
   MERGE(.(z0, z1), .(z2, z3)) -> c2(MERGE(z1, .(z2, z3)))
   MERGE(.(z0, z1), .(z2, z3)) -> c3(MERGE(.(z0, z1), z3))

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

(11) RelTrsToTrsProof (UPPER BOUND(ID))
transformed relative TRS to TRS
----------------------------------------

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

   ++'(.(z0, z1), z2) -> c5(++'(z1, z2))
   MERGE(.(z0, z1), .(z2, z3)) -> c2(MERGE(z1, .(z2, z3)))
   MERGE(.(z0, z1), .(z2, z3)) -> c3(MERGE(.(z0, z1), z3))

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

(13) CpxTrsMatchBoundsTAProof (FINISHED)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1. 

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by: 
final states : [1, 2]
transitions: 
.0(0, 0) -> 0
c50(0) -> 0
c20(0) -> 0
c30(0) -> 0
++'0(0, 0) -> 1
MERGE0(0, 0) -> 2
++'1(0, 0) -> 3
c51(3) -> 1
.1(0, 0) -> 5
MERGE1(0, 5) -> 4
c21(4) -> 2
.1(0, 0) -> 7
MERGE1(7, 0) -> 6
c31(6) -> 2
c51(3) -> 3
c21(4) -> 4
c21(4) -> 6
c31(6) -> 4
c31(6) -> 6

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

(14)
BOUNDS(1, n^1)

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

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

(16)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   merge(nil, z0) -> z0
   merge(z0, nil) -> z0
   merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3)))
   ++(nil, z0) -> z0
   ++(.(z0, z1), z2) -> .(z0, ++(z1, z2))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z0
Tuples:
   MERGE(nil, z0) -> c
   MERGE(z0, nil) -> c1
   MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3)))
   MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3))
   ++'(nil, z0) -> c4
   ++'(.(z0, z1), z2) -> c5(++'(z1, z2))
   IF(true, z0, z1) -> c6
   IF(false, z0, z1) -> c7
S tuples:
   MERGE(nil, z0) -> c
   MERGE(z0, nil) -> c1
   MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3)))
   MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3))
   ++'(nil, z0) -> c4
   ++'(.(z0, z1), z2) -> c5(++'(z1, z2))
   IF(true, z0, z1) -> c6
   IF(false, z0, z1) -> c7
K tuples:none
Defined Rule Symbols:   merge_2, ++_2, if_3

Defined Pair Symbols:   MERGE_2, ++'_2, IF_3

Compound Symbols:   c, c1, c2_2, c3_2, c4, c5_1, c6, c7


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

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

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

   MERGE(nil, z0) -> c
   MERGE(z0, nil) -> c1
   MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3)))
   MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3))
   ++'(nil, z0) -> c4
   ++'(.(z0, z1), z2) -> c5(++'(z1, z2))
   IF(true, z0, z1) -> c6
   IF(false, z0, z1) -> c7

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

   merge(nil, z0) -> z0
   merge(z0, nil) -> z0
   merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3)))
   ++(nil, z0) -> z0
   ++(.(z0, z1), z2) -> .(z0, ++(z1, z2))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z0

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

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

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

   MERGE(nil, z0) -> c
   MERGE(z0, nil) -> c1
   MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3)))
   MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3))
   ++'(nil, z0) -> c4
   ++'(.(z0, z1), z2) -> c5(++'(z1, z2))
   IF(true, z0, z1) -> c6
   IF(false, z0, z1) -> c7

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

   merge(nil, z0) -> z0
   merge(z0, nil) -> z0
   merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3)))
   ++(nil, z0) -> z0
   ++(.(z0, z1), z2) -> .(z0, ++(z1, z2))
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z0

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

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

(22)
Obligation:
Innermost TRS:
Rules:
MERGE(nil, z0) -> c
MERGE(z0, nil) -> c1
MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3)))
MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3))
++'(nil, z0) -> c4
++'(.(z0, z1), z2) -> c5(++'(z1, z2))
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
merge(nil, z0) -> z0
merge(z0, nil) -> z0
merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3)))
++(nil, z0) -> z0
++(.(z0, z1), z2) -> .(z0, ++(z1, z2))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z0

Types:
MERGE :: nil:. -> nil:. -> c:c1:c2:c3
nil :: nil:.
c :: c:c1:c2:c3
c1 :: c:c1:c2:c3
. :: a -> nil:. -> nil:.
c2 :: c6:c7 -> c:c1:c2:c3 -> c:c1:c2:c3
IF :: <:true:false -> nil:. -> nil:. -> c6:c7
< :: a -> a -> <:true:false
merge :: nil:. -> nil:. -> nil:.
c3 :: c6:c7 -> c:c1:c2:c3 -> c:c1:c2:c3
++' :: nil:. -> b -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
true :: <:true:false
c6 :: c6:c7
false :: <:true:false
c7 :: c6:c7
if :: <:true:false -> nil:. -> nil:. -> nil:.
++ :: nil:. -> nil:. -> nil:.
hole_c:c1:c2:c31_8 :: c:c1:c2:c3
hole_nil:.2_8 :: nil:.
hole_a3_8 :: a
hole_c6:c74_8 :: c6:c7
hole_<:true:false5_8 :: <:true:false
hole_c4:c56_8 :: c4:c5
hole_b7_8 :: b
gen_c:c1:c2:c38_8 :: Nat -> c:c1:c2:c3
gen_nil:.9_8 :: Nat -> nil:.
gen_c4:c510_8 :: Nat -> c4:c5

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

(23) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
MERGE, merge, ++', ++

They will be analysed ascendingly in the following order:
merge < MERGE

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

(24)
Obligation:
Innermost TRS:
Rules:
MERGE(nil, z0) -> c
MERGE(z0, nil) -> c1
MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3)))
MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3))
++'(nil, z0) -> c4
++'(.(z0, z1), z2) -> c5(++'(z1, z2))
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
merge(nil, z0) -> z0
merge(z0, nil) -> z0
merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3)))
++(nil, z0) -> z0
++(.(z0, z1), z2) -> .(z0, ++(z1, z2))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z0

Types:
MERGE :: nil:. -> nil:. -> c:c1:c2:c3
nil :: nil:.
c :: c:c1:c2:c3
c1 :: c:c1:c2:c3
. :: a -> nil:. -> nil:.
c2 :: c6:c7 -> c:c1:c2:c3 -> c:c1:c2:c3
IF :: <:true:false -> nil:. -> nil:. -> c6:c7
< :: a -> a -> <:true:false
merge :: nil:. -> nil:. -> nil:.
c3 :: c6:c7 -> c:c1:c2:c3 -> c:c1:c2:c3
++' :: nil:. -> b -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
true :: <:true:false
c6 :: c6:c7
false :: <:true:false
c7 :: c6:c7
if :: <:true:false -> nil:. -> nil:. -> nil:.
++ :: nil:. -> nil:. -> nil:.
hole_c:c1:c2:c31_8 :: c:c1:c2:c3
hole_nil:.2_8 :: nil:.
hole_a3_8 :: a
hole_c6:c74_8 :: c6:c7
hole_<:true:false5_8 :: <:true:false
hole_c4:c56_8 :: c4:c5
hole_b7_8 :: b
gen_c:c1:c2:c38_8 :: Nat -> c:c1:c2:c3
gen_nil:.9_8 :: Nat -> nil:.
gen_c4:c510_8 :: Nat -> c4:c5


Generator Equations:
gen_c:c1:c2:c38_8(0) <=> c
gen_c:c1:c2:c38_8(+(x, 1)) <=> c2(c6, gen_c:c1:c2:c38_8(x))
gen_nil:.9_8(0) <=> nil
gen_nil:.9_8(+(x, 1)) <=> .(hole_a3_8, gen_nil:.9_8(x))
gen_c4:c510_8(0) <=> c4
gen_c4:c510_8(+(x, 1)) <=> c5(gen_c4:c510_8(x))


The following defined symbols remain to be analysed:
merge, MERGE, ++', ++

They will be analysed ascendingly in the following order:
merge < MERGE

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
merge(gen_nil:.9_8(+(1, n12_8)), gen_nil:.9_8(1)) -> *11_8, rt in Omega(0)

Induction Base:
merge(gen_nil:.9_8(+(1, 0)), gen_nil:.9_8(1))

Induction Step:
merge(gen_nil:.9_8(+(1, +(n12_8, 1))), gen_nil:.9_8(1)) ->_R^Omega(0)
if(<(hole_a3_8, hole_a3_8), .(hole_a3_8, merge(gen_nil:.9_8(+(1, n12_8)), .(hole_a3_8, gen_nil:.9_8(0)))), .(hole_a3_8, merge(.(hole_a3_8, gen_nil:.9_8(+(1, n12_8))), gen_nil:.9_8(0)))) ->_IH
if(<(hole_a3_8, hole_a3_8), .(hole_a3_8, *11_8), .(hole_a3_8, merge(.(hole_a3_8, gen_nil:.9_8(+(1, n12_8))), gen_nil:.9_8(0)))) ->_R^Omega(0)
if(<(hole_a3_8, hole_a3_8), .(hole_a3_8, *11_8), .(hole_a3_8, .(hole_a3_8, gen_nil:.9_8(+(1, n12_8)))))

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

(26)
Obligation:
Innermost TRS:
Rules:
MERGE(nil, z0) -> c
MERGE(z0, nil) -> c1
MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3)))
MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3))
++'(nil, z0) -> c4
++'(.(z0, z1), z2) -> c5(++'(z1, z2))
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
merge(nil, z0) -> z0
merge(z0, nil) -> z0
merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3)))
++(nil, z0) -> z0
++(.(z0, z1), z2) -> .(z0, ++(z1, z2))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z0

Types:
MERGE :: nil:. -> nil:. -> c:c1:c2:c3
nil :: nil:.
c :: c:c1:c2:c3
c1 :: c:c1:c2:c3
. :: a -> nil:. -> nil:.
c2 :: c6:c7 -> c:c1:c2:c3 -> c:c1:c2:c3
IF :: <:true:false -> nil:. -> nil:. -> c6:c7
< :: a -> a -> <:true:false
merge :: nil:. -> nil:. -> nil:.
c3 :: c6:c7 -> c:c1:c2:c3 -> c:c1:c2:c3
++' :: nil:. -> b -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
true :: <:true:false
c6 :: c6:c7
false :: <:true:false
c7 :: c6:c7
if :: <:true:false -> nil:. -> nil:. -> nil:.
++ :: nil:. -> nil:. -> nil:.
hole_c:c1:c2:c31_8 :: c:c1:c2:c3
hole_nil:.2_8 :: nil:.
hole_a3_8 :: a
hole_c6:c74_8 :: c6:c7
hole_<:true:false5_8 :: <:true:false
hole_c4:c56_8 :: c4:c5
hole_b7_8 :: b
gen_c:c1:c2:c38_8 :: Nat -> c:c1:c2:c3
gen_nil:.9_8 :: Nat -> nil:.
gen_c4:c510_8 :: Nat -> c4:c5


Lemmas:
merge(gen_nil:.9_8(+(1, n12_8)), gen_nil:.9_8(1)) -> *11_8, rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c38_8(0) <=> c
gen_c:c1:c2:c38_8(+(x, 1)) <=> c2(c6, gen_c:c1:c2:c38_8(x))
gen_nil:.9_8(0) <=> nil
gen_nil:.9_8(+(x, 1)) <=> .(hole_a3_8, gen_nil:.9_8(x))
gen_c4:c510_8(0) <=> c4
gen_c4:c510_8(+(x, 1)) <=> c5(gen_c4:c510_8(x))


The following defined symbols remain to be analysed:
MERGE, ++', ++
----------------------------------------

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
++'(gen_nil:.9_8(n133072_8), hole_b7_8) -> gen_c4:c510_8(n133072_8), rt in Omega(1 + n133072_8)

Induction Base:
++'(gen_nil:.9_8(0), hole_b7_8) ->_R^Omega(1)
c4

Induction Step:
++'(gen_nil:.9_8(+(n133072_8, 1)), hole_b7_8) ->_R^Omega(1)
c5(++'(gen_nil:.9_8(n133072_8), hole_b7_8)) ->_IH
c5(gen_c4:c510_8(c133073_8))

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

(28)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
MERGE(nil, z0) -> c
MERGE(z0, nil) -> c1
MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3)))
MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3))
++'(nil, z0) -> c4
++'(.(z0, z1), z2) -> c5(++'(z1, z2))
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
merge(nil, z0) -> z0
merge(z0, nil) -> z0
merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3)))
++(nil, z0) -> z0
++(.(z0, z1), z2) -> .(z0, ++(z1, z2))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z0

Types:
MERGE :: nil:. -> nil:. -> c:c1:c2:c3
nil :: nil:.
c :: c:c1:c2:c3
c1 :: c:c1:c2:c3
. :: a -> nil:. -> nil:.
c2 :: c6:c7 -> c:c1:c2:c3 -> c:c1:c2:c3
IF :: <:true:false -> nil:. -> nil:. -> c6:c7
< :: a -> a -> <:true:false
merge :: nil:. -> nil:. -> nil:.
c3 :: c6:c7 -> c:c1:c2:c3 -> c:c1:c2:c3
++' :: nil:. -> b -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
true :: <:true:false
c6 :: c6:c7
false :: <:true:false
c7 :: c6:c7
if :: <:true:false -> nil:. -> nil:. -> nil:.
++ :: nil:. -> nil:. -> nil:.
hole_c:c1:c2:c31_8 :: c:c1:c2:c3
hole_nil:.2_8 :: nil:.
hole_a3_8 :: a
hole_c6:c74_8 :: c6:c7
hole_<:true:false5_8 :: <:true:false
hole_c4:c56_8 :: c4:c5
hole_b7_8 :: b
gen_c:c1:c2:c38_8 :: Nat -> c:c1:c2:c3
gen_nil:.9_8 :: Nat -> nil:.
gen_c4:c510_8 :: Nat -> c4:c5


Lemmas:
merge(gen_nil:.9_8(+(1, n12_8)), gen_nil:.9_8(1)) -> *11_8, rt in Omega(0)


Generator Equations:
gen_c:c1:c2:c38_8(0) <=> c
gen_c:c1:c2:c38_8(+(x, 1)) <=> c2(c6, gen_c:c1:c2:c38_8(x))
gen_nil:.9_8(0) <=> nil
gen_nil:.9_8(+(x, 1)) <=> .(hole_a3_8, gen_nil:.9_8(x))
gen_c4:c510_8(0) <=> c4
gen_c4:c510_8(+(x, 1)) <=> c5(gen_c4:c510_8(x))


The following defined symbols remain to be analysed:
++', ++
----------------------------------------

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

(31)
BOUNDS(n^1, INF)

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

(32)
Obligation:
Innermost TRS:
Rules:
MERGE(nil, z0) -> c
MERGE(z0, nil) -> c1
MERGE(.(z0, z1), .(z2, z3)) -> c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3)))
MERGE(.(z0, z1), .(z2, z3)) -> c3(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(.(z0, z1), z3))
++'(nil, z0) -> c4
++'(.(z0, z1), z2) -> c5(++'(z1, z2))
IF(true, z0, z1) -> c6
IF(false, z0, z1) -> c7
merge(nil, z0) -> z0
merge(z0, nil) -> z0
merge(.(z0, z1), .(z2, z3)) -> if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3)))
++(nil, z0) -> z0
++(.(z0, z1), z2) -> .(z0, ++(z1, z2))
if(true, z0, z1) -> z0
if(false, z0, z1) -> z0

Types:
MERGE :: nil:. -> nil:. -> c:c1:c2:c3
nil :: nil:.
c :: c:c1:c2:c3
c1 :: c:c1:c2:c3
. :: a -> nil:. -> nil:.
c2 :: c6:c7 -> c:c1:c2:c3 -> c:c1:c2:c3
IF :: <:true:false -> nil:. -> nil:. -> c6:c7
< :: a -> a -> <:true:false
merge :: nil:. -> nil:. -> nil:.
c3 :: c6:c7 -> c:c1:c2:c3 -> c:c1:c2:c3
++' :: nil:. -> b -> c4:c5
c4 :: c4:c5
c5 :: c4:c5 -> c4:c5
true :: <:true:false
c6 :: c6:c7
false :: <:true:false
c7 :: c6:c7
if :: <:true:false -> nil:. -> nil:. -> nil:.
++ :: nil:. -> nil:. -> nil:.
hole_c:c1:c2:c31_8 :: c:c1:c2:c3
hole_nil:.2_8 :: nil:.
hole_a3_8 :: a
hole_c6:c74_8 :: c6:c7
hole_<:true:false5_8 :: <:true:false
hole_c4:c56_8 :: c4:c5
hole_b7_8 :: b
gen_c:c1:c2:c38_8 :: Nat -> c:c1:c2:c3
gen_nil:.9_8 :: Nat -> nil:.
gen_c4:c510_8 :: Nat -> c4:c5


Lemmas:
merge(gen_nil:.9_8(+(1, n12_8)), gen_nil:.9_8(1)) -> *11_8, rt in Omega(0)
++'(gen_nil:.9_8(n133072_8), hole_b7_8) -> gen_c4:c510_8(n133072_8), rt in Omega(1 + n133072_8)


Generator Equations:
gen_c:c1:c2:c38_8(0) <=> c
gen_c:c1:c2:c38_8(+(x, 1)) <=> c2(c6, gen_c:c1:c2:c38_8(x))
gen_nil:.9_8(0) <=> nil
gen_nil:.9_8(+(x, 1)) <=> .(hole_a3_8, gen_nil:.9_8(x))
gen_c4:c510_8(0) <=> c4
gen_c4:c510_8(+(x, 1)) <=> c5(gen_c4:c510_8(x))


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

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
++(gen_nil:.9_8(n133497_8), gen_nil:.9_8(b)) -> gen_nil:.9_8(+(n133497_8, b)), rt in Omega(0)

Induction Base:
++(gen_nil:.9_8(0), gen_nil:.9_8(b)) ->_R^Omega(0)
gen_nil:.9_8(b)

Induction Step:
++(gen_nil:.9_8(+(n133497_8, 1)), gen_nil:.9_8(b)) ->_R^Omega(0)
.(hole_a3_8, ++(gen_nil:.9_8(n133497_8), gen_nil:.9_8(b))) ->_IH
.(hole_a3_8, gen_nil:.9_8(+(b, c133498_8)))

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

(34)
BOUNDS(1, INF)