An Example of a Cofinitary Group in Isabelle/HOL

Bart Kastermans 🌐

August 4, 2009

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We formalize the usual proof that the group generated by the function k -> k + 1 on the integers gives rise to a cofinitary group.


BSD License


Session CofGroups