Push compression for copy-on-write overlays

A live push which stays inside the current compressed block replaces only the private adjacent overlay head. Its physical owner, ticket, and charge are unchanged, and the child continues in overlay mode with the shared protected base untouched.

theorem IndexedGrammar.Aho.overlayScheduleRun_pushCompress {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A B : g.nt} {f : g.flag} {stack : List g.flag} {w : List T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]) (rest : g.NFParse B (f :: stack) w) (hdepthOne : 1 ∉ rest.eventDepths) (restOverlay : OverlayScheduleRun rest) : OverlayScheduleRun (NFParse.push hr hlhs hc hrhs rest)

Compress a pushed flag into the branch-local overlay head and recurse in overlay mode.