[STATEMENT]
lemma \<delta>_statesI: 
  assumes A: "(q \<rightarrow> l qs)\<in>\<delta>"
  shows "q\<in>\<delta>_states \<delta>"
        "set qs \<subseteq> \<delta>_states \<delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> \<delta>_states \<delta> &&& set qs \<subseteq> \<delta>_states \<delta>
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
q \<rightarrow> l qs \<in> \<delta>

goal (1 subgoal):
 1. q \<in> \<delta>_states \<delta> &&& set qs \<subseteq> \<delta>_states \<delta>
[PROOF STEP]
apply (unfold \<delta>_states_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. q \<rightarrow> l qs \<in> \<delta> \<Longrightarrow> q \<in> \<Union> (rule_states ` \<delta>)
 2. q \<rightarrow> l qs \<in> \<delta> \<Longrightarrow> set qs \<subseteq> \<Union> (rule_states ` \<delta>)
[PROOF STEP]
by (auto split: ta_rule.split simp add: rule_states_simp)