Preloading the canonical LR lookahead buffer

On a properly endmarked input, the buffered DPDA deterministically reads either k terminals or the earlier endmarker. The resulting parser control contains exactly observe k w, and the remaining physical input is exactly unreadAfter k w.

theorem CF_grammar.LRk.Buffered.setBuffer_observe_append_singleton {T : Type} [Fintype T] (k : ℕ) (xs : List T) (a : T) (hxs : xs.length < k) : setBuffer (observe k xs) xs.length (some a) = observe k (xs ++ [a])

Writing the next free slot of an observed short prefix extends that prefix by one terminal.

theorem CF_grammar.LRk.Buffered.finishBuffer_observe {T : Type} [Fintype T] (k : ℕ) (xs : List T) (hxs : xs.length < k) : finishBuffer (observe k xs) xs.length = observe k xs

Padding after an early marker leaves the ordinary EOF-padded observation unchanged.

theorem CF_grammar.LRk.Buffered.observe_append_of_length_eq {T : Type} [Fintype T] (k : ℕ) (xs ys : List T) (hxs : xs.length = k) : observe k (xs ++ ys) = observe k xs

Once a prefix of length k has been loaded, later terminals do not change the observation.

theorem CF_grammar.LRk.Buffered.unreadAfter_append_of_length_eq {T : Type} [Fintype T] (k : ℕ) (xs ys : List T) (hxs : xs.length = k) : unreadAfter k (xs ++ ys) = List.map some ys ++ [none]

The physical suffix after loading an exact k-terminal prefix.

theorem CF_grammar.LRk.Buffered.machine_reaches_preload {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (hk : 0 < k) (w : List T) : PDA.Reaches { state := (machine G k hk).initial_state, input := List.map some w ++ [none], stack := [(machine G k hk).start_symbol] } { state := Control.parse (scanKernel G k []) (observe k w), input := unreadAfter k w, stack := [none] }

Exact preload theorem for a properly endmarked word.