fact: Definition fractran_terminates l x := exists y, fractran_compute l x y /\ fractran_stop l y.
imports: List Arith Undecidability.Shared.Libs.DLW(gcd rel_iter pos vec) Undecidability.FRACTRAN.Util(prime_seq) Undecidability.FRACTRAN.FRACTRAN