WORST_CASE(Omega(n^1),O(n^2))
proof of input_1j4ob5fGr3.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^2).

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
    (3) CdtLeafRemovalProof [ComplexityIfPolyImplication, 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) CpxRelTRS
    (11) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) CpxWeightedTrs
    (13) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (14) CpxTypedWeightedTrs
    (15) CompletionProof [UPPER BOUND(ID), 0 ms]
    (16) CpxTypedWeightedCompleteTrs
    (17) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
    (18) CpxRNTS
    (19) CompleteCoflocoProof [FINISHED, 4039 ms]
    (20) BOUNDS(1, n^2)
(21) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(22) CdtProblem
    (23) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (24) CpxRelTRS
    (25) RenamingProof [BOTH BOUNDS(ID, ID), 1 ms]
    (26) CpxRelTRS
    (27) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (28) typed CpxTrs
    (29) OrderProof [LOWER BOUND(ID), 0 ms]
    (30) typed CpxTrs
    (31) RewriteLemmaProof [LOWER BOUND(ID), 252 ms]
    (32) BEST
        (33) proven lower bound
            (34) LowerBoundPropagationProof [FINISHED, 0 ms]
            (35) BOUNDS(n^1, INF)
        (36) typed CpxTrs
            (37) RewriteLemmaProof [LOWER BOUND(ID), 95 ms]
            (38) typed CpxTrs
            (39) RewriteLemmaProof [LOWER BOUND(ID), 74 ms]
            (40) typed CpxTrs
            (41) RewriteLemmaProof [LOWER BOUND(ID), 0 ms]
            (42) typed CpxTrs


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

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


The TRS R consists of the following rules:

   length(nil) -> 0
   length(cons(x, l)) -> s(length(l))
   lt(x, 0) -> false
   lt(0, s(y)) -> true
   lt(s(x), s(y)) -> lt(x, y)
   head(cons(x, l)) -> x
   head(nil) -> undefined
   tail(nil) -> nil
   tail(cons(x, l)) -> l
   reverse(l) -> rev(0, l, nil, l)
   rev(x, l, accu, orig) -> if(lt(x, length(orig)), x, l, accu, orig)
   if(true, x, l, accu, orig) -> rev(s(x), tail(l), cons(head(l), accu), orig)
   if(false, x, l, accu, orig) -> accu

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:
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))
   lt(z0, 0) -> false
   lt(0, s(z0)) -> true
   lt(s(z0), s(z1)) -> lt(z0, z1)
   head(cons(z0, z1)) -> z0
   head(nil) -> undefined
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   reverse(z0) -> rev(0, z0, nil, z0)
   rev(z0, z1, z2, z3) -> if(lt(z0, length(z3)), z0, z1, z2, z3)
   if(true, z0, z1, z2, z3) -> rev(s(z0), tail(z1), cons(head(z1), z2), z3)
   if(false, z0, z1, z2, z3) -> z2
Tuples:
   LENGTH(nil) -> c
   LENGTH(cons(z0, z1)) -> c1(LENGTH(z1))
   LT(z0, 0) -> c2
   LT(0, s(z0)) -> c3
   LT(s(z0), s(z1)) -> c4(LT(z0, z1))
   HEAD(cons(z0, z1)) -> c5
   HEAD(nil) -> c6
   TAIL(nil) -> c7
   TAIL(cons(z0, z1)) -> c8
   REVERSE(z0) -> c9(REV(0, z0, nil, z0))
   REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3))
   IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3), TAIL(z1))
   IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3), HEAD(z1))
   IF(false, z0, z1, z2, z3) -> c13
S tuples:
   LENGTH(nil) -> c
   LENGTH(cons(z0, z1)) -> c1(LENGTH(z1))
   LT(z0, 0) -> c2
   LT(0, s(z0)) -> c3
   LT(s(z0), s(z1)) -> c4(LT(z0, z1))
   HEAD(cons(z0, z1)) -> c5
   HEAD(nil) -> c6
   TAIL(nil) -> c7
   TAIL(cons(z0, z1)) -> c8
   REVERSE(z0) -> c9(REV(0, z0, nil, z0))
   REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3))
   IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3), TAIL(z1))
   IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3), HEAD(z1))
   IF(false, z0, z1, z2, z3) -> c13
K tuples:none
Defined Rule Symbols:   length_1, lt_2, head_1, tail_1, reverse_1, rev_4, if_5

Defined Pair Symbols:   LENGTH_1, LT_2, HEAD_1, TAIL_1, REVERSE_1, REV_4, IF_5

Compound Symbols:   c, c1_1, c2, c3, c4_1, c5, c6, c7, c8, c9_1, c10_3, c11_2, c12_2, c13


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

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 1 leading nodes:
   REVERSE(z0) -> c9(REV(0, z0, nil, z0))
Removed 8 trailing nodes:
   TAIL(cons(z0, z1)) -> c8
   LT(0, s(z0)) -> c3
   HEAD(cons(z0, z1)) -> c5
   IF(false, z0, z1, z2, z3) -> c13
   HEAD(nil) -> c6
   LT(z0, 0) -> c2
   TAIL(nil) -> c7
   LENGTH(nil) -> c

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))
   lt(z0, 0) -> false
   lt(0, s(z0)) -> true
   lt(s(z0), s(z1)) -> lt(z0, z1)
   head(cons(z0, z1)) -> z0
   head(nil) -> undefined
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   reverse(z0) -> rev(0, z0, nil, z0)
   rev(z0, z1, z2, z3) -> if(lt(z0, length(z3)), z0, z1, z2, z3)
   if(true, z0, z1, z2, z3) -> rev(s(z0), tail(z1), cons(head(z1), z2), z3)
   if(false, z0, z1, z2, z3) -> z2
Tuples:
   LENGTH(cons(z0, z1)) -> c1(LENGTH(z1))
   LT(s(z0), s(z1)) -> c4(LT(z0, z1))
   REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3))
   IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3), TAIL(z1))
   IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3), HEAD(z1))
S tuples:
   LENGTH(cons(z0, z1)) -> c1(LENGTH(z1))
   LT(s(z0), s(z1)) -> c4(LT(z0, z1))
   REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3))
   IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3), TAIL(z1))
   IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3), HEAD(z1))
K tuples:none
Defined Rule Symbols:   length_1, lt_2, head_1, tail_1, reverse_1, rev_4, if_5

Defined Pair Symbols:   LENGTH_1, LT_2, REV_4, IF_5

Compound Symbols:   c1_1, c4_1, c10_3, c11_2, c12_2


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

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))
   lt(z0, 0) -> false
   lt(0, s(z0)) -> true
   lt(s(z0), s(z1)) -> lt(z0, z1)
   head(cons(z0, z1)) -> z0
   head(nil) -> undefined
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   reverse(z0) -> rev(0, z0, nil, z0)
   rev(z0, z1, z2, z3) -> if(lt(z0, length(z3)), z0, z1, z2, z3)
   if(true, z0, z1, z2, z3) -> rev(s(z0), tail(z1), cons(head(z1), z2), z3)
   if(false, z0, z1, z2, z3) -> z2
Tuples:
   LENGTH(cons(z0, z1)) -> c1(LENGTH(z1))
   LT(s(z0), s(z1)) -> c4(LT(z0, z1))
   REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3))
   IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3))
   IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3))
S tuples:
   LENGTH(cons(z0, z1)) -> c1(LENGTH(z1))
   LT(s(z0), s(z1)) -> c4(LT(z0, z1))
   REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3))
   IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3))
   IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3))
K tuples:none
Defined Rule Symbols:   length_1, lt_2, head_1, tail_1, reverse_1, rev_4, if_5

Defined Pair Symbols:   LENGTH_1, LT_2, REV_4, IF_5

Compound Symbols:   c1_1, c4_1, c10_3, c11_1, c12_1


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

(7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   reverse(z0) -> rev(0, z0, nil, z0)
   rev(z0, z1, z2, z3) -> if(lt(z0, length(z3)), z0, z1, z2, z3)
   if(true, z0, z1, z2, z3) -> rev(s(z0), tail(z1), cons(head(z1), z2), z3)
   if(false, z0, z1, z2, z3) -> z2

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   lt(z0, 0) -> false
   lt(0, s(z0)) -> true
   lt(s(z0), s(z1)) -> lt(z0, z1)
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   head(cons(z0, z1)) -> z0
   head(nil) -> undefined
Tuples:
   LENGTH(cons(z0, z1)) -> c1(LENGTH(z1))
   LT(s(z0), s(z1)) -> c4(LT(z0, z1))
   REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3))
   IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3))
   IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3))
S tuples:
   LENGTH(cons(z0, z1)) -> c1(LENGTH(z1))
   LT(s(z0), s(z1)) -> c4(LT(z0, z1))
   REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3))
   IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3))
   IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3))
K tuples:none
Defined Rule Symbols:   lt_2, length_1, tail_1, head_1

Defined Pair Symbols:   LENGTH_1, LT_2, REV_4, IF_5

Compound Symbols:   c1_1, c4_1, c10_3, c11_1, c12_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 CpxRelTRS could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

   LENGTH(cons(z0, z1)) -> c1(LENGTH(z1))
   LT(s(z0), s(z1)) -> c4(LT(z0, z1))
   REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3))
   IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3))
   IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3))

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

   lt(z0, 0) -> false
   lt(0, s(z0)) -> true
   lt(s(z0), s(z1)) -> lt(z0, z1)
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   head(cons(z0, z1)) -> z0
   head(nil) -> undefined

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^2).


The TRS R consists of the following rules:

   LENGTH(cons(z0, z1)) -> c1(LENGTH(z1)) [1]
   LT(s(z0), s(z1)) -> c4(LT(z0, z1)) [1]
   REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3)) [1]
   IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3)) [1]
   IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3)) [1]
   lt(z0, 0) -> false [0]
   lt(0, s(z0)) -> true [0]
   lt(s(z0), s(z1)) -> lt(z0, z1) [0]
   length(nil) -> 0 [0]
   length(cons(z0, z1)) -> s(length(z1)) [0]
   tail(nil) -> nil [0]
   tail(cons(z0, z1)) -> z1 [0]
   head(cons(z0, z1)) -> z0 [0]
   head(nil) -> undefined [0]

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

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

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

   LENGTH(cons(z0, z1)) -> c1(LENGTH(z1)) [1]
   LT(s(z0), s(z1)) -> c4(LT(z0, z1)) [1]
   REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3)) [1]
   IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3)) [1]
   IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3)) [1]
   lt(z0, 0) -> false [0]
   lt(0, s(z0)) -> true [0]
   lt(s(z0), s(z1)) -> lt(z0, z1) [0]
   length(nil) -> 0 [0]
   length(cons(z0, z1)) -> s(length(z1)) [0]
   tail(nil) -> nil [0]
   tail(cons(z0, z1)) -> z1 [0]
   head(cons(z0, z1)) -> z0 [0]
   head(nil) -> undefined [0]

The TRS has the following type information:
LENGTH :: cons:nil -> c1
cons :: undefined -> cons:nil -> cons:nil
c1 :: c1 -> c1
LT :: s:0 -> s:0 -> c4
s :: s:0 -> s:0
c4 :: c4 -> c4
REV :: s:0 -> cons:nil -> cons:nil -> cons:nil -> c10
c10 :: c11:c12 -> c4 -> c1 -> c10
IF :: true:false -> s:0 -> cons:nil -> cons:nil -> cons:nil -> c11:c12
lt :: s:0 -> s:0 -> true:false
length :: cons:nil -> s:0
true :: true:false
c11 :: c10 -> c11:c12
tail :: cons:nil -> cons:nil
head :: cons:nil -> undefined
c12 :: c10 -> c11:c12
0 :: s:0
false :: true:false
nil :: cons:nil
undefined :: undefined

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

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

   lt(v0, v1) -> null_lt [0]
   length(v0) -> null_length [0]
   tail(v0) -> null_tail [0]
   head(v0) -> null_head [0]
   LENGTH(v0) -> null_LENGTH [0]
   LT(v0, v1) -> null_LT [0]
   IF(v0, v1, v2, v3, v4) -> null_IF [0]

