proposition: Corollary mm_div2_progress_0 v k st : v#>quo = 0 -> v#>rem = 0 -> div2 (v#>src) = (k,false) -> st = (6+i,v[0/src][k/quo][0/rem]) -> (i,mm_div2) // (i,v) -+> st.
proof: Proof. Proof using Hsr Hsq Hqr. intros H2 H3 H4 ?; subst. generalize (mm_div2_progress _ H2 H3). rewrite H4; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs)