For these functions, a proof that `ceil(f(x))<x`

for `x > 2`

would suffice. You could do one iteration -- to arrive at an integer number, and then proceed by simple induction.

For the general case, probably the best idea is to use well-founded induction to prove this property. However, as Moron pointed out in the comments, this could be impossible in the general case and the right ordering is, in many cases, quite hard to find.

Edit, in reply to Amnon's comment:

If you wanted to use well-founded induction, you would have to define another strict order, that would be well-founded. In case of the functions you mentioned this is not hard: you can take `x << y`

if and only if `ceil(x) < ceil(y)`

, where `<<`

is a symbol for this new order. This order is of course well-founded on numbers greater then 2, and both `sqrt`

and `log`

are decreasing with respect to it -- so you can apply well-founded induction.

Of course, in general case such an order is much more difficult to find. This is also related, in some way, to total correctness assertions in Hoare logic, where you need to guarantee similar obligations on each loop construct.