proposition: Lemma BSM_addstacks_step' n i (P : list (bsm_instr n)) m j v o v' v'' : sss_step (bsm_sss (n := n)) (i, P) (j, v) (o, v') -> sss_step (bsm_sss (n := m + n)) (i, (@bsm_addstacks n m P)) (j, vec_app v'' v) (o, vec_app v'' v').
proof: Proof. intros (? & ? & ? & ? & ? & ? & ? & ?). inv H. inv H0. unfold bsm_addstacks. rewrite map_app. cbn. eexists. eexists. eexists. eexists. eexists. split. 1: reflexivity. split. 1: rewrite map_length. 1: reflexivity. now apply BSM_addstacks_step. Qed.
imports: Undecidability.StackMachines.BSM Undecidability.StackMachines.Util.BSM_computable Undecidability.TM.TM Undecidability.TM.Util.TM_facts Undecidability.TM.Util.TM_computable Undecidability.TM(TM Arbitrary_to_Binary mTM_to_TM HaltTM_1_to_HaltKOSBTM HaltKOSBTM_to_HaltBSM) Undecidability.Shared.Libs.DLW(vec pos sss subcode) Undecidability(bsm_utils bsm_defs) Undecidability.TM.Code.Code Undecidability.TM(Single.EncodeTapes)