proposition: Lemma BSM_addstacks_step n m (P : bsm_instr n) j v o v' v'' : (bsm_sss P (j, v) (o, v') <-> bsm_sss (@bsm_addstracks' n m P) (j, vec_app v'' v) (o, vec_app v'' v')).
proof: Proof. destruct P; cbn; intros; split; inversion 1; subst. - econstructor. now rewrite vec_pos_app_right. - rewrite <- vec_change_app_right. econstructor 2. now rewrite !vec_pos_app_right. - rewrite <- vec_change_app_right. econstructor 3. now rewrite !vec_pos_app_right. - rewrite vec_pos_app_right in H1. match goal with |- bsm_sss _ _ ?st => evar (ev : bsm_state n); enough (st = ev) as ->; subst ev end. 1: econstructor 1. 1: eassumption. f_equal. now eapply vec_app_inj in H7. - rewrite vec_pos_app_right in H1. rewrite vec_change_app_right in H7. match goal with |- bsm_sss _ _ ?st => evar (ev : bsm_state n); enough (st = ev) as ->; subst ev end. 1: econstructor 2. 1: eassumption. f_equal. now eapply vec_app_inj in H7. - rewrite vec_pos_app_right in H1. rewrite vec_change_app_right in H7. match goal with |- bsm_sss _ _ ?st => evar (ev : bsm_state n); enough (st = ev) as ->; subst ev end. 1: econstructor 3. 1: eassumption. f_equal. now eapply vec_app_inj in H7. - match goal with |- bsm_sss _ _ ?st => evar (ev : bsm_state (m + n)); enough (st = ev) as ->; subst ev end. 1: econstructor 4. f_equal. now rewrite vec_change_app_right, vec_pos_app_right. - match goal with |- bsm_sss _ _ ?st => let X := type of st in evar (ev : X); enough (st = ev) as ->; subst ev end. 1: econstructor 4. f_equal. rewrite vec_change_app_right, vec_pos_app_right in H6. now eapply vec_app_inj in H6 as ->. 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)