proposition: Theorem MUREC_MM_HALTING : MUREC_HALTING ⪯ MM_HALTING.
proof: Proof. exists f; unfold f. intros g; simpl; unfold MUREC_HALTING, MM_HALTING. destruct (ra_mm_simulator g) as (m & P & H); simpl. rewrite H, vec_app_nil; tauto. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Shared.Libs.DLW(pos vec sss) Undecidability.MinskyMachines(MM MM_sss) Undecidability.MuRec.Util(recalg ra_simul)