proposition: Fact mma_decs_copy_lt_progress k i v st : v#>dst < k -> st = (q,v[0/dst][((v#>dst)+(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_lt; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)