[STATEMENT]
lemma analz_insert_freshK:
     "\<lbrakk>evs \<in> yahalom;  KAB \<notin> range shrK\<rbrakk> \<Longrightarrow>
      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
      (K = KAB | Key K \<in> analz (knows Spy evs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evs \<in> yahalom; KAB \<notin> range shrK\<rbrakk> \<Longrightarrow> (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = (K = KAB \<or> Key K \<in> analz (knows Spy evs))
[PROOF STEP]
by (simp only: analz_image_freshK analz_image_freshK_simps)