And the following fresh constants:    null_lt, null_length, null_tail, null_head, null_LENGTH, null_LT, null_IF, const

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

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

   LENGTH(cons(z0, z1)) -> c1(LENGTH(z1)) [1]
   LT(s(z0), s(z1)) -> c4(LT(z0, z1)) [1]
   REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3)) [1]
   IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3)) [1]
   IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3)) [1]
   lt(z0, 0) -> false [0]
   lt(0, s(z0)) -> true [0]
   lt(s(z0), s(z1)) -> lt(z0, z1) [0]
   length(nil) -> 0 [0]
   length(cons(z0, z1)) -> s(length(z1)) [0]
   tail(nil) -> nil [0]
   tail(cons(z0, z1)) -> z1 [0]
   head(cons(z0, z1)) -> z0 [0]
   head(nil) -> undefined [0]
   lt(v0, v1) -> null_lt [0]
   length(v0) -> null_length [0]
   tail(v0) -> null_tail [0]
   head(v0) -> null_head [0]
   LENGTH(v0) -> null_LENGTH [0]
   LT(v0, v1) -> null_LT [0]
   IF(v0, v1, v2, v3, v4) -> null_IF [0]

The TRS has the following type information:
LENGTH :: cons:nil:null_tail -> c1:null_LENGTH
cons :: undefined:null_head -> cons:nil:null_tail -> cons:nil:null_tail
c1 :: c1:null_LENGTH -> c1:null_LENGTH
LT :: s:0:null_length -> s:0:null_length -> c4:null_LT
s :: s:0:null_length -> s:0:null_length
c4 :: c4:null_LT -> c4:null_LT
REV :: s:0:null_length -> cons:nil:null_tail -> cons:nil:null_tail -> cons:nil:null_tail -> c10
c10 :: c11:c12:null_IF -> c4:null_LT -> c1:null_LENGTH -> c10
IF :: true:false:null_lt -> s:0:null_length -> cons:nil:null_tail -> cons:nil:null_tail -> cons:nil:null_tail -> c11:c12:null_IF
lt :: s:0:null_length -> s:0:null_length -> true:false:null_lt
length :: cons:nil:null_tail -> s:0:null_length
true :: true:false:null_lt
c11 :: c10 -> c11:c12:null_IF
tail :: cons:nil:null_tail -> cons:nil:null_tail
head :: cons:nil:null_tail -> undefined:null_head
c12 :: c10 -> c11:c12:null_IF
0 :: s:0:null_length
false :: true:false:null_lt
nil :: cons:nil:null_tail
undefined :: undefined:null_head
null_lt :: true:false:null_lt
null_length :: s:0:null_length
null_tail :: cons:nil:null_tail
null_head :: undefined:null_head
null_LENGTH :: c1:null_LENGTH
null_LT :: c4:null_LT
null_IF :: c11:c12:null_IF
const :: c10

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

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

   true => 2
   0 => 0
   false => 1
   nil => 0
   undefined => 1
   null_lt => 0
   null_length => 0
   null_tail => 0
   null_head => 0
   null_LENGTH => 0
   null_LT => 0
   null_IF => 0
   const => 0

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

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

   IF(z, z', z'', z4, z5) -{ 0 }-> 0 :|: z5 = v4, v0 >= 0, v4 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z4 = v3, v2 >= 0, v3 >= 0
   IF(z, z', z'', z4, z5) -{ 1 }-> 1 + REV(1 + z0, tail(z1), 1 + head(z1) + z2, z3) :|: z = 2, z1 >= 0, z0 >= 0, z5 = z3, z' = z0, z2 >= 0, z3 >= 0, z'' = z1, z4 = z2
   LENGTH(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   LENGTH(z) -{ 1 }-> 1 + LENGTH(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   LT(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   LT(z, z') -{ 1 }-> 1 + LT(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   REV(z, z', z'', z4) -{ 1 }-> 1 + IF(lt(z0, length(z3)), z0, z1, z2, z3) + LT(z0, length(z3)) + LENGTH(z3) :|: z'' = z2, z = z0, z1 >= 0, z' = z1, z0 >= 0, z4 = z3, z2 >= 0, z3 >= 0
   head(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   head(z) -{ 0 }-> 1 :|: z = 0
   head(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   length(z) -{ 0 }-> 0 :|: z = 0
   length(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   length(z) -{ 0 }-> 1 + length(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   lt(z, z') -{ 0 }-> lt(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   lt(z, z') -{ 0 }-> 2 :|: z0 >= 0, z' = 1 + z0, z = 0
   lt(z, z') -{ 0 }-> 1 :|: z = z0, z0 >= 0, z' = 0
   lt(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   tail(z) -{ 0 }-> z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   tail(z) -{ 0 }-> 0 :|: z = 0
   tail(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0

Only complete derivations are relevant for the runtime complexity.

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

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

eq(start(V, V3, V7, V6, V13),0,[fun(V, Out)],[V >= 0]).
eq(start(V, V3, V7, V6, V13),0,[fun1(V, V3, Out)],[V >= 0,V3 >= 0]).
eq(start(V, V3, V7, V6, V13),0,[fun2(V, V3, V7, V6, Out)],[V >= 0,V3 >= 0,V7 >= 0,V6 >= 0]).
eq(start(V, V3, V7, V6, V13),0,[fun3(V, V3, V7, V6, V13, Out)],[V >= 0,V3 >= 0,V7 >= 0,V6 >= 0,V13 >= 0]).
eq(start(V, V3, V7, V6, V13),0,[lt(V, V3, Out)],[V >= 0,V3 >= 0]).
eq(start(V, V3, V7, V6, V13),0,[length(V, Out)],[V >= 0]).
eq(start(V, V3, V7, V6, V13),0,[tail(V, Out)],[V >= 0]).
eq(start(V, V3, V7, V6, V13),0,[head(V, Out)],[V >= 0]).
eq(fun(V, Out),1,[fun(V1, Ret1)],[Out = 1 + Ret1,V1 >= 0,V2 >= 0,V = 1 + V1 + V2]).
eq(fun1(V, V3, Out),1,[fun1(V5, V4, Ret11)],[Out = 1 + Ret11,V4 >= 0,V = 1 + V5,V5 >= 0,V3 = 1 + V4]).
eq(fun2(V, V3, V7, V6, Out),1,[length(V10, Ret00101),lt(V9, Ret00101, Ret0010),fun3(Ret0010, V9, V8, V11, V10, Ret001),length(V10, Ret011),fun1(V9, Ret011, Ret01),fun(V10, Ret12)],[Out = 1 + Ret001 + Ret01 + Ret12,V7 = V11,V = V9,V8 >= 0,V3 = V8,V9 >= 0,V6 = V10,V11 >= 0,V10 >= 0]).
eq(fun3(V, V3, V7, V6, V13, Out),1,[tail(V15, Ret111),head(V15, Ret1201),fun2(1 + V12, Ret111, 1 + Ret1201 + V14, V16, Ret13)],[Out = 1 + Ret13,V = 2,V15 >= 0,V12 >= 0,V13 = V16,V3 = V12,V14 >= 0,V16 >= 0,V7 = V15,V6 = V14]).
eq(lt(V, V3, Out),0,[],[Out = 1,V = V17,V17 >= 0,V3 = 0]).
eq(lt(V, V3, Out),0,[],[Out = 2,V18 >= 0,V3 = 1 + V18,V = 0]).
eq(lt(V, V3, Out),0,[lt(V20, V19, Ret)],[Out = Ret,V19 >= 0,V = 1 + V20,V20 >= 0,V3 = 1 + V19]).
eq(length(V, Out),0,[],[Out = 0,V = 0]).
eq(length(V, Out),0,[length(V21, Ret14)],[Out = 1 + Ret14,V21 >= 0,V22 >= 0,V = 1 + V21 + V22]).
eq(tail(V, Out),0,[],[Out = 0,V = 0]).
eq(tail(V, Out),0,[],[Out = V23,V23 >= 0,V24 >= 0,V = 1 + V23 + V24]).
eq(head(V, Out),0,[],[Out = V25,V26 >= 0,V25 >= 0,V = 1 + V25 + V26]).
eq(head(V, Out),0,[],[Out = 1,V = 0]).
eq(lt(V, V3, Out),0,[],[Out = 0,V28 >= 0,V27 >= 0,V = V28,V3 = V27]).
eq(length(V, Out),0,[],[Out = 0,V29 >= 0,V = V29]).
eq(tail(V, Out),0,[],[Out = 0,V30 >= 0,V = V30]).
eq(head(V, Out),0,[],[Out = 0,V31 >= 0,V = V31]).
eq(fun(V, Out),0,[],[Out = 0,V32 >= 0,V = V32]).
eq(fun1(V, V3, Out),0,[],[Out = 0,V33 >= 0,V34 >= 0,V = V33,V3 = V34]).
eq(fun3(V, V3, V7, V6, V13, Out),0,[],[Out = 0,V13 = V37,V35 >= 0,V37 >= 0,V7 = V39,V36 >= 0,V = V35,V3 = V36,V6 = V38,V39 >= 0,V38 >= 0]).
input_output_vars(fun(V,Out),[V],[Out]).
input_output_vars(fun1(V,V3,Out),[V,V3],[Out]).
input_output_vars(fun2(V,V3,V7,V6,Out),[V,V3,V7,V6],[Out]).
input_output_vars(fun3(V,V3,V7,V6,V13,Out),[V,V3,V7,V6,V13],[Out]).
input_output_vars(lt(V,V3,Out),[V,V3],[Out]).
input_output_vars(length(V,Out),[V],[Out]).
input_output_vars(tail(V,Out),[V],[Out]).
input_output_vars(head(V,Out),[V],[Out]).


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

#### Computed strongly connected components 
0. recursive  : [fun/2]
1. recursive  : [fun1/3]
2. non_recursive  : [head/2]
3. non_recursive  : [tail/2]
4. recursive  : [length/2]
5. recursive  : [lt/3]
6. recursive [non_tail] : [fun2/5,fun3/6]
7. non_recursive  : [start/5]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into fun/2
1. SCC is partially evaluated into fun1/3
2. SCC is partially evaluated into head/2
3. SCC is partially evaluated into tail/2
4. SCC is partially evaluated into length/2
5. SCC is partially evaluated into lt/3
6. SCC is partially evaluated into fun2/5
7. SCC is partially evaluated into start/5

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

### Specialization of cost equations fun/2 
* CE 18 is refined into CE [27] 
* CE 17 is refined into CE [28] 


### Cost equations --> "Loop" of fun/2 
* CEs [28] --> Loop 19 
* CEs [27] --> Loop 20 

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

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


### Specialization of cost equations fun1/3 
* CE 20 is refined into CE [29] 
* CE 19 is refined into CE [30] 


### Cost equations --> "Loop" of fun1/3 
* CEs [30] --> Loop 21 
* CEs [29] --> Loop 22 

### Ranking functions of CR fun1(V,V3,Out) 
* RF of phase [21]: [V,V3]

#### Partial ranking functions of CR fun1(V,V3,Out) 
* Partial RF of phase [21]:
  - RF of loop [21:1]:
    V
    V3


### Specialization of cost equations head/2 
* CE 12 is refined into CE [31] 
* CE 14 is refined into CE [32] 
* CE 13 is refined into CE [33] 


### Cost equations --> "Loop" of head/2 
* CEs [31] --> Loop 23 
* CEs [32] --> Loop 24 
* CEs [33] --> Loop 25 

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

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


### Specialization of cost equations tail/2 
* CE 11 is refined into CE [34] 
* CE 10 is refined into CE [35] 


### Cost equations --> "Loop" of tail/2 
* CEs [34] --> Loop 26 
* CEs [35] --> Loop 27 

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

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


### Specialization of cost equations length/2 
* CE 25 is refined into CE [36] 
* CE 26 is refined into CE [37] 


### Cost equations --> "Loop" of length/2 
* CEs [37] --> Loop 28 
* CEs [36] --> Loop 29 

### Ranking functions of CR length(V,Out) 
* RF of phase [28]: [V]

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


### Specialization of cost equations lt/3 
* CE 24 is refined into CE [38] 
* CE 21 is refined into CE [39] 
* CE 22 is refined into CE [40] 
* CE 23 is refined into CE [41] 


### Cost equations --> "Loop" of lt/3 
* CEs [41] --> Loop 30 
* CEs [38] --> Loop 31 
* CEs [39] --> Loop 32 
* CEs [40] --> Loop 33 

### Ranking functions of CR lt(V,V3,Out) 
* RF of phase [30]: [V,V3]

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


### Specialization of cost equations fun2/5 
* CE 16 is refined into CE [42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91] 
* CE 15 is refined into CE [92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125] 


### Cost equations --> "Loop" of fun2/5 
* CEs [97,103,113,119,125] --> Loop 34 
* CEs [93,95,96,99,101,102,105,107,109,111,112,115,117,118,121,123,124] --> Loop 35 
* CEs [92,94,98,100,104,106,108,110,114,116,120,122] --> Loop 36 
* CEs [85] --> Loop 37 
* CEs [81,83,84] --> Loop 38 
* CEs [80,82] --> Loop 39 
* CEs [79,91] --> Loop 40 
* CEs [75,77,78,87,89,90] --> Loop 41 
* CEs [74,76,86,88] --> Loop 42 
* CEs [73] --> Loop 43 
* CEs [69,71,72] --> Loop 44 
* CEs [68,70] --> Loop 45 
* CEs [67] --> Loop 46 
* CEs [63,65,66] --> Loop 47 
* CEs [62,64] --> Loop 48 
* CEs [55,57] --> Loop 49 
* CEs [54,56] --> Loop 50 
* CEs [51,53,59,61] --> Loop 51 
* CEs [50,52,58,60] --> Loop 52 
* CEs [47,49] --> Loop 53 
* CEs [46,48] --> Loop 54 
* CEs [43,45] --> Loop 55 
* CEs [42,44] --> Loop 56 

### Ranking functions of CR fun2(V,V3,V7,V6,Out) 
* RF of phase [37,38,39,40,41,42]: [-V+V6,V3]
* RF of phase [43,44,45,46,47,48]: [-V+V6]

#### Partial ranking functions of CR fun2(V,V3,V7,V6,Out) 
* Partial RF of phase [37,38,39,40,41,42]:
  - RF of loop [37:1,38:1,39:1,40:1,41:1,42:1]:
    -V+V6
    V3
* Partial RF of phase [43,44,45,46,47,48]:
  - RF of loop [43:1,44:1,45:1,46:1,47:1,48:1]:
    -V+V6


### Specialization of cost equations start/5 
* CE 1 is refined into CE [126] 
* CE 2 is refined into CE [127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146] 
* CE 3 is refined into CE [147,148] 
* CE 4 is refined into CE [149,150] 
* CE 5 is refined into CE [151,152,153,154,155,156,157,158,159,160] 
* CE 6 is refined into CE [161,162,163,164,165] 
* CE 7 is refined into CE [166,167] 
* CE 8 is refined into CE [168,169] 
* CE 9 is refined into CE [170,171,172] 


### Cost equations --> "Loop" of start/5 
* CEs [162] --> Loop 57 
* CEs [127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146] --> Loop 58 
* CEs [126,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,163,164,165,166,167,168,169,170,171,172] --> Loop 59 

### Ranking functions of CR start(V,V3,V7,V6,V13) 

#### Partial ranking functions of CR start(V,V3,V7,V6,V13) 


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

#### Cost of chains of fun(V,Out):
* Chain [[19],20]: 1*it(19)+0
  Such that:it(19) =< V

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

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


#### Cost of chains of fun1(V,V3,Out):
* Chain [[21],22]: 1*it(21)+0
  Such that:it(21) =< Out

  with precondition: [Out>=1,V>=Out,V3>=Out] 

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


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

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

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


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

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


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

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


#### Cost of chains of lt(V,V3,Out):
* Chain [[30],33]: 0
  with precondition: [Out=2,V>=1,V3>=V+1] 

* Chain [[30],32]: 0
  with precondition: [Out=1,V3>=1,V>=V3] 

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

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

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

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


#### Cost of chains of fun2(V,V3,V7,V6,Out):
* Chain [[43,44,45,46,47,48],36]: 12*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+1
  Such that:aux(13) =< V6
aux(14) =< -V+V6
it(43) =< aux(14)
aux(5) =< aux(13)
aux(7) =< aux(13)+1
s(21) =< it(43)*aux(13)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V>=1,V3>=0,V7>=0,Out>=3,V6>=V+1] 

* Chain [[43,44,45,46,47,48],35]: 12*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+17*s(31)+1
  Such that:aux(16) =< -V+V6
aux(17) =< V6
s(31) =< aux(17)
it(43) =< aux(16)
aux(5) =< aux(17)
aux(7) =< aux(17)+1
s(21) =< it(43)*aux(17)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V>=1,V3>=0,V7>=0,Out>=4,V6>=V+1] 

* Chain [[43,44,45,46,47,48],34]: 12*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+10*s(48)+1
  Such that:aux(23) =< -V+V6
aux(24) =< V6
s(48) =< aux(24)
it(43) =< aux(23)
aux(5) =< aux(24)
aux(7) =< aux(24)+1
s(21) =< it(43)*aux(24)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V>=1,V3>=0,V7>=0,Out>=5,V6>=V+1] 

* Chain [[37,38,39,40,41,42],[43,44,45,46,47,48],36]: 12*it(37)+12*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+1
  Such that:aux(43) =< -V+V6
aux(44) =< V3
aux(45) =< V6
it(43) =< aux(43)
aux(5) =< aux(45)
aux(7) =< aux(45)+1
s(21) =< it(43)*aux(45)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)
it(37) =< aux(43)
it(37) =< aux(44)
s(86) =< it(37)*aux(45)
s(90) =< it(37)*aux(5)
s(93) =< it(37)*aux(7)
s(89) =< it(37)*aux(5)
s(88) =< s(90)

  with precondition: [V>=1,V3>=1,V7>=0,Out>=5,V6>=V+2] 

* Chain [[37,38,39,40,41,42],[43,44,45,46,47,48],35]: 12*it(37)+12*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+17*s(31)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+1
  Such that:aux(46) =< -V+V6
aux(47) =< V3
aux(48) =< V6
s(31) =< aux(48)
it(43) =< aux(46)
aux(5) =< aux(48)
aux(7) =< aux(48)+1
s(21) =< it(43)*aux(48)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)
it(37) =< aux(46)
it(37) =< aux(47)
s(86) =< it(37)*aux(48)
s(90) =< it(37)*aux(5)
s(93) =< it(37)*aux(7)
s(89) =< it(37)*aux(5)
s(88) =< s(90)

  with precondition: [V>=1,V3>=1,V7>=0,Out>=6,V6>=V+2] 

* Chain [[37,38,39,40,41,42],[43,44,45,46,47,48],34]: 12*it(37)+12*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+10*s(48)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+1
  Such that:aux(49) =< -V+V6
aux(50) =< V3
aux(51) =< V6
s(48) =< aux(51)
it(43) =< aux(49)
aux(5) =< aux(51)
aux(7) =< aux(51)+1
s(21) =< it(43)*aux(51)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)
it(37) =< aux(49)
it(37) =< aux(50)
s(86) =< it(37)*aux(51)
s(90) =< it(37)*aux(5)
s(93) =< it(37)*aux(7)
s(89) =< it(37)*aux(5)
s(88) =< s(90)

  with precondition: [V>=1,V3>=1,V7>=0,Out>=7,V6>=V+2] 

* Chain [[37,38,39,40,41,42],36]: 12*it(37)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+1
  Such that:aux(38) =< -V+V6
aux(42) =< V6
aux(52) =< V3
it(37) =< aux(38)
it(37) =< aux(52)
aux(31) =< aux(42)
aux(34) =< aux(42)+1
s(86) =< it(37)*aux(42)
s(90) =< it(37)*aux(31)
s(93) =< it(37)*aux(34)
s(89) =< it(37)*aux(31)
s(88) =< s(90)

  with precondition: [V>=1,V3>=1,V7>=0,Out>=3,V6>=V+1] 

* Chain [[37,38,39,40,41,42],35]: 12*it(37)+16*s(31)+1*s(47)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+1
  Such that:aux(38) =< -V+V6
s(47) =< V+V3
aux(53) =< V3
aux(54) =< V6
s(31) =< aux(54)
it(37) =< aux(38)
it(37) =< aux(53)
aux(31) =< aux(54)
aux(34) =< aux(54)+1
s(86) =< it(37)*aux(54)
s(90) =< it(37)*aux(31)
s(93) =< it(37)*aux(34)
s(89) =< it(37)*aux(31)
s(88) =< s(90)

  with precondition: [V>=1,V3>=1,V7>=0,Out>=4,V6>=V+1] 

* Chain [[37,38,39,40,41,42],34]: 12*it(37)+9*s(48)+1*s(56)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+1
  Such that:aux(38) =< -V+V6
s(56) =< V+V3
aux(55) =< V3
aux(56) =< V6
s(48) =< aux(56)
it(37) =< aux(38)
it(37) =< aux(55)
aux(31) =< aux(56)
aux(34) =< aux(56)+1
s(86) =< it(37)*aux(56)
s(90) =< it(37)*aux(31)
s(93) =< it(37)*aux(34)
s(89) =< it(37)*aux(31)
s(88) =< s(90)

  with precondition: [V>=1,V3>=1,V7>=0,Out>=5,V6>=V+1] 

* Chain [56,[43,44,45,46,47,48],36]: 12*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(57) =< V6
it(43) =< aux(57)
aux(5) =< aux(57)
aux(7) =< aux(57)+1
s(21) =< it(43)*aux(57)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3=0,V7>=0,V6>=2,Out>=5] 

* Chain [56,[43,44,45,46,47,48],35]: 29*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(58) =< V6
it(43) =< aux(58)
aux(5) =< aux(58)
aux(7) =< aux(58)+1
s(21) =< it(43)*aux(58)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3=0,V7>=0,V6>=2,Out>=6] 

* Chain [56,[43,44,45,46,47,48],34]: 22*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(59) =< V6
it(43) =< aux(59)
aux(5) =< aux(59)
aux(7) =< aux(59)+1
s(21) =< it(43)*aux(59)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3=0,V7>=0,V6>=2,Out>=7] 

* Chain [56,36]: 3
  with precondition: [V=0,V3=0,Out=3,V7>=0,V6>=1] 

* Chain [56,35]: 16*s(31)+1*s(47)+3
  Such that:s(47) =< 1
aux(15) =< V6
s(31) =< aux(15)

  with precondition: [V=0,V3=0,V7>=0,Out>=4,V6+3>=Out] 

* Chain [56,34]: 9*s(48)+1*s(56)+3
  Such that:s(56) =< 1
aux(22) =< V6
s(48) =< aux(22)

  with precondition: [V=0,V3=0,V7>=0,Out>=5,V6+4>=Out] 

* Chain [55,[43,44,45,46,47,48],36]: 14*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(61) =< V6
it(43) =< aux(61)
aux(5) =< aux(61)
aux(7) =< aux(61)+1
s(21) =< it(43)*aux(61)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3=0,V7>=0,V6>=2,Out>=6] 

* Chain [55,[43,44,45,46,47,48],35]: 31*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(62) =< V6
it(43) =< aux(62)
aux(5) =< aux(62)
aux(7) =< aux(62)+1
s(21) =< it(43)*aux(62)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3=0,V7>=0,V6>=2,Out>=7] 

* Chain [55,[43,44,45,46,47,48],34]: 24*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(63) =< V6
it(43) =< aux(63)
aux(5) =< aux(63)
aux(7) =< aux(63)+1
s(21) =< it(43)*aux(63)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3=0,V7>=0,V6>=2,Out>=8] 

