# An Example of a Cofinitary Group in Isabelle/HOL

 Title: An Example of a Cofinitary Group in Isabelle/HOL Author: Bart Kastermans Submission date: 2009-08-04 Abstract: We formalize the usual proof that the group generated by the function k -> k + 1 on the integers gives rise to a cofinitary group. BibTeX: @article{CofGroups-AFP, author = {Bart Kastermans}, title = {An Example of a Cofinitary Group in Isabelle/HOL}, journal = {Archive of Formal Proofs}, month = aug, year = 2009, note = {\url{http://isa-afp.org/entries/CofGroups.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License