proposition: Lemma ra_dio_poly_find_rel w : (exists e, ⟦ra_dio_poly_find⟧ w e) <-> exists x, ⟦ra_dio_poly_test p q⟧ (x##w) 0.
proof: Proof. simpl; unfold s_min. apply μ_min_of_total. + intros ? ? ?; apply ra_rel_fun. + intros x; destruct (ra_dio_poly_test_val x w) as (e & ? & _). exists e; auto. Qed.
imports: List Arith Undecidability.Shared.Libs.DLW(utils_tac utils_nat pos vec) Undecidability.MuRec.Util(recalg ra_utils recomp ra_recomp) Undecidability.H10.Dio(dio_single)