proposition: Lemma BSM_addstacks n i (P : list (bsm_instr n)) m : {P' | length P = length P' /\ (forall j v o v', BSM.eval n (i, P) (j, v) (o, v') -> forall v'', BSM.eval (m + n) (i, P') (j, Vector.append v'' v) (o, Vector.append v'' v')) /\ forall v v'' j out, BSM.eval (m + n) (i, P') (j, Vector.append v'' v) out -> exists out, BSM.eval n (i, P) (j, v) out}.
proof: Proof. exists (bsm_addstacks m P). split. { unfold bsm_addstacks. now rewrite map_length. } setoid_rewrite eval_iff. split. - intros j v o v' [[steps H1] H2] v''. split. 2:{ cbn. unfold bsm_addstacks. rewrite map_length. exact H2. } exists steps. rewrite <- !vec_app_spec. now eapply BSM_addstacks'. - intros v v'' j [o1 o2] H. eapply eval_iff in H as [[steps H1] H2]. rewrite <- vec_app_spec in H1. eapply BSM_addstacks_bwd' in H1 as (? & ? & ? & ?). inv H. eexists (_, _). eapply eval_iff. split. 1: eexists. 1: eapply H0. cbn in *. unfold bsm_addstacks in H2. rewrite map_length in H2. exact H2. 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)