Counted PDA runs retaining a stack frame

PDA.RetainedFrameRun P frame n c d records a selected counted run whose steps all occur strictly above the unchanged stack suffix frame. Each step stores its frame-free source and target; the indexed configurations are the corresponding configurations with frame appended. This is stronger than bare reachability in a nondeterministic PDA and permits the retained frame to be replaced uniformly.

inductive PDA.RetainedFrameRun {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (P : PDA Q T S) (frame : List S) : ℕ → P.conf → P.conf → Prop

A counted run together with a selected stack suffix which no step examines or changes.

• refl {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {P : PDA Q T S} {frame : List S} (q : Q) (input : List T) (upper : List S) : P.RetainedFrameRun frame 0 { state := q, input := input, stack := upper ++ frame } { state := q, input := input, stack := upper ++ frame }
• step {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {P : PDA Q T S} {frame : List S} {n : ℕ} {start : P.conf} {q p : Q} {input output : List T} {upper upper' : List S} (run : P.RetainedFrameRun frame n start { state := q, input := input, stack := upper ++ frame }) (last : Reaches₁ { state := q, input := input, stack := upper } { state := p, input := output, stack := upper' }) : P.RetainedFrameRun frame (n + 1) start { state := p, input := output, stack := upper' ++ frame }

theorem PDA.RetainedFrameRun.toReachesIn {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {P : PDA Q T S} {frame : List S} {n : ℕ} {c d : P.conf} (h : P.RetainedFrameRun frame n c d) : ReachesIn n c d

Forgetting the retained-frame certificate gives the corresponding counted run of the original PDA.

theorem PDA.RetainedFrameRun.appendInput {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {P : PDA Q T S} {frame : List S} {n : ℕ} {c d : P.conf} (h : P.RetainedFrameRun frame n c d) (suffix : List T) : P.RetainedFrameRun frame n (c.appendInput suffix) (d.appendInput suffix)

Append an untouched input suffix uniformly to a retained-frame run.

theorem PDA.RetainedFrameRun.ofReachesIn {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {P : PDA Q T S} {frame : List S} {n : ℕ} {c d : P.conf} (h : ReachesIn n c d) : P.RetainedFrameRun frame n (c.appendStack frame) (d.appendStack frame)

Any counted run can be lifted under an arbitrary retained stack frame.

theorem PDA.RetainedFrameRun.changeFrame {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {P : PDA Q T S} {frame : List S} {n : ℕ} {q p : Q} {input output : List T} {upper upper' : List S} (h : P.RetainedFrameRun frame n { state := q, input := input, stack := upper ++ frame } { state := p, input := output, stack := upper' ++ frame }) (newFrame : List S) : P.RetainedFrameRun newFrame n { state := q, input := input, stack := upper ++ newFrame } { state := p, input := output, stack := upper' ++ newFrame }

Replace the untouched suffix of a retained-frame run.

theorem PDA.RetainedFrameRun.end_shape {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {P : PDA Q T S} {frame : List S} {n : ℕ} {c d : P.conf} (h : P.RetainedFrameRun frame n c d) : ∃ (q : Q) (input : List T) (upper : List S), d = { state := q, input := input, stack := upper ++ frame }

The final configuration of a retained-frame run exposes its retained suffix.

theorem PDA.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} {finish : P.conf} (h : P.RetainedFrameRun frame n { state := q, input := input, stack := frame } finish) : n = 0

A retained-frame run starting with no stack above its retained suffix is necessarily reflexive: a PDA has no transition from the corresponding stripped empty-stack configuration.

theorem PDA.RetainedFrameRun.split_add {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {P : PDA Q T S} {frame : List S} {n m : ℕ} {c d : P.conf} (h : P.RetainedFrameRun frame (n + m) c d) : ∃ (q : Q) (input : List T) (upper : List S), P.RetainedFrameRun frame n c { state := q, input := input, stack := upper ++ frame } ∧ P.RetainedFrameRun frame m { state := q, input := input, stack := upper ++ frame } d

Split a retained-frame run at an exact step count. The intermediate configuration exposes the same retained suffix.