Three Dollar Quill

Hm. I'm a little further along representing the Josephus problem in marimo and Dafny, but I'm not sure that what I have really constitutes a closed form.

I didn't figure out a way to use the standard library for this, so instead I ended up writing a helper that zeroes out the lower digits. If I can figure out a faster version of that, then I'll be happy, but I think for now I'll move on.

Also, I continue to thank Dafny for just how much math it seems to be able to do.

In any case, I think I managed to read the text closely enough to move onto generalizing it some. Let's see how that goes.

...

Hm.

I'm at the end of the section, and I haven't got code for this last example. Actually representing it looks like a bit much. I need to have d values of beta and d - 1 values of alpha, along with a value for c.

Whatever, I'll figure that part out later. For the moment, I can take a look at the exercises, and go "oh, past me did most of these, so there's really not much to be done here".

But really for the moment, I should get to bed.

Good night.