proposition: Lemma Q_step_spec (Q : list (bsm_instr 4)) offset i v j w : Q_step Q offset i v = Some (j, w) -> sss_step (bsm_sss (n:=4)) (offset, Q) (i + offset, v) (j, w).
proof: Proof. rewrite /Q_step. case E: (nth_error Q i) => [t|]; last done. move: E => /(@nth_error_split (bsm_instr 4)) => - [l] [r] [-> <-]. move=> Ht. exists offset, l, t, r, v. split; [|split]; [done|congr pair; lia|]. move: t Ht => []. - move=> x p' q' [<-]. move Ex: (vec_pos v x) => [|[] ?]; by auto using bsm_sss. - move=> x b [<-] <-. by auto using bsm_sss. 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