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


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 193 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(4) CdtProblem
    (5) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
    (6) CdtProblem
    (7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CpxRelTRS
    (11) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) CpxWeightedTrs
    (13) CpxWeightedTrsRenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (14) CpxWeightedTrs
    (15) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (16) CpxTypedWeightedTrs
    (17) CompletionProof [UPPER BOUND(ID), 0 ms]
    (18) CpxTypedWeightedCompleteTrs
    (19) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
    (20) CpxRNTS
    (21) CompleteCoflocoProof [FINISHED, 507 ms]
    (22) BOUNDS(1, n^1)
(23) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(24) CdtProblem
    (25) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (26) CpxRelTRS
    (27) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (28) CpxRelTRS
    (29) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (30) typed CpxTrs
    (31) OrderProof [LOWER BOUND(ID), 0 ms]
    (32) typed CpxTrs
    (33) RewriteLemmaProof [LOWER BOUND(ID), 294 ms]
    (34) typed CpxTrs
    (35) RewriteLemmaProof [LOWER BOUND(ID), 129 ms]
    (36) typed CpxTrs
    (37) RewriteLemmaProof [LOWER BOUND(ID), 756 ms]
    (38) BEST
        (39) proven lower bound
            (40) LowerBoundPropagationProof [FINISHED, 0 ms]
            (41) BOUNDS(n^1, INF)
        (42) typed CpxTrs
            (43) RewriteLemmaProof [LOWER BOUND(ID), 73 ms]
            (44) BOUNDS(1, INF)


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

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


The TRS R consists of the following rules:

   merge(Cons(x, xs), Nil) -> Cons(x, xs)
   merge(Cons(x', xs'), Cons(x, xs)) -> merge[Ite](<=(x', x), Cons(x', xs'), Cons(x, xs))
   merge(Nil, ys) -> ys
   goal(xs, ys) -> merge(xs, ys)

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

   <=(S(x), S(y)) -> <=(x, y)
   <=(0, y) -> True
   <=(S(x), 0) -> False
   merge[Ite](False, xs', Cons(x, xs)) -> Cons(x, merge(xs', xs))
   merge[Ite](True, Cons(x, xs), ys) -> Cons(x, merge(xs, ys))

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

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


The TRS R consists of the following rules:

   merge(Cons(x, xs), Nil) -> Cons(x, xs)
   merge(Cons(x', xs'), Cons(x, xs)) -> merge[Ite](<=(x', x), Cons(x', xs'), Cons(x, xs))
   merge(Nil, ys) -> ys
   goal(xs, ys) -> merge(xs, ys)

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

   <=(S(x), S(y)) -> <=(x, y)
   <=(0, y) -> True
   <=(S(x), 0) -> False
   merge[Ite](False, xs', Cons(x, xs)) -> Cons(x, merge(xs', xs))
   merge[Ite](True, Cons(x, xs), ys) -> Cons(x, merge(xs, ys))

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   <=(S(z0), S(z1)) -> <=(z0, z1)
   <=(0, z0) -> True
   <=(S(z0), 0) -> False
   merge[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, merge(z0, z2))
   merge[Ite](True, Cons(z0, z1), z2) -> Cons(z0, merge(z1, z2))
   merge(Cons(z0, z1), Nil) -> Cons(z0, z1)
   merge(Cons(z0, z1), Cons(z2, z3)) -> merge[Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3))
   merge(Nil, z0) -> z0
   goal(z0, z1) -> merge(z0, z1)
Tuples:
   <='(S(z0), S(z1)) -> c(<='(z0, z1))
   <='(0, z0) -> c1
   <='(S(z0), 0) -> c2
   MERGE[ITE](False, z0, Cons(z1, z2)) -> c3(MERGE(z0, z2))
   MERGE[ITE](True, Cons(z0, z1), z2) -> c4(MERGE(z1, z2))
   MERGE(Cons(z0, z1), Nil) -> c5
   MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
   MERGE(Nil, z0) -> c7
   GOAL(z0, z1) -> c8(MERGE(z0, z1))
S tuples:
   MERGE(Cons(z0, z1), Nil) -> c5
   MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
   MERGE(Nil, z0) -> c7
   GOAL(z0, z1) -> c8(MERGE(z0, z1))
K tuples:none
Defined Rule Symbols:   merge_2, goal_2, <=_2, merge[Ite]_3

Defined Pair Symbols:   <='_2, MERGE[ITE]_3, MERGE_2, GOAL_2

Compound Symbols:   c_1, c1, c2, c3_1, c4_1, c5, c6_2, c7, c8_1


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

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 1 leading nodes:
   GOAL(z0, z1) -> c8(MERGE(z0, z1))
Removed 2 trailing nodes:
   <='(0, z0) -> c1
   <='(S(z0), 0) -> c2

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   <=(S(z0), S(z1)) -> <=(z0, z1)
   <=(0, z0) -> True
   <=(S(z0), 0) -> False
   merge[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, merge(z0, z2))
   merge[Ite](True, Cons(z0, z1), z2) -> Cons(z0, merge(z1, z2))
   merge(Cons(z0, z1), Nil) -> Cons(z0, z1)
   merge(Cons(z0, z1), Cons(z2, z3)) -> merge[Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3))
   merge(Nil, z0) -> z0
   goal(z0, z1) -> merge(z0, z1)
Tuples:
   <='(S(z0), S(z1)) -> c(<='(z0, z1))
   MERGE[ITE](False, z0, Cons(z1, z2)) -> c3(MERGE(z0, z2))
   MERGE[ITE](True, Cons(z0, z1), z2) -> c4(MERGE(z1, z2))
   MERGE(Cons(z0, z1), Nil) -> c5
   MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
   MERGE(Nil, z0) -> c7
S tuples:
   MERGE(Cons(z0, z1), Nil) -> c5
   MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
   MERGE(Nil, z0) -> c7
K tuples:none
Defined Rule Symbols:   merge_2, goal_2, <=_2, merge[Ite]_3

Defined Pair Symbols:   <='_2, MERGE[ITE]_3, MERGE_2

Compound Symbols:   c_1, c3_1, c4_1, c5, c6_2, c7


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

