[STATEMENT]
lemma normalize1_dverts_split:
  "dverts (normalize1 t1)
  = {v \<in> dverts (normalize1 t1). v \<notin> dverts t1} \<union> {v \<in> dverts (normalize1 t1). v \<in> dverts t1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dverts (normalize1 t1) = {v \<in> dverts (normalize1 t1). v \<notin> dverts t1} \<union> {v \<in> dverts (normalize1 t1). v \<in> dverts t1}
[PROOF STEP]
by blast