proposition: Lemma simulation_step_Some q t q' t' : step M (q, t) = Some (q', t') -> exists k, (1, P) // (encode_config (q, t)) -[S k]-> (encode_config (q', t')).
proof: Proof. move=> /PROG_spec_Some [k] H. exists k. apply: subcode_sss_steps; [|by eassumption]. by 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