Productive transition rules

A retained rule headed by a characteristic single nonterminal is precisely the first move of a net-pop computation. This file packages that observation with the actual terminal completion of the rule's right side. It is the local semantic ingredient in the reverse-handle argument: equal one-symbol lookahead makes two productive rules for the same single nonterminal equal.

theorem DPDA_to_LR.reaches_of_characteristic_derives_list {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q p : State M} {gamma : List (StackSymbol M)} {w : List T} (hgamma : ↑gamma.length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (hderive : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.list q gamma p)] (List.map symbol.terminal w)) : PDA.Reaches { state := q, input := w, stack := gamma } { state := p, input := [], stack := [] }

An exact terminal completion of a retained list nonterminal realizes its encoded net-pop computation.

theorem DPDA_to_LR.reaches_of_characteristic_derives_single {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q p : State M} {Z : StackSymbol M} {w : List T} (hderive : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.single q Z p)] (List.map symbol.terminal w)) : PDA.Reaches { state := q, input := w, stack := [Z] } { state := p, input := [], stack := [] }

An exact terminal completion of a retained single nonterminal realizes the corresponding one-symbol net-pop computation.

theorem DPDA_to_LR.productiveFirstMove_of_single_rule {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {r : (characteristicGrammar M).nt × List (symbol T (characteristicGrammar M).nt)} (hr : r ∈ (characteristicGrammar M).rules) {q target : State M} {Z : StackSymbol M} (hlhs : r.1 = PDA_to_CFG.N.single q Z target) {w : List T} (hcomplete : (characteristicGrammar M).DerivesRightmost r.2 (List.map symbol.terminal w)) : ∃ (sig : FirstMoveSignature M), ProductiveFirstMove M q Z w target sig ∧ match sig.consumes with | true => ∃ (a : T) (tail : List T), w = a :: tail ∧ r.2 = [symbol.terminal a, symbol.nonterminal (PDA_to_CFG.N.list sig.nextState sig.replacement target)] | false => r.2 = [symbol.nonterminal (PDA_to_CFG.N.list sig.nextState sig.replacement target)]

A retained transition rule, together with a concrete terminal completion of its right side, supplies its productive first-move signature.

theorem DPDA_to_LR.single_rule_unique_of_completion {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {r₁ r₂ : (characteristicGrammar M).nt × List (symbol T (characteristicGrammar M).nt)} (hr₁ : r₁ ∈ (characteristicGrammar M).rules) (hr₂ : r₂ ∈ (characteristicGrammar M).rules) {q target : State M} {Z : StackSymbol M} (hlhs₁ : r₁.1 = PDA_to_CFG.N.single q Z target) (hlhs₂ : r₂.1 = PDA_to_CFG.N.single q Z target) {x y : List T} (hx : (characteristicGrammar M).DerivesRightmost r₁.2 (List.map symbol.terminal x)) (hy : (characteristicGrammar M).DerivesRightmost r₂.2 (List.map symbol.terminal y)) (hlook : List.take 1 x = List.take 1 y) : r₁ = r₂

Productive retained rules for the same single nonterminal are selected uniquely by one terminal of their completed yields.