proposition: Theorem FRACTRAN_HALTING_on_exp_diophantine n l : 𝔻R (fun ν => l /F/ ps 1 * exp 1 (fun2vec 0 n ν) ↓).
proof: Proof. apply dio_rel_compose with (R := fun x v => l /F/ x ↓); [ dio auto | ]. apply FRACTRAN_HALTING_on_diophantine; dio auto. Qed.
imports: List Arith Undecidability.Shared.Libs(utils_tac utils_list sums rel_iter gcd pos vec) Undecidability.FRACTRAN(FRACTRAN fractran_utils prime_seq) Undecidability.H10.Dio(dio_logic dio_bounded dio_rt_closure dio_single dio_expo)