proposition: Lemma FRACTRAN_HALTING_l_1_no_zero_den l x : l <> nil -> x <> 0 -> Forall (fun c => fst c <> 0) l -> FRACTRAN_HALTING (l,x) <-> FRACTRAN_HALTING (remove_zero_den l,x).
proof: Proof. intros H1 H2 H3. generalize (fractran_step_zero H3); intros H4. assert (forall n y, fractran_steps l n x y -> y <> 0) as H5. { intros n y H ?; subst; apply H2; revert H; apply fractran_rt_no_zero_num; auto. } assert (forall n y, fractran_steps (remove_zero_den l) n x y -> y <> 0) as H6. { intros n y H ?; subst; apply H2; revert H; apply fractran_rt_no_zero_num; auto; apply Forall_filter; auto. } assert (forall n y, rel_iter (fractran_step l) n x y <-> rel_iter (fractran_step (remove_zero_den l)) n x y) as H7. { induction n as [ | n IHn ]; intros y. + simpl; try tauto. + do 2 rewrite rel_iter_S; split. * intros (a & G1 & G2); exists a; split. - apply IHn; auto. - apply H4; auto. apply H5 with (1 := G1). * intros (a & G1 & G2); exists a; split. - apply IHn; auto. - apply H4; auto. apply H6 with (1 := G1). } split; intros (y & (n & G1) & G3); exists y; split. + exists n; apply H7; auto. + intros z Hz; apply (G3 z); revert Hz; apply H4, H5 with n; auto. + exists n; apply H7; auto. + intros z Hz; apply (G3 z); revert Hz; apply H4, H6 with n; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)