Counted operational semantics of characteristic spines

The ordinary zipper invariant records reachability of every active grammar node. Return-interval arguments additionally need the exact position of the node on a selected computation. This file supplies that counted view and a retained-frame realization of completed single nonterminals.

theorem DPDA_to_LR.ConcreteOperationalSpine.exists_prefixRunIn {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {A : Nonterminal M} {suffix preWord : List T} {context : List (StackSymbol M)} (h : ConcreteOperationalSpine M p A suffix preWord context) : ∃ (n : ℕ), PDA.ReachesIn n { state := (emptyStackPDA M).initial_state, input := preWord, stack := [(emptyStackPDA M).start_symbol] } { state := spineCutState M A, input := [], stack := spineCutStack M A context }

A concrete operational spine carries a selected counted prefix run to its exact physical cut.

theorem DPDA_to_LR.completedSingle_exists_retainedFrameRun {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q target : State M} {Z : StackSymbol M} {word : List T} {frame : List (StackSymbol M)} (hcomplete : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.single q Z target)] (List.map symbol.terminal word)) : ∃ (n : ℕ), 0 < n ∧ (emptyStackPDA M).RetainedFrameRun frame n { state := q, input := word, stack := Z :: frame } { state := target, input := [], stack := frame }

A terminal completion of a characteristic single is a selected nonempty net-pop interval which retains any supplied outer stack frame.

theorem DPDA_to_LR.prefixRunIn_trans_retainedFrameRun {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {P : PDA Q T S} {n m : ℕ} {root source target : P.conf} {frame : List S} (hprefix : PDA.ReachesIn n root source) (hreturn : P.RetainedFrameRun frame m source target) : PDA.ReachesIn (n + m) root target

Concatenate a counted global prefix with a retained return interval.