proposition: Theorem PCP_chain_ILL : PCP ⪯ PCPb /\ PCPb ⪯ iPCPb /\ iPCPb ⪯ Halt_BSM /\ Halt_BSM ⪯ MM_HALTS_ON_ZERO /\ MM_HALTS_ON_ZERO ⪯ EILL_PROVABILITY /\ EILL_PROVABILITY ⪯ ILL_PROVABILITY.
proof: Proof. msplit 5. + apply PCP_to_PCPb.reduction. + apply PCPb_iff_iPCPb.reductionLR. + apply iBPCP_chain_MM. + apply iBPCP_chain_MM. + apply MM_HALTS_ON_ZERO_EILL_PROVABILITY. + apply EILL_ILL_PROVABILITY. Qed.
imports: Undecidability.Shared.Libs.DLW(utils_tac) Undecidability.Synthetic.Undecidability Undecidability.Synthetic.ReducibilityFacts Undecidability.PCP(PCP PCP_undec) Undecidability.StackMachines(BSM) Undecidability.MinskyMachines(MM MM_sss) Undecidability.ILL(EILL ILL iBPCP_MM MM_EILL EILL_ILL) Undecidability.PCP.Reductions.HaltTM_1_to_PCPb