* Chain [55,36]: 2*s(99)+3
  Such that:aux(60) =< V6
s(99) =< aux(60)

  with precondition: [V=0,V3=0,V7>=0,Out>=4,V6+3>=Out] 

* Chain [55,35]: 18*s(31)+1*s(47)+3
  Such that:s(47) =< 1
aux(64) =< V6
s(31) =< aux(64)

  with precondition: [V=0,V3=0,V7>=0,Out>=5,2*V6+3>=Out] 

* Chain [55,34]: 11*s(48)+1*s(56)+3
  Such that:s(56) =< 1
aux(65) =< V6
s(48) =< aux(65)

  with precondition: [V=0,V3=0,V7>=0,Out>=6,2*V6+4>=Out] 

* Chain [54,[43,44,45,46,47,48],36]: 12*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(66) =< V6
it(43) =< aux(66)
aux(5) =< aux(66)
aux(7) =< aux(66)+1
s(21) =< it(43)*aux(66)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3>=0,V7>=0,V6>=2,Out>=5] 

* Chain [54,[43,44,45,46,47,48],35]: 29*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(67) =< V6
it(43) =< aux(67)
aux(5) =< aux(67)
aux(7) =< aux(67)+1
s(21) =< it(43)*aux(67)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3>=0,V7>=0,V6>=2,Out>=6] 

* Chain [54,[43,44,45,46,47,48],34]: 22*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(68) =< V6
it(43) =< aux(68)
aux(5) =< aux(68)
aux(7) =< aux(68)+1
s(21) =< it(43)*aux(68)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3>=0,V7>=0,V6>=2,Out>=7] 

* Chain [54,36]: 3
  with precondition: [V=0,Out=3,V3>=0,V7>=0,V6>=1] 

* Chain [54,35]: 16*s(31)+1*s(47)+3
  Such that:s(47) =< 1
aux(15) =< V6
s(31) =< aux(15)

  with precondition: [V=0,V3>=0,V7>=0,Out>=4,V6+3>=Out] 

* Chain [54,34]: 9*s(48)+1*s(56)+3
  Such that:s(56) =< 1
