Productive completion of characteristic right-sentential forms

Every retained characteristic rule is fully productive. Consequently every nonterminal in a reachable right-sentential form can be completed, and the completion can be scheduled rightmost. These facts let the LR proof extend a candidate handle to a genuine accepting computation.

theorem DPDA_to_LR.productive_characteristic_iff_raw {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {A : (characteristicGrammar M).nt} : productive (characteristicGrammar M) A ↔ productive (rawCharacteristicGrammar M) A

Productivity is unchanged by the productive-rule filter.

theorem DPDA_to_LR.characteristic_rule_lhs_productive_reduced {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) : productive (characteristicGrammar M) r.1

The left side of every retained rule is productive in the reduced grammar.

theorem DPDA_to_LR.characteristic_rule_rhs_productive_reduced {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) {A : (characteristicGrammar M).nt} (hA : symbol.nonterminal A ∈ r.2) : productive (characteristicGrammar M) A

Every nonterminal on the right side of a retained rule is productive in the reduced grammar.

theorem DPDA_to_LR.derivesRightmost_terminal_of_all_productive {T : Type} [Fintype T] (G : CF_grammar T) {u : List (symbol T G.nt)} (hprod : ∀ (A : G.nt), symbol.nonterminal A ∈ u → productive G A) : ∃ (w : List T), G.DerivesRightmost u (List.map symbol.terminal w)

A list whose nonterminals are productive has a terminal rightmost completion.

theorem DPDA_to_LR.prehandle_all_nonterminals_productive {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) {p : List (symbol T (characteristicGrammar M).nt)} {s : List T} (hderive : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (characteristicGrammar M).initial] (p ++ [symbol.nonterminal r.1] ++ List.map symbol.terminal s)) (A : (characteristicGrammar M).nt) : symbol.nonterminal A ∈ p ++ [symbol.nonterminal r.1] ++ List.map symbol.terminal s → productive (characteristicGrammar M) A

Every nonterminal in a reachable characteristic prehandle is productive.

theorem DPDA_to_LR.prehandle_prefix_completion {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) {p : List (symbol T (characteristicGrammar M).nt)} {s : List T} (hderive : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (characteristicGrammar M).initial] (p ++ [symbol.nonterminal r.1] ++ List.map symbol.terminal s)) : ∃ (w : List T), (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal w)

The prefix before a reachable handle has a terminal rightmost completion.

theorem DPDA_to_LR.characteristic_rule_rhs_completion {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) : ∃ (w : List T), (characteristicGrammar M).DerivesRightmost r.2 (List.map symbol.terminal w)

The right side of a retained rule has a terminal rightmost completion.

theorem DPDA_to_LR.prehandle_post_completion {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) {p : List (symbol T (characteristicGrammar M).nt)} {s : List T} (hderive : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (characteristicGrammar M).initial] (p ++ [symbol.nonterminal r.1] ++ List.map symbol.terminal s)) : ∃ (w : List T), (characteristicGrammar M).DerivesRightmost (p ++ r.2 ++ List.map symbol.terminal s) (List.map symbol.terminal w)

Applying a reachable rule and completing its result yields a terminal rightmost derivation.