466   then show "p \<bullet> x = x" using eq by simp

   466   then show "p \<bullet> x = x" using eq by simp

   467 qed

   467 qed

   468 

   468 

   469 section {* at_set_avoiding2 *}

   469 section {* at_set_avoiding2 *}

   470 

   470 

   472   assumes "finite xs"

   472   assumes "finite xs"

   473   and     "finite (supp c)" "finite (supp x)"

   473   and     "finite (supp c)" "finite (supp x)"

   474   and     "xs \<sharp>* x"

   474   and     "xs \<sharp>* x"

   475   shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p"

   475   shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p"

   476 using assms

   476 using assms