Here comes the README:
To be compiled with Coq 8.4.
Use "make gallinahtml" to generate the short html documentation.
Use "pdflatex report" to generate the pdf of the technical report.
Summary of files:
----------------
- DeltaList: lists of natural numbers with constrained differences
- Fib: Fibonacci sequence and decomposition
- FunG: Hofstadter's G function and tree
- FunG_prog: Alternative definition of Hofstadter's G function
- Phi: Hofstadter G function and the golden ratio
- FlipG: Hofstadter's flipped G tree
References:
----------
- Hofstadter's book: Goedel, Escher, Bach, page 137.
- For G : http://oeis.org/A005206
- For flipped-G : http://oeis.org/A123070
License
-------
The Coq files of this development are released in the Public Domain,
see the LICENSE file in the current directory.
The technical report report.tex is released under the CC-BY 4.0 license,
see http://creativecommons.org/licenses/by/4.0/