proposition: Theorem DIO_LOGIC_ELEM_SAT : DIO_LOGIC_SAT ⪯ DIO_ELEM_SAT.
proof: Proof. apply reduces_dependent; exists. intros (A,v). destruct (dio_formula_elem A) as (l & _ & _ & Hl). exists (l,v); apply Hl. 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)