[STATEMENT]
lemma valuate_with_dim_poly: "z \<lbrace> X \<rbrace> = (\<Sum>i\<in>{0..<dim_poly z}. coeff z i * X i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<lbrace> X \<rbrace> = (\<Sum>i = 0..<dim_poly z. Abstract_Linear_Poly.coeff z i * X i)
[PROOF STEP]
using eval_poly_with_sum_superset[of "{0..<dim_poly z}" z X]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite {0..<dim_poly z}; vars z \<subseteq> {0..<dim_poly z}\<rbrakk> \<Longrightarrow> z \<lbrace> X \<rbrace> = (\<Sum>x = 0..<dim_poly z. Abstract_Linear_Poly.coeff z x * X x)

goal (1 subgoal):
 1. z \<lbrace> X \<rbrace> = (\<Sum>i = 0..<dim_poly z. Abstract_Linear_Poly.coeff z i * X i)
[PROOF STEP]
using vars_subset_0_dim_poly
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite {0..<dim_poly z}; vars z \<subseteq> {0..<dim_poly z}\<rbrakk> \<Longrightarrow> z \<lbrace> X \<rbrace> = (\<Sum>x = 0..<dim_poly z. Abstract_Linear_Poly.coeff z x * X x)
vars ?z \<subseteq> {0..<dim_poly ?z}

goal (1 subgoal):
 1. z \<lbrace> X \<rbrace> = (\<Sum>i = 0..<dim_poly z. Abstract_Linear_Poly.coeff z i * X i)
[PROOF STEP]
by blast