proposition: Lemma PREP1_spec k Σ n : { PREP1 : list (bsm_instr ((1 + k) + 4)) | forall v : Vector.t nat k, (0, PREP1) // (0, Vector.append ([] ::: Vector.map (fun n0 : nat => repeat true n0) v) (Vector.const [] 4)) ->> (length PREP1, Vector.append ([] ::: Vector.map (fun n0 : nat => repeat true n0) v) ((@encode_bsm Σ _ (Vector.const niltape n)))) }.
proof: Proof. exists (push_exactly (pos_right (1 + k) Fin0) ((@encode_bsm Σ _ (Vector.const niltape n))@[Fin0]) ++ push_exactly (pos_right (1 + k) Fin1) ((@encode_bsm Σ _ (Vector.const niltape n))@[Fin1]) ++ push_exactly (pos_right (1 + k) Fin2) ((@encode_bsm Σ _ (Vector.const niltape n))@[Fin2]) ++ push_exactly (pos_right (1 + k) Fin3) ((@encode_bsm Σ _ (Vector.const niltape n))@[Fin3])). intros v. eapply subcode_sss_compute_trans. 2: eapply (push_exactly_spec (pos_right (1 + k) Fin0) 0 ((@encode_bsm Σ _ (Vector.const niltape n))@[Fin0])). 1:auto. eapply subcode_sss_compute_trans. 2: eapply (push_exactly_spec (pos_right (1 + k) Fin1) _ ((@encode_bsm Σ _ (Vector.const niltape n))@[Fin1])). 1:auto. eapply subcode_sss_compute_trans. 2: eapply (push_exactly_spec (pos_right (1 + k) Fin2) _ ((@encode_bsm Σ _ (Vector.const niltape n))@[Fin2])). 1:auto. eapply subcode_sss_compute_trans. 2: eapply (push_exactly_spec (pos_right (1 + k) Fin3) _ ((@encode_bsm Σ _ (Vector.const niltape n))@[Fin3])). 1:auto. bsm sss stop. apply f_equal2. 1:rewrite !app_length; lia. eapply vec_pos_ext. eapply pos_left_right_rect. - rewrite <- !vec_app_spec. symmetry. rewrite vec_pos_app_left. rewrite !vec_change_neq; auto. now rewrite vec_pos_app_left. - rewrite <- !vec_app_spec. rewrite !vec_pos_app_right. intros p; eapply (Fin.caseS' p); clear p. 1:{ repeat (rewrite vec_change_neq; [ | intros ? % pos_right_inj; congruence]). rewrite vec_change_eq; [ | auto]. rewrite vec_pos_app_right. now rewrite vec_pos_const, app_nil_r, vec_pos_spec. } intros p; eapply (Fin.caseS' p); clear p. 1:{ rewrite vec_change_neq; [ | intros ? % pos_right_inj % pos_nxt_inj; congruence]. rewrite vec_change_neq; [ | intros ? % pos_right_inj % pos_nxt_inj; congruence]. rewrite vec_change_eq; [ | auto]. rewrite vec_pos_app_right. rewrite vec_pos_const. rewrite vec_change_neq; [ | intros ? % pos_right_inj; congruence]. rewrite vec_pos_app_right. now rewrite vec_pos_const, app_nil_r, vec_pos_spec. } intros p; eapply (Fin.caseS' p); clear p. 1:{ rewrite vec_change_neq; [ | intros ? % pos_right_inj % pos_nxt_inj % pos_nxt_inj; congruence]. rewrite vec_change_eq; [ | auto]. rewrite vec_pos_app_right. rewrite vec_pos_const. rewrite vec_change_neq; [ | intros ? % pos_right_inj % pos_nxt_inj; congruence]. rewrite vec_change_neq; [ | intros ? % pos_right_inj; congruence]. rewrite vec_pos_app_right. now rewrite vec_pos_const, app_nil_r, vec_pos_spec. } intros p; eapply (Fin.caseS' p); clear p. 1:{ rewrite vec_change_eq; [ | auto]. rewrite vec_pos_app_right. rewrite vec_pos_const. rewrite vec_change_neq; [ | intros ? % pos_right_inj % pos_nxt_inj % pos_nxt_inj; congruence]. rewrite vec_change_neq; [ | intros ? % pos_right_inj % pos_nxt_inj; congruence]. rewrite vec_change_neq; [ | intros ? % pos_right_inj; congruence]. rewrite vec_pos_app_right. now rewrite vec_pos_const, app_nil_r, vec_pos_spec. } apply Fin.case0. 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)