The one-factor shrinking theorem for indexed languages

This file lifts the grammar-level critical-scope theorem through the finite-support normal-form construction. Consequently the statement applies to an arbitrary indexed language, independently of the grammar used to present it.

The two outer contexts are fixed by every shrinking. They can be treated as at most two additional factors when the usual whole-word formulation is needed.

Reference

• R. H. Gilman, "A shrinking lemma for indexed languages", Theoretical Computer Science 163 (1996), 277--281.

structure IndexedScopedOneFactorShrinking {T : Type} (L : Language T) (w : List T) (bound : ℕ) : Type

The class-level critical-scope form of the one-factor shrinking theorem.

• 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 ∧ self.leftContext ++ kept.flatten ++ self.rightContext ∈ L

theorem exists_indexedScopedOneFactorShrinking {T : Type} [Fintype T] [Inhabited T] {L : Language T} (hL : is_Indexed L) : ∃ k > 0, ∀ w ∈ L, k ≤ w.length → Nonempty (IndexedScopedOneFactorShrinking L w (k - 2))

Every indexed language over a finite alphabet satisfies the critical-scope one-factor shrinking theorem.