proposition: Theorem fractran_eval_old_diophantine n l : 𝔻R (fun ν => fractran_eval_old l (ps 1 * exp 2 (fun2vec 1 n ν⭳)) (ν 0 * qs 1 ^ (ν 1))).
proof: Proof. apply dio_rel_compose with (R := fun x v => fractran_eval_old l x _); [ dio auto | ]. apply dio_rel_compose with (R := fun x v => fractran_eval_old l _ x); [ dio auto | ]. apply dio_rel_fractran_eval; 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)