proposition: Theorem ra_dio_poly_find_spec w : ex (⟦ra_dio_poly_find⟧ w) <-> exists v, dp_eval (vec_pos v) (vec_pos w) p = dp_eval (vec_pos v) (vec_pos w) q.
proof: Proof. rewrite ra_dio_poly_find_rel; split. + intros (x & Hx). destruct (ra_dio_poly_test_val x w) as (e & H1 & H2). generalize (ra_rel_fun _ _ _ _ H1 Hx); rewrite H2. exists (project n x); auto. eq goal H; f_equal; apply dp_eval_ext; intro; try rewrite vec_pos_app_left; auto; rewrite vec_pos_app_right; auto. + intros (v & Hv). exists (inject v). destruct (ra_dio_poly_test_val (inject v) w) as (e & H1 & H2). rewrite project_inject in H2. assert (e=0); try (subst; auto; fail). apply H2. eq goal Hv; f_equal; apply dp_eval_ext; intro; try rewrite vec_pos_app_left; auto; rewrite vec_pos_app_right; 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)