Padded-row reachability for Aho's machine

This file proves that the semantic padded-row presentation is neither weaker nor stronger than the bounded composite machine. In particular, a path starting at a raw input row can initialize only once. Every later running row uniquely determines both the immutable input word and the complete marked machine configuration.

def IndexedGrammar.Aho.paddedReachLanguage {T : Type} (g : IndexedGrammar T) [Fintype g.nt] : _root_.Language T

The nonempty language accepted by semantic padded-row reachability.

Equations

• One or more equations did not get rendered due to their size.

theorem IndexedGrammar.Aho.inputRow_injective {T : Type} (g : IndexedGrammar T) : Function.Injective (inputRow g)

Raw input rows retain their input word injectively.

theorem IndexedGrammar.Aho.inputRow_ne_encodeRunRow_of_ne_nil {T : Type} (g : IndexedGrammar T) (w : List T) (hw : w ≠ []) (u : List T) (c : Config g) : inputRow g w ≠ encodeRunRow g u c

A nonempty raw input row cannot also be a packed running row.

theorem IndexedGrammar.Aho.initialConfig_within_padded_bound {T : Type} (g : IndexedGrammar T) (w : List T) (hw : w ≠ []) : Config.Within (w.length * workWidth) (initialConfig g)

The initial marked work word fits in the twenty-one-slot block of every nonempty input.

theorem IndexedGrammar.Aho.finalConfig_within_padded_bound {T : Type} (g : IndexedGrammar T) (w : List T) (hw : w ≠ []) : Config.Within (w.length * workWidth) (finalConfig g w.length)

The final marked work word fits in the twenty-one-slot block of every nonempty input.

theorem IndexedGrammar.Aho.mem_paddedReachLanguage_of_boundedReaches {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {w : List T} (hw : w ≠ []) (hreach : BoundedReaches g w (w.length * workWidth) (initialConfig g) (finalConfig g w.length)) : w ∈ paddedReachLanguage g

A bounded accepting composite run gives an accepting semantic padded-row run.

theorem IndexedGrammar.Aho.boundedReaches_of_mem_paddedReachLanguage {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {w : List T} (hmem : w ∈ paddedReachLanguage g) : BoundedReaches g w (w.length * workWidth) (initialConfig g) (finalConfig g w.length)

An accepting semantic padded-row path decodes to a bounded accepting composite run.

theorem IndexedGrammar.Aho.mem_paddedReachLanguage_iff_boundedReaches {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {w : List T} : w ∈ paddedReachLanguage g ↔ w ≠ [] ∧ BoundedReaches g w (w.length * workWidth) (initialConfig g) (finalConfig g w.length)

Semantic padded-row reachability is exactly bounded acceptance by Aho's composite machine.