proposition: Lemma BSM_addstacks_bwd' n i (P : list (bsm_instr n)) m k j v v'' out : sss_steps (bsm_sss (n := m + n)) (i, (@bsm_addstacks n m P)) k (j, vec_app v'' v) out -> exists o v', out = (o, vec_app v'' v') /\ sss_steps (bsm_sss (n := n)) (i, P) k (j, v) (o, v').
proof: Proof. induction k in j, v, out |- *; inversion 1; subst. - repeat econstructor. - eapply BSM_addstacks_step_bwd' in H1 as (? & ? & ? & ?). subst. eapply IHk in H2 as (? & ? & ? & ?). subst. repeat eexists. econstructor. 1: eauto. eauto. 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)