fact: Definition mm_copy i := mm_erase dst zero i ++ mm_transfert src tmp zero (2+i) ++ mm_dup tmp src dst zero (5+i).
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines.MMenv(env mme_defs)