proposition: Lemma PREPMORE'_spec i x (w : Vector.t nat k) n'' n' : forall E : n'' + n' = n, forall H, (i, PREPMORE' n'' H) /MM/ (i, Vector.append (Vector.append (x ## w) (Vector.const 0 n)) (0 ## 0 ## 0 ## vec_nil)) ~~> (i + n'', Vector.append (Vector.append (x ## w) (Vector.cast (Vector.append (Vector.const 1 n'') (Vector.const 0 n')) E)) (0 ## 0 ## 0 ## vec_nil)).
proof: Proof. intros E Hle. split. 2:{ cbn. rewrite PREPMORE'_length. lia. } revert n' E Hle. induction n''; intros n' E Hle. - cbn [PREPMORE']. mm sss stop. f_equal. 1: lia. 1: repeat f_equal. cbn. destruct E. now rewrite cast_eq_refl. - cbn [PREPMORE']. eapply subcode_sss_compute_trans with (P := (i, PREPMORE' n'' (PREPMORE'_subproof n'' Hle))). 1: auto. { eapply IHn''. } mm sss INC with (pos_left 3 (pos_right (1 + k) (Fin.of_nat_lt (PREPMORE'_subproof0 n'' Hle)))). { eexists. eexists. split. 1: reflexivity. now rewrite PREPMORE'_length. } mm sss stop. f_equal. 1: lia. rewrite <- !vec_app_spec. rewrite !vec_pos_app_left. rewrite !vec_pos_app_right. eapply vec_list_inj. rewrite vec_list_vec_change. rewrite !vec_list_vec_app. rewrite pos_left_spec. rewrite Fin.L_sanity. rewrite pos_right_spec. rewrite Fin.R_sanity. rewrite Fin.to_nat_of_nat. cbn [proj1_sig plus]. rewrite update_app_left. 2:{ rewrite !app_length, !vec_list_length. lia. } f_equal. rewrite update_app_right. 2:{ cbn. rewrite !vec_list_length. lia. } f_equal. rewrite vec_list_length. replace (S (k + n'') - S k) with n'' by lia. rewrite !vec_list_cast. rewrite !vec_list_vec_app. rewrite update_app_right. 2:{ cbn. rewrite !vec_list_length. lia. } rewrite (@vec_list_vec_app nat (S n'') n'). replace (S n'') with (n'' + 1) by lia. rewrite vec_list_length. rewrite Nat.sub_diag. instantiate (2 := 1 + n'). cbn. rewrite !vec_list_const. rewrite repeat_app. cbn. rewrite <- !app_assoc. f_equal. cbn. f_equal. f_equal. eapply nth_error_vec_list. rewrite vec_list_cast, !vec_list_vec_app; cbn. rewrite nth_error_app2. 2: rewrite vec_list_length; lia. now rewrite vec_list_length, Nat.sub_diag. 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)