Aaron Jacobs on Nostr: nprofile1q…6gyrf Thanks, this is a much more elegant way to put it. I think my same ...

nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqf3nlrmpjja65pzmvlegyl27l0y2m007nncxttdwqndrejajvdzask6gyrf (nprofile…gyrf) Thanks, this is a much more elegant way to put it. I think my same concern about termination applies, but I guess it’s a dumb concern: to prove the function correct it’s sufficient to prove the things you mentioned and separately that the loop terminates. (In this case: fewer bits are set in each iteration.)

Thanks for the references! I never studied any of this stuff formally.