proposition: Fact mma_div_branch_0_progress a v st : v#>z = 0 -> 0 < k -> v#>x = a*k -> st = (j,v[a/x]) -> (i, mma_div_branch) // (i,v) -+> st.
proof: Proof. Proof using Hxz. intros H1 H2 H3 ->; unfold mma_div_branch. apply sss_progress_trans with (st2 := (p,v[0/x][(a*k)/z])). 1:{ apply subcode_sss_progress with (P := (i,MOD_CSTₐ x z p q k i)); auto. apply mma_mod_cst_divides_progress with a; auto. do 2 f_equal; lia. } apply sss_progress_trans with (st2 := (11+7*k+i,v[a/x])). 1:{ apply subcode_sss_progress with (P := (p,DIV_CSTₐ z x k p)); auto. apply mma_div_cst_progress with a; auto; rew vec. unfold p. f_equal; try lia. apply vec_pos_ext; intros y. dest y x; dest y z. } 1:{ apply subcode_sss_progress with (P := (11+7*k+i,JUMPₐ j z)); auto. apply mma_jump_progress; auto. } Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)