proposition: Fact mma_fractran_one_nok_progress v : ~ divides q (p*(v#>src)) -> v#>dst = 0 -> (i0,mma_fractran_one) //ₐ (i0,v) -+> (length mma_fractran_one+i0,v).
proof: Proof. Proof using Hq. rewrite mma_fractran_one_length. intros H1 H2; unfold mma_fractran_one. rewrite divides_rem_eq in H1. revert H1. generalize (div_rem_spec1 (p*(v#>src)) q) (div_rem_spec2 (p*(v#>src)) Hq). generalize (div (p*(v#>src)) q) (rem (p*(v#>src)) q); intros x y H3 H4 H5. apply sss_progress_trans with (i1,v[0/src][(x*q+y)/dst]). { apply subcode_sss_progress with (P := (i0,mma_mult_cst src dst p i0)); auto. apply mma_mult_cst_progress; auto. rewrite H2, <- H3; do 2 f_equal; lia. } apply sss_progress_trans with (i5,v[(p*(v#>src))/src][0/dst]). { apply subcode_sss_progress with (P := (i1,mma_mod_cst dst src i2 i5 q i1)); auto. apply mma_mod_cst_not_divides_progress with x y; rew vec; try lia. f_equal; apply vec_pos_ext; intros c; dest c dst; try lia; dest c src; lia. } apply sss_progress_trans with (i6,v[0/src][(v#>src)/dst]). { apply subcode_sss_progress with (P := (i5,mma_div_cst src dst p i5)); auto. apply mma_div_cst_progress with (v#>src); auto; rew vec; try lia; try ring. f_equal; try lia. apply vec_pos_ext; intros c; dest c dst; try lia; dest c src. } apply subcode_sss_progress with (P := (i6,mma_transfert dst src i6)); auto. apply mma_transfert_progress; auto. f_equal; try lia. apply vec_pos_ext; intros c; dest c dst; try lia; dest c 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)