A one-factor shrinking theorem for indexed languages

This is the m = 1 form of Gilman's shrinking theorem. A long generated word contains one critical scope. Its ordered nonempty factors have bounded length, and after any one factor is distinguished a proper retained subproduct can replace that scope while remaining generated.

structure IndexedGrammar.NFParse.ScopedOneFactorShrinking {T : Type} (g : IndexedGrammar T) (w : List T) (bound : ℕ) : Type

The critical-scope form of the one-factor shrinking conclusion. The two contexts are kept fixed; adding either nonempty context as an outer factor recovers the usual proper-subproduct statement for the whole word.

• leftContext : List T
• factors : List (List T)
• rightContext : List T
• word_eq : w = self.leftContext ++ self.factors.flatten ++ self.rightContext
• two_le : 2 ≤ self.factors.length
• length_le : self.factors.length ≤ bound
• factors_nonempty (factor : List T) : factor ∈ self.factors → factor ≠ []
• shrink (i : Fin self.factors.length) : ∃ (kept : List (List T)), MarkedHigman.RetainsAt kept self.factors i ∧ kept.length < self.factors.length ∧ g.Generates (self.leftContext ++ kept.flatten ++ self.rightContext)

theorem IndexedGrammar.NFParse.exists_scopedOneFactorShrinking {T : Type} (g : IndexedGrammar T) [Fintype T] [Fintype g.nt] [Fintype g.flag] [DecidableEq g.nt] (hNF : g.IsNormalForm) : ∃ k > 0, ∀ (w : List T), g.Generates w → k ≤ w.length → Nonempty (ScopedOneFactorShrinking g w (k - 2))

Grammar-level one-factor shrinking theorem.