On Mon, 14 Oct 2024 15:44:20 GMT, fabioromano1 <d...@openjdk.org> wrote:
>> OK, let me give it a try, maybe tomorrow. > > @rgiulietti Or maybe "i.e., 5^(2^i) is larger than the largest power of five > that is still removable from intVal", could it be ok? While I intuitively understand, and I'm convinced of the clever algorithm, I'm struggling to find a proof, in particular to formulate a useful invariant for the first loop which seamlessly would bind with the second loop and its invariant. I need to find more time for this. ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/21323#discussion_r1800684712
