[STATEMENT]
lemma successor_is_node[elim]: "\<lbrakk>n \<in> set (predecessors g n'); n \<in> set (\<alpha>n g); invar g\<rbrakk> \<Longrightarrow> n' \<in> set (\<alpha>n g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<in> set (predecessors g n'); n \<in> set (\<alpha>n g); invar g\<rbrakk> \<Longrightarrow> n' \<in> set (\<alpha>n g)
[PROOF STEP]
unfolding predecessors_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<in> set (map getFrom (inEdges g n')); n \<in> set (\<alpha>n g); invar g\<rbrakk> \<Longrightarrow> n' \<in> set (\<alpha>n g)
[PROOF STEP]
by (fastforce intro: rev_image_eqI)