proposition: Lemma BSM_addstacks_step_bwd n m (P : bsm_instr n) j v out v'' : bsm_sss (@bsm_addstracks' n m P) (j, vec_app v'' v) out -> exists o v', out = (o, vec_app v'' v') /\ bsm_sss P (j, v) (o, v').
proof: Proof. destruct P; cbn; inversion 1; subst. - repeat eexists. econstructor. now rewrite vec_pos_app_right in H6. - repeat eexists. 1: rewrite vec_change_app_right. 1: reflexivity. rewrite vec_pos_app_right in H6. now econstructor 2. - repeat eexists. 1: rewrite vec_change_app_right. 1: reflexivity. rewrite vec_pos_app_right in H6. now econstructor 3. - repeat eexists. 1: rewrite vec_change_app_right. 1: reflexivity. rewrite vec_pos_app_right. econstructor 4. 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)