proposition: Lemma BSM_addstacks_step_bwd' n i (P : list (bsm_instr n)) m j v v'' out : sss_step (bsm_sss (n := m + n)) (i, (@bsm_addstacks n m P)) (j, vec_app v'' v) out -> exists o v', out = (o, vec_app v'' v') /\ sss_step (bsm_sss (n := n)) (i, P) (j, v) (o, v').
proof: Proof. intros (? & ? & ? & ? & ? & ? & ? & ?). inv H. inv H0. assert (nth_error (bsm_addstacks m P) (length x0) = Some x1). 1: rewrite H4. 1: rewrite nth_error_app2. 2:lia. 1: rewrite Nat.sub_diag. 1: reflexivity. unfold bsm_addstacks in H. destruct (nth_error_Some P (|x0|)) as [_ HH]. destruct (nth_error P (|x0|)) as [d | ] eqn:E. 2:{ exfalso. eapply HH; try reflexivity. erewrite <- (map_length _ P). unfold bsm_addstacks in H4. rewrite H4. rewrite app_length. cbn. lia. } pose proof (E' := E). eapply map_nth_error in E. unfold bsm_addstacks in H4. rewrite H4 in E. rewrite nth_error_app2 in E. 2:lia. rewrite Nat.sub_diag in E. cbn in E. inv E. eapply BSM_addstacks_step_bwd in H1 as (? & ? & ? & ?). subst. repeat eexists; eauto. 1: f_equal. 1: instantiate (2 := firstn (length x0) P). 1: instantiate (1 := skipn (1 + length x0) P). 2:{ f_equal. rewrite firstn_length. enough (|x0| < |P|). 1: lia. eapply nth_error_Some. now rewrite E'. } rewrite <- (firstn_skipn (length x0) P) at 1. f_equal. clear - H4. induction x0 in P, H4 |- *. - cbn in *. destruct P; inv H4. destruct b, d; inv H0; eapply pos_right_inj in H1; subst; reflexivity. - destruct P; cbn in *; inv H4. now rewrite IHx0. 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)