proposition: Corollary FRACTRAN_HALTING_l_0_no_zero_den l : l <> nil -> fractran_regular l -> FRACTRAN_HALTING (l,0) <-> False.
proof: Proof. intros H1 H2; split; try tauto. generalize (fractran_rt_no_zero_den_0_0 H1 H2); intros H3. intros (y & (n & H5) & H6). apply fractran_rt_no_zero_den in H5; auto; subst. apply (H6 0); auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)