proposition: Lemma fractran_stop_ndiv_singleton x c d (Hc : c <> 0) (Hd : d <> 0) : ~ divides d c -> [(c,d)] /F/ (S x) ↓.
proof: Proof. intros [p H]%(prime_divides_lt' Hc Hd). induction x as [x IH] using (induction_ltof1 _ (fun x => (count_pow p x))); unfold ltof in IH. destruct (fractran_step_dec [(c,d)] (S x)) as [[y Hxy]|Hs]. - revert Hxy. intros [|[? Hxy]]%fractran_step_cons_inv. + destruct y as [|y]; [lia|]. specialize (H x y ltac:(lia)). apply IH in H as [y' [[n Hyy'] Hs']]. exists y'. split; [|exact Hs']. exists (1+n), (S y). now split; [constructor|]. + inversion Hxy. - exists (S x). now split; [exists 0|]. Qed.
imports: Coq(List Arith Lia Permutation Wf_nat) Undecidability.Shared.Libs.DLW(gcd prime) Undecidability.FRACTRAN(FRACTRAN fractran_utils)