proposition: Theorem DPRM_n n (R : vec nat n -> Prop) : (mm_recognisable_n R -> dio_rec_form_n R) * (dio_rec_form_n R -> dio_rec_elem_n R) * (dio_rec_elem_n R -> dio_rec_single_n R) * (dio_rec_single_n R -> mu_recursive_n R) * (mu_recursive_n R -> mm_recognisable_n R).
proof: Proof. lsplit 4; 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)