proposition: Theorem DIO_SINGLE_SAT_H10 : DIO_SINGLE_SAT ⪯ H10.
proof: Proof. apply reduces_dependent; exists. intros (E,v). destruct (dio_poly_eq_pos E) as (n & p & q & H). exists (existT _ n (dp_inst_par _ v p, dp_inst_par _ v q)). unfold DIO_SINGLE_SAT, H10. rewrite H. unfold dio_single_pred. split; intros (phi & H1); exists phi; revert H1; cbn; rewrite !dp_inst_par_eval; auto. 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