Comparison of globally reachable FS→ES cuts

The normalized DPDA is deterministic inside the simulation component. This module packages that ordering at the concrete FS→ES configuration level and is the prerequisite for the corresponding drain and mixed-cut comparisons.

The deterministic drain tail

First-final cuts

theorem DPDA_to_LR.emptyStack_global_simulation_cuts_comparable {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {w input : List T} {q₁ q₂ : Q × Bool} {stack₁ stack₂ : List (Option S)} (h₁ : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] } { state := Sum.inl q₁, input := input, stack := stack₁ }) (h₂ : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] } { state := Sum.inl q₂, input := input, stack := stack₂ }) : PDA.Reaches { state := Sum.inl q₁, input := input, stack := stack₁ } { state := Sum.inl q₂, input := input, stack := stack₂ } ∨ PDA.Reaches { state := Sum.inl q₂, input := input, stack := stack₂ } { state := Sum.inl q₁, input := input, stack := stack₁ }

Globally reachable cuts that both remain in the simulation component of the FS→ES machine are linearly ordered.

theorem DPDA_to_LR.emptyStack_global_drain_cuts_comparable {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {w input : List T} {stack₁ stack₂ : List (Option S)} (h₁ : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] } { state := Sum.inr 1, input := input, stack := stack₁ }) (h₂ : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] } { state := Sum.inr 1, input := input, stack := stack₂ }) : PDA.Reaches { state := Sum.inr 1, input := input, stack := stack₁ } { state := Sum.inr 1, input := input, stack := stack₂ } ∨ PDA.Reaches { state := Sum.inr 1, input := input, stack := stack₂ } { state := Sum.inr 1, input := input, stack := stack₁ }

Globally reachable cuts in the drain component are linearly ordered. This holds for every shared remaining input, not only for accepting computations at empty input.

theorem DPDA_to_LR.emptyStack_global_simulation_drain_useful {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {w input : List T} {q : Q × Bool} {simStack drainStack : List (Option S)} {final₁ final₂ : EState M} (hsimGlobal : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] } { state := Sum.inl q, input := input, stack := simStack }) (hdrainGlobal : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] } { state := Sum.inr 1, input := input, stack := drainStack }) (hsimUseful : PDA.Reaches { state := Sum.inl q, input := input, stack := simStack } { state := final₁, input := [], stack := [] }) (hdrainUseful : PDA.Reaches { state := Sum.inr 1, input := input, stack := drainStack } { state := final₂, input := [], stack := [] }) : PDA.Reaches { state := Sum.inl q, input := input, stack := simStack } { state := Sum.inr 1, input := input, stack := drainStack }

A useful globally reachable simulation cut precedes every useful drain cut at the same remaining input. Usefulness of the drain cut first forces that input to be empty; first-final normalization then rules out the only possible reverse ordering in the normalized simulation.

theorem DPDA_to_LR.emptyStack_global_useful_nonboot_cuts_comparable {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {w input : List T} {q₁ q₂ final₁ final₂ : EState M} {stack₁ stack₂ : List (EStack M)} (hglobal₁ : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] } { state := q₁, input := input, stack := stack₁ }) (hglobal₂ : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] } { state := q₂, input := input, stack := stack₂ }) (huseful₁ : PDA.Reaches { state := q₁, input := input, stack := stack₁ } { state := final₁, input := [], stack := [] }) (huseful₂ : PDA.Reaches { state := q₂, input := input, stack := stack₂ } { state := final₂, input := [], stack := [] }) (hnonboot₁ : q₁ ≠ Sum.inr 0) (hnonboot₂ : q₂ ≠ Sum.inr 0) : PDA.Reaches { state := q₁, input := input, stack := stack₁ } { state := q₂, input := input, stack := stack₂ } ∨ PDA.Reaches { state := q₂, input := input, stack := stack₂ } { state := q₁, input := input, stack := stack₁ }

Two useful non-boot cuts reached at the same input position lie on one ordered computation of the normalized empty-stack machine. This packages the simulation/simulation, drain/drain, and mixed phase comparisons behind a single phase-independent interface.