proposition: Lemma PROG_spec_Some q t q' t' : step M (q, t) = Some (q', t') -> exists k, (!q, PROG q) // (encode_config (q, t)) -[S k]-> (encode_config (q', t')).
proof: Proof. move: t => [[ls a] rs] /=. rewrite /step. case E: (δ (q, a)) => [[[??]d]|]; last done. move=> [<- <-]. have ->: !q = 0 + !q by done. move: d a ls rs E => [] [] [|[] ls] [|[] rs] E. all: eexists; rewrite /PROG /box E. all: do ? ((by apply: in_sss_steps_0) || (apply: in_sss_steps_S; [by apply: Q_step_spec|])). Qed.
imports: Undecidability.StackMachines(BSM BSM.bsm_defs) Undecidability.TM(SBTM Util.SBTM_facts) Undecidability.Shared.Libs.DLW(vec subcode sss) PeanoNat List Lia ssreflect ssrbool ssrfun