We provide a method, based on automata theory, to mechanically prove the correctness of many numeration systems based on Fibonacci numbers. With it, long case-based and induction-based proofs of correctness can be replaced by simply constructing a regular expression (or finite automaton) specifying the rules for valid representations, followed by a short computation. Examples of the systems that can be handled using our technique include Brown's lazy representation (1965), the far-difference representation developed by Alpert (2009), and three representations proposed by Hajnal (2023). We also provide three additional systems and prove their validity.

翻译：本文提出一种基于自动机理论的通用方法，用于机械证明基于斐波那契数的多种记数系统的正确性。借助该方法，冗长且依赖分情形讨论与归纳法的正确性证明，可简化为两步：首先构建描述有效表示规则的常规表达式（或有限自动机），其次执行简短的计算机验证。本方法可处理的系统示例包括：Brown的惰性表示（1965）、Alpert提出的远差分表示（2009），以及Hajnal提出的三种表示（2023）。此外，我们另提出三种新系统并证明其有效性。