proposition: Theorem DIO_ELEM_H10C_SAT : DIO_ELEM_SAT ⪯ H10C_SAT.
proof: Proof. exists f. intros (l,ν); simpl; unfold H10C_SAT; rewrite dc_list_h10c_spec. split; intros (phi & Hphi); exists phi; revert Hphi; rewrite Forall_forall; auto. Qed.
imports: List Arith Lia Max Undecidability.Synthetic.Definitions Undecidability(Shared.Libs.DLW.Utils.utils H10.Dio.dio_logic H10.Dio.dio_elem) Undecidability(H10.FRACTRAN_DIO FRACTRAN.FRACTRAN) Undecidability.DiophantineConstraints.H10C