[Family] Exponential counters

Exponential counters


Exponential counters are machine that seem to be counting in a base > 1.

(need for a better description)


#14,244,805; #10,936,909; #3,840,180


You can write one!

FWIW, I just wrote a blog post outlining a way to hand-prove counters via Induction: BB Counters and Proof by Induction | sligocki

I don’t yet have any proof automation in my system to automatically construct such proofs, but it feels within reach to modify my existing method for proving Meta Rules to one that can prove Inductive Rules.

1 Like

Thank you for sharing, it’s very interesting!