proposition: Theorem Hilberts_Tenth : HaltTM 1 ⪯ PCPb /\ PCPb ⪯ Halt_MM /\ Halt_MM ⪯ Halt_FRACTRAN /\ Halt_FRACTRAN ⪯ DIO_LOGIC_SAT /\ DIO_LOGIC_SAT ⪯ DIO_ELEM_SAT /\ DIO_ELEM_SAT ⪯ DIO_SINGLE_SAT /\ DIO_SINGLE_SAT ⪯ H10.
proof: Proof. msplit 6. + apply HaltTM_1_to_PCPb. + apply PCPb_MM_HALTING. + apply MM_FRACTRAN_HALTING. + apply FRACTRAN_HALTING_DIO_LOGIC_SAT. + apply DIO_LOGIC_ELEM_SAT. + apply DIO_ELEM_SINGLE_SAT. + apply DIO_SINGLE_SAT_H10. Qed.
imports: Undecidability.Shared.Libs.DLW(utils_tac) Undecidability.Synthetic(Undecidability) Undecidability.Synthetic.ReducibilityFacts Undecidability.TM.TM Undecidability.PCP.PCP Undecidability.PCP.Reductions.HaltTM_1_to_PCPb Undecidability.MinskyMachines(MM PCPb_to_MM) Undecidability.FRACTRAN(FRACTRAN FRACTRAN_undec MM_FRACTRAN) Undecidability.H10(H10 FRACTRAN_DIO) Undecidability.H10.Dio(dio_logic dio_elem dio_single) Undecidability.TM.TM_undec