aux(22) =< V6
s(48) =< aux(22)

  with precondition: [V=0,V3>=0,V7>=0,Out>=5,V6+4>=Out] 

* Chain [53,[43,44,45,46,47,48],36]: 14*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(70) =< V6
it(43) =< aux(70)
aux(5) =< aux(70)
aux(7) =< aux(70)+1
s(21) =< it(43)*aux(70)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3>=0,V7>=0,V6>=2,Out>=6] 

* Chain [53,[43,44,45,46,47,48],35]: 31*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(71) =< V6
it(43) =< aux(71)
aux(5) =< aux(71)
aux(7) =< aux(71)+1
s(21) =< it(43)*aux(71)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3>=0,V7>=0,V6>=2,Out>=7] 

* Chain [53,[43,44,45,46,47,48],34]: 24*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(72) =< V6
it(43) =< aux(72)
aux(5) =< aux(72)
aux(7) =< aux(72)+1
s(21) =< it(43)*aux(72)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3>=0,V7>=0,V6>=2,Out>=8] 

* Chain [53,36]: 2*s(101)+3
  Such that:aux(69) =< V6
s(101) =< aux(69)

  with precondition: [V=0,V3>=0,V7>=0,Out>=4,V6+3>=Out] 

* Chain [53,35]: 18*s(31)+1*s(47)+3
  Such that:s(47) =< 1
aux(73) =< V6
s(31) =< aux(73)

  with precondition: [V=0,V3>=0,V7>=0,Out>=5,2*V6+3>=Out] 

* Chain [53,34]: 11*s(48)+1*s(56)+3
  Such that:s(56) =< 1
aux(74) =< V6
s(48) =< aux(74)

  with precondition: [V=0,V3>=0,V7>=0,Out>=6,2*V6+4>=Out] 

* Chain [52,[43,44,45,46,47,48],36]: 12*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(75) =< V6
it(43) =< aux(75)
aux(5) =< aux(75)
aux(7) =< aux(75)+1
s(21) =< it(43)*aux(75)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3>=1,V7>=0,V6>=2,Out>=5] 

* Chain [52,[43,44,45,46,47,48],35]: 29*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(76) =< V6
it(43) =< aux(76)
aux(5) =< aux(76)
aux(7) =< aux(76)+1
s(21) =< it(43)*aux(76)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3>=1,V7>=0,V6>=2,Out>=6] 

* Chain [52,[43,44,45,46,47,48],34]: 22*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(77) =< V6
it(43) =< aux(77)
aux(5) =< aux(77)
aux(7) =< aux(77)+1
s(21) =< it(43)*aux(77)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3>=1,V7>=0,V6>=2,Out>=7] 

* Chain [52,[37,38,39,40,41,42],[43,44,45,46,47,48],36]: 12*it(37)+12*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(44) =< V3
aux(78) =< V6
it(43) =< aux(78)
aux(5) =< aux(78)
aux(7) =< aux(78)+1
s(21) =< it(43)*aux(78)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)
it(37) =< aux(78)
it(37) =< aux(44)
s(86) =< it(37)*aux(78)
s(90) =< it(37)*aux(5)
s(93) =< it(37)*aux(7)
s(89) =< it(37)*aux(5)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=3,Out>=7] 

* Chain [52,[37,38,39,40,41,42],[43,44,45,46,47,48],35]: 12*it(37)+29*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(47) =< V3
aux(79) =< V6
it(43) =< aux(79)
aux(5) =< aux(79)
aux(7) =< aux(79)+1
s(21) =< it(43)*aux(79)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)
it(37) =< aux(79)
it(37) =< aux(47)
s(86) =< it(37)*aux(79)
s(90) =< it(37)*aux(5)
s(93) =< it(37)*aux(7)
s(89) =< it(37)*aux(5)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=3,Out>=8] 

* Chain [52,[37,38,39,40,41,42],[43,44,45,46,47,48],34]: 12*it(37)+22*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(50) =< V3
aux(80) =< V6
it(43) =< aux(80)
aux(5) =< aux(80)
aux(7) =< aux(80)+1
s(21) =< it(43)*aux(80)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)
it(37) =< aux(80)
it(37) =< aux(50)
s(86) =< it(37)*aux(80)
s(90) =< it(37)*aux(5)
s(93) =< it(37)*aux(7)
s(89) =< it(37)*aux(5)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=3,Out>=9] 

* Chain [52,[37,38,39,40,41,42],36]: 12*it(37)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(52) =< V3
aux(81) =< V6
it(37) =< aux(81)
it(37) =< aux(52)
aux(31) =< aux(81)
aux(34) =< aux(81)+1
s(86) =< it(37)*aux(81)
s(90) =< it(37)*aux(31)
s(93) =< it(37)*aux(34)
s(89) =< it(37)*aux(31)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=2,Out>=5] 

* Chain [52,[37,38,39,40,41,42],35]: 12*it(37)+16*s(31)+1*s(47)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(82) =< V3
aux(83) =< V6
s(47) =< aux(82)
s(31) =< aux(83)
it(37) =< aux(83)
it(37) =< aux(82)
aux(31) =< aux(83)
aux(34) =< aux(83)+1
s(86) =< it(37)*aux(83)
s(90) =< it(37)*aux(31)
s(93) =< it(37)*aux(34)
s(89) =< it(37)*aux(31)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=2,Out>=6] 

* Chain [52,[37,38,39,40,41,42],34]: 12*it(37)+9*s(48)+1*s(56)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(84) =< V3
aux(85) =< V6
s(56) =< aux(84)
s(48) =< aux(85)
it(37) =< aux(85)
it(37) =< aux(84)
aux(31) =< aux(85)
aux(34) =< aux(85)+1
s(86) =< it(37)*aux(85)
s(90) =< it(37)*aux(31)
s(93) =< it(37)*aux(34)
s(89) =< it(37)*aux(31)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=2,Out>=7] 

* Chain [52,36]: 3
  with precondition: [V=0,Out=3,V3>=1,V7>=0,V6>=1] 

* Chain [52,35]: 16*s(31)+1*s(47)+3
  Such that:s(47) =< 1
aux(15) =< V6
s(31) =< aux(15)

  with precondition: [V=0,V3>=1,V7>=0,Out>=4,V6+3>=Out] 

* Chain [52,34]: 9*s(48)+1*s(56)+3
  Such that:s(56) =< 1
aux(22) =< V6
s(48) =< aux(22)

  with precondition: [V=0,V3>=1,V7>=0,Out>=5,V6+4>=Out] 

* Chain [51,[43,44,45,46,47,48],36]: 16*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(87) =< V6
it(43) =< aux(87)
aux(5) =< aux(87)
aux(7) =< aux(87)+1
s(21) =< it(43)*aux(87)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3>=1,V7>=0,V6>=2,Out>=6] 

* Chain [51,[43,44,45,46,47,48],35]: 33*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(88) =< V6
it(43) =< aux(88)
aux(5) =< aux(88)
aux(7) =< aux(88)+1
s(21) =< it(43)*aux(88)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3>=1,V7>=0,V6>=2,Out>=7] 

* Chain [51,[43,44,45,46,47,48],34]: 26*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(89) =< V6
it(43) =< aux(89)
aux(5) =< aux(89)
aux(7) =< aux(89)+1
s(21) =< it(43)*aux(89)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3>=1,V7>=0,V6>=2,Out>=8] 

* Chain [51,[37,38,39,40,41,42],[43,44,45,46,47,48],36]: 12*it(37)+16*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(44) =< V3
aux(90) =< V6
it(43) =< aux(90)
aux(5) =< aux(90)
aux(7) =< aux(90)+1
s(21) =< it(43)*aux(90)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)
it(37) =< aux(90)
it(37) =< aux(44)
s(86) =< it(37)*aux(90)
s(90) =< it(37)*aux(5)
s(93) =< it(37)*aux(7)
s(89) =< it(37)*aux(5)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=3,Out>=8] 

* Chain [51,[37,38,39,40,41,42],[43,44,45,46,47,48],35]: 12*it(37)+33*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(47) =< V3
aux(91) =< V6
it(43) =< aux(91)
aux(5) =< aux(91)
aux(7) =< aux(91)+1
s(21) =< it(43)*aux(91)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)
it(37) =< aux(91)
it(37) =< aux(47)
s(86) =< it(37)*aux(91)
s(90) =< it(37)*aux(5)
s(93) =< it(37)*aux(7)
s(89) =< it(37)*aux(5)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=3,Out>=9] 

* Chain [51,[37,38,39,40,41,42],[43,44,45,46,47,48],34]: 12*it(37)+26*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(50) =< V3
aux(92) =< V6
it(43) =< aux(92)
aux(5) =< aux(92)
aux(7) =< aux(92)+1
s(21) =< it(43)*aux(92)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)
it(37) =< aux(92)
it(37) =< aux(50)
s(86) =< it(37)*aux(92)
s(90) =< it(37)*aux(5)
s(93) =< it(37)*aux(7)
s(89) =< it(37)*aux(5)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=3,Out>=10] 

* Chain [51,[37,38,39,40,41,42],36]: 12*it(37)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+4*s(103)+3
  Such that:aux(52) =< V3
aux(93) =< V6
it(37) =< aux(93)
it(37) =< aux(52)
aux(31) =< aux(93)
aux(34) =< aux(93)+1
s(86) =< it(37)*aux(93)
s(90) =< it(37)*aux(31)
s(93) =< it(37)*aux(34)
s(89) =< it(37)*aux(31)
s(88) =< s(90)
s(103) =< aux(93)

  with precondition: [V=0,V3>=2,V7>=0,V6>=2,Out>=6] 

* Chain [51,[37,38,39,40,41,42],35]: 12*it(37)+20*s(31)+1*s(47)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(94) =< V3
aux(95) =< V6
s(47) =< aux(94)
s(31) =< aux(95)
it(37) =< aux(95)
it(37) =< aux(94)
aux(31) =< aux(95)
aux(34) =< aux(95)+1
s(86) =< it(37)*aux(95)
s(90) =< it(37)*aux(31)
s(93) =< it(37)*aux(34)
s(89) =< it(37)*aux(31)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=2,Out>=7] 

* Chain [51,[37,38,39,40,41,42],34]: 12*it(37)+13*s(48)+1*s(56)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(96) =< V3
aux(97) =< V6
s(56) =< aux(96)
s(48) =< aux(97)
it(37) =< aux(97)
it(37) =< aux(96)
aux(31) =< aux(97)
aux(34) =< aux(97)+1
s(86) =< it(37)*aux(97)
s(90) =< it(37)*aux(31)
s(93) =< it(37)*aux(34)
s(89) =< it(37)*aux(31)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=2,Out>=8] 

* Chain [51,36]: 4*s(103)+3
  Such that:aux(86) =< V6
s(103) =< aux(86)

  with precondition: [V=0,V3>=1,V7>=0,Out>=4,V6+3>=Out] 

* Chain [51,35]: 20*s(31)+1*s(47)+3
  Such that:s(47) =< 1
aux(98) =< V6
s(31) =< aux(98)

  with precondition: [V=0,V3>=1,V7>=0,Out>=5,2*V6+3>=Out] 

* Chain [51,34]: 13*s(48)+1*s(56)+3
  Such that:s(56) =< 1
aux(99) =< V6
s(48) =< aux(99)

  with precondition: [V=0,V3>=1,V7>=0,Out>=6,2*V6+4>=Out] 

* Chain [50,[43,44,45,46,47,48],36]: 12*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(100) =< V6
it(43) =< aux(100)
aux(5) =< aux(100)
aux(7) =< aux(100)+1
s(21) =< it(43)*aux(100)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3>=1,V7>=0,V6>=2,Out>=5] 

* Chain [50,[43,44,45,46,47,48],35]: 29*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(101) =< V6
it(43) =< aux(101)
aux(5) =< aux(101)
aux(7) =< aux(101)+1
s(21) =< it(43)*aux(101)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3>=1,V7>=0,V6>=2,Out>=6] 

* Chain [50,[43,44,45,46,47,48],34]: 22*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(102) =< V6
it(43) =< aux(102)
aux(5) =< aux(102)
aux(7) =< aux(102)+1
s(21) =< it(43)*aux(102)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3>=1,V7>=0,V6>=2,Out>=7] 

* Chain [50,[37,38,39,40,41,42],[43,44,45,46,47,48],36]: 12*it(37)+12*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(44) =< V3
aux(103) =< V6
it(43) =< aux(103)
aux(5) =< aux(103)
aux(7) =< aux(103)+1
s(21) =< it(43)*aux(103)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)
it(37) =< aux(103)
it(37) =< aux(44)
s(86) =< it(37)*aux(103)
s(90) =< it(37)*aux(5)
s(93) =< it(37)*aux(7)
s(89) =< it(37)*aux(5)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=3,Out>=7] 

