(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS sqrt)) (VAR A B C D) (RULES sqrt(A, B, C, D) -> Com_1(f(0, 1, 1, D)) f(A, B, C, D) -> Com_1(f(A + 1, B + 2, C + B + 2, D)) [ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ A + C - 1 >= 0 /\ -A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ D >= C /\ B >= 0 ] f(A, B, C, D) -> Com_1(end(A, B, C, D)) [ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ A + C - 1 >= 0 /\ -A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ C >= D + 1 ] )