One-way-liveness proof: Model

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Automata/Model.lean

Module and namespace names, imports, and formatting are adapted to complexitylib. The machine definitions are shared through Models.FiniteAutomaton.Defs.