proposition: Lemma finalization v w n m : (1, P') // (S (length P), Vector.append (n ## v) (Vector.append w (m ## vec_nil))) ->> (5 + length P, Vector.append ((n+m) ## v) (Vector.append w (0 ## vec_nil))).
proof: Proof. exists (2+m*2+1). econstructor. { eexists 1, _, _, _, _. split; [reflexivity|split]. - rewrite map_length. reflexivity. - by constructor. } econstructor. { eexists 1, (map shift_instr P ++ [INC F1']), _, _, _. rewrite -app_assoc. split; [reflexivity|split]. - rewrite app_length map_length /=. congr pair. lia. - apply: in_mma_sss_dec_1'; [done..|]. by rewrite !vec_app_eq !vec_pos_app_right !vec_change_app_right !vec_pos_app_right. } rewrite -/(Nat.add _ _). rewrite !vec_app_eq !vec_pos_app_right !vec_change_app_right /=. elim: m n. { move=> n. rewrite Nat.add_0_r. econstructor; [|econstructor]. eexists 1, (map shift_instr P ++ [_; _; _]), _, _, _. rewrite -app_assoc. split; [reflexivity|split]. - rewrite app_length map_length /=. congr pair. lia. - apply: in_mma_sss_dec_0'; [done..|]. by rewrite (vec_pos_app_right (n ## v)) vec_pos_app_right. } move=> m IH n. econstructor. { eexists 1, (map shift_instr P ++ [_; _; _]), _, _, _. rewrite -app_assoc. split; [reflexivity|split]. - rewrite app_length map_length /=. congr pair. lia. - apply: in_mma_sss_dec_1'; [done..|]. by rewrite (vec_pos_app_right (n ## v)) vec_pos_app_right. } econstructor. { eexists 1, (map shift_instr P ++ [_; _]), _, _, _. rewrite -app_assoc. split; [reflexivity|split]. - rewrite app_length map_length /=. congr pair. lia. - by apply: in_mma_sss_inc'. } have := IH (S n). rewrite -(Nat.add_succ_comm n m). congr sss_steps. congr pair. by rewrite vec_change_F1' -!vec_app_eq. Qed.
imports: Undecidability(TM.TM) Undecidability.MinskyMachines(MM MMA MMA.mma_defs Util.MMA_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) List PeanoNat Lia Relations ssreflect