proposition: Fact mma_div2_branch_progress v st : let (k,b) := div2 (v#>x) in st = (if b then j1 else j0,v[0/x][(k+(v#>q))/q]) -> (i,mma_div2_branch) // (i,v) -+> st.
proof: Proof. Proof using Hxq. generalize (div2_spec (v#>x)). destruct (div2 (v#>x)) as (k,[]); intros Hv ->. + apply mma_div2_branch_2k1 with k; auto. + apply mma_div2_branch_2k with k; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs mma_utils)