proposition: Lemma fractran_stop_zero_den_1 c s (Hc : c <> 0) : [(c, 0)] /F/ s ↓.
proof: Proof. destruct s as [|s]; simpl. - exists 1. constructor. + exists 1. exists 1. constructor; [|reflexivity]. now constructor. + intros z [?|[? Hz]]%fractran_step_cons_inv; [lia|inversion Hz]. - exists (S s). constructor. + now exists 0. + intros z [?|[? Hz]]%fractran_step_cons_inv; [lia|inversion Hz]. Qed.
imports: Coq(List Arith Lia Permutation Wf_nat) Undecidability.Shared.Libs.DLW(gcd prime) Undecidability.FRACTRAN(FRACTRAN fractran_utils)