proposition: Lemma fractran_step_iff_decide {l1 l2 n} : (forall s t, l1 /F/ s ≻ t <-> l2 /F/ s ≻ t) -> ((l1 /F/ n ↓) + (not (l1 /F/ n ↓))) -> ((l2 /F/ n ↓) + (not (l2 /F/ n ↓))).
proof: Proof. intros H [|Hn]; [left|right]. - eapply fractran_step_iff_halt; eassumption. - intros ?. apply Hn. eapply fractran_step_iff_halt; [|eassumption]. firstorder easy. Qed.
imports: Coq(List Arith Lia Permutation Wf_nat) Undecidability.Shared.Libs.DLW(gcd prime) Undecidability.FRACTRAN(FRACTRAN fractran_utils)