(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS eval_realshellsort_start)) (VAR v_0 v_21 v_5 v_array_size v_array_size_sink v_i_0 v_j_0) (RULES eval_realshellsort_start(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_bb0_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0)) eval_realshellsort_bb0_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_0(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0)) eval_realshellsort_0(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_1(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0)) eval_realshellsort_1(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_2(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0)) eval_realshellsort_2(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_3(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0)) eval_realshellsort_3(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_4(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0)) eval_realshellsort_4(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_5(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0)) eval_realshellsort_5(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_6(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0)) eval_realshellsort_6(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_7(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0)) eval_realshellsort_7(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_bb1_in(v_0, v_21, v_5, v_array_size, v_array_size, v_i_0, v_j_0)) eval_realshellsort_bb1_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_bb2_in(nondef_0, v_21, v_5, v_array_size, v_array_size_sink, 0, v_j_0)) [ v_array_size - v_array_size_sink >= 0 /\ v_array_size_sink > 0 /\ nondef_0 >= 0 /\ v_array_size_sink - 2*nondef_0 >= 0 /\ v_array_size_sink - 2*nondef_0 < 2 /\ nondef_0 > 0 ] eval_realshellsort_bb1_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_bb7_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0)) [ v_array_size - v_array_size_sink >= 0 /\ v_array_size_sink = 0 /\ nondef_0 = 0 /\ nondef_0 <= 0 ] eval_realshellsort_bb1_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_bb7_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0)) [ v_array_size - v_array_size_sink >= 0 /\ v_array_size_sink > 0 /\ nondef_0 >= 0 /\ v_array_size_sink - 2*nondef_0 >= 0 /\ v_array_size_sink - 2*nondef_0 < 2 /\ nondef_0 <= 0 ] eval_realshellsort_bb1_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_bb7_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0)) [ v_array_size - v_array_size_sink >= 0 /\ v_array_size_sink < 0 /\ nondef_0 <= 0 /\ -v_array_size_sink + 2*nondef_0 >= 0 /\ -v_array_size_sink + 2*nondef_0 < 2 ] eval_realshellsort_bb2_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_bb3_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0)) [ v_i_0 >= 0 /\ v_array_size_sink + v_i_0 - 2 >= 0 /\ v_array_size + v_i_0 - 2 >= 0 /\ v_0 + v_i_0 - 1 >= 0 /\ v_array_size - v_array_size_sink >= 0 /\ v_array_size_sink - 2 >= 0 /\ v_array_size + v_array_size_sink - 4 >= 0 /\ v_0 + v_array_size_sink - 3 >= 0 /\ -v_0 + v_array_size_sink >= 0 /\ v_array_size - 2 >= 0 /\ v_0 + v_array_size - 3 >= 0 /\ -v_0 + v_array_size >= 0 /\ v_0 - 1 >= 0 /\ v_i_0 < v_array_size ] eval_realshellsort_bb2_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_bb1_in(v_0, v_21, v_5, v_array_size, v_0, v_i_0, v_j_0)) [ v_i_0 >= 0 /\ v_array_size_sink + v_i_0 - 2 >= 0 /\ v_array_size + v_i_0 - 2 >= 0 /\ v_0 + v_i_0 - 1 >= 0 /\ v_array_size - v_array_size_sink >= 0 /\ v_array_size_sink - 2 >= 0 /\ v_array_size + v_array_size_sink - 4 >= 0 /\ v_0 + v_array_size_sink - 3 >= 0 /\ -v_0 + v_array_size_sink >= 0 /\ v_array_size - 2 >= 0 /\ v_0 + v_array_size - 3 >= 0 /\ -v_0 + v_array_size >= 0 /\ v_0 - 1 >= 0 /\ v_i_0 >= v_array_size ] eval_realshellsort_bb3_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_bb4_in(v_0, v_21, nondef_1, v_array_size, v_array_size_sink, v_i_0, v_i_0)) [ v_array_size - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_array_size_sink + v_i_0 - 2 >= 0 /\ v_array_size + v_i_0 - 2 >= 0 /\ v_0 + v_i_0 - 1 >= 0 /\ v_array_size - v_array_size_sink >= 0 /\ v_array_size_sink - 2 >= 0 /\ v_array_size + v_array_size_sink - 4 >= 0 /\ v_0 + v_array_size_sink - 3 >= 0 /\ -v_0 + v_array_size_sink >= 0 /\ v_array_size - 2 >= 0 /\ v_0 + v_array_size - 3 >= 0 /\ -v_0 + v_array_size >= 0 /\ v_0 - 1 >= 0 ] eval_realshellsort_bb4_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_bb5_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0)) [ v_i_0 - v_j_0 >= 0 /\ v_array_size - v_j_0 - 1 >= 0 /\ v_i_0 + v_j_0 >= 0 /\ v_array_size_sink + v_j_0 - 1 >= 0 /\ v_array_size + v_j_0 - 2 >= 0 /\ v_0 + v_j_0 - 1 >= 0 /\ v_array_size - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_array_size_sink + v_i_0 - 2 >= 0 /\ v_array_size + v_i_0 - 2 >= 0 /\ v_0 + v_i_0 - 1 >= 0 /\ v_array_size - v_array_size_sink >= 0 /\ v_array_size_sink - 2 >= 0 /\ v_array_size + v_array_size_sink - 4 >= 0 /\ v_0 + v_array_size_sink - 3 >= 0 /\ -v_0 + v_array_size_sink >= 0 /\ v_array_size - 2 >= 0 /\ v_0 + v_array_size - 3 >= 0 /\ -v_0 + v_array_size >= 0 /\ v_0 - 1 >= 0 /\ v_j_0 >= v_0 ] eval_realshellsort_bb4_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort__critedge_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0)) [ v_i_0 - v_j_0 >= 0 /\ v_array_size - v_j_0 - 1 >= 0 /\ v_i_0 + v_j_0 >= 0 /\ v_array_size_sink + v_j_0 - 1 >= 0 /\ v_array_size + v_j_0 - 2 >= 0 /\ v_0 + v_j_0 - 1 >= 0 /\ v_array_size - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_array_size_sink + v_i_0 - 2 >= 0 /\ v_array_size + v_i_0 - 2 >= 0 /\ v_0 + v_i_0 - 1 >= 0 /\ v_array_size - v_array_size_sink >= 0 /\ v_array_size_sink - 2 >= 0 /\ v_array_size + v_array_size_sink - 4 >= 0 /\ v_0 + v_array_size_sink - 3 >= 0 /\ -v_0 + v_array_size_sink >= 0 /\ v_array_size - 2 >= 0 /\ v_0 + v_array_size - 3 >= 0 /\ -v_0 + v_array_size >= 0 /\ v_0 - 1 >= 0 /\ v_j_0 < v_0 ] eval_realshellsort_bb5_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_bb6_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0)) [ v_i_0 - v_j_0 >= 0 /\ v_array_size - v_j_0 - 1 >= 0 /\ v_j_0 - 1 >= 0 /\ v_i_0 + v_j_0 - 2 >= 0 /\ v_array_size_sink + v_j_0 - 3 >= 0 /\ v_array_size + v_j_0 - 3 >= 0 /\ v_0 + v_j_0 - 2 >= 0 /\ -v_0 + v_j_0 >= 0 /\ v_array_size - v_i_0 - 1 >= 0 /\ v_i_0 - 1 >= 0 /\ v_array_size_sink + v_i_0 - 3 >= 0 /\ v_array_size + v_i_0 - 3 >= 0 /\ v_0 + v_i_0 - 2 >= 0 /\ -v_0 + v_i_0 >= 0 /\ v_array_size - v_array_size_sink >= 0 /\ v_array_size_sink - 2 >= 0 /\ v_array_size + v_array_size_sink - 4 >= 0 /\ v_0 + v_array_size_sink - 3 >= 0 /\ -v_0 + v_array_size_sink >= 0 /\ v_array_size - 2 >= 0 /\ v_0 + v_array_size - 3 >= 0 /\ -v_0 + v_array_size - 1 >= 0 /\ v_0 - 1 >= 0 /\ nondef_2 > v_5 ] eval_realshellsort_bb5_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort__critedge_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0)) [ v_i_0 - v_j_0 >= 0 /\ v_array_size - v_j_0 - 1 >= 0 /\ v_j_0 - 1 >= 0 /\ v_i_0 + v_j_0 - 2 >= 0 /\ v_array_size_sink + v_j_0 - 3 >= 0 /\ v_array_size + v_j_0 - 3 >= 0 /\ v_0 + v_j_0 - 2 >= 0 /\ -v_0 + v_j_0 >= 0 /\ v_array_size - v_i_0 - 1 >= 0 /\ v_i_0 - 1 >= 0 /\ v_array_size_sink + v_i_0 - 3 >= 0 /\ v_array_size + v_i_0 - 3 >= 0 /\ v_0 + v_i_0 - 2 >= 0 /\ -v_0 + v_i_0 >= 0 /\ v_array_size - v_array_size_sink >= 0 /\ v_array_size_sink - 2 >= 0 /\ v_array_size + v_array_size_sink - 4 >= 0 /\ v_0 + v_array_size_sink - 3 >= 0 /\ -v_0 + v_array_size_sink >= 0 /\ v_array_size - 2 >= 0 /\ v_0 + v_array_size - 3 >= 0 /\ -v_0 + v_array_size - 1 >= 0 /\ v_0 - 1 >= 0 /\ nondef_2 <= v_5 ] eval_realshellsort_bb6_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_bb4_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0 - v_0)) [ v_i_0 - v_j_0 >= 0 /\ v_array_size - v_j_0 - 1 >= 0 /\ v_j_0 - 1 >= 0 /\ v_i_0 + v_j_0 - 2 >= 0 /\ v_array_size_sink + v_j_0 - 3 >= 0 /\ v_array_size + v_j_0 - 3 >= 0 /\ v_0 + v_j_0 - 2 >= 0 /\ -v_0 + v_j_0 >= 0 /\ v_array_size - v_i_0 - 1 >= 0 /\ v_i_0 - 1 >= 0 /\ v_array_size_sink + v_i_0 - 3 >= 0 /\ v_array_size + v_i_0 - 3 >= 0 /\ v_0 + v_i_0 - 2 >= 0 /\ -v_0 + v_i_0 >= 0 /\ v_array_size - v_array_size_sink >= 0 /\ v_array_size_sink - 2 >= 0 /\ v_array_size + v_array_size_sink - 4 >= 0 /\ v_0 + v_array_size_sink - 3 >= 0 /\ -v_0 + v_array_size_sink >= 0 /\ v_array_size - 2 >= 0 /\ v_0 + v_array_size - 3 >= 0 /\ -v_0 + v_array_size - 1 >= 0 /\ v_0 - 1 >= 0 ] eval_realshellsort__critedge_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_27(v_0, v_i_0 + 1, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0)) [ v_i_0 - v_j_0 >= 0 /\ v_array_size - v_j_0 - 1 >= 0 /\ v_i_0 + v_j_0 >= 0 /\ v_array_size_sink + v_j_0 - 1 >= 0 /\ v_array_size + v_j_0 - 2 >= 0 /\ v_0 + v_j_0 - 1 >= 0 /\ v_array_size - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_array_size_sink + v_i_0 - 2 >= 0 /\ v_array_size + v_i_0 - 2 >= 0 /\ v_0 + v_i_0 - 1 >= 0 /\ v_array_size - v_array_size_sink >= 0 /\ v_array_size_sink - 2 >= 0 /\ v_array_size + v_array_size_sink - 4 >= 0 /\ v_0 + v_array_size_sink - 3 >= 0 /\ -v_0 + v_array_size_sink >= 0 /\ v_array_size - 2 >= 0 /\ v_0 + v_array_size - 3 >= 0 /\ -v_0 + v_array_size >= 0 /\ v_0 - 1 >= 0 ] eval_realshellsort_27(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_28(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0)) [ v_i_0 - v_j_0 >= 0 /\ v_array_size - v_j_0 - 1 >= 0 /\ v_21 - v_j_0 - 1 >= 0 /\ v_i_0 + v_j_0 >= 0 /\ v_array_size_sink + v_j_0 - 1 >= 0 /\ v_array_size + v_j_0 - 2 >= 0 /\ v_21 + v_j_0 - 1 >= 0 /\ v_0 + v_j_0 - 1 >= 0 /\ v_array_size - v_i_0 - 1 >= 0 /\ v_21 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_array_size_sink + v_i_0 - 2 >= 0 /\ v_array_size + v_i_0 - 2 >= 0 /\ v_21 + v_i_0 - 1 >= 0 /\ -v_21 + v_i_0 + 1 >= 0 /\ v_0 + v_i_0 - 1 >= 0 /\ v_array_size - v_array_size_sink >= 0 /\ v_array_size_sink - 2 >= 0 /\ v_array_size + v_array_size_sink - 4 >= 0 /\ v_21 + v_array_size_sink - 3 >= 0 /\ v_0 + v_array_size_sink - 3 >= 0 /\ -v_0 + v_array_size_sink >= 0 /\ v_array_size - 2 >= 0 /\ v_21 + v_array_size - 3 >= 0 /\ -v_21 + v_array_size >= 0 /\ v_0 + v_array_size - 3 >= 0 /\ -v_0 + v_array_size >= 0 /\ v_21 - 1 >= 0 /\ v_0 + v_21 - 2 >= 0 /\ v_0 - 1 >= 0 ] eval_realshellsort_28(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_bb2_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_21, v_j_0)) [ v_i_0 - v_j_0 >= 0 /\ v_array_size - v_j_0 - 1 >= 0 /\ v_21 - v_j_0 - 1 >= 0 /\ v_i_0 + v_j_0 >= 0 /\ v_array_size_sink + v_j_0 - 1 >= 0 /\ v_array_size + v_j_0 - 2 >= 0 /\ v_21 + v_j_0 - 1 >= 0 /\ v_0 + v_j_0 - 1 >= 0 /\ v_array_size - v_i_0 - 1 >= 0 /\ v_21 - v_i_0 - 1 >= 0 /\ v_i_0 >= 0 /\ v_array_size_sink + v_i_0 - 2 >= 0 /\ v_array_size + v_i_0 - 2 >= 0 /\ v_21 + v_i_0 - 1 >= 0 /\ -v_21 + v_i_0 + 1 >= 0 /\ v_0 + v_i_0 - 1 >= 0 /\ v_array_size - v_array_size_sink >= 0 /\ v_array_size_sink - 2 >= 0 /\ v_array_size + v_array_size_sink - 4 >= 0 /\ v_21 + v_array_size_sink - 3 >= 0 /\ v_0 + v_array_size_sink - 3 >= 0 /\ -v_0 + v_array_size_sink >= 0 /\ v_array_size - 2 >= 0 /\ v_21 + v_array_size - 3 >= 0 /\ -v_21 + v_array_size >= 0 /\ v_0 + v_array_size - 3 >= 0 /\ -v_0 + v_array_size >= 0 /\ v_21 - 1 >= 0 /\ v_0 + v_21 - 2 >= 0 /\ v_0 - 1 >= 0 ] eval_realshellsort_bb7_in(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0) -> Com_1(eval_realshellsort_stop(v_0, v_21, v_5, v_array_size, v_array_size_sink, v_i_0, v_j_0)) [ -v_array_size_sink + 1 >= 0 /\ v_array_size - v_array_size_sink >= 0 ] )