proposition: Fact mma_fractran_one_ok_progress k v : k*q = p*(v#>src) -> v#>dst = 0 -> (i0,mma_fractran_one) //ₐ (i0,v) -+> (j,v[k/src]).
proof: Proof. Proof using Hq. intros H1 H2; unfold mma_fractran_one. apply sss_progress_trans with (i1,v[0/src][(k*q)/dst]). { apply subcode_sss_progress with (P := (i,mma_mult_cst src dst p i)); auto. apply mma_mult_cst_progress; auto. rewrite H2, <- H1; do 2 f_equal; lia. } apply sss_progress_trans with (i2,v[(k*q)/src][0/dst]). { apply subcode_sss_progress with (P := (i1,mma_mod_cst dst src i2 i5 q i1)); auto. apply mma_mod_cst_divides_progress with k; rew vec; try lia. f_equal; apply vec_pos_ext; intros y; dest y dst; try lia; dest y src. } apply sss_progress_trans with (i3,v[0/src][k/dst]). { apply subcode_sss_progress with (P := (i2,mma_div_cst src dst q i2)); auto. apply mma_div_cst_progress with k; auto; rew vec; try lia. f_equal; try lia. apply vec_pos_ext; intros y; dest y dst; try lia; dest y src. } apply sss_progress_trans with (i4,v[k/src][0/dst]). { apply subcode_sss_progress with (P := (i3,mma_transfert dst src i3)); auto. apply mma_transfert_progress; auto. f_equal; try lia. apply vec_pos_ext; intros y; dest y dst; try lia; dest y src. } apply sss_progress_compute_trans with (j,v[k/src][0/dst]). { apply subcode_sss_progress with (P := (i4,JUMPₐ j dst)); auto. apply mma_jump_progress; auto. } mma sss stop; f_equal. apply vec_pos_ext; intros y; dest y dst; try lia; dest y src. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs mma_utils) Undecidability.FRACTRAN(FRACTRAN fractran_utils)