proposition: Lemma fractran_step_iff_halt l1 l2 : (forall s t, l1 /F/ s ≻ t <-> l2 /F/ s ≻ t) -> (forall x, l1 /F/ x ↓ -> l2 /F/ x ↓).
proof: Proof. intros H x. intros [y [[n Hn] Hs]]. exists y. constructor. - exists n. revert x Hn. induction n as [|n IHn]; simpl; auto. intros x [y' [Hy' Hs']]. exists y'. constructor; [now apply H|now apply IHn]. - intros z Hs'. now apply (Hs z), H. Qed.
imports: Coq(List Arith Lia Permutation Wf_nat) Undecidability.Shared.Libs.DLW(gcd prime) Undecidability.FRACTRAN(FRACTRAN fractran_utils)