fact: Definition fractran_reversible (P : list (nat * nat)) := forall n1 n2 m, P /F/ n1 ≻ m -> P /F/ n2 ≻ m -> n1 = n2.
imports: Vector List Arith Undecidability.Shared.Libs.DLW(gcd rel_iter pos vec) Undecidability.FRACTRAN(prime_seq)