proposition: Theorem MM_FRACTRAN_ALT_HALTING : Halt_MM ⪯ FRACTRAN_ALT_HALTING.
proof: Proof. exists f; intros (n & P & v). setoid_rewrite Halt_MM_iff. simpl. destruct (mm_fractran_n P) as (l & H1 & H2); simpl; auto. Qed.
imports: Undecidability.Shared.Libs.DLW(pos vec sss) Undecidability.MinskyMachines(mm_defs) Undecidability.FRACTRAN(FRACTRAN fractran_utils mm_fractran prime_seq FRACTRAN_sss) Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts