Library DeltaList: lists of natural numbers with constrained differences
Library Fib: Fibonacci sequence and decomposition
- Fibonacci sequence
- Decomposition via sums of Fibonacci numbers.
- The sumfib function
- Zeckendorf's Theorem
- Normalisation of a Fibonacci decomposition.
- Classification of Fibonacci decompositions
- Decomposition of the predecessor of a Fibonacci number
- Classification of successor's decomposition
- Classification of predecessor's decomposition
- Two consecutive ThreeOdd numbers are separated by 5 or 8
Library FunG: Hofstadter's G function and tree
- Statement of the G equations as an inductive relation.
- The g function, implementing the G relation.
- Properties of g
- Antecedents by g
- The G tree
- Shape of the G tree
- Another equation about g
- Depth in the G tree
- g and Fibonacci decomposition.
- g and classification of Fibonacci decompositions.
- Fibonacci decomposition and G node arity
- g and "delta" equations
Library FunG_prog: Alternative definition of Hofstadter's G function
Library Phi: Hofstadter G function and the golden ratio
- Phi and tau
- A bit of irrationality theory
- Some complements about integer part and fractional part
- The main theorem
Library FlipG: Hofstadter's flipped G tree
This page has been generated by coqdoc