proposition: Lemma PREP2_spec'' k (Σ : finType) (x : pos k) i s b : { PREP2 : list (bsm_instr ((1 + k) + 4)) | length PREP2 = 2 + (length (strpush_common_short s b)) + length ((strpush_succ s b)) /\ forall v : Vector.t (list bool) k, forall n, forall t : Vector.t (tape Σ) n, forall m m', v @[x] = repeat true m -> (i, PREP2) // (i, Vector.append ([] ::: v) ((@encode_bsm Σ _ (encNatTM s b m' ::: t)))) ->> (i + length PREP2, Vector.append ([] ::: vec_change v x nil) ((@encode_bsm Σ _ (encNatTM s b (m + m') ::: t)))) }.
proof: Proof. exists (POP (pos_left 4 (pos_right 1 x)) 0 (i + 2 + (length (strpush_common_short s b)) + length ((strpush_succ s b))) :: pop_many (pos_right (1 + k) Fin2) (length (strpush_common_short s b)) (1 + i) ++ push_exactly (pos_right (1 + k) Fin2) (strpush_succ s b) ++ POP (pos_left 4 Fin0) 0 i :: nil). split. { cbn. rewrite !app_length. cbn. rewrite pop_many_length, push_exactly_length. lia. } intros v n t m m' Hx. induction m in v, m', Hx |- *. - bsm sss POP empty with (pos_left 4 (pos_right 1 x)) 0 (i + 2 + (length (strpush_common_short s b)) + length ((strpush_succ s b))). 1: rewrite <- !vec_app_spec, vec_pos_app_left. 1: cbn in *. 1: rewrite vec_pos_spec, Hx. 1: reflexivity. bsm sss stop. apply f_equal2. 1: { cbn. rewrite !app_length, pop_many_length, push_exactly_length. cbn. lia. } cbn in Hx. rewrite <- Hx. now rewrite <- vec_pos_spec, vec_change_same. - bsm sss POP one with (pos_left 4 (pos_right 1 x)) 0 (i + 2 + (length (strpush_common_short s b)) + length ((strpush_succ s b))) (repeat true m). 1:{ rewrite <- !vec_app_spec, vec_pos_app_left. cbn. rewrite vec_pos_spec, Hx. reflexivity. } eapply subcode_sss_compute_trans. 2: eapply (pop_many_spec (pos_right (1 + k) Fin2) (length (strpush_common_short s b)) (1 + i)). 1:auto. eapply subcode_sss_compute_trans. 2: eapply (push_exactly_spec (pos_right (1 + k) Fin2) _ (strpush_succ s b)). { eexists (POP _ _ _ :: pop_many _ _ _), ([POP _ _ _]). split. 1: reflexivity. cbn; rewrite pop_many_length. lia. } bsm sss POP empty with (pos_left 4 Fin0) 0 i. { eexists (POP _ _ _ :: pop_many _ _ _ ++ push_exactly _ _), []. cbn. simpl_list. split. 1: reflexivity. rewrite pop_many_length, push_exactly_length. lia. } specialize IHm with (m' := (S m')). replace (S m + m') with (m + S m') by lia. 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 : Vector.t (list bool) ((1 + k) + 4)); enough (st = ev) as ->; subst ev end. 1: eapply IHm with (v := vec_change v x (repeat true m)). 1: now rewrite <- vec_pos_spec, vec_change_eq. 1: now rewrite vec_change_idem. rewrite <- !vec_app_spec. eapply vec_pos_ext. eapply pos_left_right_rect. + symmetry. rewrite vec_pos_app_left. rewrite vec_change_neq; auto. rewrite vec_change_neq; auto. cbn in p. eapply (Fin.caseS' p); clear p. 1: reflexivity. intros p. destruct (pos_eq_dec p x). * rewrite vec_change_eq. 2: now subst. cbn. subst. now rewrite vec_change_eq. * rewrite vec_change_neq. 2: intros ? % pos_left_inj % pos_nxt_inj; auto. rewrite vec_pos_app_left. cbn. rewrite vec_change_neq; auto. + intros p. symmetry. rewrite !vec_pos_app_right. symmetry. rewrite !vec_change_idem. revert p. apply Fin4_cases. * repeat (rewrite vec_change_neq; [ | intros ? % pos_right_inj; congruence]). rewrite vec_change_neq; [ | eapply pos_right_left]. rewrite vec_pos_app_right. now rewrite !vec_pos_spec, !encode_bsm_at0. * rewrite vec_change_neq; [ | intros ? % pos_right_inj % pos_nxt_inj; congruence]. rewrite vec_change_neq; [ | auto]. now rewrite vec_pos_app_right, !vec_pos_spec, !encode_bsm_at1. * rewrite vec_change_eq; auto. rewrite vec_change_eq; auto. rewrite vec_change_neq; auto. rewrite vec_pos_app_right. now rewrite !vec_pos_spec, encode_bsm_succ. * rewrite vec_change_neq; [ | intros ? % pos_right_inj % pos_nxt_inj % pos_nxt_inj; congruence]. rewrite vec_change_neq; [ | auto]. now rewrite vec_pos_app_right, !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)