LR core of the productive characteristic grammar

The syntactic reduction in this file leaves exactly two semantic spine properties: uniqueness of the edge introducing a visible final list child, and uniqueness of an empty-list return. All characteristic rule-shape pairs are discharged uniformly from those properties.

theorem DPDA_to_LR.retained_rule_base_or_finalList {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {r : Nonterminal M × List (symbol T (Nonterminal M))} (hr : r ∈ (characteristicGrammar M).rules) {p : List (symbol T (Nonterminal M))} (hp : PendingPrefix M p) : (∃ (q : State M), r = (PDA_to_CFG.N.list q [] q, [])) ∨ ∃ (action : List (symbol T (Nonterminal M))) (q : State M) (target : State M) (gamma : List (StackSymbol M)), r.2 = action ++ [symbol.nonterminal (PDA_to_CFG.N.list q gamma target)] ∧ ∀ X ∈ p ++ action, ¬IsListSymbol M X

A retained rule is either the unique empty-list shape, or its right side has one final characteristic-list marker preceded only by non-list symbols in the displayed pending prefix.

def DPDA_to_LR.EmptyListHandlesUnique {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : Prop

The remaining semantic obligation for base productions.

Equations

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

theorem DPDA_to_LR.characteristicGrammar_coreIsLR1_of_spine {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (hedges : IntroducingEdgesUnique M) (hempty : EmptyListHandlesUnique M) : (characteristicGrammar M).CoreIsLRk 1

The complete LR(1) core follows from the two operational spine uniqueness properties.

theorem DPDA_to_LR.characteristicGrammar_isLR1_of_spine {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (hedges : IntroducingEdgesUnique M) (hempty : EmptyListHandlesUnique M) : (characteristicGrammar M).IsLRk 1

Augmented LR(1), still parameterized only by the two operational spine uniqueness properties.