[STATEMENT]
lemma synth_analz_insert_eq [rule_format]:
     "X \<in> synth (analz H) 
      \<Longrightarrow> \<forall> G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> synth (analz H) \<Longrightarrow> \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)
[PROOF STEP]
apply (erule synth.induct)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>X. X \<in> analz H \<Longrightarrow> \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)
 2. \<And>agt. \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert (Agent agt) G)) = (Key K \<in> analz G)
 3. \<And>n. \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert (Number n) G)) = (Key K \<in> analz G)
 4. \<And>X. \<lbrakk>X \<in> synth (analz H); \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)\<rbrakk> \<Longrightarrow> \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert (Hash X) G)) = (Key K \<in> analz G)
 5. \<And>X Y. \<lbrakk>X \<in> synth (analz H); \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G); Y \<in> synth (analz H); \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert Y G)) = (Key K \<in> analz G)\<rbrakk> \<Longrightarrow> \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert \<lbrace>X, Y\<rbrace> G)) = (Key K \<in> analz G)
 6. \<And>X Ka. \<lbrakk>X \<in> synth (analz H); \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G); Key Ka \<in> analz H\<rbrakk> \<Longrightarrow> \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert (Crypt Ka X) G)) = (Key K \<in> analz G)
[PROOF STEP]
apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done