[STATEMENT]
lemma is_pred_succ_no_node: "\<lbrakk>is_adj_map a; u\<notin>V\<rbrakk> \<Longrightarrow> a u = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_adj_map a; u \<notin> V\<rbrakk> \<Longrightarrow> a u = []
[PROOF STEP]
unfolding is_adj_map_def V_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>u. distinct (a u) \<and> set (a u) = E `` {u} \<union> E\<inverse> `` {u}; u \<notin> {u. \<exists>v. (u, v) \<in> E \<or> (v, u) \<in> E}\<rbrakk> \<Longrightarrow> a u = []
[PROOF STEP]
by auto