proposition: Lemma simulation_step_None q t : step M (q, t) = None -> exists v, (1, P) // (encode_config (q, t)) ->> (0, v).
proof: Proof. move=> /PROG_spec_None [v Hv]. exists v. by apply: subcode_sss_compute; [apply: PROG_sc|]. 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