fact: Definition FRACTRAN_REG_PROBLEM := { l : list (nat*nat) & { _ : nat | fractran_regular l } }.
imports: List Arith Undecidability.Shared.Libs.DLW(gcd rel_iter pos vec) Undecidability.FRACTRAN.Util(prime_seq) Undecidability.FRACTRAN.FRACTRAN