LanglibNesting of useful return intervals in the empty-stack wrapper #
Useful paths of the normalized final-state-to-empty-stack wrapper are deterministic even though the raw wrapper has an extra drain edge. Combining that useful-path determinism with retained stack frames gives the return interval nesting theorem needed by the characteristic-grammar spine proof.
theorem
DPDA_to_LR.emptyStack_no_properly_nested_productive_retained_returns_of_segments
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{a b c : ℕ}
{source returnState final : EState M}
{sourceInput returnInput : List T}
{Z : EStack M}
{outerFrame innerFrame : List (EStack M)}
(before :
(emptyStackPDA M).RetainedFrameRun outerFrame a { state := source, input := sourceInput, stack := Z :: outerFrame }
{ state := source, input := sourceInput, stack := Z :: innerFrame })
(inner :
(emptyStackPDA M).RetainedFrameRun innerFrame b { state := source, input := sourceInput, stack := Z :: innerFrame }
{ state := returnState, input := returnInput, stack := innerFrame })
(after :
(emptyStackPDA M).RetainedFrameRun outerFrame c { state := returnState, input := returnInput, stack := innerFrame }
{ state := returnState, input := returnInput, stack := outerFrame })
(hproper : 0 < a ∧ 0 < c)
(huseful :
PDA.Reaches { state := returnState, input := returnInput, stack := outerFrame }
{ state := final, input := [], stack := [] })
:
Segment form of the proper-nesting obstruction for the normalized empty-stack wrapper.
theorem
DPDA_to_LR.emptyStack_no_properly_nested_productive_retained_returns
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{w : List T}
{n a b c : ℕ}
{source returnState outerFinal innerFinal : EState M}
{sourceInput returnInput : List T}
{Z : EStack M}
{outerFrame innerFrame : List (EStack M)}
(houterPrefix :
PDA.ReachesIn n { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] }
{ state := source, input := sourceInput, stack := Z :: outerFrame })
(houter :
(emptyStackPDA M).RetainedFrameRun outerFrame (a + b + c)
{ state := source, input := sourceInput, stack := Z :: outerFrame }
{ state := returnState, input := returnInput, stack := outerFrame })
(hinnerPrefix :
PDA.ReachesIn (n + a)
{ state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] }
{ state := source, input := sourceInput, stack := Z :: innerFrame })
(hinner :
(emptyStackPDA M).RetainedFrameRun innerFrame b { state := source, input := sourceInput, stack := Z :: innerFrame }
{ state := returnState, input := returnInput, stack := innerFrame })
(ha : 0 < a)
(hc : 0 < c)
(houterUseful :
PDA.Reaches { state := returnState, input := returnInput, stack := outerFrame }
{ state := outerFinal, input := [], stack := [] })
(hinnerUseful :
PDA.Reaches { state := returnState, input := returnInput, stack := innerFrame }
{ state := innerFinal, input := [], stack := [] })
:
Rooted/count-indexed proper-nesting obstruction for emptyStackPDA.
Both return endpoints are assumed useful so that useful-path determinism can
identify the two boundaries of the nested interval inside the outer one.
theorem
DPDA_to_LR.emptyStack_no_strictly_crossing_retained_returns
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{w : List T}
{n a b c : ℕ}
{q₁ q₂ returnState final₁ final₂ : EState M}
{input₁ input₂ returnInput : List T}
{Z₁ Z₂ : EStack M}
{frame₁ frame₂ : List (EStack M)}
(hprefix₁ :
PDA.ReachesIn n { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] }
{ state := q₁, input := input₁, stack := Z₁ :: frame₁ })
(hreturn₁ :
(emptyStackPDA M).RetainedFrameRun frame₁ (a + b) { state := q₁, input := input₁, stack := Z₁ :: frame₁ }
{ state := returnState, input := returnInput, stack := frame₁ })
(hprefix₂ :
PDA.ReachesIn (n + a)
{ state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] }
{ state := q₂, input := input₂, stack := Z₂ :: frame₂ })
(hreturn₂ :
(emptyStackPDA M).RetainedFrameRun frame₂ (b + c) { state := q₂, input := input₂, stack := Z₂ :: frame₂ }
{ state := returnState, input := returnInput, stack := frame₂ })
(hb : 0 < b)
(hc : 0 < c)
(huseful₁ :
PDA.Reaches { state := returnState, input := returnInput, stack := frame₁ }
{ state := final₁, input := [], stack := [] })
(huseful₂ :
PDA.Reaches { state := returnState, input := returnInput, stack := frame₂ }
{ state := final₂, input := [], stack := [] })
:
Two useful one-symbol return intervals on a globally rooted computation
of emptyStackPDA cannot strictly cross.
The first interval occupies [n, n + a + b]; the second occupies
[n + a, n + a + b + c]. Positive b and c express a strict overlap and
a strict overhang.