proposition: Lemma PREP_spec_strong i x w k'' k' v1 v2 v : forall E : k'' + k' = k, v = (Vector.cast (Vector.append v1 v2) E) -> x = 0 -> forall H, (i, PREP' k'' H i) /MM/ (i, Vector.append (Vector.append (x ## v) w) (0 ## 0 ## 0 ## vec_nil)) ~~> (i + (k'' * 14), Vector.append (Vector.append (x ## (Vector.cast (Vector.append (Vector.map (fun n => stack_enc (List.repeat true n)) v1) v2) E)) w) (0 ## 0 ## 0 ## vec_nil)).
proof: Proof. intros E -> -> Hle. split. 2:{ cbn. rewrite PREP'_length. right. lia. } revert i v1 k' Hle E v2. induction k'' as [ | k'' ]; intros i v1 k' Hle E v2. - cbn. mm sss stop. f_equal. 1: lia. revert v1. eapply Vector.case0. cbn. reflexivity. - cbn [PREP']. edestruct (vector_inv_back v1) as [(x, v1l) Hv1]. assert (H1 : k'' <= k) by lia. assert (H2 : k'' + S k' = k) by lia. specialize (IHk'' i v1l (S k') (PREP'_subproof k'' Hle) H2 (x ## v2)). eapply subcode_sss_compute_trans with (P := (i, PREP' k'' (PREP'_subproof k'' Hle) i)). 1: auto. 1: match type of IHk'' with sss_compute _ _ (_, ?st) _ => evar (Vector.t nat (1 + k + n + 3)); enough (Eq : st = t) end; subst t. 1: rewrite Eq in IHk''. 1: eapply IHk''. { rewrite Hv1. repeat f_equal. eapply vec_list_inj. rewrite !vec_list_cast, <- !vec_app_spec, !vec_list_vec_app. rewrite vec_list_cast. rewrite vec_list_vec_app. cbn. now rewrite <- app_assoc. } replace (14 * k'' + i) with (i + k'' * 14) by lia. eapply subcode_sss_compute_trans with (P := (i + k'' * 14, prep (Fin.of_nat_lt (PREP'_subproof0 k'' Hle)) (i + k'' * 14))). { eexists. eexists. split. 1: reflexivity. rewrite PREP'_length. lia. } 1: eapply prep_spec. + reflexivity. + cbn. rewrite <- !vec_app_spec. rewrite vec_pos_app_right. reflexivity. + cbn. rewrite <- !vec_app_spec. rewrite vec_pos_app_right. reflexivity. + cbn. rewrite <- !vec_app_spec. rewrite !vec_pos_app_left. reflexivity. + mm sss stop. f_equal. 1:lia. rewrite <- !vec_app_spec. eapply vec_list_inj. rewrite vec_list_vec_change. rewrite !(@vec_list_vec_app nat (1 + k + n) 3). rewrite !vec_list_vec_app. cbn [vec_list]. rewrite !vec_list_cast. rewrite !vec_list_vec_app. cbn [vec_list]. rewrite !vec_list_vec_map. rewrite Hv1. rewrite vec_list_cast. rewrite <- !vec_app_spec. rewrite !vec_list_vec_app. cbn [vec_list]. clear. fold plus. rewrite pos_left_spec. pose proof (@Fin.L_sanity (S (k + n)) 3). cbn in H. rewrite H. clear H. rewrite pos_left_spec. pose proof (@Fin.L_sanity (S (k)) n). cbn in H. rewrite H. clear H. rewrite pos_right_spec. pose proof (@Fin.R_sanity k 1 ). cbn [plus] in H. rewrite H. clear H. rewrite Fin.to_nat_of_nat. cbn [proj1_sig update app]. f_equal. rewrite map_app. cbn [map]. rewrite <- !pos_left_spec. rewrite update_app_left. 2:{ simpl_list. rewrite vec_list_length. cbn. lia. } rewrite update_app_left. 2:{ simpl_list. rewrite vec_list_length. cbn. lia. } rewrite update_app_right. 2:{ simpl_list. rewrite vec_list_length. cbn. lia. } simpl_list. rewrite vec_list_length. rewrite Nat.sub_diag. cbn [update]. f_equal. f_equal. rewrite <- !app_assoc. f_equal. cbn [app]. f_equal. f_equal. f_equal. rewrite (@vec_pos_app_left nat (add (S k) n) 3). rewrite <- pos_left_spec. rewrite (@vec_pos_app_left nat (S k) n). rewrite <- pos_right_spec. cbn [pos_right]. cbn. eapply nth_error_vec_list. rewrite vec_list_cast, !vec_list_vec_app. rewrite nth_error_app2; rewrite vec_list_length. 2: lia. rewrite Nat.sub_diag. reflexivity. Unshelve. lia. Qed.
imports: Undecidability.MinskyMachines(MM_computable MM_sss mm_utils) Undecidability.StackMachines(BSM_computable) Undecidability.Shared.Libs.DLW(vec pos sss subcode) Lia Vector Nat Arith List Undecidability.MinskyMachines.MM(mm_defs mm_utils mm_comp_strong)