* Chain [50,[37,38,39,40,41,42],[43,44,45,46,47,48],35]: 12*it(37)+29*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(47) =< V3
aux(104) =< V6
it(43) =< aux(104)
aux(5) =< aux(104)
aux(7) =< aux(104)+1
s(21) =< it(43)*aux(104)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)
it(37) =< aux(104)
it(37) =< aux(47)
s(86) =< it(37)*aux(104)
s(90) =< it(37)*aux(5)
s(93) =< it(37)*aux(7)
s(89) =< it(37)*aux(5)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=3,Out>=8] 

* Chain [50,[37,38,39,40,41,42],[43,44,45,46,47,48],34]: 12*it(37)+22*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(50) =< V3
aux(105) =< V6
it(43) =< aux(105)
aux(5) =< aux(105)
aux(7) =< aux(105)+1
s(21) =< it(43)*aux(105)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)
it(37) =< aux(105)
it(37) =< aux(50)
s(86) =< it(37)*aux(105)
s(90) =< it(37)*aux(5)
s(93) =< it(37)*aux(7)
s(89) =< it(37)*aux(5)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=3,Out>=9] 

* Chain [50,[37,38,39,40,41,42],36]: 12*it(37)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(52) =< V3
aux(106) =< V6
it(37) =< aux(106)
it(37) =< aux(52)
aux(31) =< aux(106)
aux(34) =< aux(106)+1
s(86) =< it(37)*aux(106)
s(90) =< it(37)*aux(31)
s(93) =< it(37)*aux(34)
s(89) =< it(37)*aux(31)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=2,Out>=5] 

* Chain [50,[37,38,39,40,41,42],35]: 12*it(37)+16*s(31)+1*s(47)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(107) =< V3
aux(108) =< V6
s(47) =< aux(107)
s(31) =< aux(108)
it(37) =< aux(108)
it(37) =< aux(107)
aux(31) =< aux(108)
aux(34) =< aux(108)+1
s(86) =< it(37)*aux(108)
s(90) =< it(37)*aux(31)
s(93) =< it(37)*aux(34)
s(89) =< it(37)*aux(31)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=2,Out>=6] 

* Chain [50,[37,38,39,40,41,42],34]: 12*it(37)+9*s(48)+1*s(56)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(109) =< V3
aux(110) =< V6
s(56) =< aux(109)
s(48) =< aux(110)
it(37) =< aux(110)
it(37) =< aux(109)
aux(31) =< aux(110)
aux(34) =< aux(110)+1
s(86) =< it(37)*aux(110)
s(90) =< it(37)*aux(31)
s(93) =< it(37)*aux(34)
s(89) =< it(37)*aux(31)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=2,Out>=7] 

* Chain [50,36]: 3
  with precondition: [V=0,Out=3,V3>=1,V7>=0,V6>=1] 

* Chain [50,35]: 16*s(31)+1*s(47)+3
  Such that:s(47) =< 1
aux(15) =< V6
s(31) =< aux(15)

  with precondition: [V=0,V3>=1,V7>=0,Out>=4,V6+3>=Out] 

* Chain [50,34]: 9*s(48)+1*s(56)+3
  Such that:s(56) =< 1
aux(22) =< V6
s(48) =< aux(22)

  with precondition: [V=0,V3>=1,V7>=0,Out>=5,V6+4>=Out] 

* Chain [49,[43,44,45,46,47,48],36]: 14*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(112) =< V6
it(43) =< aux(112)
aux(5) =< aux(112)
aux(7) =< aux(112)+1
s(21) =< it(43)*aux(112)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3>=1,V7>=0,V6>=2,Out>=6] 

* Chain [49,[43,44,45,46,47,48],35]: 31*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(113) =< V6
it(43) =< aux(113)
aux(5) =< aux(113)
aux(7) =< aux(113)+1
s(21) =< it(43)*aux(113)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3>=1,V7>=0,V6>=2,Out>=7] 

* Chain [49,[43,44,45,46,47,48],34]: 24*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+3
  Such that:aux(114) =< V6
it(43) =< aux(114)
aux(5) =< aux(114)
aux(7) =< aux(114)+1
s(21) =< it(43)*aux(114)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)

  with precondition: [V=0,V3>=1,V7>=0,V6>=2,Out>=8] 

* Chain [49,[37,38,39,40,41,42],[43,44,45,46,47,48],36]: 12*it(37)+14*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(44) =< V3
aux(115) =< V6
it(43) =< aux(115)
aux(5) =< aux(115)
aux(7) =< aux(115)+1
s(21) =< it(43)*aux(115)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)
it(37) =< aux(115)
it(37) =< aux(44)
s(86) =< it(37)*aux(115)
s(90) =< it(37)*aux(5)
s(93) =< it(37)*aux(7)
s(89) =< it(37)*aux(5)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=3,Out>=8] 

* Chain [49,[37,38,39,40,41,42],[43,44,45,46,47,48],35]: 12*it(37)+31*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(47) =< V3
aux(116) =< V6
it(43) =< aux(116)
aux(5) =< aux(116)
aux(7) =< aux(116)+1
s(21) =< it(43)*aux(116)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)
it(37) =< aux(116)
it(37) =< aux(47)
s(86) =< it(37)*aux(116)
s(90) =< it(37)*aux(5)
s(93) =< it(37)*aux(7)
s(89) =< it(37)*aux(5)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=3,Out>=9] 

* Chain [49,[37,38,39,40,41,42],[43,44,45,46,47,48],34]: 12*it(37)+24*it(43)+2*s(21)+4*s(23)+3*s(24)+1*s(26)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(50) =< V3
aux(117) =< V6
it(43) =< aux(117)
aux(5) =< aux(117)
aux(7) =< aux(117)+1
s(21) =< it(43)*aux(117)
s(25) =< it(43)*aux(5)
s(24) =< it(43)*aux(5)
s(26) =< it(43)*aux(7)
s(23) =< s(25)
it(37) =< aux(117)
it(37) =< aux(50)
s(86) =< it(37)*aux(117)
s(90) =< it(37)*aux(5)
s(93) =< it(37)*aux(7)
s(89) =< it(37)*aux(5)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=3,Out>=10] 

* Chain [49,[37,38,39,40,41,42],36]: 12*it(37)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+2*s(107)+3
  Such that:aux(52) =< V3
aux(118) =< V6
it(37) =< aux(118)
it(37) =< aux(52)
aux(31) =< aux(118)
aux(34) =< aux(118)+1
s(86) =< it(37)*aux(118)
s(90) =< it(37)*aux(31)
s(93) =< it(37)*aux(34)
s(89) =< it(37)*aux(31)
s(88) =< s(90)
s(107) =< aux(118)

  with precondition: [V=0,V3>=2,V7>=0,V6>=2,Out>=6] 

* Chain [49,[37,38,39,40,41,42],35]: 12*it(37)+18*s(31)+1*s(47)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(119) =< V3
aux(120) =< V6
s(47) =< aux(119)
s(31) =< aux(120)
it(37) =< aux(120)
it(37) =< aux(119)
aux(31) =< aux(120)
aux(34) =< aux(120)+1
s(86) =< it(37)*aux(120)
s(90) =< it(37)*aux(31)
s(93) =< it(37)*aux(34)
s(89) =< it(37)*aux(31)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=2,Out>=7] 

* Chain [49,[37,38,39,40,41,42],34]: 12*it(37)+11*s(48)+1*s(56)+2*s(86)+10*s(88)+2*s(89)+1*s(93)+3
  Such that:aux(121) =< V3
aux(122) =< V6
s(56) =< aux(121)
s(48) =< aux(122)
it(37) =< aux(122)
it(37) =< aux(121)
aux(31) =< aux(122)
aux(34) =< aux(122)+1
s(86) =< it(37)*aux(122)
s(90) =< it(37)*aux(31)
s(93) =< it(37)*aux(34)
s(89) =< it(37)*aux(31)
s(88) =< s(90)

  with precondition: [V=0,V3>=2,V7>=0,V6>=2,Out>=8] 

* Chain [49,36]: 2*s(107)+3
  Such that:aux(111) =< V6
s(107) =< aux(111)

  with precondition: [V=0,V3>=1,V7>=0,Out>=4,V6+3>=Out] 

* Chain [49,35]: 18*s(31)+1*s(47)+3
  Such that:s(47) =< 1
aux(123) =< V6
s(31) =< aux(123)

  with precondition: [V=0,V3>=1,V7>=0,Out>=5,2*V6+3>=Out] 

* Chain [49,34]: 11*s(48)+1*s(56)+3
  Such that:s(56) =< 1
aux(124) =< V6
s(48) =< aux(124)

  with precondition: [V=0,V3>=1,V7>=0,Out>=6,2*V6+4>=Out] 

* Chain [36]: 1
  with precondition: [Out=1,V>=0,V3>=0,V7>=0,V6>=0] 

* Chain [35]: 16*s(31)+1*s(47)+1
  Such that:s(47) =< V
aux(15) =< V6
s(31) =< aux(15)

  with precondition: [V>=0,V3>=0,V7>=0,Out>=2,V6+1>=Out] 

* Chain [34]: 9*s(48)+1*s(56)+1
  Such that:s(56) =< V
aux(22) =< V6
s(48) =< aux(22)

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


#### Cost of chains of start(V,V3,V7,V6,V13):
* Chain [59]: 3*s(830)+9*s(831)+1256*s(835)+288*s(836)+48*s(839)+24*s(841)+48*s(842)+240*s(843)+72*s(844)+108*s(846)+36*s(847)+144*s(848)+16*s(851)+2*s(871)+72*s(873)+12*s(876)+6*s(878)+12*s(879)+60*s(880)+72*s(881)+12*s(882)+18*s(884)+6*s(885)+24*s(886)+3
  Such that:s(867) =< -V+V6
s(868) =< V+V3
aux(137) =< 1
aux(138) =< V
aux(139) =< V3
aux(140) =< V6
s(851) =< aux(137)
s(830) =< aux(138)
s(831) =< aux(139)
s(835) =< aux(140)
s(871) =< s(868)
s(873) =< s(867)
s(873) =< aux(139)
s(837) =< aux(140)
s(838) =< aux(140)+1
s(876) =< s(873)*aux(140)
s(877) =< s(873)*s(837)
s(878) =< s(873)*s(838)
s(879) =< s(873)*s(837)
s(880) =< s(877)
s(881) =< s(867)
s(882) =< s(881)*aux(140)
s(883) =< s(881)*s(837)
s(884) =< s(881)*s(837)
s(885) =< s(881)*s(838)
s(886) =< s(883)
s(836) =< aux(140)
s(836) =< aux(139)
s(839) =< s(836)*aux(140)
s(840) =< s(836)*s(837)
s(841) =< s(836)*s(838)
s(842) =< s(836)*s(837)
s(843) =< s(840)
s(844) =< s(835)*aux(140)
s(845) =< s(835)*s(837)
s(846) =< s(835)*s(837)
s(847) =< s(835)*s(838)
s(848) =< s(845)

  with precondition: [V>=0] 

* Chain [58]: 16*s(890)+520*s(892)+360*s(907)+60*s(908)+90*s(910)+30*s(911)+120*s(912)+4*s(975)+144*s(977)+24*s(980)+12*s(982)+24*s(983)+120*s(984)+2
  Such that:aux(141) =< -V3+V13
aux(142) =< V3+1
aux(143) =< V3+V7
aux(144) =< V7
aux(145) =< V13
s(890) =< aux(142)
s(892) =< aux(145)
s(900) =< aux(145)
s(901) =< aux(145)+1
s(907) =< aux(141)
s(908) =< s(907)*aux(145)
s(909) =< s(907)*s(900)
s(910) =< s(907)*s(900)
s(911) =< s(907)*s(901)
s(912) =< s(909)
s(975) =< aux(143)
s(977) =< aux(141)
s(977) =< aux(144)
s(980) =< s(977)*aux(145)
s(981) =< s(977)*s(900)
s(982) =< s(977)*s(901)
s(983) =< s(977)*s(900)
s(984) =< s(981)

  with precondition: [V=2,V3>=0,V7>=0,V6>=0,V13>=0] 

* Chain [57]: 0
  with precondition: [V3=0,V>=0] 


Closed-form bounds of start(V,V3,V7,V6,V13): 
-------------------------------------
* Chain [59] with precondition: [V>=0] 
    - Upper bound: 3*V+19+nat(V3)*9+nat(V6)*1604+nat(V6)*720*nat(V6)+nat(V6)*150*nat(-V+V6)+nat(V+V3)*2+nat(-V+V6)*156 
    - Complexity: n^2 
