proposition: Theorem H10UPC_SAT_compl_undec : undecidable (complement H10UPC_SAT).
proof: Proof. apply (undecidability_from_reducibility complement_SBTM_HALT_undec). apply reduces_complement. eapply reduces_transitive; last apply H10UC_SAT_to_H10UPC_SAT.reduction. eapply reduces_transitive; last apply H10SQC_SAT_to_H10UC_SAT.reduction. eapply reduces_transitive; last apply H10C_SAT_to_H10SQC_SAT.reduction. eapply reduces_transitive; last apply FRACTRAN_to_H10C_SAT.DIO_ELEM_H10C_SAT. eapply reduces_transitive; last apply FRACTRAN_DIO.DIO_LOGIC_ELEM_SAT. eapply reduces_transitive; last apply FRACTRAN_DIO.FRACTRAN_HALTING_DIO_LOGIC_SAT. eapply reduces_transitive; last apply FRACTRAN_REG_FRACTRAN_HALTING. eapply reduces_transitive; last apply MM_FRACTRAN_REG_HALTING. eapply reduces_transitive; last apply BSM_MM_HALTING. red. unfold Definitions.reduction. setoid_rewrite BSM_sss.Halt_BSM_iff. exact SBTM_HALT_to_HaltBSM.reduction. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.Synthetic.ReducibilityFacts Undecidability.DiophantineConstraints.H10C Undecidability.FRACTRAN(FRACTRAN Reductions.MM_FRACTRAN) Undecidability.MinskyMachines(MM Reductions.BSM_MM) Undecidability.StackMachines(BSM Reductions.SBTM_HALT_to_HaltBSM) Undecidability.TM.SBTM_undec Undecidability.FRACTRAN(FRACTRAN FRACTRAN_undec)