proposition: Fact mma_mod_cst_divides_progress v a st : v#>x = a*k -> st = (p,v[0/x][((v#>x)+(v#>t))/t]) -> (i,mma_mod_cst) // (i,v) -+> st.
proof: Proof. Proof using Hxt Hk. intros H1 ?; subst st. apply sss_compute_progress_trans with (i,v[0/x][((v#>x)+(v#>t))/t]). + apply mma_mod_cst_spec_1 with (a := a) (b := 0); try lia. rewrite <- H1; auto. + apply mma_mod_cst_spec_0; rew vec. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)