proposition: Fact mma_div_branch_1_progress v st : v#>z = 0 -> 0 < k -> ~ divides k (v#>x) -> st = (16+7*k+i,v) -> (i, mma_div_branch) // (i,v) -+> st.
proof: Proof. Proof using Hxz. intros H1 H2 H3 ->; unfold mma_div_branch. destruct (div_full (v#>x) k) as (a & r & H5 & H6). assert (0 < r < k) as H7. 1:{ split; destruct r; try lia. destruct H3; exists a; lia. } apply sss_progress_trans with (st2 := (q,v[0/x][(v#>x)/z])). 1:{ apply subcode_sss_progress with (P := (i,MOD_CSTₐ x z p q k i)); auto. apply mma_mod_cst_not_divides_progress with (3 := H5); auto. do 2 f_equal; lia. } 1:{ apply subcode_sss_progress with (P := (q,TRANSFERTₐ z x q)); auto. apply mma_transfert_progress; auto. f_equal; rew vec. apply vec_pos_ext; intros y. dest y x; dest y z. } Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)