One useful wrapper step under two input tails

Two productive computations may have different unconsumed tails while still sharing the next input symbol. Since a pushdown transition sees only that symbol, the control state, and the top stack symbol, their next useful moves have the same control and stack effects. This file records the corresponding relation between the two input components as well.

def DPDA_to_LR.CorrespondingInputStep {T : Type} (before₁ before₂ after₁ after₂ : List T) : Prop

Two steps with corresponding source inputs either both preserve their respective inputs, or both consume the same leading terminal.

Equations

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

theorem DPDA_to_LR.emptyStack_globally_useful_step_cross_input {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {w₁ w₂ sourceInput₁ sourceInput₂ : List T} {sourceState : EState M} {sourceStack : List (EStack M)} {next₁ next₂ : (emptyStackPDA M).conf} {final₁ final₂ : EState M} (hlook : List.take 1 sourceInput₁ = List.take 1 sourceInput₂) (hglobal₁ : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := w₁, stack := [(emptyStackPDA M).start_symbol] } { state := sourceState, input := sourceInput₁, stack := sourceStack }) (hglobal₂ : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := w₂, stack := [(emptyStackPDA M).start_symbol] } { state := sourceState, input := sourceInput₂, stack := sourceStack }) (hstep₁ : PDA.Reaches₁ { state := sourceState, input := sourceInput₁, stack := sourceStack } next₁) (hstep₂ : PDA.Reaches₁ { state := sourceState, input := sourceInput₂, stack := sourceStack } next₂) (huseful₁ : PDA.Reaches next₁ { state := final₁, input := [], stack := [] }) (huseful₂ : PDA.Reaches next₂ { state := final₂, input := [], stack := [] }) : next₁.state = next₂.state ∧ next₁.stack = next₂.stack ∧ CorrespondingInputStep sourceInput₁ sourceInput₂ next₁.input next₂.input

Useful one-step computations from equal state/stack cuts and inputs with the same one-symbol lookahead have equal state and stack effects. Their input effects correspond in the sense of CorrespondingInputStep.

The two source cuts may be reached from different complete input words.