* Chain [58] with precondition: [V=2,V3>=0,V7>=0,V6>=0,V13>=0] 
    - Upper bound: 520*V13+2+480*V13*nat(-V3+V13)+(4*V3+4*V7)+(16*V3+16)+nat(-V3+V13)*546 
    - Complexity: n^2 
* Chain [57] with precondition: [V3=0,V>=0] 
    - Upper bound: 0 
    - Complexity: constant 

### Maximum cost of start(V,V3,V7,V6,V13): max([nat(V13)*520+2+nat(V13)*480*nat(-V3+V13)+nat(V3+V7)*4+nat(V3+1)*16+nat(-V3+V13)*546,3*V+19+nat(V3)*9+nat(V6)*1604+nat(V6)*720*nat(V6)+nat(V6)*150*nat(-V+V6)+nat(V+V3)*2+nat(-V+V6)*156]) 
Asymptotic class: n^2 
* Total analysis performed in 3818 ms.


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

(20)
BOUNDS(1, n^2)

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

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

(22)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))
   lt(z0, 0) -> false
   lt(0, s(z0)) -> true
   lt(s(z0), s(z1)) -> lt(z0, z1)
   head(cons(z0, z1)) -> z0
   head(nil) -> undefined
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   reverse(z0) -> rev(0, z0, nil, z0)
   rev(z0, z1, z2, z3) -> if(lt(z0, length(z3)), z0, z1, z2, z3)
   if(true, z0, z1, z2, z3) -> rev(s(z0), tail(z1), cons(head(z1), z2), z3)
   if(false, z0, z1, z2, z3) -> z2
Tuples:
   LENGTH(nil) -> c
   LENGTH(cons(z0, z1)) -> c1(LENGTH(z1))
   LT(z0, 0) -> c2
   LT(0, s(z0)) -> c3
   LT(s(z0), s(z1)) -> c4(LT(z0, z1))
   HEAD(cons(z0, z1)) -> c5
   HEAD(nil) -> c6
   TAIL(nil) -> c7
   TAIL(cons(z0, z1)) -> c8
   REVERSE(z0) -> c9(REV(0, z0, nil, z0))
   REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3))
   IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3), TAIL(z1))
   IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3), HEAD(z1))
   IF(false, z0, z1, z2, z3) -> c13
S tuples:
   LENGTH(nil) -> c
   LENGTH(cons(z0, z1)) -> c1(LENGTH(z1))
   LT(z0, 0) -> c2
   LT(0, s(z0)) -> c3
   LT(s(z0), s(z1)) -> c4(LT(z0, z1))
   HEAD(cons(z0, z1)) -> c5
   HEAD(nil) -> c6
   TAIL(nil) -> c7
   TAIL(cons(z0, z1)) -> c8
   REVERSE(z0) -> c9(REV(0, z0, nil, z0))
   REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3))
   IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3), TAIL(z1))
   IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3), HEAD(z1))
   IF(false, z0, z1, z2, z3) -> c13
K tuples:none
Defined Rule Symbols:   length_1, lt_2, head_1, tail_1, reverse_1, rev_4, if_5

Defined Pair Symbols:   LENGTH_1, LT_2, HEAD_1, TAIL_1, REVERSE_1, REV_4, IF_5