(7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   merge[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, merge(z0, z2))
   merge[Ite](True, Cons(z0, z1), z2) -> Cons(z0, merge(z1, z2))
   merge(Cons(z0, z1), Nil) -> Cons(z0, z1)
   merge(Cons(z0, z1), Cons(z2, z3)) -> merge[Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3))
   merge(Nil, z0) -> z0
   goal(z0, z1) -> merge(z0, z1)

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   <=(S(z0), S(z1)) -> <=(z0, z1)
   <=(0, z0) -> True
   <=(S(z0), 0) -> False
Tuples:
   <='(S(z0), S(z1)) -> c(<='(z0, z1))
   MERGE[ITE](False, z0, Cons(z1, z2)) -> c3(MERGE(z0, z2))
   MERGE[ITE](True, Cons(z0, z1), z2) -> c4(MERGE(z1, z2))
   MERGE(Cons(z0, z1), Nil) -> c5
   MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
   MERGE(Nil, z0) -> c7
S tuples:
   MERGE(Cons(z0, z1), Nil) -> c5
   MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
   MERGE(Nil, z0) -> c7
K tuples:none
Defined Rule Symbols:   <=_2

Defined Pair Symbols:   <='_2, MERGE[ITE]_3, MERGE_2

Compound Symbols:   c_1, c3_1, c4_1, c5, c6_2, c7


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

(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 CpxRelTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

   MERGE(Cons(z0, z1), Nil) -> c5
   MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
   MERGE(Nil, z0) -> c7

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

   <='(S(z0), S(z1)) -> c(<='(z0, z1))
   MERGE[ITE](False, z0, Cons(z1, z2)) -> c3(MERGE(z0, z2))
   MERGE[ITE](True, Cons(z0, z1), z2) -> c4(MERGE(z1, z2))
   <=(S(z0), S(z1)) -> <=(z0, z1)
   <=(0, z0) -> True
   <=(S(z0), 0) -> False

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

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

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

   MERGE(Cons(z0, z1), Nil) -> c5 [1]
   MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2)) [1]
   MERGE(Nil, z0) -> c7 [1]
   <='(S(z0), S(z1)) -> c(<='(z0, z1)) [0]
   MERGE[ITE](False, z0, Cons(z1, z2)) -> c3(MERGE(z0, z2)) [0]
   MERGE[ITE](True, Cons(z0, z1), z2) -> c4(MERGE(z1, z2)) [0]
   <=(S(z0), S(z1)) -> <=(z0, z1) [0]
   <=(0, z0) -> True [0]
   <=(S(z0), 0) -> False [0]

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

(13) CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID))
Renamed defined symbols to avoid conflicts with arithmetic symbols:

<= => lteq

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

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

   MERGE(Cons(z0, z1), Nil) -> c5 [1]
   MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](lteq(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2)) [1]
   MERGE(Nil, z0) -> c7 [1]
   <='(S(z0), S(z1)) -> c(<='(z0, z1)) [0]
   MERGE[ITE](False, z0, Cons(z1, z2)) -> c3(MERGE(z0, z2)) [0]
   MERGE[ITE](True, Cons(z0, z1), z2) -> c4(MERGE(z1, z2)) [0]
   lteq(S(z0), S(z1)) -> lteq(z0, z1) [0]
   lteq(0, z0) -> True [0]
   lteq(S(z0), 0) -> False [0]

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

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

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

   MERGE(Cons(z0, z1), Nil) -> c5 [1]
   MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](lteq(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2)) [1]
   MERGE(Nil, z0) -> c7 [1]
   <='(S(z0), S(z1)) -> c(<='(z0, z1)) [0]
   MERGE[ITE](False, z0, Cons(z1, z2)) -> c3(MERGE(z0, z2)) [0]
   MERGE[ITE](True, Cons(z0, z1), z2) -> c4(MERGE(z1, z2)) [0]
   lteq(S(z0), S(z1)) -> lteq(z0, z1) [0]
   lteq(0, z0) -> True [0]
   lteq(S(z0), 0) -> False [0]

The TRS has the following type information:
MERGE :: Cons:Nil -> Cons:Nil -> c5:c6:c7
Cons :: S:0 -> Cons:Nil -> Cons:Nil
Nil :: Cons:Nil
c5 :: c5:c6:c7
c6 :: c3:c4 -> c -> c5:c6:c7
MERGE[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c3:c4
lteq :: S:0 -> S:0 -> False:True
<=' :: S:0 -> S:0 -> c
c7 :: c5:c6:c7
S :: S:0 -> S:0
c :: c -> c
False :: False:True
c3 :: c5:c6:c7 -> c3:c4
True :: False:True
c4 :: c5:c6:c7 -> c3:c4
0 :: S:0

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

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

   <='(v0, v1) -> null_<=' [0]
   MERGE[ITE](v0, v1, v2) -> null_MERGE[ITE] [0]
   lteq(v0, v1) -> null_lteq [0]

And the following fresh constants:    null_<=', null_MERGE[ITE], null_lteq

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

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

   MERGE(Cons(z0, z1), Nil) -> c5 [1]
   MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](lteq(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2)) [1]
   MERGE(Nil, z0) -> c7 [1]
   <='(S(z0), S(z1)) -> c(<='(z0, z1)) [0]
   MERGE[ITE](False, z0, Cons(z1, z2)) -> c3(MERGE(z0, z2)) [0]
   MERGE[ITE](True, Cons(z0, z1), z2) -> c4(MERGE(z1, z2)) [0]
   lteq(S(z0), S(z1)) -> lteq(z0, z1) [0]
   lteq(0, z0) -> True [0]
   lteq(S(z0), 0) -> False [0]
   <='(v0, v1) -> null_<=' [0]
   MERGE[ITE](v0, v1, v2) -> null_MERGE[ITE] [0]
   lteq(v0, v1) -> null_lteq [0]

The TRS has the following type information:
MERGE :: Cons:Nil -> Cons:Nil -> c5:c6:c7
Cons :: S:0 -> Cons:Nil -> Cons:Nil
Nil :: Cons:Nil
c5 :: c5:c6:c7
c6 :: c3:c4:null_MERGE[ITE] -> c:null_<=' -> c5:c6:c7
MERGE[ITE] :: False:True:null_lteq -> Cons:Nil -> Cons:Nil -> c3:c4:null_MERGE[ITE]
lteq :: S:0 -> S:0 -> False:True:null_lteq
<=' :: S:0 -> S:0 -> c:null_<='
c7 :: c5:c6:c7
S :: S:0 -> S:0
c :: c:null_<=' -> c:null_<='
False :: False:True:null_lteq
c3 :: c5:c6:c7 -> c3:c4:null_MERGE[ITE]
True :: False:True:null_lteq
c4 :: c5:c6:c7 -> c3:c4:null_MERGE[ITE]
0 :: S:0
null_<=' :: c:null_<='
null_MERGE[ITE] :: c3:c4:null_MERGE[ITE]
null_lteq :: False:True:null_lteq

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

