[STATEMENT]
lemma nxt_Power_dfa [simp]: "dfa.nxt Power_dfa = (\<lambda>Q x. HF(\<Union>q \<in> epsclo (hfset Q). epsclo (nxt M q x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfa.nxt Power_dfa = (\<lambda>Q x. HF (\<Union>q\<in>epsclo (hfset Q). epsclo (nfa.nxt M q x)))
[PROOF STEP]
by (simp add: Power_dfa_def)