(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS eval_realheapsort_step2_start))
(VAR v_57 v_N v_j_0 v_k_0 v_m_0)
(RULES
  eval_realheapsort_step2_start(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_bb0_in(v_57, v_N, v_j_0, v_k_0, v_m_0))
  eval_realheapsort_step2_bb0_in(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_0(v_57, v_N, v_j_0, v_k_0, v_m_0))
  eval_realheapsort_step2_0(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_1(v_57, v_N, v_j_0, v_k_0, v_m_0))
  eval_realheapsort_step2_1(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_2(v_57, v_N, v_j_0, v_k_0, v_m_0))
  eval_realheapsort_step2_2(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_bb12_in(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_N <= 2 ]
  eval_realheapsort_step2_2(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_bb1_in(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_N > 2 ]
  eval_realheapsort_step2_bb12_in(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_stop(v_57, v_N, v_j_0, v_k_0, v_m_0))
  eval_realheapsort_step2_bb1_in(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_3(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_N - 3 >= 0 ]
  eval_realheapsort_step2_3(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_4(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_N - 3 >= 0 ]
  eval_realheapsort_step2_4(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_5(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_N - 3 >= 0 ]
  eval_realheapsort_step2_5(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_6(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_N - 3 >= 0 ]
  eval_realheapsort_step2_6(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_7(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_N - 3 >= 0 ]
  eval_realheapsort_step2_7(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_8(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_N - 3 >= 0 ]
  eval_realheapsort_step2_8(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_9(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_N - 3 >= 0 ]
  eval_realheapsort_step2_9(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_10(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_N - 3 >= 0 ]
  eval_realheapsort_step2_10(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_11(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_N - 3 >= 0 ]
  eval_realheapsort_step2_11(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_12(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_N - 3 >= 0 ]
  eval_realheapsort_step2_12(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_bb2_in(v_57, v_N, v_j_0, 0, v_m_0)) [ v_N - 3 >= 0 ]
  eval_realheapsort_step2_bb2_in(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_bb12_in(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_k_0 >= 0 /\ v_N + v_k_0 - 3 >= 0 /\ v_N - 3 >= 0 /\ v_k_0 > v_N - 2 ]
  eval_realheapsort_step2_bb2_in(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_bb3_in(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_k_0 >= 0 /\ v_N + v_k_0 - 3 >= 0 /\ v_N - 3 >= 0 /\ v_k_0 <= v_N - 2 ]
  eval_realheapsort_step2_bb3_in(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_bb4_in(v_57, v_N, 0, v_k_0, v_m_0)) [ v_N - v_k_0 - 2 >= 0 /\ v_k_0 >= 0 /\ v_N + v_k_0 - 3 >= 0 /\ v_N - 3 >= 0 ]
  eval_realheapsort_step2_bb4_in(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_bb11_in(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_k_0 >= 0 /\ v_j_0 + v_k_0 >= 0 /\ v_N + v_k_0 - 3 >= 0 /\ v_j_0 >= 0 /\ v_N + v_j_0 - 3 >= 0 /\ v_N - 3 >= 0 /\ 2*v_j_0 + 1 > v_N - v_k_0 - 2 ]
  eval_realheapsort_step2_bb4_in(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_bb5_in(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_k_0 >= 0 /\ v_j_0 + v_k_0 >= 0 /\ v_N + v_k_0 - 3 >= 0 /\ v_j_0 >= 0 /\ v_N + v_j_0 - 3 >= 0 /\ v_N - 3 >= 0 /\ 2*v_j_0 + 1 <= v_N - v_k_0 - 2 ]
  eval_realheapsort_step2_bb11_in(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_58(v_k_0 + 1, v_N, v_j_0, v_k_0, v_m_0)) [ v_k_0 >= 0 /\ v_j_0 + v_k_0 >= 0 /\ v_N + v_k_0 - 3 >= 0 /\ v_j_0 >= 0 /\ v_N + v_j_0 - 3 >= 0 /\ v_N - 3 >= 0 ]
  eval_realheapsort_step2_bb5_in(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_bb6_in(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_N - v_k_0 - 3 >= 0 /\ v_k_0 >= 0 /\ v_j_0 + v_k_0 >= 0 /\ v_N + v_k_0 - 3 >= 0 /\ v_N - v_j_0 - 3 >= 0 /\ v_j_0 >= 0 /\ v_N + v_j_0 - 3 >= 0 /\ v_N - 3 >= 0 /\ 2*v_j_0 + 1 < v_N - v_k_0 - 2 ]
  eval_realheapsort_step2_bb5_in(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_bb7_in(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_N - v_k_0 - 3 >= 0 /\ v_k_0 >= 0 /\ v_j_0 + v_k_0 >= 0 /\ v_N + v_k_0 - 3 >= 0 /\ v_N - v_j_0 - 3 >= 0 /\ v_j_0 >= 0 /\ v_N + v_j_0 - 3 >= 0 /\ v_N - 3 >= 0 /\ 2*v_j_0 + 1 = v_N - v_k_0 - 2 ]
  eval_realheapsort_step2_58(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_59(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_57 - v_k_0 - 1 >= 0 /\ v_k_0 >= 0 /\ v_j_0 + v_k_0 >= 0 /\ v_N + v_k_0 - 3 >= 0 /\ v_57 + v_k_0 - 1 >= 0 /\ -v_57 + v_k_0 + 1 >= 0 /\ v_j_0 >= 0 /\ v_N + v_j_0 - 3 >= 0 /\ v_57 + v_j_0 - 1 >= 0 /\ v_N - 3 >= 0 /\ v_57 + v_N - 4 >= 0 /\ v_57 - 1 >= 0 ]
  eval_realheapsort_step2_bb6_in(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_bb8_in(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_N - v_k_0 - 4 >= 0 /\ v_k_0 >= 0 /\ v_j_0 + v_k_0 >= 0 /\ v_N + v_k_0 - 4 >= 0 /\ v_N - v_j_0 - 4 >= 0 /\ v_j_0 >= 0 /\ v_N + v_j_0 - 4 >= 0 /\ v_N - 4 >= 0 ]
  eval_realheapsort_step2_bb6_in(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_bb7_in(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_N - v_k_0 - 4 >= 0 /\ v_k_0 >= 0 /\ v_j_0 + v_k_0 >= 0 /\ v_N + v_k_0 - 4 >= 0 /\ v_N - v_j_0 - 4 >= 0 /\ v_j_0 >= 0 /\ v_N + v_j_0 - 4 >= 0 /\ v_N - 4 >= 0 ]
  eval_realheapsort_step2_bb7_in(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_bb9_in(v_57, v_N, v_j_0, v_k_0, 2*v_j_0 + 1)) [ v_N - v_k_0 - 3 >= 0 /\ v_k_0 >= 0 /\ v_j_0 + v_k_0 >= 0 /\ v_N + v_k_0 - 3 >= 0 /\ v_N - v_j_0 - 3 >= 0 /\ v_j_0 >= 0 /\ v_N + v_j_0 - 3 >= 0 /\ v_N - 3 >= 0 ]
  eval_realheapsort_step2_59(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_bb2_in(v_57, v_N, v_j_0, v_57, v_m_0)) [ v_57 - v_k_0 - 1 >= 0 /\ v_k_0 >= 0 /\ v_j_0 + v_k_0 >= 0 /\ v_N + v_k_0 - 3 >= 0 /\ v_57 + v_k_0 - 1 >= 0 /\ -v_57 + v_k_0 + 1 >= 0 /\ v_j_0 >= 0 /\ v_N + v_j_0 - 3 >= 0 /\ v_57 + v_j_0 - 1 >= 0 /\ v_N - 3 >= 0 /\ v_57 + v_N - 4 >= 0 /\ v_57 - 1 >= 0 ]
  eval_realheapsort_step2_bb9_in(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_bb4_in(v_57, v_N, v_N, v_k_0, v_m_0)) [ v_m_0 - 1 >= 0 /\ v_k_0 + v_m_0 - 1 >= 0 /\ v_j_0 + v_m_0 - 1 >= 0 /\ -v_j_0 + v_m_0 - 1 >= 0 /\ v_N + v_m_0 - 4 >= 0 /\ v_N - v_k_0 - 3 >= 0 /\ v_k_0 >= 0 /\ v_j_0 + v_k_0 >= 0 /\ v_N + v_k_0 - 3 >= 0 /\ v_N - v_j_0 - 3 >= 0 /\ v_j_0 >= 0 /\ v_N + v_j_0 - 3 >= 0 /\ v_N - 3 >= 0 ]
  eval_realheapsort_step2_bb9_in(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_bb10_in(v_57, v_N, v_j_0, v_k_0, v_m_0)) [ v_m_0 - 1 >= 0 /\ v_k_0 + v_m_0 - 1 >= 0 /\ v_j_0 + v_m_0 - 1 >= 0 /\ -v_j_0 + v_m_0 - 1 >= 0 /\ v_N + v_m_0 - 4 >= 0 /\ v_N - v_k_0 - 3 >= 0 /\ v_k_0 >= 0 /\ v_j_0 + v_k_0 >= 0 /\ v_N + v_k_0 - 3 >= 0 /\ v_N - v_j_0 - 3 >= 0 /\ v_j_0 >= 0 /\ v_N + v_j_0 - 3 >= 0 /\ v_N - 3 >= 0 ]
  eval_realheapsort_step2_bb8_in(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_bb9_in(v_57, v_N, v_j_0, v_k_0, 2*v_j_0 + 2)) [ v_N - v_k_0 - 4 >= 0 /\ v_k_0 >= 0 /\ v_j_0 + v_k_0 >= 0 /\ v_N + v_k_0 - 4 >= 0 /\ v_N - v_j_0 - 4 >= 0 /\ v_j_0 >= 0 /\ v_N + v_j_0 - 4 >= 0 /\ v_N - 4 >= 0 ]
  eval_realheapsort_step2_bb10_in(v_57, v_N, v_j_0, v_k_0, v_m_0) -> Com_1(eval_realheapsort_step2_bb4_in(v_57, v_N, v_m_0, v_k_0, v_m_0)) [ v_m_0 - 1 >= 0 /\ v_k_0 + v_m_0 - 1 >= 0 /\ v_j_0 + v_m_0 - 1 >= 0 /\ -v_j_0 + v_m_0 - 1 >= 0 /\ v_N + v_m_0 - 4 >= 0 /\ v_N - v_k_0 - 3 >= 0 /\ v_k_0 >= 0 /\ v_j_0 + v_k_0 >= 0 /\ v_N + v_k_0 - 3 >= 0 /\ v_N - v_j_0 - 3 >= 0 /\ v_j_0 >= 0 /\ v_N + v_j_0 - 3 >= 0 /\ v_N - 3 >= 0 ]
)