LanglibPrefix uniqueness of productive single completions #
Two retained returns from the same globally reached stack cut cannot complete
the same characteristic single on strictly prefix-related words. Lifting
the shorter return under the unmatched suffix puts both runs at one common
source. At the shorter endpoint the retained frame is already exposed, so
the longer retained run has no legal step left.
theorem
DPDA_to_LR.productiveRetainedReturn_prefix_eq
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{beforeWord word extra tail : List T}
{prefixSteps shortSteps longSteps : ℕ}
{source returnState shortFinal longFinal : EState M}
{top : EStack M}
{frame : List (EStack M)}
(global :
PDA.ReachesIn prefixSteps
{ state := (emptyStackPDA M).initial_state, input := beforeWord ++ (word ++ (extra ++ tail)),
stack := [(emptyStackPDA M).start_symbol] }
{ state := source, input := word ++ (extra ++ tail), stack := top :: frame })
(short :
(emptyStackPDA M).RetainedFrameRun frame shortSteps { state := source, input := word, stack := top :: frame }
{ state := returnState, input := [], stack := frame })
(long :
(emptyStackPDA M).RetainedFrameRun frame longSteps { state := source, input := word ++ extra, stack := top :: frame }
{ state := returnState, input := [], stack := frame })
(shortUseful :
PDA.Reaches { state := returnState, input := extra ++ tail, stack := frame }
{ state := shortFinal, input := [], stack := [] })
(longUseful :
PDA.Reaches { state := returnState, input := tail, stack := frame } { state := longFinal, input := [], stack := [] })
:
Productive retained returns from one globally reached cut have prefix-incomparable consumed words. The stated prefix is therefore equal.
theorem
DPDA_to_LR.productiveRetainedReturn_prefix_eq_cross_input
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{beforeWord word extra tail₁ tail₂ : List T}
{prefixSteps shortSteps longSteps : ℕ}
{source returnState shortFinal longFinal : EState M}
{top : EStack M}
{frame : List (EStack M)}
(global :
PDA.ReachesIn prefixSteps
{ state := (emptyStackPDA M).initial_state, input := beforeWord ++ (word ++ extra),
stack := [(emptyStackPDA M).start_symbol] }
{ state := source, input := word ++ extra, stack := top :: frame })
(short :
(emptyStackPDA M).RetainedFrameRun frame shortSteps { state := source, input := word, stack := top :: frame }
{ state := returnState, input := [], stack := frame })
(long :
(emptyStackPDA M).RetainedFrameRun frame longSteps { state := source, input := word ++ extra, stack := top :: frame }
{ state := returnState, input := [], stack := frame })
(shortUseful :
PDA.Reaches { state := returnState, input := extra ++ tail₁, stack := frame }
{ state := shortFinal, input := [], stack := [] })
(longUseful :
PDA.Reaches { state := returnState, input := tail₂, stack := frame } { state := longFinal, input := [], stack := [] })
(hlook : List.take 1 tail₁ = List.take 1 tail₂)
:
Cross-input form of productiveRetainedReturn_prefix_eq. The two
productive continuations may have different tails, provided that their next
visible input symbols agree.