proposition: Theorem FRACTRAN_HALTING_DIO_LOGIC_SAT : Halt_FRACTRAN ⪯ DIO_LOGIC_SAT.
proof: Proof. apply reduces_dependent; exists. intros (l & x). destruct FRACTRAN_HALTING_on_diophantine with (ll := l) (x := fun _ : nat -> nat => x) as (f & Hf); simpl. + dio_rel_auto. + exists (f, fun _ => x). setoid_rewrite eval_iff. unfold DIO_LOGIC_SAT; rewrite Hf; 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)