proposition: Fact mma_decs_copy_le_progress k i v st : k <= v#>dst -> st = (p,v[((v#>dst)-k)/dst][(k+(v#>tmp))/tmp]) -> (i,mma_decs_copy k i) // (i,v) -+> st.
proof: Proof. Proof using Hdt. intros H1 ?; subst st. apply mma_decs_copy_spec_le; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)