Lax Lean Archive

Proof of `Linearly-finite and recognisable series` (7th statement)

groundedproofs/Lax619925Proofs/Recognisable.lean · lax-619925

What this proof establishes

no assumptions

thm✓Lax619925.Recognisable (7th statement)

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

Description

The transposed representation (k,y,x,MT)(k, y, x, Mᵀ) recognises reversalfreversal f: on a word ww it computes y⋅(M(w.reverse))T⋅xy · (M(w.reverse))ᵀ · x, which equals x⋅M(w.reverse)⋅y=f(w.reverse)x · M(w.reverse) · y = f (w.reverse) by the bilinear-form identity.