[STATEMENT]
lemma reach_is_node: "\<lbrakk>reach trans p w q; is_node p; list_all is_alpha w\<rbrakk> \<Longrightarrow> is_node q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reach trans p w q; is_node p; list_all is_alpha w\<rbrakk> \<Longrightarrow> is_node q
[PROOF STEP]
by (simp add: steps_is_node reach_def)