proposition: Theorem FRACTRAN_REG_MMA2_HALTS_ON_ZERO : FRACTRAN_REG_HALTING ⪯ MMA2_HALTS_ON_ZERO.
proof: Proof. exists f; intros (? & ? & ?); simpl. now apply fractran_reg_mma0_reductions. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Shared.Libs.DLW(pos vec sss) Undecidability.FRACTRAN(FRACTRAN FRACTRAN_sss) Undecidability.MinskyMachines(mma_defs fractran_mma)