This is a technical report about a theory named Automata. Automata is an
arithmetic for synchronous circuits. It provides means for representing
and transforming circuit descriptions at the RT level and gate level in a
mathemtical manner. Automata has been implemented in the HOL theorem
proving environment. Preproven theorems are designed for performing
standard synthesis steps such as state encoding, retiming and state
minimization in a mathematical manner via logical derivation.