fact: Definition FRACTRAN_computable {k} (R : Vector.t nat k -> nat -> Prop) := exists P : list (nat * nat), fractran_regular P /\ forall v : Vector.t nat k, (forall m, R v m <-> exists j, fractran_eval P (ps 1 * enc 2 v) (j * (qs 1)^m) /\ ~ divides (qs 1) j).
imports: Vector List Arith Undecidability.Shared.Libs.DLW(gcd rel_iter pos vec) Undecidability.FRACTRAN(prime_seq)