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