proposition: Fact ra_dio_poly_test_val x w : { e | ⟦ra_dio_poly_test p q⟧ (x##w) e /\ (e = 0 <-> dp_eval (φ x w) (ν x w) p = dp_eval (φ x w) (ν x w) q) }.
proof: Proof. destruct (ra_dio_poly_eq_val (vec_app (project n x) w) p q) as (e & H1 & H2). exists e; split; auto. exists (vec_app (project n x) w); split; auto. intros i; repeat rewrite vec_pos_set. generalize (pos_lr_both n m i). destruct (pos_both n m i) as [ j | j ]; intros Hj; subst i; simpl. * unfold vec_app; rewrite vec_pos_set, pos_both_left. exists (x##vec_nil); split. - apply ra_project_val. - intros k; analyse pos k; simpl; cbv; auto. * unfold vec_app; rewrite vec_pos_set, pos_both_right; reflexivity. 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)