(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS eval_realselect_start))
(VAR v_2 v_21 v_array_size v_i_0 v_j_0_sink)
(RULES
  eval_realselect_start(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_bb0_in(v_2, v_21, v_array_size, v_i_0, v_j_0_sink))
  eval_realselect_bb0_in(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_0(v_2, v_21, v_array_size, v_i_0, v_j_0_sink))
  eval_realselect_0(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_1(v_2, v_21, v_array_size, v_i_0, v_j_0_sink))
  eval_realselect_1(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_2(v_2, v_21, v_array_size, v_i_0, v_j_0_sink))
  eval_realselect_2(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_3(v_2, v_21, v_array_size, v_i_0, v_j_0_sink))
  eval_realselect_3(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_4(v_2, v_21, v_array_size, v_i_0, v_j_0_sink))
  eval_realselect_4(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_5(v_2, v_21, v_array_size, v_i_0, v_j_0_sink))
  eval_realselect_5(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_6(v_2, v_21, v_array_size, v_i_0, v_j_0_sink))
  eval_realselect_6(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_bb1_in(v_2, v_21, v_array_size, 0, v_j_0_sink))
  eval_realselect_bb1_in(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_bb2_in(v_2, v_21, v_array_size, v_i_0, v_i_0)) [ v_i_0 >= 0 /\ v_i_0 < v_array_size - 1 ]
  eval_realselect_bb1_in(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_bb5_in(v_2, v_21, v_array_size, v_i_0, v_j_0_sink)) [ v_i_0 >= 0 /\ v_i_0 >= v_array_size - 1 ]
  eval_realselect_bb2_in(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_bb3_in(v_j_0_sink + 1, v_21, v_array_size, v_i_0, v_j_0_sink)) [ v_j_0_sink >= 0 /\ v_i_0 + v_j_0_sink >= 0 /\ -v_i_0 + v_j_0_sink >= 0 /\ v_array_size + v_j_0_sink - 2 >= 0 /\ v_array_size - v_i_0 - 2 >= 0 /\ v_i_0 >= 0 /\ v_array_size + v_i_0 - 2 >= 0 /\ v_array_size - 2 >= 0 /\ v_j_0_sink + 1 < v_array_size ]
  eval_realselect_bb2_in(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_bb4_in(v_j_0_sink + 1, v_21, v_array_size, v_i_0, v_j_0_sink)) [ v_j_0_sink >= 0 /\ v_i_0 + v_j_0_sink >= 0 /\ -v_i_0 + v_j_0_sink >= 0 /\ v_array_size + v_j_0_sink - 2 >= 0 /\ v_array_size - v_i_0 - 2 >= 0 /\ v_i_0 >= 0 /\ v_array_size + v_i_0 - 2 >= 0 /\ v_array_size - 2 >= 0 /\ v_j_0_sink + 1 >= v_array_size ]
  eval_realselect_bb3_in(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_bb2_in(v_2, v_21, v_array_size, v_i_0, v_2)) [ v_array_size - v_j_0_sink - 2 >= 0 /\ v_2 - v_j_0_sink - 1 >= 0 /\ v_j_0_sink >= 0 /\ v_i_0 + v_j_0_sink >= 0 /\ -v_i_0 + v_j_0_sink >= 0 /\ v_array_size + v_j_0_sink - 2 >= 0 /\ v_2 + v_j_0_sink - 1 >= 0 /\ -v_2 + v_j_0_sink + 1 >= 0 /\ v_array_size - v_i_0 - 2 >= 0 /\ v_2 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_array_size + v_i_0 - 2 >= 0 /\ v_2 + v_i_0 - 1 >= 0 /\ v_array_size - 2 >= 0 /\ v_2 + v_array_size - 3 >= 0 /\ -v_2 + v_array_size - 1 >= 0 /\ v_2 - 1 >= 0 /\ nondef_0 < nondef_1 ]
  eval_realselect_bb3_in(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_bb2_in(v_2, v_21, v_array_size, v_i_0, v_2)) [ v_array_size - v_j_0_sink - 2 >= 0 /\ v_2 - v_j_0_sink - 1 >= 0 /\ v_j_0_sink >= 0 /\ v_i_0 + v_j_0_sink >= 0 /\ -v_i_0 + v_j_0_sink >= 0 /\ v_array_size + v_j_0_sink - 2 >= 0 /\ v_2 + v_j_0_sink - 1 >= 0 /\ -v_2 + v_j_0_sink + 1 >= 0 /\ v_array_size - v_i_0 - 2 >= 0 /\ v_2 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_array_size + v_i_0 - 2 >= 0 /\ v_2 + v_i_0 - 1 >= 0 /\ v_array_size - 2 >= 0 /\ v_2 + v_array_size - 3 >= 0 /\ -v_2 + v_array_size - 1 >= 0 /\ v_2 - 1 >= 0 /\ nondef_0 >= nondef_1 ]
  eval_realselect_bb4_in(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_19(v_2, v_21, v_array_size, v_i_0, v_j_0_sink)) [ v_2 - v_j_0_sink - 1 >= 0 /\ v_j_0_sink - 1 >= 0 /\ v_i_0 + v_j_0_sink - 1 >= 0 /\ -v_i_0 + v_j_0_sink - 1 >= 0 /\ v_array_size + v_j_0_sink - 3 >= 0 /\ -v_array_size + v_j_0_sink + 1 >= 0 /\ v_2 + v_j_0_sink - 3 >= 0 /\ -v_2 + v_j_0_sink + 1 >= 0 /\ v_array_size - v_i_0 - 2 >= 0 /\ v_2 - v_i_0 - 2 >= 0 /\ v_i_0 >= 0 /\ v_array_size + v_i_0 - 2 >= 0 /\ v_2 + v_i_0 - 2 >= 0 /\ v_2 - v_array_size >= 0 /\ v_array_size - 2 >= 0 /\ v_2 + v_array_size - 4 >= 0 /\ v_2 - 2 >= 0 ]
  eval_realselect_19(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_20(v_2, v_21, v_array_size, v_i_0, v_j_0_sink)) [ v_2 - v_j_0_sink - 1 >= 0 /\ v_j_0_sink - 1 >= 0 /\ v_i_0 + v_j_0_sink - 1 >= 0 /\ -v_i_0 + v_j_0_sink - 1 >= 0 /\ v_array_size + v_j_0_sink - 3 >= 0 /\ -v_array_size + v_j_0_sink + 1 >= 0 /\ v_2 + v_j_0_sink - 3 >= 0 /\ -v_2 + v_j_0_sink + 1 >= 0 /\ v_array_size - v_i_0 - 2 >= 0 /\ v_2 - v_i_0 - 2 >= 0 /\ v_i_0 >= 0 /\ v_array_size + v_i_0 - 2 >= 0 /\ v_2 + v_i_0 - 2 >= 0 /\ v_2 - v_array_size >= 0 /\ v_array_size - 2 >= 0 /\ v_2 + v_array_size - 4 >= 0 /\ v_2 - 2 >= 0 ]
  eval_realselect_20(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_27(v_2, v_i_0 + 1, v_array_size, v_i_0, v_j_0_sink)) [ v_2 - v_j_0_sink - 1 >= 0 /\ v_j_0_sink - 1 >= 0 /\ v_i_0 + v_j_0_sink - 1 >= 0 /\ -v_i_0 + v_j_0_sink - 1 >= 0 /\ v_array_size + v_j_0_sink - 3 >= 0 /\ -v_array_size + v_j_0_sink + 1 >= 0 /\ v_2 + v_j_0_sink - 3 >= 0 /\ -v_2 + v_j_0_sink + 1 >= 0 /\ v_array_size - v_i_0 - 2 >= 0 /\ v_2 - v_i_0 - 2 >= 0 /\ v_i_0 >= 0 /\ v_array_size + v_i_0 - 2 >= 0 /\ v_2 + v_i_0 - 2 >= 0 /\ v_2 - v_array_size >= 0 /\ v_array_size - 2 >= 0 /\ v_2 + v_array_size - 4 >= 0 /\ v_2 - 2 >= 0 ]
  eval_realselect_27(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_28(v_2, v_21, v_array_size, v_i_0, v_j_0_sink)) [ v_2 - v_j_0_sink - 1 >= 0 /\ v_j_0_sink - 1 >= 0 /\ v_i_0 + v_j_0_sink - 1 >= 0 /\ -v_i_0 + v_j_0_sink - 1 >= 0 /\ v_array_size + v_j_0_sink - 3 >= 0 /\ -v_array_size + v_j_0_sink + 1 >= 0 /\ v_21 + v_j_0_sink - 2 >= 0 /\ -v_21 + v_j_0_sink >= 0 /\ v_2 + v_j_0_sink - 3 >= 0 /\ -v_2 + v_j_0_sink + 1 >= 0 /\ v_array_size - v_i_0 - 2 >= 0 /\ v_21 - v_i_0 - 1 >= 0 /\ v_2 - v_i_0 - 2 >= 0 /\ v_i_0 >= 0 /\ v_array_size + v_i_0 - 2 >= 0 /\ v_21 + v_i_0 - 1 >= 0 /\ -v_21 + v_i_0 + 1 >= 0 /\ v_2 + v_i_0 - 2 >= 0 /\ v_2 - v_array_size >= 0 /\ v_array_size - 2 >= 0 /\ v_21 + v_array_size - 3 >= 0 /\ -v_21 + v_array_size - 1 >= 0 /\ v_2 + v_array_size - 4 >= 0 /\ v_2 - v_21 - 1 >= 0 /\ v_21 - 1 >= 0 /\ v_2 + v_21 - 3 >= 0 /\ v_2 - 2 >= 0 ]
  eval_realselect_28(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_bb1_in(v_2, v_21, v_array_size, v_21, v_j_0_sink)) [ v_2 - v_j_0_sink - 1 >= 0 /\ v_j_0_sink - 1 >= 0 /\ v_i_0 + v_j_0_sink - 1 >= 0 /\ -v_i_0 + v_j_0_sink - 1 >= 0 /\ v_array_size + v_j_0_sink - 3 >= 0 /\ -v_array_size + v_j_0_sink + 1 >= 0 /\ v_21 + v_j_0_sink - 2 >= 0 /\ -v_21 + v_j_0_sink >= 0 /\ v_2 + v_j_0_sink - 3 >= 0 /\ -v_2 + v_j_0_sink + 1 >= 0 /\ v_array_size - v_i_0 - 2 >= 0 /\ v_21 - v_i_0 - 1 >= 0 /\ v_2 - v_i_0 - 2 >= 0 /\ v_i_0 >= 0 /\ v_array_size + v_i_0 - 2 >= 0 /\ v_21 + v_i_0 - 1 >= 0 /\ -v_21 + v_i_0 + 1 >= 0 /\ v_2 + v_i_0 - 2 >= 0 /\ v_2 - v_array_size >= 0 /\ v_array_size - 2 >= 0 /\ v_21 + v_array_size - 3 >= 0 /\ -v_21 + v_array_size - 1 >= 0 /\ v_2 + v_array_size - 4 >= 0 /\ v_2 - v_21 - 1 >= 0 /\ v_21 - 1 >= 0 /\ v_2 + v_21 - 3 >= 0 /\ v_2 - 2 >= 0 ]
  eval_realselect_bb5_in(v_2, v_21, v_array_size, v_i_0, v_j_0_sink) -> Com_1(eval_realselect_stop(v_2, v_21, v_array_size, v_i_0, v_j_0_sink)) [ v_i_0 >= 0 /\ -v_array_size + v_i_0 + 1 >= 0 ]
)