fact: Definition mm_recognisable_n := { m & { M : list (mm_instr (pos (n+m))) | forall v, P v <-> (1,M) /MM/ (1,vec_app v vec_zero) ↓ } }.
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)