proposition: Theorem DIO_ELEM_SINGLE_SAT : DIO_ELEM_SAT ⪯ DIO_SINGLE_SAT.
proof: Proof. apply reduces_dependent; exists. intros (l,v). destruct (dio_elem_equation l) as (E & _ & HE). exists (E,v). unfold DIO_ELEM_SAT, DIO_SINGLE_SAT. rewrite <- HE; tauto. Qed.
imports: List Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.Shared.Libs.DLW(utils_tac pos vec) Undecidability.FRACTRAN(FRACTRAN MM_FRACTRAN FRACTRAN_sss) Undecidability.H10.Fractran(fractran_dio) Undecidability.H10.Dio(dio_elem dio_single dio_logic)