Lax Lean Archive

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

Proof of `Checking the output of a configuration graph against a regular language`

groundedproofs/Lax916827Proofs/Results.lean · lax-916827

What this proof establishes

no assumptions

thm✓Lax916827.ConfigurationGraphOutput

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

The representations whose output lies in a regular language form a regular language (Lemma C.2.4), Transducers.twoWayencOutputLangisRegularTransducers.twoWay_encOutputLang_isRegular.

Proof strategy

The concept's language is the inverse image of the source's under the letter-to-letter bijection cletToSrcMcletToSrc M (enctoSrcenc_toSrc, computespathTranscomputes_pathTrans of the bridge), and inverse images under letter-to-letter maps preserve regularity (isRegularmapisRegular_map, the source's continuousmapcontinuous_map).

Attribution

Lemma C.2.4 of Transducers, Part C; formalised by Aristotle (Harmonic), PartC/ConfGraphReg.leanPartC/ConfGraphReg.lean, PartC/ConfGraphRun.leanPartC/ConfGraphRun.lean.