Soundness and exactness of Aho's certified row system

This is the physical-to-semantic direction. Successful finite-control evaluations are decoded into input and work traces, then into semantic padded machine steps. Together with row-system completeness, this yields exact language equality and the positive-input LBA recognizer.

theorem IndexedGrammar.Aho.paddedCompositeStep_of_evalStep_composite {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (old new : List (RowCell g)) (certs : List (RowCert g)) (cert : CompositeCert g) (inputState : InputPhase) (workState : WorkScanState g) (heval : (ahoRowSystem g).evalStep RowState.start old new certs = some (RowState.composite cert inputState workState)) (hdone : rowStepDone (RowState.composite cert inputState workState) = true) : PaddedCompositeStep g old new

A successful physical composite scan decodes to one bounded semantic Aho step.

theorem IndexedGrammar.Aho.paddedRowStep_of_rowStep {T : Type} (g : IndexedGrammar T) [Fintype g.nt] {old new : List (RowCell g)} (h : (ahoRowSystem g).RowStep old new) : PaddedRowStep g old new

Every accepted finite certificate row is one of the intended semantic padded-row edges.

theorem IndexedGrammar.Aho.ahoRowSystem_rowStep_iff_paddedRowStep {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (old new : List (RowCell g)) : (ahoRowSystem g).RowStep old new ↔ PaddedRowStep g old new

Exactness of the physical synchronized checker on a single row transition.

theorem IndexedGrammar.Aho.paddedReachLanguage_of_rowReachLanguage {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) : input ∈ (ahoRowSystem g).rowReachLanguage → input ∈ paddedReachLanguage g

Soundness converse of rowReachLanguage_of_paddedReachLanguage: every accepting physical row-system run decodes to semantic bounded reachability.

theorem IndexedGrammar.Aho.paddedReachLanguage_eq_rowReachLanguage {T : Type} (g : IndexedGrammar T) [Fintype g.nt] : paddedReachLanguage g = (ahoRowSystem g).rowReachLanguage

The executable finite row system recognizes exactly semantic bounded Aho reachability.

theorem IndexedGrammar.Aho.is_LBA_pos_paddedReachLanguage {T : Type} [Fintype T] [DecidableEq T] (g : IndexedGrammar T) [Fintype g.nt] [Fintype g.flag] : is_LBA_pos (paddedReachLanguage g)

Semantic bounded Aho reachability is recognized on exactly the input-sized LBA tape.