proposition: Fact ra_dio_poly_val p : ⟦ra_dio_poly p⟧ v (dp_eval φ ν p).
proof: Proof. induction p as [ c | i | x | [] p Hp q Hq ]; simpl. + apply ra_cst_n_val. + cbv; auto. + cbv; auto. + exists (dp_eval φ ν p ## dp_eval φ ν q ## vec_nil); split. * apply ra_plus_val. * intros j; analyse pos j; simpl; auto. + exists (dp_eval φ ν p ## dp_eval φ ν q ## vec_nil); split. * apply ra_mult_val. * intros j; analyse pos j; simpl; 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)