proposition: Theorem DPRM_1 (P : nat -> Prop) : (mm_recognisable P -> fractran_recognisable P) * (fractran_recognisable P -> dio_rec_single P) * (dio_rec_single P -> mu_recursive P) * (mu_recursive P -> mm_recognisable P).
proof: Proof. lsplit 3; auto. Qed.
imports: List Arith Undecidability.Shared.Libs.DLW(utils_tac utils_list sums pos vec subcode sss) Undecidability.MinskyMachines(mm_defs) Undecidability.FRACTRAN(FRACTRAN mm_fractran prime_seq FRACTRAN_sss) Undecidability.H10.Fractran(fractran_dio) Undecidability.H10.Dio(dio_logic dio_elem dio_single) Undecidability.MuRec.Util(recalg ra_utils recomp ra_recomp ra_dio_poly ra_mm ra_simul)