fact: Definition mm_var_map (X Y : Set) (f : X -> Y) (i : mm_instr X) := match i with | INC x => INC (f x) | DEC x p => DEC (f x) p end.
imports: List Arith Lia Max Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines(env mm_defs mme_defs mme_utils) Undecidability.MuRec.Util(recalg ra_mm_env)