(19) 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
   c5 => 0
   c7 => 1
   False => 1
   True => 2
   0 => 0
   null_<=' => 0
   null_MERGE[ITE] => 0
   null_lteq => 0

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

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

   <='(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   <='(z, z') -{ 0 }-> 1 + <='(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   MERGE(z, z') -{ 1 }-> 1 :|: z0 >= 0, z = 0, z' = z0
   MERGE(z, z') -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' = 0
   MERGE(z, z') -{ 1 }-> 1 + MERGE[ITE](lteq(z0, z2), 1 + z0 + z1, 1 + z2 + z3) + <='(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0
   MERGE[ITE](z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   MERGE[ITE](z, z', z'') -{ 0 }-> 1 + MERGE(z0, z2) :|: z1 >= 0, z = 1, z'' = 1 + z1 + z2, z0 >= 0, z' = z0, z2 >= 0
   MERGE[ITE](z, z', z'') -{ 0 }-> 1 + MERGE(z1, z2) :|: z = 2, z'' = z2, z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z2 >= 0
   lteq(z, z') -{ 0 }-> lteq(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   lteq(z, z') -{ 0 }-> 2 :|: z0 >= 0, z = 0, z' = z0
   lteq(z, z') -{ 0 }-> 1 :|: z = 1 + z0, z0 >= 0, z' = 0
   lteq(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1

Only complete derivations are relevant for the runtime complexity.

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

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

eq(start(V1, V, V12),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V12),0,[fun2(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V, V12),0,[fun1(V1, V, V12, Out)],[V1 >= 0,V >= 0,V12 >= 0]).
eq(start(V1, V, V12),0,[lteq(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(fun(V1, V, Out),1,[],[Out = 0,V2 >= 0,V3 >= 0,V1 = 1 + V2 + V3,V = 0]).
eq(fun(V1, V, Out),1,[lteq(V5, V7, Ret010),fun1(Ret010, 1 + V5 + V4, 1 + V7 + V6, Ret01),fun2(V5, V7, Ret1)],[Out = 1 + Ret01 + Ret1,V4 >= 0,V = 1 + V6 + V7,V5 >= 0,V1 = 1 + V4 + V5,V7 >= 0,V6 >= 0]).
eq(fun(V1, V, Out),1,[],[Out = 1,V8 >= 0,V1 = 0,V = V8]).
eq(fun2(V1, V, Out),0,[fun2(V9, V10, Ret11)],[Out = 1 + Ret11,V10 >= 0,V1 = 1 + V9,V9 >= 0,V = 1 + V10]).
eq(fun1(V1, V, V12, Out),0,[fun(V11, V13, Ret12)],[Out = 1 + Ret12,V14 >= 0,V1 = 1,V12 = 1 + V13 + V14,V11 >= 0,V = V11,V13 >= 0]).
eq(fun1(V1, V, V12, Out),0,[fun(V15, V17, Ret13)],[Out = 1 + Ret13,V1 = 2,V12 = V17,V = 1 + V15 + V16,V15 >= 0,V16 >= 0,V17 >= 0]).
eq(lteq(V1, V, Out),0,[lteq(V19, V18, Ret)],[Out = Ret,V18 >= 0,V1 = 1 + V19,V19 >= 0,V = 1 + V18]).
eq(lteq(V1, V, Out),0,[],[Out = 2,V20 >= 0,V1 = 0,V = V20]).
eq(lteq(V1, V, Out),0,[],[Out = 1,V1 = 1 + V21,V21 >= 0,V = 0]).
eq(fun2(V1, V, Out),0,[],[Out = 0,V23 >= 0,V22 >= 0,V1 = V23,V = V22]).
eq(fun1(V1, V, V12, Out),0,[],[Out = 0,V25 >= 0,V12 = V26,V24 >= 0,V1 = V25,V = V24,V26 >= 0]).
eq(lteq(V1, V, Out),0,[],[Out = 0,V28 >= 0,V27 >= 0,V1 = V28,V = V27]).
input_output_vars(fun(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun2(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun1(V1,V,V12,Out),[V1,V,V12],[Out]).
input_output_vars(lteq(V1,V,Out),[V1,V],[Out]).


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

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

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

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

### Specialization of cost equations fun2/3 
* CE 13 is refined into CE [18] 
* CE 12 is refined into CE [19] 


### Cost equations --> "Loop" of fun2/3 
* CEs [19] --> Loop 14 
* CEs [18] --> Loop 15 

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

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


### Specialization of cost equations lteq/3 
* CE 17 is refined into CE [20] 
* CE 16 is refined into CE [21] 
* CE 15 is refined into CE [22] 
* CE 14 is refined into CE [23] 


### Cost equations --> "Loop" of lteq/3 
* CEs [23] --> Loop 16 
* CEs [20] --> Loop 17 
* CEs [21] --> Loop 18 
* CEs [22] --> Loop 19 

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

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


### Specialization of cost equations fun/3 
* CE 7 is refined into CE [24,25,26,27,28,29,30,31] 
* CE 10 is refined into CE [32] 
* CE 11 is refined into CE [33] 
* CE 8 is refined into CE [34,35,36] 
* CE 9 is refined into CE [37,38,39] 


### Cost equations --> "Loop" of fun/3 
* CEs [36] --> Loop 20 
* CEs [34,35] --> Loop 21 
* CEs [39] --> Loop 22 
* CEs [37,38] --> Loop 23 
* CEs [27,29,31] --> Loop 24 
* CEs [24,25,26,28,30] --> Loop 25 
* CEs [32] --> Loop 26 
* CEs [33] --> Loop 27 

### Ranking functions of CR fun(V1,V,Out) 
* RF of phase [20,21,22,23]: [V1+V-1,V1+2*V-2]

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


### Specialization of cost equations start/3 
* CE 2 is refined into CE [40,41,42,43,44] 
* CE 1 is refined into CE [45] 
* CE 3 is refined into CE [46,47,48,49,50] 
* CE 4 is refined into CE [51,52,53,54,55] 
* CE 5 is refined into CE [56,57] 
* CE 6 is refined into CE [58,59,60,61,62] 


### Cost equations --> "Loop" of start/3 
* CEs [40,41,42,43,44] --> Loop 28 
* CEs [47,48,49,50] --> Loop 29 
* CEs [46,52,59] --> Loop 30 
* CEs [45,51,53,54,55,56,57,58,60,61,62] --> Loop 31 

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

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


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

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

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


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

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

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

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

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

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


#### Cost of chains of fun(V1,V,Out):
* Chain [[20,21,22,23],27]: 2*it(20)+2*it(22)+1
  Such that:aux(9) =< V1
aux(10) =< V1+V
aux(11) =< V1+2*V
aux(12) =< V
it(20) =< aux(9)
it(20) =< aux(10)
it(22) =< aux(10)
it(20) =< aux(11)
it(22) =< aux(11)
it(22) =< aux(12)

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

* Chain [[20,21,22,23],26]: 2*it(20)+2*it(22)+1
  Such that:aux(13) =< V1
aux(14) =< V1+V
aux(15) =< V1+2*V
aux(16) =< V
it(20) =< aux(13)
it(20) =< aux(14)
it(22) =< aux(14)
it(20) =< aux(15)
it(22) =< aux(15)
it(22) =< aux(16)

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

* Chain [[20,21,22,23],25]: 2*it(20)+2*it(22)+1
  Such that:aux(17) =< V1
aux(18) =< V1+V
aux(19) =< V1+2*V
aux(20) =< V
it(20) =< aux(17)
it(20) =< aux(18)
it(22) =< aux(18)
it(20) =< aux(19)
it(22) =< aux(19)
it(22) =< aux(20)

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

* Chain [[20,21,22,23],24]: 2*it(20)+2*it(22)+1
  Such that:aux(21) =< V1
aux(22) =< V1+V
aux(23) =< V1+2*V
aux(24) =< V
it(20) =< aux(21)
it(20) =< aux(22)
it(22) =< aux(22)
it(20) =< aux(23)
it(22) =< aux(23)
it(22) =< aux(24)

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

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

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

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

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


#### Cost of chains of start(V1,V,V12):
* Chain [31]: 8*s(29)+8*s(30)+1
  Such that:aux(29) =< V1
aux(30) =< V1+V
aux(31) =< V1+2*V
aux(32) =< V
s(29) =< aux(29)
s(29) =< aux(30)
s(30) =< aux(30)
s(29) =< aux(31)
s(30) =< aux(31)
s(30) =< aux(32)

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

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

* Chain [29]: 8*s(41)+8*s(42)+1
  Such that:aux(33) =< V
aux(34) =< V+V12
aux(35) =< V+2*V12
aux(36) =< V12
s(41) =< aux(33)
s(41) =< aux(34)
s(42) =< aux(34)
s(41) =< aux(35)
s(42) =< aux(35)
s(42) =< aux(36)

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

* Chain [28]: 8*s(53)+8*s(54)+1
  Such that:aux(37) =< V
aux(38) =< V+V12
aux(39) =< V+2*V12
aux(40) =< V12
s(53) =< aux(37)
s(53) =< aux(38)
s(54) =< aux(38)
s(53) =< aux(39)
s(54) =< aux(39)
s(54) =< aux(40)

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


Closed-form bounds of start(V1,V,V12): 
-------------------------------------
* Chain [31] with precondition: [V1>=0,V>=0] 
    - Upper bound: 16*V1+8*V+1 
    - Complexity: n 
* Chain [30] with precondition: [V=0,V1>=1] 
    - Upper bound: 1 
    - Complexity: constant 
* Chain [29] with precondition: [V1=1,V>=1,V12>=1] 
    - Upper bound: 16*V+8*V12+1 
    - Complexity: n 
* Chain [28] with precondition: [V1=2,V>=1,V12>=0] 
    - Upper bound: 16*V+8*V12+1 
    - Complexity: n 

### Maximum cost of start(V1,V,V12): max([16*V1+8*V,nat(V+V12)*8+8*V])+1 
Asymptotic class: n 
* Total analysis performed in 451 ms.


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

(22)
BOUNDS(1, n^1)

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

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

(24)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   <=(S(z0), S(z1)) -> <=(z0, z1)
   <=(0, z0) -> True
   <=(S(z0), 0) -> False
   merge[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, merge(z0, z2))
   merge[Ite](True, Cons(z0, z1), z2) -> Cons(z0, merge(z1, z2))
   merge(Cons(z0, z1), Nil) -> Cons(z0, z1)
   merge(Cons(z0, z1), Cons(z2, z3)) -> merge[Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3))
   merge(Nil, z0) -> z0
   goal(z0, z1) -> merge(z0, z1)
Tuples:
   <='(S(z0), S(z1)) -> c(<='(z0, z1))
   <='(0, z0) -> c1
   <='(S(z0), 0) -> c2
   MERGE[ITE](False, z0, Cons(z1, z2)) -> c3(MERGE(z0, z2))
   MERGE[ITE](True, Cons(z0, z1), z2) -> c4(MERGE(z1, z2))
   MERGE(Cons(z0, z1), Nil) -> c5
   MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
   MERGE(Nil, z0) -> c7
   GOAL(z0, z1) -> c8(MERGE(z0, z1))
S tuples:
   MERGE(Cons(z0, z1), Nil) -> c5
   MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
   MERGE(Nil, z0) -> c7
   GOAL(z0, z1) -> c8(MERGE(z0, z1))
K tuples:none
Defined Rule Symbols:   merge_2, goal_2, <=_2, merge[Ite]_3

Defined Pair Symbols:   <='_2, MERGE[ITE]_3, MERGE_2, GOAL_2

Compound Symbols:   c_1, c1, c2, c3_1, c4_1, c5, c6_2, c7, c8_1


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

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

(26)
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(Cons(z0, z1), Nil) -> c5
   MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
   MERGE(Nil, z0) -> c7
   GOAL(z0, z1) -> c8(MERGE(z0, z1))

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

   <='(S(z0), S(z1)) -> c(<='(z0, z1))
   <='(0, z0) -> c1
   <='(S(z0), 0) -> c2
   MERGE[ITE](False, z0, Cons(z1, z2)) -> c3(MERGE(z0, z2))
   MERGE[ITE](True, Cons(z0, z1), z2) -> c4(MERGE(z1, z2))
   <=(S(z0), S(z1)) -> <=(z0, z1)
   <=(0, z0) -> True
   <=(S(z0), 0) -> False
   merge[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, merge(z0, z2))
   merge[Ite](True, Cons(z0, z1), z2) -> Cons(z0, merge(z1, z2))
   merge(Cons(z0, z1), Nil) -> Cons(z0, z1)
   merge(Cons(z0, z1), Cons(z2, z3)) -> merge[Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3))
   merge(Nil, z0) -> z0
   goal(z0, z1) -> merge(z0, z1)

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

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

(28)
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(Cons(z0, z1), Nil) -> c5
   MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
   MERGE(Nil, z0) -> c7
   GOAL(z0, z1) -> c8(MERGE(z0, z1))

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

   <='(S(z0), S(z1)) -> c(<='(z0, z1))
   <='(0', z0) -> c1
   <='(S(z0), 0') -> c2
   MERGE[ITE](False, z0, Cons(z1, z2)) -> c3(MERGE(z0, z2))
   MERGE[ITE](True, Cons(z0, z1), z2) -> c4(MERGE(z1, z2))
   <=(S(z0), S(z1)) -> <=(z0, z1)
   <=(0', z0) -> True
   <=(S(z0), 0') -> False
   merge[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, merge(z0, z2))
   merge[Ite](True, Cons(z0, z1), z2) -> Cons(z0, merge(z1, z2))
   merge(Cons(z0, z1), Nil) -> Cons(z0, z1)
   merge(Cons(z0, z1), Cons(z2, z3)) -> merge[Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3))
   merge(Nil, z0) -> z0
   goal(z0, z1) -> merge(z0, z1)

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

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

(30)
Obligation:
Innermost TRS:
Rules:
MERGE(Cons(z0, z1), Nil) -> c5
MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
MERGE(Nil, z0) -> c7
GOAL(z0, z1) -> c8(MERGE(z0, z1))
<='(S(z0), S(z1)) -> c(<='(z0, z1))
<='(0', z0) -> c1
<='(S(z0), 0') -> c2
MERGE[ITE](False, z0, Cons(z1, z2)) -> c3(MERGE(z0, z2))
MERGE[ITE](True, Cons(z0, z1), z2) -> c4(MERGE(z1, z2))
<=(S(z0), S(z1)) -> <=(z0, z1)
<=(0', z0) -> True
<=(S(z0), 0') -> False
merge[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, merge(z0, z2))
merge[Ite](True, Cons(z0, z1), z2) -> Cons(z0, merge(z1, z2))
merge(Cons(z0, z1), Nil) -> Cons(z0, z1)
merge(Cons(z0, z1), Cons(z2, z3)) -> merge[Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3))
merge(Nil, z0) -> z0
goal(z0, z1) -> merge(z0, z1)

Types:
MERGE :: Cons:Nil -> Cons:Nil -> c5:c6:c7
Cons :: S:0' -> Cons:Nil -> Cons:Nil
Nil :: Cons:Nil
c5 :: c5:c6:c7
c6 :: c3:c4 -> c:c1:c2 -> c5:c6:c7
MERGE[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c3:c4
<= :: S:0' -> S:0' -> False:True
<=' :: S:0' -> S:0' -> c:c1:c2
c7 :: c5:c6:c7
GOAL :: Cons:Nil -> Cons:Nil -> c8
c8 :: c5:c6:c7 -> c8
S :: S:0' -> S:0'
c :: c:c1:c2 -> c:c1:c2
0' :: S:0'
c1 :: c:c1:c2
c2 :: c:c1:c2
False :: False:True
c3 :: c5:c6:c7 -> c3:c4
True :: False:True
c4 :: c5:c6:c7 -> c3:c4
merge[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
merge :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c5:c6:c71_9 :: c5:c6:c7
hole_Cons:Nil2_9 :: Cons:Nil
hole_S:0'3_9 :: S:0'
hole_c3:c44_9 :: c3:c4
hole_c:c1:c25_9 :: c:c1:c2
hole_False:True6_9 :: False:True
hole_c87_9 :: c8
gen_Cons:Nil8_9 :: Nat -> Cons:Nil
gen_S:0'9_9 :: Nat -> S:0'
gen_c:c1:c210_9 :: Nat -> c:c1:c2

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

(31) 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
<= < merge

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

(32)
Obligation:
Innermost TRS:
Rules:
MERGE(Cons(z0, z1), Nil) -> c5
MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
MERGE(Nil, z0) -> c7
GOAL(z0, z1) -> c8(MERGE(z0, z1))
<='(S(z0), S(z1)) -> c(<='(z0, z1))
<='(0', z0) -> c1
<='(S(z0), 0') -> c2
MERGE[ITE](False, z0, Cons(z1, z2)) -> c3(MERGE(z0, z2))
MERGE[ITE](True, Cons(z0, z1), z2) -> c4(MERGE(z1, z2))
<=(S(z0), S(z1)) -> <=(z0, z1)
<=(0', z0) -> True
<=(S(z0), 0') -> False
merge[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, merge(z0, z2))
merge[Ite](True, Cons(z0, z1), z2) -> Cons(z0, merge(z1, z2))
merge(Cons(z0, z1), Nil) -> Cons(z0, z1)
merge(Cons(z0, z1), Cons(z2, z3)) -> merge[Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3))
merge(Nil, z0) -> z0
goal(z0, z1) -> merge(z0, z1)

Types:
MERGE :: Cons:Nil -> Cons:Nil -> c5:c6:c7
Cons :: S:0' -> Cons:Nil -> Cons:Nil
Nil :: Cons:Nil
c5 :: c5:c6:c7
c6 :: c3:c4 -> c:c1:c2 -> c5:c6:c7
MERGE[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c3:c4
<= :: S:0' -> S:0' -> False:True
<=' :: S:0' -> S:0' -> c:c1:c2
c7 :: c5:c6:c7
GOAL :: Cons:Nil -> Cons:Nil -> c8
c8 :: c5:c6:c7 -> c8
S :: S:0' -> S:0'
c :: c:c1:c2 -> c:c1:c2
0' :: S:0'
c1 :: c:c1:c2
c2 :: c:c1:c2
False :: False:True
c3 :: c5:c6:c7 -> c3:c4
True :: False:True
c4 :: c5:c6:c7 -> c3:c4
merge[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
merge :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c5:c6:c71_9 :: c5:c6:c7
hole_Cons:Nil2_9 :: Cons:Nil
hole_S:0'3_9 :: S:0'
hole_c3:c44_9 :: c3:c4
hole_c:c1:c25_9 :: c:c1:c2
hole_False:True6_9 :: False:True
hole_c87_9 :: c8
gen_Cons:Nil8_9 :: Nat -> Cons:Nil
gen_S:0'9_9 :: Nat -> S:0'
gen_c:c1:c210_9 :: Nat -> c:c1:c2


Generator Equations:
gen_Cons:Nil8_9(0) <=> Nil
gen_Cons:Nil8_9(+(x, 1)) <=> Cons(0', gen_Cons:Nil8_9(x))
gen_S:0'9_9(0) <=> 0'
gen_S:0'9_9(+(x, 1)) <=> S(gen_S:0'9_9(x))
gen_c:c1:c210_9(0) <=> c1
gen_c:c1:c210_9(+(x, 1)) <=> c(gen_c:c1:c210_9(x))


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

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

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

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
<=(gen_S:0'9_9(n12_9), gen_S:0'9_9(n12_9)) -> True, rt in Omega(0)

Induction Base:
<=(gen_S:0'9_9(0), gen_S:0'9_9(0)) ->_R^Omega(0)
True

Induction Step:
<=(gen_S:0'9_9(+(n12_9, 1)), gen_S:0'9_9(+(n12_9, 1))) ->_R^Omega(0)
<=(gen_S:0'9_9(n12_9), gen_S:0'9_9(n12_9)) ->_IH
True

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

(34)
Obligation:
Innermost TRS:
Rules:
MERGE(Cons(z0, z1), Nil) -> c5
MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
MERGE(Nil, z0) -> c7
GOAL(z0, z1) -> c8(MERGE(z0, z1))
<='(S(z0), S(z1)) -> c(<='(z0, z1))
<='(0', z0) -> c1
<='(S(z0), 0') -> c2
MERGE[ITE](False, z0, Cons(z1, z2)) -> c3(MERGE(z0, z2))
MERGE[ITE](True, Cons(z0, z1), z2) -> c4(MERGE(z1, z2))
<=(S(z0), S(z1)) -> <=(z0, z1)
<=(0', z0) -> True
<=(S(z0), 0') -> False
merge[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, merge(z0, z2))
merge[Ite](True, Cons(z0, z1), z2) -> Cons(z0, merge(z1, z2))
merge(Cons(z0, z1), Nil) -> Cons(z0, z1)
merge(Cons(z0, z1), Cons(z2, z3)) -> merge[Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3))
merge(Nil, z0) -> z0
goal(z0, z1) -> merge(z0, z1)

Types:
MERGE :: Cons:Nil -> Cons:Nil -> c5:c6:c7
Cons :: S:0' -> Cons:Nil -> Cons:Nil
Nil :: Cons:Nil
c5 :: c5:c6:c7
c6 :: c3:c4 -> c:c1:c2 -> c5:c6:c7
MERGE[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c3:c4
<= :: S:0' -> S:0' -> False:True
<=' :: S:0' -> S:0' -> c:c1:c2
c7 :: c5:c6:c7
GOAL :: Cons:Nil -> Cons:Nil -> c8
c8 :: c5:c6:c7 -> c8
S :: S:0' -> S:0'
c :: c:c1:c2 -> c:c1:c2
0' :: S:0'
c1 :: c:c1:c2
c2 :: c:c1:c2
False :: False:True
c3 :: c5:c6:c7 -> c3:c4
True :: False:True
c4 :: c5:c6:c7 -> c3:c4
merge[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
merge :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c5:c6:c71_9 :: c5:c6:c7
hole_Cons:Nil2_9 :: Cons:Nil
hole_S:0'3_9 :: S:0'
hole_c3:c44_9 :: c3:c4
hole_c:c1:c25_9 :: c:c1:c2
hole_False:True6_9 :: False:True
hole_c87_9 :: c8
gen_Cons:Nil8_9 :: Nat -> Cons:Nil
gen_S:0'9_9 :: Nat -> S:0'
gen_c:c1:c210_9 :: Nat -> c:c1:c2


Lemmas:
<=(gen_S:0'9_9(n12_9), gen_S:0'9_9(n12_9)) -> True, rt in Omega(0)


Generator Equations:
gen_Cons:Nil8_9(0) <=> Nil
gen_Cons:Nil8_9(+(x, 1)) <=> Cons(0', gen_Cons:Nil8_9(x))
gen_S:0'9_9(0) <=> 0'
gen_S:0'9_9(+(x, 1)) <=> S(gen_S:0'9_9(x))
gen_c:c1:c210_9(0) <=> c1
gen_c:c1:c210_9(+(x, 1)) <=> c(gen_c:c1:c210_9(x))


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

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

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

(35) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
<='(gen_S:0'9_9(n279_9), gen_S:0'9_9(n279_9)) -> gen_c:c1:c210_9(n279_9), rt in Omega(0)

Induction Base:
<='(gen_S:0'9_9(0), gen_S:0'9_9(0)) ->_R^Omega(0)
c1

Induction Step:
<='(gen_S:0'9_9(+(n279_9, 1)), gen_S:0'9_9(+(n279_9, 1))) ->_R^Omega(0)
c(<='(gen_S:0'9_9(n279_9), gen_S:0'9_9(n279_9))) ->_IH
c(gen_c:c1:c210_9(c280_9))

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

(36)
Obligation:
Innermost TRS:
Rules:
MERGE(Cons(z0, z1), Nil) -> c5
MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
MERGE(Nil, z0) -> c7
GOAL(z0, z1) -> c8(MERGE(z0, z1))
<='(S(z0), S(z1)) -> c(<='(z0, z1))
<='(0', z0) -> c1
<='(S(z0), 0') -> c2
MERGE[ITE](False, z0, Cons(z1, z2)) -> c3(MERGE(z0, z2))
MERGE[ITE](True, Cons(z0, z1), z2) -> c4(MERGE(z1, z2))
<=(S(z0), S(z1)) -> <=(z0, z1)
<=(0', z0) -> True
<=(S(z0), 0') -> False
merge[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, merge(z0, z2))
merge[Ite](True, Cons(z0, z1), z2) -> Cons(z0, merge(z1, z2))
merge(Cons(z0, z1), Nil) -> Cons(z0, z1)
merge(Cons(z0, z1), Cons(z2, z3)) -> merge[Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3))
merge(Nil, z0) -> z0
goal(z0, z1) -> merge(z0, z1)

Types:
MERGE :: Cons:Nil -> Cons:Nil -> c5:c6:c7
Cons :: S:0' -> Cons:Nil -> Cons:Nil
Nil :: Cons:Nil
c5 :: c5:c6:c7
c6 :: c3:c4 -> c:c1:c2 -> c5:c6:c7
MERGE[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c3:c4
<= :: S:0' -> S:0' -> False:True
<=' :: S:0' -> S:0' -> c:c1:c2
c7 :: c5:c6:c7
GOAL :: Cons:Nil -> Cons:Nil -> c8
c8 :: c5:c6:c7 -> c8
S :: S:0' -> S:0'
c :: c:c1:c2 -> c:c1:c2
0' :: S:0'
c1 :: c:c1:c2
c2 :: c:c1:c2
False :: False:True
c3 :: c5:c6:c7 -> c3:c4
True :: False:True
c4 :: c5:c6:c7 -> c3:c4
merge[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
merge :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c5:c6:c71_9 :: c5:c6:c7
hole_Cons:Nil2_9 :: Cons:Nil
hole_S:0'3_9 :: S:0'
hole_c3:c44_9 :: c3:c4
hole_c:c1:c25_9 :: c:c1:c2
hole_False:True6_9 :: False:True
hole_c87_9 :: c8
gen_Cons:Nil8_9 :: Nat -> Cons:Nil
gen_S:0'9_9 :: Nat -> S:0'
gen_c:c1:c210_9 :: Nat -> c:c1:c2


Lemmas:
<=(gen_S:0'9_9(n12_9), gen_S:0'9_9(n12_9)) -> True, rt in Omega(0)
<='(gen_S:0'9_9(n279_9), gen_S:0'9_9(n279_9)) -> gen_c:c1:c210_9(n279_9), rt in Omega(0)


Generator Equations:
gen_Cons:Nil8_9(0) <=> Nil
gen_Cons:Nil8_9(+(x, 1)) <=> Cons(0', gen_Cons:Nil8_9(x))
gen_S:0'9_9(0) <=> 0'
gen_S:0'9_9(+(x, 1)) <=> S(gen_S:0'9_9(x))
gen_c:c1:c210_9(0) <=> c1
gen_c:c1:c210_9(+(x, 1)) <=> c(gen_c:c1:c210_9(x))


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

(37) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MERGE(gen_Cons:Nil8_9(+(1, n840_9)), gen_Cons:Nil8_9(1)) -> *11_9, rt in Omega(n840_9)

Induction Base:
MERGE(gen_Cons:Nil8_9(+(1, 0)), gen_Cons:Nil8_9(1))

Induction Step:
MERGE(gen_Cons:Nil8_9(+(1, +(n840_9, 1))), gen_Cons:Nil8_9(1)) ->_R^Omega(1)
c6(MERGE[ITE](<=(0', 0'), Cons(0', gen_Cons:Nil8_9(+(1, n840_9))), Cons(0', gen_Cons:Nil8_9(0))), <='(0', 0')) ->_L^Omega(0)
c6(MERGE[ITE](True, Cons(0', gen_Cons:Nil8_9(+(1, n840_9))), Cons(0', gen_Cons:Nil8_9(0))), <='(0', 0')) ->_R^Omega(0)
c6(c4(MERGE(gen_Cons:Nil8_9(+(1, n840_9)), Cons(0', gen_Cons:Nil8_9(0)))), <='(0', 0')) ->_IH
c6(c4(*11_9), <='(0', 0')) ->_L^Omega(0)
c6(c4(*11_9), gen_c:c1:c210_9(0))

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

(38)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
MERGE(Cons(z0, z1), Nil) -> c5
MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
MERGE(Nil, z0) -> c7
GOAL(z0, z1) -> c8(MERGE(z0, z1))
<='(S(z0), S(z1)) -> c(<='(z0, z1))
<='(0', z0) -> c1
<='(S(z0), 0') -> c2
MERGE[ITE](False, z0, Cons(z1, z2)) -> c3(MERGE(z0, z2))
MERGE[ITE](True, Cons(z0, z1), z2) -> c4(MERGE(z1, z2))
<=(S(z0), S(z1)) -> <=(z0, z1)
<=(0', z0) -> True
<=(S(z0), 0') -> False
merge[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, merge(z0, z2))
merge[Ite](True, Cons(z0, z1), z2) -> Cons(z0, merge(z1, z2))
merge(Cons(z0, z1), Nil) -> Cons(z0, z1)
merge(Cons(z0, z1), Cons(z2, z3)) -> merge[Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3))
merge(Nil, z0) -> z0
goal(z0, z1) -> merge(z0, z1)

Types:
MERGE :: Cons:Nil -> Cons:Nil -> c5:c6:c7
Cons :: S:0' -> Cons:Nil -> Cons:Nil
Nil :: Cons:Nil
c5 :: c5:c6:c7
c6 :: c3:c4 -> c:c1:c2 -> c5:c6:c7
MERGE[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c3:c4
<= :: S:0' -> S:0' -> False:True
<=' :: S:0' -> S:0' -> c:c1:c2
c7 :: c5:c6:c7
GOAL :: Cons:Nil -> Cons:Nil -> c8
c8 :: c5:c6:c7 -> c8
S :: S:0' -> S:0'
c :: c:c1:c2 -> c:c1:c2
0' :: S:0'
c1 :: c:c1:c2
c2 :: c:c1:c2
False :: False:True
c3 :: c5:c6:c7 -> c3:c4
True :: False:True
c4 :: c5:c6:c7 -> c3:c4
merge[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
merge :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c5:c6:c71_9 :: c5:c6:c7
hole_Cons:Nil2_9 :: Cons:Nil
hole_S:0'3_9 :: S:0'
hole_c3:c44_9 :: c3:c4
hole_c:c1:c25_9 :: c:c1:c2
hole_False:True6_9 :: False:True
hole_c87_9 :: c8
gen_Cons:Nil8_9 :: Nat -> Cons:Nil
gen_S:0'9_9 :: Nat -> S:0'
gen_c:c1:c210_9 :: Nat -> c:c1:c2


Lemmas:
<=(gen_S:0'9_9(n12_9), gen_S:0'9_9(n12_9)) -> True, rt in Omega(0)
<='(gen_S:0'9_9(n279_9), gen_S:0'9_9(n279_9)) -> gen_c:c1:c210_9(n279_9), rt in Omega(0)


Generator Equations:
gen_Cons:Nil8_9(0) <=> Nil
gen_Cons:Nil8_9(+(x, 1)) <=> Cons(0', gen_Cons:Nil8_9(x))
gen_S:0'9_9(0) <=> 0'
gen_S:0'9_9(+(x, 1)) <=> S(gen_S:0'9_9(x))
gen_c:c1:c210_9(0) <=> c1
gen_c:c1:c210_9(+(x, 1)) <=> c(gen_c:c1:c210_9(x))


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

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

(41)
BOUNDS(n^1, INF)

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

(42)
Obligation:
Innermost TRS:
Rules:
MERGE(Cons(z0, z1), Nil) -> c5
MERGE(Cons(z0, z1), Cons(z2, z3)) -> c6(MERGE[ITE](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)), <='(z0, z2))
MERGE(Nil, z0) -> c7
GOAL(z0, z1) -> c8(MERGE(z0, z1))
<='(S(z0), S(z1)) -> c(<='(z0, z1))
<='(0', z0) -> c1
<='(S(z0), 0') -> c2
MERGE[ITE](False, z0, Cons(z1, z2)) -> c3(MERGE(z0, z2))
MERGE[ITE](True, Cons(z0, z1), z2) -> c4(MERGE(z1, z2))
<=(S(z0), S(z1)) -> <=(z0, z1)
<=(0', z0) -> True
<=(S(z0), 0') -> False
merge[Ite](False, z0, Cons(z1, z2)) -> Cons(z1, merge(z0, z2))
merge[Ite](True, Cons(z0, z1), z2) -> Cons(z0, merge(z1, z2))
merge(Cons(z0, z1), Nil) -> Cons(z0, z1)
merge(Cons(z0, z1), Cons(z2, z3)) -> merge[Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3))
merge(Nil, z0) -> z0
goal(z0, z1) -> merge(z0, z1)

Types:
MERGE :: Cons:Nil -> Cons:Nil -> c5:c6:c7
Cons :: S:0' -> Cons:Nil -> Cons:Nil
Nil :: Cons:Nil
c5 :: c5:c6:c7
c6 :: c3:c4 -> c:c1:c2 -> c5:c6:c7
MERGE[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c3:c4
<= :: S:0' -> S:0' -> False:True
<=' :: S:0' -> S:0' -> c:c1:c2
c7 :: c5:c6:c7
GOAL :: Cons:Nil -> Cons:Nil -> c8
c8 :: c5:c6:c7 -> c8
S :: S:0' -> S:0'
c :: c:c1:c2 -> c:c1:c2
0' :: S:0'
c1 :: c:c1:c2
c2 :: c:c1:c2
False :: False:True
c3 :: c5:c6:c7 -> c3:c4
True :: False:True
c4 :: c5:c6:c7 -> c3:c4
merge[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil
merge :: Cons:Nil -> Cons:Nil -> Cons:Nil
goal :: Cons:Nil -> Cons:Nil -> Cons:Nil
hole_c5:c6:c71_9 :: c5:c6:c7
hole_Cons:Nil2_9 :: Cons:Nil
hole_S:0'3_9 :: S:0'
hole_c3:c44_9 :: c3:c4
hole_c:c1:c25_9 :: c:c1:c2
hole_False:True6_9 :: False:True
hole_c87_9 :: c8
gen_Cons:Nil8_9 :: Nat -> Cons:Nil
gen_S:0'9_9 :: Nat -> S:0'
gen_c:c1:c210_9 :: Nat -> c:c1:c2


Lemmas:
<=(gen_S:0'9_9(n12_9), gen_S:0'9_9(n12_9)) -> True, rt in Omega(0)
<='(gen_S:0'9_9(n279_9), gen_S:0'9_9(n279_9)) -> gen_c:c1:c210_9(n279_9), rt in Omega(0)
MERGE(gen_Cons:Nil8_9(+(1, n840_9)), gen_Cons:Nil8_9(1)) -> *11_9, rt in Omega(n840_9)


Generator Equations:
gen_Cons:Nil8_9(0) <=> Nil
gen_Cons:Nil8_9(+(x, 1)) <=> Cons(0', gen_Cons:Nil8_9(x))
gen_S:0'9_9(0) <=> 0'
gen_S:0'9_9(+(x, 1)) <=> S(gen_S:0'9_9(x))
gen_c:c1:c210_9(0) <=> c1
gen_c:c1:c210_9(+(x, 1)) <=> c(gen_c:c1:c210_9(x))


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

(43) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
merge(gen_Cons:Nil8_9(n7110_9), gen_Cons:Nil8_9(1)) -> gen_Cons:Nil8_9(+(1, n7110_9)), rt in Omega(0)

Induction Base:
merge(gen_Cons:Nil8_9(0), gen_Cons:Nil8_9(1)) ->_R^Omega(0)
gen_Cons:Nil8_9(1)

Induction Step:
merge(gen_Cons:Nil8_9(+(n7110_9, 1)), gen_Cons:Nil8_9(1)) ->_R^Omega(0)
merge[Ite](<=(0', 0'), Cons(0', gen_Cons:Nil8_9(n7110_9)), Cons(0', gen_Cons:Nil8_9(0))) ->_L^Omega(0)
merge[Ite](True, Cons(0', gen_Cons:Nil8_9(n7110_9)), Cons(0', gen_Cons:Nil8_9(0))) ->_R^Omega(0)
Cons(0', merge(gen_Cons:Nil8_9(n7110_9), Cons(0', gen_Cons:Nil8_9(0)))) ->_IH
Cons(0', gen_Cons:Nil8_9(+(1, c7111_9)))

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

(44)
BOUNDS(1, INF)