proposition: Theorem FRACTRAN_ALT_HALTING_HALTING : FRACTRAN_ALT_HALTING ⪯ Halt_FRACTRAN.
proof: Proof. exists f; intros (n & P & v). rewrite Halt_FRACTRAN_iff. simpl. firstorder. 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