Introducing edges in an active characteristic spine

This file gives the top-edge interface used by the LR-core proof. It exposes the parent handle and retained production which introduced a displayed active child, while hiding the auxiliary decomposition witnesses of ActiveSpine.

def DPDA_to_LR.Introduces {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (childPrefix : List (symbol T (Nonterminal M))) (child : Nonterminal M) (childSuffix : List T) (parentPrefix : List (symbol T (Nonterminal M))) (parent : Nonterminal M) (rule : Nonterminal M × List (symbol T (Nonterminal M))) : Prop

A concrete retained production is the final edge of an active derivation spine. The indices record both the visible child prehandle and its parent prehandle.

Equations

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

theorem DPDA_to_LR.Introduces.of_descend {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {childPrefix : List (symbol T (Nonterminal M))} {child : Nonterminal M} {childSuffix : List T} {parentPrefix : List (symbol T (Nonterminal M))} {parent : Nonterminal M} {rule : Nonterminal M × List (symbol T (Nonterminal M))} {alpha beta : List (symbol T (Nonterminal M))} {t z : List T} (hparent : ActiveSpine M parentPrefix parent t) (hrule : rule ∈ (characteristicGrammar M).rules) (hlhs : rule.1 = parent) (hrhs : rule.2 = alpha ++ [symbol.nonterminal child] ++ beta) (hbeta : (characteristicGrammar M).DerivesRightmost beta (List.map symbol.terminal z)) (hprefix : childPrefix = parentPrefix ++ alpha) (hsuffix : childSuffix = z ++ t) : Introduces M childPrefix child childSuffix parentPrefix parent rule

Direct constructor for an introducing edge.

theorem DPDA_to_LR.Introduces.finalChild {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {parentPrefix action : List (symbol T (Nonterminal M))} {parent child : Nonterminal M} {suffix : List T} {rule : Nonterminal M × List (symbol T (Nonterminal M))} (hparent : ActiveSpine M parentPrefix parent suffix) (hrule : rule ∈ (characteristicGrammar M).rules) (hlhs : rule.1 = parent) (hrhs : rule.2 = action ++ [symbol.nonterminal child]) : Introduces M (parentPrefix ++ action) child suffix parentPrefix parent rule

Applying a nonbase rule whose last symbol is child adds an introducing edge with unchanged terminal suffix.

theorem DPDA_to_LR.Introduces.activeSpine {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {childPrefix : List (symbol T (Nonterminal M))} {child : Nonterminal M} {childSuffix : List T} {parentPrefix : List (symbol T (Nonterminal M))} {parent : Nonterminal M} {rule : Nonterminal M × List (symbol T (Nonterminal M))} (h : Introduces M childPrefix child childSuffix parentPrefix parent rule) : ActiveSpine M childPrefix child childSuffix

The introducing-edge witness itself reconstructs the visible child spine.

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

The semantic top-edge property needed by the nonbase LR-core cases: one visible active child and one symbol of following input determine its parent handle and the production which introduced it.

Equations

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

theorem DPDA_to_LR.nonbase_collision_of_introducingEdgesUnique {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (hedges : IntroducingEdgesUnique M) {r₁ r₂ : Nonterminal M × List (symbol T (Nonterminal M))} (hr₁ : r₁ ∈ (characteristicGrammar M).rules) (hr₂ : r₂ ∈ (characteristicGrammar M).rules) {p₁ p₂ action₁ action₂ : List (symbol T (Nonterminal M))} {s₁ s₂ y : List T} {q₁ q₂ target₁ target₂ : State M} {gamma₁ gamma₂ : List (StackSymbol M)} (hspine₁ : ActiveSpine M p₁ r₁.1 s₁) (hspine₂ : ActiveSpine M p₂ r₂.1 s₂) (hrhs₁ : r₁.2 = action₁ ++ [symbol.nonterminal (PDA_to_CFG.N.list q₁ gamma₁ target₁)]) (hrhs₂ : r₂.2 = action₂ ++ [symbol.nonterminal (PDA_to_CFG.N.list q₂ gamma₂ target₂)]) (hleft₁ : ∀ X ∈ p₁ ++ action₁, ¬IsListSymbol M X) (hleft₂ : ∀ X ∈ p₂ ++ action₂, ¬IsListSymbol M X) (hform : p₂ ++ r₂.2 ++ List.map symbol.terminal s₂ = p₁ ++ r₁.2 ++ List.map symbol.terminal y) (hlook : List.take 1 s₁ = List.take 1 y) : p₁ = p₂ ∧ r₁ = r₂

Once top-edge uniqueness is available, all nonbase handle comparisons reduce uniformly to cancellation of their final characteristic-list marker.