proposition: Fact mm_div2_progress v : v#>quo = 0 -> v#>rem = 0 -> let (k,b) := div2 (v#>src) in (i,mm_div2) // (i,v) -+> (6+i,v[0/src][k/quo][(if b then 1 else 0)/rem]).
proof: Proof. Proof using Hsr Hsq Hqr. intros H2 H3. generalize (div2_spec (v#>src)). destruct (div2 (v#>src)) as (k,[]); intros H4. apply mm_div2_spec_1 with k; auto. lia. apply vec_pos_ext; intros p. dest p rem; dest p quo; lia. apply mm_div2_spec_0 with k; auto. apply vec_pos_ext; intros p. dest p rem; dest p quo; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs)