Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Proof of `Aperiodic Mealy machines are exactly the compositions of flip-flops`

groundedproofs/Lax765601Proofs/Results.lean · lax-765601

What this proof establishes

thm✓Lax765601.AperiodicMealy

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

In the paper

Description

Theorem A.2.8 as a biconditional, glued from its two halves: the statements FlipFlopsOfAperiodicFlipFlopsOfAperiodic and AperiodicOfFlipFlopsAperiodicOfFlipFlops are its assumptions.