proposition: Lemma PREP2_spec' k (Σ : finType) (x : pos k) i s b n : { PREP2 : list (bsm_instr ((1 + k) + 4)) | length PREP2 = PREP2''_length s b /\ forall v : Vector.t (list bool) k, forall t : Vector.t (tape Σ) n, forall m, v @[x] = repeat true m -> (i, PREP2) // (i, Vector.append ([] ::: v) ((@encode_bsm Σ _ t))) ->> (i + length PREP2, Vector.append ([] ::: vec_change v x nil) ((@encode_bsm Σ _ (encNatTM s b m ::: t)))) }.
proof: Proof. unfold PREP2''_length. destruct (encode_bsm_zero s b) as [n' Hn']. destruct (PREP2_spec'' x (i + n' + length (strpush_zero s b)) s b) as [PREP2 [Hl2 H]]. exists (pop_many (pos_right (1 + k) Fin2) n' i ++ push_exactly (pos_right (1 + k) Fin2) (strpush_zero s b) ++ PREP2). split. { cbn. rewrite !app_length, pop_many_length, push_exactly_length. cbn in Hl2. lia. } intros v t m Hm. eapply subcode_sss_compute_trans. 2: eapply (pop_many_spec (pos_right (1 + k) Fin2) n' i). 1:auto. eapply subcode_sss_compute_trans. 2: eapply (push_exactly_spec (pos_right (1 + k) Fin2) _ (strpush_zero s b)). { eexists (pop_many _ _ _), PREP2. split. 1: reflexivity. rewrite pop_many_length. lia. } specialize H with (m' := 0) (v := v) (1 := Hm). replace (m + 0) with m in H by lia. eapply subcode_sss_compute_trans. 2:{ match goal with [ |- sss_compute _ _ (_, ?st) _ ] => evar (ev : Vector.t (list bool) ((1 + k) + 4)); enough (st = ev) as ->; subst ev end. 1: match goal with [ |- sss_compute _ _ (?st, _) _ ] => evar (ev : nat); enough (st = ev) as ->; subst ev end. - eapply H. - rewrite push_exactly_length. lia. - eapply vec_pos_ext. eapply pos_left_right_rect. + intros p. rewrite <- !vec_app_spec, !vec_pos_app_left. rewrite vec_change_neq; auto. rewrite vec_change_neq; auto. now rewrite vec_pos_app_left. + rewrite <- !vec_app_spec. eapply Fin4_cases. * rewrite vec_change_neq; [ | intros ? % pos_right_inj; congruence]. rewrite vec_change_neq; [ | intros ? % pos_right_inj; congruence]. rewrite !vec_pos_app_right. rewrite !vec_pos_spec. now rewrite !encode_bsm_at0. * rewrite vec_change_neq; [ | intros ? % pos_right_inj % pos_nxt_inj; congruence]. rewrite vec_change_neq; [ | intros ? % pos_right_inj % pos_nxt_inj; congruence]. now rewrite !vec_pos_app_right, !vec_pos_spec, !encode_bsm_at1. * rewrite vec_change_eq; auto. rewrite vec_change_eq; eauto. rewrite !vec_pos_app_right. now rewrite !vec_pos_spec, Hn'. * 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 % pos_nxt_inj; congruence]. now rewrite !vec_pos_app_right, !vec_pos_spec, !encode_bsm_at3. } { eexists (pop_many _ _ _ ++ push_exactly _ _), []. rewrite app_nil_r. split. 1: now simpl_list. rewrite app_length, pop_many_length, push_exactly_length. lia. } bsm sss stop. apply f_equal2; [|reflexivity]. rewrite !app_length, pop_many_length, push_exactly_length. lia. 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)