proposition: Lemma dio_rel_fractran_step l x y : 𝔻F x -> 𝔻F y -> 𝔻R (fun ν => l /F/ x ν → y ν).
proof: Proof. intros Hx Hy. induction l as [ | (p,q) l IHl ]. + by dio equiv (fun _ => False). abstract (intros v; rewrite fractran_step_nil_inv; split; tauto). + dio by lemma (fun v => fractran_step_cons_inv p q l (x v) (y v)). Defined.
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)