proposition: Lemma PREP3_spec k n Σ i : { PREP3 | forall v : Vector.t (list bool) k, forall t : Vector.t _ n, (i, PREP3) // (i, v +++ @encode_bsm Σ _ t) ->> (i + length PREP3, v +++ (@encode_bsm Σ _ (niltape ::: t))) }.
proof: Proof. edestruct (@encode_bsm_nil Σ n) as ([str n'] & H). exists (pop_many (pos_right k Fin2) n' i ++ push_exactly (pos_right k Fin2) str). intros v t. eapply subcode_sss_compute_trans with (P := (i, pop_many (pos_right k Fin2) n' i)). 1: auto. 1: eapply pop_many_spec. eapply subcode_sss_compute_trans with (P := (n' + i, push_exactly (pos_right k Fin2) str)). { exists (pop_many (pos_right k Fin2) n' i), []. split. 1: now rewrite app_nil_r. rewrite pop_many_length; lia. } 1: eapply push_exactly_spec. bsm sss stop. f_equal. 1: rewrite app_length, pop_many_length, push_exactly_length; lia. rewrite !vec_change_idem. rewrite vec_change_eq; auto. rewrite <- !vec_app_spec. rewrite vec_pos_app_right. eapply vec_pos_ext. eapply pos_left_right_rect. - intros p. rewrite vec_pos_app_left. rewrite vec_change_neq; auto. now rewrite vec_pos_app_left. - eapply Fin4_cases. + rewrite !vec_pos_app_right. rewrite vec_change_neq; [ | intros ? % pos_right_inj; congruence]. rewrite vec_pos_app_right. now rewrite !vec_pos_spec, !encode_bsm_at0. + rewrite !vec_pos_app_right. rewrite vec_change_neq; [ | intros ? % pos_right_inj % pos_nxt_inj; congruence]. rewrite vec_pos_app_right. now rewrite !vec_pos_spec, !encode_bsm_at1. + rewrite !vec_pos_app_right. rewrite vec_change_eq; auto. now rewrite !vec_pos_spec, H. + rewrite !vec_pos_app_right. rewrite vec_change_neq; [ | intros ? % pos_right_inj % pos_nxt_inj % pos_nxt_inj; congruence]. rewrite vec_pos_app_right. now rewrite !vec_pos_spec, !encode_bsm_at3. 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)