proposition: Lemma PROG_spec_None q t : step M (q, t) = None -> exists v, (!q, PROG q) // (encode_config (q, t)) ->> (0, v).
proof: Proof. move: t => [[ls a] rs] /=. rewrite /step. case E: (δ (q, a)) => [[[??]d]|]; first done. move=> _. have ->: !q = 0 + !q by done. move: a E => [] E. all: exists [ ls ; []%list ; rs ; []%list ]%vector. 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