Nesting of retained pushdown return intervals

A run which removes one displayed stack symbol while retaining the suffix below it is a return interval. Two such intervals on one deterministic run may be disjoint or nested, but cannot strictly cross before a productive continuation. At a putative crossing, each interval boundary occurs inside the other retained-frame run. The resulting two suffix equations force the retained frames to coincide, leaving a nonempty cycle at the common return configuration.

theorem DPDA.retainedFrameRun_eq_zero_of_start_at_frame {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {P : PDA Q T S} {frame : List S} {n : ℕ} {q : Q} {input : List T} {d : P.conf} (h : P.RetainedFrameRun frame n { state := q, input := input, stack := frame } d) : n = 0

theorem DPDA.no_strictly_crossing_retained_returns {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {root : M.toPDA.conf} {n a b c : ℕ} {q₁ q₂ returnState final : Q} {input₁ input₂ returnInput : List T} {Z₁ Z₂ : S} {frame₁ frame₂ : List S} (hprefix₁ : PDA.ReachesIn n root { state := q₁, input := input₁, stack := Z₁ :: frame₁ }) (hreturn₁ : M.toPDA.RetainedFrameRun frame₁ (a + b) { state := q₁, input := input₁, stack := Z₁ :: frame₁ } { state := returnState, input := returnInput, stack := frame₁ }) (hprefix₂ : PDA.ReachesIn (n + a) root { state := q₂, input := input₂, stack := Z₂ :: frame₂ }) (hreturn₂ : M.toPDA.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 := [] }) : False

Two one-symbol net-pop intervals on a deterministic run cannot strictly cross before a productive empty-stack continuation.

The first interval starts after n steps and lasts a + b steps. The second starts after n + a steps and lasts b + c steps. Thus b > 0 places the second start strictly inside the first interval, while c > 0 places the second endpoint strictly after the first endpoint. Both runs retain their respective suffixes and return to the same state and input.