Proving Properties of $Ï$-Representations with the Walnut Theorem-Prover
For researchers in automata theory and number representations, the paper offers a more efficient proof technique, but the results are incremental.
The paper revisits a theorem on automata for φ-representations, providing a computationally direct proof method that yields simple, induction-free proofs of existing results and new results on φ-representations.
We revisit a classic theorem of Frougny and Sakarovitch concerning automata for $Ï$-representations, and show how to obtain it in a different and more computationally direct way. Using it, we can find simple, induction-free proofs of existing results in the literature about these representations, in a uniform and straightforward manner. In particular, we can easily and "automatically'' recover many of the results of recent papers of Dekking and Van Loon. We also obtain a number of new results on $Ï$-representations.