Productive structural steps for protected tasks

The protected atomic runner handles a unary interval ending in a pop. At a productive binary event the two children may consume different aligned prefixes of the shared protected layout; at a push event the runner allocates a fresh compressed singleton.

def IndexedGrammar.Aho.ProtectedScheduleRunAtOrBelow {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A : g.nt} {stack : List g.flag} {w : List T} (parse : g.NFParse A stack w) : Prop

Protected-mode entry with only the common non-strict parking bound.

This deliberately weaker interface is used only while sealing an overlay at a binary fork. Both binary child windows start strictly after the parent base, so the implementation restores ParkingBelow before invoking any ordinary child runner.

Equations

• One or more equations did not get rendered due to their size.

theorem IndexedGrammar.Aho.ProtectedScheduleRunAtOrBelow.toProtectedScheduleRun {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A : g.nt} {stack : List g.flag} {w : List T} {parse : g.NFParse A stack w} (run : ProtectedScheduleRunAtOrBelow parse) : ProtectedScheduleRun parse

An at-or-below protected implementation is an ordinary protected implementation whenever the caller supplies the ordinary strict bound.

theorem IndexedGrammar.Aho.protectedScheduleRun_binary_atOrBelow {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A B C : g.nt} {stack : List g.flag} {u v : 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 none, IRhsSymbol.nonterminal C none]) (leftParse : g.NFParse B stack u) (rightParse : g.NFParse C stack v) (leftRuns : OrdinaryScheduleRuns leftParse) (rightRuns : OrdinaryScheduleRuns rightParse) : ProtectedScheduleRunAtOrBelow (NFParse.binary hr hlhs hc hrhs leftParse rightParse)

Split a protected binary task at the aligned maximal consumed prefixes of its children and run the two terminal intervals in order, assuming only the parent non-strict parking bound.

theorem IndexedGrammar.Aho.protectedScheduleRun_binary {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A B C : g.nt} {stack : List g.flag} {u v : 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 none, IRhsSymbol.nonterminal C none]) (leftParse : g.NFParse B stack u) (rightParse : g.NFParse C stack v) (leftRuns : OrdinaryScheduleRuns leftParse) (rightRuns : OrdinaryScheduleRuns rightParse) : ProtectedScheduleRun (NFParse.binary hr hlhs hc hrhs leftParse rightParse)

Ordinary protected binary entry. The strict parent invariant supplies the weaker premise of the shared binary implementation.

theorem IndexedGrammar.Aho.protectedScheduleRun_of_smaller {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A : g.nt} {stack : List g.flag} {w : List T} (parse : g.NFParse A stack w) (ih : ∀ {B : g.nt} {residualStack : List g.flag} {v : List T} (q : g.NFParse B residualStack v), q.nodeCount < parse.nodeCount → OrdinaryScheduleRuns q) (overlayIH : ∀ {B : g.nt} {residualStack : List g.flag} {v : List T} (q : g.NFParse B residualStack v), q.nodeCount < parse.nodeCount → OverlayScheduleRun q) : ProtectedScheduleRun parse

Complete protected-mode constructor dispatch under the mutual strong-induction hypothesis.