(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS eval_real2_start)) (VAR v_again_0 v_again_1 v_again_2 v_i_0 v_len) (RULES eval_real2_bb5_in(v_again_0, v_again_1, v_again_2, v_i_0, v_len) -> Com_1(eval_real2_bb2_in(v_again_0, v_again_2, v_again_2, v_i_0 + 1, v_len)) [ v_len - 2 >= 0 /\ v_i_0 + v_len - 2 >= 0 /\ -v_i_0 + v_len - 2 >= 0 /\ v_again_2 + v_len - 2 >= 0 /\ -v_again_2 + v_len - 1 >= 0 /\ v_again_1 + v_len - 2 >= 0 /\ -v_again_1 + v_len - 2 >= 0 /\ v_i_0 >= 0 /\ v_again_2 + v_i_0 >= 0 /\ -v_again_2 + v_i_0 + 1 >= 0 /\ v_again_1 + v_i_0 >= 0 /\ -v_again_1 + v_i_0 >= 0 /\ v_again_1 - v_again_2 + 1 >= 0 /\ v_again_2 >= 0 /\ v_again_1 + v_again_2 >= 0 /\ v_again_1 >= 0 ] eval_real2_bb4_in(v_again_0, v_again_1, v_again_2, v_i_0, v_len) -> Com_1(eval_real2_bb5_in(v_again_0, v_again_1, 1, v_i_0, v_len)) [ v_len - 2 >= 0 /\ v_i_0 + v_len - 2 >= 0 /\ -v_i_0 + v_len - 2 >= 0 /\ v_again_1 + v_len - 2 >= 0 /\ -v_again_1 + v_len - 2 >= 0 /\ v_i_0 >= 0 /\ v_again_1 + v_i_0 >= 0 /\ -v_again_1 + v_i_0 >= 0 /\ v_again_1 >= 0 ] eval_real2_bb6_in(v_again_0, v_again_1, v_again_2, v_i_0, v_len) -> Com_1(eval_real2_stop(v_again_0, v_again_1, v_again_2, v_i_0, v_len)) [ -v_again_0 >= 0 /\ v_again_0 >= 0 ] eval_real2_bb1_in(v_again_0, v_again_1, v_again_2, v_i_0, v_len) -> Com_1(eval_real2_bb6_in(v_again_0, v_again_1, v_again_2, v_i_0, v_len)) [ v_again_0 = 0 ] eval_real2_bb3_in(v_again_0, v_again_1, v_again_2, v_i_0, v_len) -> Com_1(eval_real2_bb5_in(v_again_0, v_again_1, v_again_1, v_i_0, v_len)) [ v_len - 2 >= 0 /\ v_i_0 + v_len - 2 >= 0 /\ -v_i_0 + v_len - 2 >= 0 /\ v_again_1 + v_len - 2 >= 0 /\ -v_again_1 + v_len - 2 >= 0 /\ v_i_0 >= 0 /\ v_again_1 + v_i_0 >= 0 /\ -v_again_1 + v_i_0 >= 0 /\ v_again_1 >= 0 /\ nondef_0 <= nondef_1 ] eval_real2_bb3_in(v_again_0, v_again_1, v_again_2, v_i_0, v_len) -> Com_1(eval_real2_bb4_in(v_again_0, v_again_1, v_again_2, v_i_0, v_len)) [ v_len - 2 >= 0 /\ v_i_0 + v_len - 2 >= 0 /\ -v_i_0 + v_len - 2 >= 0 /\ v_again_1 + v_len - 2 >= 0 /\ -v_again_1 + v_len - 2 >= 0 /\ v_i_0 >= 0 /\ v_again_1 + v_i_0 >= 0 /\ -v_again_1 + v_i_0 >= 0 /\ v_again_1 >= 0 /\ nondef_0 > nondef_1 ] eval_real2_bb2_in(v_again_0, v_again_1, v_again_2, v_i_0, v_len) -> Com_1(eval_real2_bb1_in(v_again_1, v_again_1, v_again_2, v_i_0, v_len)) [ v_i_0 >= 0 /\ v_again_1 + v_i_0 >= 0 /\ -v_again_1 + v_i_0 >= 0 /\ v_again_1 >= 0 /\ v_i_0 >= v_len - 1 ] eval_real2_bb2_in(v_again_0, v_again_1, v_again_2, v_i_0, v_len) -> Com_1(eval_real2_bb3_in(v_again_0, v_again_1, v_again_2, v_i_0, v_len)) [ v_i_0 >= 0 /\ v_again_1 + v_i_0 >= 0 /\ -v_again_1 + v_i_0 >= 0 /\ v_again_1 >= 0 /\ v_i_0 < v_len - 1 ] eval_real2_bb1_in(v_again_0, v_again_1, v_again_2, v_i_0, v_len) -> Com_1(eval_real2_bb2_in(v_again_0, 0, v_again_2, 0, v_len)) [ v_again_0 > 0 ] eval_real2_8(v_again_0, v_again_1, v_again_2, v_i_0, v_len) -> Com_1(eval_real2_bb1_in(1, v_again_1, v_again_2, v_i_0, v_len)) eval_real2_7(v_again_0, v_again_1, v_again_2, v_i_0, v_len) -> Com_1(eval_real2_8(v_again_0, v_again_1, v_again_2, v_i_0, v_len)) eval_real2_6(v_again_0, v_again_1, v_again_2, v_i_0, v_len) -> Com_1(eval_real2_7(v_again_0, v_again_1, v_again_2, v_i_0, v_len)) eval_real2_5(v_again_0, v_again_1, v_again_2, v_i_0, v_len) -> Com_1(eval_real2_6(v_again_0, v_again_1, v_again_2, v_i_0, v_len)) eval_real2_4(v_again_0, v_again_1, v_again_2, v_i_0, v_len) -> Com_1(eval_real2_5(v_again_0, v_again_1, v_again_2, v_i_0, v_len)) eval_real2_3(v_again_0, v_again_1, v_again_2, v_i_0, v_len) -> Com_1(eval_real2_4(v_again_0, v_again_1, v_again_2, v_i_0, v_len)) eval_real2_2(v_again_0, v_again_1, v_again_2, v_i_0, v_len) -> Com_1(eval_real2_3(v_again_0, v_again_1, v_again_2, v_i_0, v_len)) eval_real2_1(v_again_0, v_again_1, v_again_2, v_i_0, v_len) -> Com_1(eval_real2_2(v_again_0, v_again_1, v_again_2, v_i_0, v_len)) eval_real2_0(v_again_0, v_again_1, v_again_2, v_i_0, v_len) -> Com_1(eval_real2_1(v_again_0, v_again_1, v_again_2, v_i_0, v_len)) eval_real2_bb0_in(v_again_0, v_again_1, v_again_2, v_i_0, v_len) -> Com_1(eval_real2_0(v_again_0, v_again_1, v_again_2, v_i_0, v_len)) eval_real2_start(v_again_0, v_again_1, v_again_2, v_i_0, v_len) -> Com_1(eval_real2_bb0_in(v_again_0, v_again_1, v_again_2, v_i_0, v_len)) )