proposition: Lemma simulation q t k : steps M k (q, t) = None -> exists v, (1, P) // (encode_config (q, t)) ->> (0, v).
proof: Proof. elim: k q t; first done. move=> k IH q t. rewrite (steps_plus 1) /=. case E: (step M (q, t)) => [[q' t']|]. - move=> /IH [v] Hv. exists v. move: E => /simulation_step_Some [?] /sss_steps_compute /sss_compute_trans. by apply. - by move: E => /simulation_step_None. 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