proposition: Lemma decide_spec : decider decide Halt_REV_FRACTRAN.
proof: Proof. intros [[P HP] x]. unfold reflects. simpl. destruct (Argument.decision P x HP) as [[y Hy%eval_iff]|HPx]. - firstorder easy. - split; [|easy]. intros [y ?%eval_iff]. firstorder easy. Qed.
imports: Coq(List Arith Lia Permutation Wf_nat) Undecidability.Shared.Libs.DLW(gcd prime) Undecidability.FRACTRAN(FRACTRAN fractran_utils) Undecidability.Synthetic.Definitions