[STATEMENT]
lemma step_symb_closed: "step_symb q q' \<Longrightarrow> q' \<in> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_symb q q' \<Longrightarrow> q' \<in> Q
[PROOF STEP]
using transs_q_in_set state_closed
[PROOF STATE]
proof (prove)
using this:
?q \<in> NFA.SQ ?q0.0 ?transs \<Longrightarrow> ?transs ! (?q - ?q0.0) \<in> set ?transs
?t \<in> set transs \<Longrightarrow> state_set ?t \<subseteq> Q

goal (1 subgoal):
 1. step_symb q q' \<Longrightarrow> q' \<in> Q
[PROOF STEP]
by (fastforce simp add: NFA.step_symb_def split: transition.splits)