proposition: Lemma ComputationalSplitter' : FullySharpened (string_spec ab_star_grammar HSL).
proof: Proof. start sharpening ADT. start honing parser using indexed representation. hone method "splits". { simplify parser splitter. finish honing parser method. } finish_Sharpening_SplitterADT. Defined.
imports: Fiat.Parsers.Grammars.ABStar Fiat.Parsers.Refinement.Tactics