Compound Symbols:   c, c1_1, c2, c3, c4_1, c5, c6, c7, c8, c9_1, c10_3, c11_2, c12_2, c13


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

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

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

   LENGTH(nil) -> c
   LENGTH(cons(z0, z1)) -> c1(LENGTH(z1))
   LT(z0, 0) -> c2
   LT(0, s(z0)) -> c3
   LT(s(z0), s(z1)) -> c4(LT(z0, z1))
   HEAD(cons(z0, z1)) -> c5
   HEAD(nil) -> c6
   TAIL(nil) -> c7
   TAIL(cons(z0, z1)) -> c8
   REVERSE(z0) -> c9(REV(0, z0, nil, z0))
   REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3))
   IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3), TAIL(z1))
   IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3), HEAD(z1))
   IF(false, z0, z1, z2, z3) -> c13

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

   length(nil) -> 0
   length(cons(z0, z1)) -> s(length(z1))
   lt(z0, 0) -> false
   lt(0, s(z0)) -> true
   lt(s(z0), s(z1)) -> lt(z0, z1)
   head(cons(z0, z1)) -> z0
   head(nil) -> undefined
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   reverse(z0) -> rev(0, z0, nil, z0)
   rev(z0, z1, z2, z3) -> if(lt(z0, length(z3)), z0, z1, z2, z3)
   if(true, z0, z1, z2, z3) -> rev(s(z0), tail(z1), cons(head(z1), z2), z3)
   if(false, z0, z1, z2, z3) -> z2

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

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

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

   LENGTH(nil) -> c
   LENGTH(cons(z0, z1)) -> c1(LENGTH(z1))
   LT(z0, 0') -> c2
   LT(0', s(z0)) -> c3
   LT(s(z0), s(z1)) -> c4(LT(z0, z1))
   HEAD(cons(z0, z1)) -> c5
   HEAD(nil) -> c6
   TAIL(nil) -> c7
   TAIL(cons(z0, z1)) -> c8
   REVERSE(z0) -> c9(REV(0', z0, nil, z0))
   REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3))
   IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3), TAIL(z1))
   IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3), HEAD(z1))
   IF(false, z0, z1, z2, z3) -> c13

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

   length(nil) -> 0'
   length(cons(z0, z1)) -> s(length(z1))
   lt(z0, 0') -> false
   lt(0', s(z0)) -> true
   lt(s(z0), s(z1)) -> lt(z0, z1)
   head(cons(z0, z1)) -> z0
   head(nil) -> undefined
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   reverse(z0) -> rev(0', z0, nil, z0)
   rev(z0, z1, z2, z3) -> if(lt(z0, length(z3)), z0, z1, z2, z3)
   if(true, z0, z1, z2, z3) -> rev(s(z0), tail(z1), cons(head(z1), z2), z3)
   if(false, z0, z1, z2, z3) -> z2

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

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

(28)
Obligation:
Innermost TRS:
Rules:
LENGTH(nil) -> c
LENGTH(cons(z0, z1)) -> c1(LENGTH(z1))
LT(z0, 0') -> c2
LT(0', s(z0)) -> c3
LT(s(z0), s(z1)) -> c4(LT(z0, z1))
HEAD(cons(z0, z1)) -> c5
HEAD(nil) -> c6
TAIL(nil) -> c7
TAIL(cons(z0, z1)) -> c8
REVERSE(z0) -> c9(REV(0', z0, nil, z0))
REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3))
IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3), TAIL(z1))
IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3), HEAD(z1))
IF(false, z0, z1, z2, z3) -> c13
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
lt(z0, 0') -> false
lt(0', s(z0)) -> true
lt(s(z0), s(z1)) -> lt(z0, z1)
head(cons(z0, z1)) -> z0
head(nil) -> undefined
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
reverse(z0) -> rev(0', z0, nil, z0)
rev(z0, z1, z2, z3) -> if(lt(z0, length(z3)), z0, z1, z2, z3)
if(true, z0, z1, z2, z3) -> rev(s(z0), tail(z1), cons(head(z1), z2), z3)
if(false, z0, z1, z2, z3) -> z2

Types:
LENGTH :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: undefined -> nil:cons -> nil:cons
c1 :: c:c1 -> c:c1
LT :: 0':s -> 0':s -> c2:c3:c4
0' :: 0':s
c2 :: c2:c3:c4
s :: 0':s -> 0':s
c3 :: c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
HEAD :: nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
TAIL :: nil:cons -> c7:c8
c7 :: c7:c8
c8 :: c7:c8
REVERSE :: nil:cons -> c9
c9 :: c10 -> c9
REV :: 0':s -> nil:cons -> nil:cons -> nil:cons -> c10
c10 :: c11:c12:c13 -> c2:c3:c4 -> c:c1 -> c10
IF :: true:false -> 0':s -> nil:cons -> nil:cons -> nil:cons -> c11:c12:c13
lt :: 0':s -> 0':s -> true:false
length :: nil:cons -> 0':s
true :: true:false
c11 :: c10 -> c7:c8 -> c11:c12:c13
tail :: nil:cons -> nil:cons
head :: nil:cons -> undefined
c12 :: c10 -> c5:c6 -> c11:c12:c13
false :: true:false
c13 :: c11:c12:c13
undefined :: undefined
reverse :: nil:cons -> nil:cons
rev :: 0':s -> nil:cons -> nil:cons -> nil:cons -> nil:cons
if :: true:false -> 0':s -> nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_14 :: c:c1
hole_nil:cons2_14 :: nil:cons
hole_undefined3_14 :: undefined
hole_c2:c3:c44_14 :: c2:c3:c4
hole_0':s5_14 :: 0':s
hole_c5:c66_14 :: c5:c6
hole_c7:c87_14 :: c7:c8
hole_c98_14 :: c9
hole_c109_14 :: c10
hole_c11:c12:c1310_14 :: c11:c12:c13
hole_true:false11_14 :: true:false
gen_c:c112_14 :: Nat -> c:c1
gen_nil:cons13_14 :: Nat -> nil:cons
gen_c2:c3:c414_14 :: Nat -> c2:c3:c4
gen_0':s15_14 :: Nat -> 0':s

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

(29) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
LENGTH, LT, REV, lt, length, rev

They will be analysed ascendingly in the following order:
LENGTH < REV
LT < REV
lt < REV
length < REV
lt < rev
length < rev

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

(30)
Obligation:
Innermost TRS:
Rules:
LENGTH(nil) -> c
LENGTH(cons(z0, z1)) -> c1(LENGTH(z1))
LT(z0, 0') -> c2
LT(0', s(z0)) -> c3
LT(s(z0), s(z1)) -> c4(LT(z0, z1))
HEAD(cons(z0, z1)) -> c5
HEAD(nil) -> c6
TAIL(nil) -> c7
TAIL(cons(z0, z1)) -> c8
REVERSE(z0) -> c9(REV(0', z0, nil, z0))
REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3))
IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3), TAIL(z1))
IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3), HEAD(z1))
IF(false, z0, z1, z2, z3) -> c13
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
lt(z0, 0') -> false
lt(0', s(z0)) -> true
lt(s(z0), s(z1)) -> lt(z0, z1)
head(cons(z0, z1)) -> z0
head(nil) -> undefined
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
reverse(z0) -> rev(0', z0, nil, z0)
rev(z0, z1, z2, z3) -> if(lt(z0, length(z3)), z0, z1, z2, z3)
if(true, z0, z1, z2, z3) -> rev(s(z0), tail(z1), cons(head(z1), z2), z3)
if(false, z0, z1, z2, z3) -> z2

Types:
LENGTH :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: undefined -> nil:cons -> nil:cons
c1 :: c:c1 -> c:c1
LT :: 0':s -> 0':s -> c2:c3:c4
0' :: 0':s
c2 :: c2:c3:c4
s :: 0':s -> 0':s
c3 :: c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
HEAD :: nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
TAIL :: nil:cons -> c7:c8
c7 :: c7:c8
c8 :: c7:c8
REVERSE :: nil:cons -> c9
c9 :: c10 -> c9
REV :: 0':s -> nil:cons -> nil:cons -> nil:cons -> c10
c10 :: c11:c12:c13 -> c2:c3:c4 -> c:c1 -> c10
IF :: true:false -> 0':s -> nil:cons -> nil:cons -> nil:cons -> c11:c12:c13
lt :: 0':s -> 0':s -> true:false
length :: nil:cons -> 0':s
true :: true:false
c11 :: c10 -> c7:c8 -> c11:c12:c13
tail :: nil:cons -> nil:cons
head :: nil:cons -> undefined
c12 :: c10 -> c5:c6 -> c11:c12:c13
false :: true:false
c13 :: c11:c12:c13
undefined :: undefined
reverse :: nil:cons -> nil:cons
rev :: 0':s -> nil:cons -> nil:cons -> nil:cons -> nil:cons
if :: true:false -> 0':s -> nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_14 :: c:c1
hole_nil:cons2_14 :: nil:cons
hole_undefined3_14 :: undefined
hole_c2:c3:c44_14 :: c2:c3:c4
hole_0':s5_14 :: 0':s
hole_c5:c66_14 :: c5:c6
hole_c7:c87_14 :: c7:c8
hole_c98_14 :: c9
hole_c109_14 :: c10
hole_c11:c12:c1310_14 :: c11:c12:c13
hole_true:false11_14 :: true:false
gen_c:c112_14 :: Nat -> c:c1
gen_nil:cons13_14 :: Nat -> nil:cons
gen_c2:c3:c414_14 :: Nat -> c2:c3:c4
gen_0':s15_14 :: Nat -> 0':s


Generator Equations:
gen_c:c112_14(0) <=> c
gen_c:c112_14(+(x, 1)) <=> c1(gen_c:c112_14(x))
gen_nil:cons13_14(0) <=> nil
gen_nil:cons13_14(+(x, 1)) <=> cons(undefined, gen_nil:cons13_14(x))
gen_c2:c3:c414_14(0) <=> c2
gen_c2:c3:c414_14(+(x, 1)) <=> c4(gen_c2:c3:c414_14(x))
gen_0':s15_14(0) <=> 0'
gen_0':s15_14(+(x, 1)) <=> s(gen_0':s15_14(x))


The following defined symbols remain to be analysed:
LENGTH, LT, REV, lt, length, rev

They will be analysed ascendingly in the following order:
LENGTH < REV
LT < REV
lt < REV
length < REV
lt < rev
length < rev

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

(31) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LENGTH(gen_nil:cons13_14(n17_14)) -> gen_c:c112_14(n17_14), rt in Omega(1 + n17_14)

Induction Base:
LENGTH(gen_nil:cons13_14(0)) ->_R^Omega(1)
c

Induction Step:
LENGTH(gen_nil:cons13_14(+(n17_14, 1))) ->_R^Omega(1)
c1(LENGTH(gen_nil:cons13_14(n17_14))) ->_IH
c1(gen_c:c112_14(c18_14))

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

(32)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
LENGTH(nil) -> c
LENGTH(cons(z0, z1)) -> c1(LENGTH(z1))
LT(z0, 0') -> c2
LT(0', s(z0)) -> c3
LT(s(z0), s(z1)) -> c4(LT(z0, z1))
HEAD(cons(z0, z1)) -> c5
HEAD(nil) -> c6
TAIL(nil) -> c7
TAIL(cons(z0, z1)) -> c8
REVERSE(z0) -> c9(REV(0', z0, nil, z0))
REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3))
IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3), TAIL(z1))
IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3), HEAD(z1))
IF(false, z0, z1, z2, z3) -> c13
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
lt(z0, 0') -> false
lt(0', s(z0)) -> true
lt(s(z0), s(z1)) -> lt(z0, z1)
head(cons(z0, z1)) -> z0
head(nil) -> undefined
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
reverse(z0) -> rev(0', z0, nil, z0)
rev(z0, z1, z2, z3) -> if(lt(z0, length(z3)), z0, z1, z2, z3)
if(true, z0, z1, z2, z3) -> rev(s(z0), tail(z1), cons(head(z1), z2), z3)
if(false, z0, z1, z2, z3) -> z2

Types:
LENGTH :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: undefined -> nil:cons -> nil:cons
c1 :: c:c1 -> c:c1
LT :: 0':s -> 0':s -> c2:c3:c4
0' :: 0':s
c2 :: c2:c3:c4
s :: 0':s -> 0':s
c3 :: c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
HEAD :: nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
TAIL :: nil:cons -> c7:c8
c7 :: c7:c8
c8 :: c7:c8
REVERSE :: nil:cons -> c9
c9 :: c10 -> c9
REV :: 0':s -> nil:cons -> nil:cons -> nil:cons -> c10
c10 :: c11:c12:c13 -> c2:c3:c4 -> c:c1 -> c10
IF :: true:false -> 0':s -> nil:cons -> nil:cons -> nil:cons -> c11:c12:c13
lt :: 0':s -> 0':s -> true:false
length :: nil:cons -> 0':s
true :: true:false
c11 :: c10 -> c7:c8 -> c11:c12:c13
tail :: nil:cons -> nil:cons
head :: nil:cons -> undefined
c12 :: c10 -> c5:c6 -> c11:c12:c13
false :: true:false
c13 :: c11:c12:c13
undefined :: undefined
reverse :: nil:cons -> nil:cons
rev :: 0':s -> nil:cons -> nil:cons -> nil:cons -> nil:cons
if :: true:false -> 0':s -> nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_14 :: c:c1
hole_nil:cons2_14 :: nil:cons
hole_undefined3_14 :: undefined
hole_c2:c3:c44_14 :: c2:c3:c4
hole_0':s5_14 :: 0':s
hole_c5:c66_14 :: c5:c6
hole_c7:c87_14 :: c7:c8
hole_c98_14 :: c9
hole_c109_14 :: c10
hole_c11:c12:c1310_14 :: c11:c12:c13
hole_true:false11_14 :: true:false
gen_c:c112_14 :: Nat -> c:c1
gen_nil:cons13_14 :: Nat -> nil:cons
gen_c2:c3:c414_14 :: Nat -> c2:c3:c4
gen_0':s15_14 :: Nat -> 0':s


Generator Equations:
gen_c:c112_14(0) <=> c
gen_c:c112_14(+(x, 1)) <=> c1(gen_c:c112_14(x))
gen_nil:cons13_14(0) <=> nil
gen_nil:cons13_14(+(x, 1)) <=> cons(undefined, gen_nil:cons13_14(x))
gen_c2:c3:c414_14(0) <=> c2
gen_c2:c3:c414_14(+(x, 1)) <=> c4(gen_c2:c3:c414_14(x))
gen_0':s15_14(0) <=> 0'
gen_0':s15_14(+(x, 1)) <=> s(gen_0':s15_14(x))


The following defined symbols remain to be analysed:
LENGTH, LT, REV, lt, length, rev

They will be analysed ascendingly in the following order:
LENGTH < REV
LT < REV
lt < REV
length < REV
lt < rev
length < rev

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

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

(35)
BOUNDS(n^1, INF)

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

(36)
Obligation:
Innermost TRS:
Rules:
LENGTH(nil) -> c
LENGTH(cons(z0, z1)) -> c1(LENGTH(z1))
LT(z0, 0') -> c2
LT(0', s(z0)) -> c3
LT(s(z0), s(z1)) -> c4(LT(z0, z1))
HEAD(cons(z0, z1)) -> c5
HEAD(nil) -> c6
TAIL(nil) -> c7
TAIL(cons(z0, z1)) -> c8
REVERSE(z0) -> c9(REV(0', z0, nil, z0))
REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3))
IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3), TAIL(z1))
IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3), HEAD(z1))
IF(false, z0, z1, z2, z3) -> c13
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
lt(z0, 0') -> false
lt(0', s(z0)) -> true
lt(s(z0), s(z1)) -> lt(z0, z1)
head(cons(z0, z1)) -> z0
head(nil) -> undefined
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
reverse(z0) -> rev(0', z0, nil, z0)
rev(z0, z1, z2, z3) -> if(lt(z0, length(z3)), z0, z1, z2, z3)
if(true, z0, z1, z2, z3) -> rev(s(z0), tail(z1), cons(head(z1), z2), z3)
if(false, z0, z1, z2, z3) -> z2

Types:
LENGTH :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: undefined -> nil:cons -> nil:cons
c1 :: c:c1 -> c:c1
LT :: 0':s -> 0':s -> c2:c3:c4
0' :: 0':s
c2 :: c2:c3:c4
s :: 0':s -> 0':s
c3 :: c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
HEAD :: nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
TAIL :: nil:cons -> c7:c8
c7 :: c7:c8
c8 :: c7:c8
REVERSE :: nil:cons -> c9
c9 :: c10 -> c9
REV :: 0':s -> nil:cons -> nil:cons -> nil:cons -> c10
c10 :: c11:c12:c13 -> c2:c3:c4 -> c:c1 -> c10
IF :: true:false -> 0':s -> nil:cons -> nil:cons -> nil:cons -> c11:c12:c13
lt :: 0':s -> 0':s -> true:false
length :: nil:cons -> 0':s
true :: true:false
c11 :: c10 -> c7:c8 -> c11:c12:c13
tail :: nil:cons -> nil:cons
head :: nil:cons -> undefined
c12 :: c10 -> c5:c6 -> c11:c12:c13
false :: true:false
c13 :: c11:c12:c13
undefined :: undefined
reverse :: nil:cons -> nil:cons
rev :: 0':s -> nil:cons -> nil:cons -> nil:cons -> nil:cons
if :: true:false -> 0':s -> nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_14 :: c:c1
hole_nil:cons2_14 :: nil:cons
hole_undefined3_14 :: undefined
hole_c2:c3:c44_14 :: c2:c3:c4
hole_0':s5_14 :: 0':s
hole_c5:c66_14 :: c5:c6
hole_c7:c87_14 :: c7:c8
hole_c98_14 :: c9
hole_c109_14 :: c10
hole_c11:c12:c1310_14 :: c11:c12:c13
hole_true:false11_14 :: true:false
gen_c:c112_14 :: Nat -> c:c1
gen_nil:cons13_14 :: Nat -> nil:cons
gen_c2:c3:c414_14 :: Nat -> c2:c3:c4
gen_0':s15_14 :: Nat -> 0':s


Lemmas:
LENGTH(gen_nil:cons13_14(n17_14)) -> gen_c:c112_14(n17_14), rt in Omega(1 + n17_14)


Generator Equations:
gen_c:c112_14(0) <=> c
gen_c:c112_14(+(x, 1)) <=> c1(gen_c:c112_14(x))
gen_nil:cons13_14(0) <=> nil
gen_nil:cons13_14(+(x, 1)) <=> cons(undefined, gen_nil:cons13_14(x))
gen_c2:c3:c414_14(0) <=> c2
gen_c2:c3:c414_14(+(x, 1)) <=> c4(gen_c2:c3:c414_14(x))
gen_0':s15_14(0) <=> 0'
gen_0':s15_14(+(x, 1)) <=> s(gen_0':s15_14(x))


The following defined symbols remain to be analysed:
LT, REV, lt, length, rev

They will be analysed ascendingly in the following order:
LT < REV
lt < REV
length < REV
lt < rev
length < rev

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

(37) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LT(gen_0':s15_14(n333_14), gen_0':s15_14(n333_14)) -> gen_c2:c3:c414_14(n333_14), rt in Omega(1 + n333_14)

Induction Base:
LT(gen_0':s15_14(0), gen_0':s15_14(0)) ->_R^Omega(1)
c2

Induction Step:
LT(gen_0':s15_14(+(n333_14, 1)), gen_0':s15_14(+(n333_14, 1))) ->_R^Omega(1)
c4(LT(gen_0':s15_14(n333_14), gen_0':s15_14(n333_14))) ->_IH
c4(gen_c2:c3:c414_14(c334_14))

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

(38)
Obligation:
Innermost TRS:
Rules:
LENGTH(nil) -> c
LENGTH(cons(z0, z1)) -> c1(LENGTH(z1))
LT(z0, 0') -> c2
LT(0', s(z0)) -> c3
LT(s(z0), s(z1)) -> c4(LT(z0, z1))
HEAD(cons(z0, z1)) -> c5
HEAD(nil) -> c6
TAIL(nil) -> c7
TAIL(cons(z0, z1)) -> c8
REVERSE(z0) -> c9(REV(0', z0, nil, z0))
REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3))
IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3), TAIL(z1))
IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3), HEAD(z1))
IF(false, z0, z1, z2, z3) -> c13
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
lt(z0, 0') -> false
lt(0', s(z0)) -> true
lt(s(z0), s(z1)) -> lt(z0, z1)
head(cons(z0, z1)) -> z0
head(nil) -> undefined
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
reverse(z0) -> rev(0', z0, nil, z0)
rev(z0, z1, z2, z3) -> if(lt(z0, length(z3)), z0, z1, z2, z3)
if(true, z0, z1, z2, z3) -> rev(s(z0), tail(z1), cons(head(z1), z2), z3)
if(false, z0, z1, z2, z3) -> z2

Types:
LENGTH :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: undefined -> nil:cons -> nil:cons
c1 :: c:c1 -> c:c1
LT :: 0':s -> 0':s -> c2:c3:c4
0' :: 0':s
c2 :: c2:c3:c4
s :: 0':s -> 0':s
c3 :: c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
HEAD :: nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
TAIL :: nil:cons -> c7:c8
c7 :: c7:c8
c8 :: c7:c8
REVERSE :: nil:cons -> c9
c9 :: c10 -> c9
REV :: 0':s -> nil:cons -> nil:cons -> nil:cons -> c10
c10 :: c11:c12:c13 -> c2:c3:c4 -> c:c1 -> c10
IF :: true:false -> 0':s -> nil:cons -> nil:cons -> nil:cons -> c11:c12:c13
lt :: 0':s -> 0':s -> true:false
length :: nil:cons -> 0':s
true :: true:false
c11 :: c10 -> c7:c8 -> c11:c12:c13
tail :: nil:cons -> nil:cons
head :: nil:cons -> undefined
c12 :: c10 -> c5:c6 -> c11:c12:c13
false :: true:false
c13 :: c11:c12:c13
undefined :: undefined
reverse :: nil:cons -> nil:cons
rev :: 0':s -> nil:cons -> nil:cons -> nil:cons -> nil:cons
if :: true:false -> 0':s -> nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_14 :: c:c1
hole_nil:cons2_14 :: nil:cons
hole_undefined3_14 :: undefined
hole_c2:c3:c44_14 :: c2:c3:c4
hole_0':s5_14 :: 0':s
hole_c5:c66_14 :: c5:c6
hole_c7:c87_14 :: c7:c8
hole_c98_14 :: c9
hole_c109_14 :: c10
hole_c11:c12:c1310_14 :: c11:c12:c13
hole_true:false11_14 :: true:false
gen_c:c112_14 :: Nat -> c:c1
gen_nil:cons13_14 :: Nat -> nil:cons
gen_c2:c3:c414_14 :: Nat -> c2:c3:c4
gen_0':s15_14 :: Nat -> 0':s


Lemmas:
LENGTH(gen_nil:cons13_14(n17_14)) -> gen_c:c112_14(n17_14), rt in Omega(1 + n17_14)
LT(gen_0':s15_14(n333_14), gen_0':s15_14(n333_14)) -> gen_c2:c3:c414_14(n333_14), rt in Omega(1 + n333_14)


Generator Equations:
gen_c:c112_14(0) <=> c
gen_c:c112_14(+(x, 1)) <=> c1(gen_c:c112_14(x))
gen_nil:cons13_14(0) <=> nil
gen_nil:cons13_14(+(x, 1)) <=> cons(undefined, gen_nil:cons13_14(x))
gen_c2:c3:c414_14(0) <=> c2
gen_c2:c3:c414_14(+(x, 1)) <=> c4(gen_c2:c3:c414_14(x))
gen_0':s15_14(0) <=> 0'
gen_0':s15_14(+(x, 1)) <=> s(gen_0':s15_14(x))


The following defined symbols remain to be analysed:
lt, REV, length, rev

They will be analysed ascendingly in the following order:
lt < REV
length < REV
lt < rev
length < rev

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

(39) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
lt(gen_0':s15_14(n1014_14), gen_0':s15_14(n1014_14)) -> false, rt in Omega(0)

Induction Base:
lt(gen_0':s15_14(0), gen_0':s15_14(0)) ->_R^Omega(0)
false

Induction Step:
lt(gen_0':s15_14(+(n1014_14, 1)), gen_0':s15_14(+(n1014_14, 1))) ->_R^Omega(0)
lt(gen_0':s15_14(n1014_14), gen_0':s15_14(n1014_14)) ->_IH
false

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

(40)
Obligation:
Innermost TRS:
Rules:
LENGTH(nil) -> c
LENGTH(cons(z0, z1)) -> c1(LENGTH(z1))
LT(z0, 0') -> c2
LT(0', s(z0)) -> c3
LT(s(z0), s(z1)) -> c4(LT(z0, z1))
HEAD(cons(z0, z1)) -> c5
HEAD(nil) -> c6
TAIL(nil) -> c7
TAIL(cons(z0, z1)) -> c8
REVERSE(z0) -> c9(REV(0', z0, nil, z0))
REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3))
IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3), TAIL(z1))
IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3), HEAD(z1))
IF(false, z0, z1, z2, z3) -> c13
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
lt(z0, 0') -> false
lt(0', s(z0)) -> true
lt(s(z0), s(z1)) -> lt(z0, z1)
head(cons(z0, z1)) -> z0
head(nil) -> undefined
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
reverse(z0) -> rev(0', z0, nil, z0)
rev(z0, z1, z2, z3) -> if(lt(z0, length(z3)), z0, z1, z2, z3)
if(true, z0, z1, z2, z3) -> rev(s(z0), tail(z1), cons(head(z1), z2), z3)
if(false, z0, z1, z2, z3) -> z2

Types:
LENGTH :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: undefined -> nil:cons -> nil:cons
c1 :: c:c1 -> c:c1
LT :: 0':s -> 0':s -> c2:c3:c4
0' :: 0':s
c2 :: c2:c3:c4
s :: 0':s -> 0':s
c3 :: c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
HEAD :: nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
TAIL :: nil:cons -> c7:c8
c7 :: c7:c8
c8 :: c7:c8
REVERSE :: nil:cons -> c9
c9 :: c10 -> c9
REV :: 0':s -> nil:cons -> nil:cons -> nil:cons -> c10
c10 :: c11:c12:c13 -> c2:c3:c4 -> c:c1 -> c10
IF :: true:false -> 0':s -> nil:cons -> nil:cons -> nil:cons -> c11:c12:c13
lt :: 0':s -> 0':s -> true:false
length :: nil:cons -> 0':s
true :: true:false
c11 :: c10 -> c7:c8 -> c11:c12:c13
tail :: nil:cons -> nil:cons
head :: nil:cons -> undefined
c12 :: c10 -> c5:c6 -> c11:c12:c13
false :: true:false
c13 :: c11:c12:c13
undefined :: undefined
reverse :: nil:cons -> nil:cons
rev :: 0':s -> nil:cons -> nil:cons -> nil:cons -> nil:cons
if :: true:false -> 0':s -> nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_14 :: c:c1
hole_nil:cons2_14 :: nil:cons
hole_undefined3_14 :: undefined
hole_c2:c3:c44_14 :: c2:c3:c4
hole_0':s5_14 :: 0':s
hole_c5:c66_14 :: c5:c6
hole_c7:c87_14 :: c7:c8
hole_c98_14 :: c9
hole_c109_14 :: c10
hole_c11:c12:c1310_14 :: c11:c12:c13
hole_true:false11_14 :: true:false
gen_c:c112_14 :: Nat -> c:c1
gen_nil:cons13_14 :: Nat -> nil:cons
gen_c2:c3:c414_14 :: Nat -> c2:c3:c4
gen_0':s15_14 :: Nat -> 0':s


Lemmas:
LENGTH(gen_nil:cons13_14(n17_14)) -> gen_c:c112_14(n17_14), rt in Omega(1 + n17_14)
LT(gen_0':s15_14(n333_14), gen_0':s15_14(n333_14)) -> gen_c2:c3:c414_14(n333_14), rt in Omega(1 + n333_14)
lt(gen_0':s15_14(n1014_14), gen_0':s15_14(n1014_14)) -> false, rt in Omega(0)


Generator Equations:
gen_c:c112_14(0) <=> c
gen_c:c112_14(+(x, 1)) <=> c1(gen_c:c112_14(x))
gen_nil:cons13_14(0) <=> nil
gen_nil:cons13_14(+(x, 1)) <=> cons(undefined, gen_nil:cons13_14(x))
gen_c2:c3:c414_14(0) <=> c2
gen_c2:c3:c414_14(+(x, 1)) <=> c4(gen_c2:c3:c414_14(x))
gen_0':s15_14(0) <=> 0'
gen_0':s15_14(+(x, 1)) <=> s(gen_0':s15_14(x))


The following defined symbols remain to be analysed:
length, REV, rev

They will be analysed ascendingly in the following order:
length < REV
length < rev

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

(41) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
length(gen_nil:cons13_14(n1398_14)) -> gen_0':s15_14(n1398_14), rt in Omega(0)

Induction Base:
length(gen_nil:cons13_14(0)) ->_R^Omega(0)
0'

Induction Step:
length(gen_nil:cons13_14(+(n1398_14, 1))) ->_R^Omega(0)
s(length(gen_nil:cons13_14(n1398_14))) ->_IH
s(gen_0':s15_14(c1399_14))

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

(42)
Obligation:
Innermost TRS:
Rules:
LENGTH(nil) -> c
LENGTH(cons(z0, z1)) -> c1(LENGTH(z1))
LT(z0, 0') -> c2
LT(0', s(z0)) -> c3
LT(s(z0), s(z1)) -> c4(LT(z0, z1))
HEAD(cons(z0, z1)) -> c5
HEAD(nil) -> c6
TAIL(nil) -> c7
TAIL(cons(z0, z1)) -> c8
REVERSE(z0) -> c9(REV(0', z0, nil, z0))
REV(z0, z1, z2, z3) -> c10(IF(lt(z0, length(z3)), z0, z1, z2, z3), LT(z0, length(z3)), LENGTH(z3))
IF(true, z0, z1, z2, z3) -> c11(REV(s(z0), tail(z1), cons(head(z1), z2), z3), TAIL(z1))
IF(true, z0, z1, z2, z3) -> c12(REV(s(z0), tail(z1), cons(head(z1), z2), z3), HEAD(z1))
IF(false, z0, z1, z2, z3) -> c13
length(nil) -> 0'
length(cons(z0, z1)) -> s(length(z1))
lt(z0, 0') -> false
lt(0', s(z0)) -> true
lt(s(z0), s(z1)) -> lt(z0, z1)
head(cons(z0, z1)) -> z0
head(nil) -> undefined
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
reverse(z0) -> rev(0', z0, nil, z0)
rev(z0, z1, z2, z3) -> if(lt(z0, length(z3)), z0, z1, z2, z3)
if(true, z0, z1, z2, z3) -> rev(s(z0), tail(z1), cons(head(z1), z2), z3)
if(false, z0, z1, z2, z3) -> z2

Types:
LENGTH :: nil:cons -> c:c1
nil :: nil:cons
c :: c:c1
cons :: undefined -> nil:cons -> nil:cons
c1 :: c:c1 -> c:c1
LT :: 0':s -> 0':s -> c2:c3:c4
0' :: 0':s
c2 :: c2:c3:c4
s :: 0':s -> 0':s
c3 :: c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
HEAD :: nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
TAIL :: nil:cons -> c7:c8
c7 :: c7:c8
c8 :: c7:c8
REVERSE :: nil:cons -> c9
c9 :: c10 -> c9
REV :: 0':s -> nil:cons -> nil:cons -> nil:cons -> c10
c10 :: c11:c12:c13 -> c2:c3:c4 -> c:c1 -> c10
IF :: true:false -> 0':s -> nil:cons -> nil:cons -> nil:cons -> c11:c12:c13
lt :: 0':s -> 0':s -> true:false
length :: nil:cons -> 0':s
true :: true:false
c11 :: c10 -> c7:c8 -> c11:c12:c13
tail :: nil:cons -> nil:cons
head :: nil:cons -> undefined
c12 :: c10 -> c5:c6 -> c11:c12:c13
false :: true:false
c13 :: c11:c12:c13
undefined :: undefined
reverse :: nil:cons -> nil:cons
rev :: 0':s -> nil:cons -> nil:cons -> nil:cons -> nil:cons
if :: true:false -> 0':s -> nil:cons -> nil:cons -> nil:cons -> nil:cons
hole_c:c11_14 :: c:c1
hole_nil:cons2_14 :: nil:cons
hole_undefined3_14 :: undefined
hole_c2:c3:c44_14 :: c2:c3:c4
hole_0':s5_14 :: 0':s
hole_c5:c66_14 :: c5:c6
hole_c7:c87_14 :: c7:c8
hole_c98_14 :: c9
hole_c109_14 :: c10
hole_c11:c12:c1310_14 :: c11:c12:c13
hole_true:false11_14 :: true:false
gen_c:c112_14 :: Nat -> c:c1
gen_nil:cons13_14 :: Nat -> nil:cons
gen_c2:c3:c414_14 :: Nat -> c2:c3:c4
gen_0':s15_14 :: Nat -> 0':s


Lemmas:
LENGTH(gen_nil:cons13_14(n17_14)) -> gen_c:c112_14(n17_14), rt in Omega(1 + n17_14)
LT(gen_0':s15_14(n333_14), gen_0':s15_14(n333_14)) -> gen_c2:c3:c414_14(n333_14), rt in Omega(1 + n333_14)
lt(gen_0':s15_14(n1014_14), gen_0':s15_14(n1014_14)) -> false, rt in Omega(0)
length(gen_nil:cons13_14(n1398_14)) -> gen_0':s15_14(n1398_14), rt in Omega(0)


Generator Equations:
gen_c:c112_14(0) <=> c
gen_c:c112_14(+(x, 1)) <=> c1(gen_c:c112_14(x))
gen_nil:cons13_14(0) <=> nil
gen_nil:cons13_14(+(x, 1)) <=> cons(undefined, gen_nil:cons13_14(x))
gen_c2:c3:c414_14(0) <=> c2
gen_c2:c3:c414_14(+(x, 1)) <=> c4(gen_c2:c3:c414_14(x))
gen_0':s15_14(0) <=> 0'
gen_0':s15_14(+(x, 1)) <=> s(gen_0':s15_14(x))


The following defined symbols remain to be analysed:
REV, rev