fact: Definition ra_compiler_stm n f := forall i p o m, o < m -> ~ p <= o < n+p -> n+p <= m -> @ra_compiler_spec n f i p o m.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils finite pos vec subcode sss) Undecidability.MinskyMachines(env mme_defs mme_utils) Undecidability.MuRec.Util(recalg)