proposition: Lemma FRACTRAN_HALTING_hard p l : p <> 0 -> FRACTRAN_HALTING ((p,0)::l,0) <-> exists x, x <> 0 /\ FRACTRAN_HALTING ((p,0)::l,x).
proof: Proof. intros H; split. + intros (y & (n & H1) & H2). assert (y <> 0) as Hy. { intro; subst; apply (H2 0); constructor; auto. } unfold fractran_steps in H1; rewrite rel_iter_sequence in H1. destruct H1 as (f & F1 & F2 & F3). destruct (first_non_zero f n) as (i & G1 & G2 & G3); subst; auto. exists (f (i+1)); split; auto. exists (f n); split; auto. exists (n-i-1); red; rewrite rel_iter_sequence. exists (fun j => f (j+i+1)); split; auto. split; [ f_equal; lia | ]. intros j Hj; apply F3; lia. + intros (x & H1 & (y & (n & Hn) & H2)). exists y; split; auto. exists (S n), x; split; auto. constructor 1; ring. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)