fact: Definition Halt_REV_FRACTRAN : { P : list (nat * nat) | fractran_reversible P } * nat -> Prop := fun '(P, n) => exists m, (proj1_sig P) /F/ n ▹ m.
imports: Vector List Arith Undecidability.Shared.Libs.DLW(gcd rel_iter pos vec) Undecidability.FRACTRAN(prime_seq)