[STATEMENT]
lemma analz_Un_EncSet2:
assumes "Enc_keys_clean H" and "K \<subseteq> range LtK" and "K \<inter> synth (analz H) = {}"
shows "analz (EncSet G K \<union> H) \<subseteq> EncSet G K \<union> analz H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz (EncSet G K \<union> H) \<subseteq> EncSet G K \<union> analz H
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> analz (EncSet G K \<union> H) \<Longrightarrow> x \<in> EncSet G K \<union> analz H
[PROOF STEP]
fix X
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> analz (EncSet G K \<union> H) \<Longrightarrow> x \<in> EncSet G K \<union> analz H
[PROOF STEP]
assume "X \<in> analz (EncSet G K \<union> H)"
[PROOF STATE]
proof (state)
this:
X \<in> analz (EncSet G K \<union> H)

goal (1 subgoal):
 1. \<And>x. x \<in> analz (EncSet G K \<union> H) \<Longrightarrow> x \<in> EncSet G K \<union> analz H
[PROOF STEP]
thus "X \<in> EncSet G K \<union> analz H"
[PROOF STATE]
proof (prove)
using this:
X \<in> analz (EncSet G K \<union> H)

goal (1 subgoal):
 1. X \<in> EncSet G K \<union> analz H
[PROOF STEP]
proof (induction X rule: analz.induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>X. X \<in> EncSet G K \<union> H \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 2. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 3. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
 4. \<And>X Y. \<lbrakk>Enc X Y \<in> analz (EncSet G K \<union> H); Enc X Y \<in> EncSet G K \<union> analz H; Y \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 5. \<And>X Y. \<lbrakk>Aenc X (pubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (pubK Y) \<in> EncSet G K \<union> analz H; priK Y \<in> analz (EncSet G K \<union> H); priK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 6. \<And>X Y. \<lbrakk>Aenc X (epubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (epubK Y) \<in> EncSet G K \<union> analz H; epriK Y \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 7. \<And>X Y. \<lbrakk>Sign X (priK Y) \<in> analz (EncSet G K \<union> H); Sign X (priK Y) \<in> EncSet G K \<union> analz H; pubK Y \<in> analz (EncSet G K \<union> H); pubK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
[PROOF STEP]
case (Dec Y K')
[PROOF STATE]
proof (state)
this:
Enc Y K' \<in> analz (EncSet G K \<union> H)
Enc Y K' \<in> EncSet G K \<union> analz H
K' \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})

goal (7 subgoals):
 1. \<And>X. X \<in> EncSet G K \<union> H \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 2. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 3. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
 4. \<And>X Y. \<lbrakk>Enc X Y \<in> analz (EncSet G K \<union> H); Enc X Y \<in> EncSet G K \<union> analz H; Y \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 5. \<And>X Y. \<lbrakk>Aenc X (pubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (pubK Y) \<in> EncSet G K \<union> analz H; priK Y \<in> analz (EncSet G K \<union> H); priK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 6. \<And>X Y. \<lbrakk>Aenc X (epubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (epubK Y) \<in> EncSet G K \<union> analz H; epriK Y \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 7. \<And>X Y. \<lbrakk>Sign X (priK Y) \<in> analz (EncSet G K \<union> H); Sign X (priK Y) \<in> EncSet G K \<union> analz H; pubK Y \<in> analz (EncSet G K \<union> H); pubK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
[PROOF STEP]
from Dec.IH(1)
[PROOF STATE]
proof (chain)
picking this:
Enc Y K' \<in> EncSet G K \<union> analz H
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Enc Y K' \<in> EncSet G K \<union> analz H

goal (1 subgoal):
 1. Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
 2. Enc Y K' \<in> analz H \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
assume "Enc Y K' \<in> analz H"
[PROOF STATE]
proof (state)
this:
Enc Y K' \<in> analz H

goal (2 subgoals):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
 2. Enc Y K' \<in> analz H \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Enc Y K' \<in> analz H

goal (2 subgoals):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
 2. Enc Y K' \<in> analz H \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
have "K' \<in> synth (analz H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K' \<in> synth (analz H)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. K' \<in> synth (analz H)
[PROOF STEP]
have "K' \<in> range LtK \<union> payload"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K' \<in> range LtK \<union> payload
[PROOF STEP]
using \<open>Enc Y K' \<in> analz H\<close> assms(1)
[PROOF STATE]
proof (prove)
using this:
Enc Y K' \<in> analz H
Enc_keys_clean H

goal (1 subgoal):
 1. K' \<in> range LtK \<union> payload
[PROOF STEP]
by (auto dest: Enc_keys_clean_analz)
[PROOF STATE]
proof (state)
this:
K' \<in> range LtK \<union> payload

goal (1 subgoal):
 1. K' \<in> synth (analz H)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
K' \<in> range LtK \<union> payload

goal (1 subgoal):
 1. K' \<in> synth (analz H)
[PROOF STEP]
from Dec.IH(2)
[PROOF STATE]
proof (chain)
picking this:
K' \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})
[PROOF STEP]
have H: "K' \<in> synth (EncSet G K \<union> analz H)"
[PROOF STATE]
proof (prove)
using this:
K' \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})

goal (1 subgoal):
 1. K' \<in> synth (EncSet G K \<union> analz H)
[PROOF STEP]
by (auto simp add: Collect_disj_eq dest: synth_Int2)
[PROOF STATE]
proof (state)
this:
K' \<in> synth (EncSet G K \<union> analz H)

goal (1 subgoal):
 1. K' \<in> synth (analz H)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
K' \<in> synth (EncSet G K \<union> analz H)

goal (1 subgoal):
 1. K' \<in> synth (analz H)
[PROOF STEP]
hence "K' \<in> synth (analz H) \<union> -payload"
[PROOF STATE]
proof (prove)
using this:
K' \<in> synth (EncSet G K \<union> analz H)

goal (1 subgoal):
 1. K' \<in> synth (analz H) \<union> - payload
[PROOF STEP]
proof (rule synth_payload2 [THEN [2] rev_subsetD], auto elim!: payload_Enc)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X Y. \<lbrakk>K' \<in> synth (EncSet G K \<union> analz H); X \<in> payload; Y \<in> payload; X \<in> G; Y \<in> K\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix X Y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X Y. \<lbrakk>K' \<in> synth (EncSet G K \<union> analz H); X \<in> payload; Y \<in> payload; X \<in> G; Y \<in> K\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "Y \<in> K" "Y \<in> payload"
[PROOF STATE]
proof (state)
this:
Y \<in> K
Y \<in> payload

goal (1 subgoal):
 1. \<And>X Y. \<lbrakk>K' \<in> synth (EncSet G K \<union> analz H); X \<in> payload; Y \<in> payload; X \<in> G; Y \<in> K\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with \<open>K \<subseteq> range LtK\<close>
[PROOF STATE]
proof (chain)
picking this:
K \<subseteq> range LtK
Y \<in> K
Y \<in> payload
[PROOF STEP]
obtain KK where "Y = LtK KK"
[PROOF STATE]
proof (prove)
using this:
K \<subseteq> range LtK
Y \<in> K
Y \<in> payload

goal (1 subgoal):
 1. (\<And>KK. Y = LtK KK \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Y = LtK KK

goal (1 subgoal):
 1. \<And>X Y. \<lbrakk>K' \<in> synth (EncSet G K \<union> analz H); X \<in> payload; Y \<in> payload; X \<in> G; Y \<in> K\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with \<open>Y \<in> payload\<close>
[PROOF STATE]
proof (chain)
picking this:
Y \<in> payload
Y = LtK KK
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Y \<in> payload
Y = LtK KK

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
K' \<in> synth (analz H) \<union> - payload

goal (1 subgoal):
 1. K' \<in> synth (analz H)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
K' \<in> range LtK \<union> payload
K' \<in> synth (EncSet G K \<union> analz H)
K' \<in> synth (analz H) \<union> - payload
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
K' \<in> range LtK \<union> payload
K' \<in> synth (EncSet G K \<union> analz H)
K' \<in> synth (analz H) \<union> - payload

goal (1 subgoal):
 1. K' \<in> synth (analz H)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
K' \<in> synth (analz H)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
K' \<in> synth (analz H)

goal (2 subgoals):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
 2. Enc Y K' \<in> analz H \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Enc Y K' \<in> analz H
K' \<in> synth (analz H)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Enc Y K' \<in> analz H
K' \<in> synth (analz H)

goal (1 subgoal):
 1. Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Y \<in> EncSet G K \<union> analz H

goal (1 subgoal):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
assume "Enc Y K' \<in> EncSet G K"
[PROOF STATE]
proof (state)
this:
Enc Y K' \<in> EncSet G K

goal (1 subgoal):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Enc Y K' \<in> EncSet G K

goal (1 subgoal):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
hence "K' \<in> K"
[PROOF STATE]
proof (prove)
using this:
Enc Y K' \<in> EncSet G K

goal (1 subgoal):
 1. K' \<in> K
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
K' \<in> K

goal (1 subgoal):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
K' \<in> K

goal (1 subgoal):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
with \<open>K \<subseteq> range LtK\<close>
[PROOF STATE]
proof (chain)
picking this:
K \<subseteq> range LtK
K' \<in> K
[PROOF STEP]
obtain KK where "K' = LtK KK"
[PROOF STATE]
proof (prove)
using this:
K \<subseteq> range LtK
K' \<in> K

goal (1 subgoal):
 1. (\<And>KK. K' = LtK KK \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
K' = LtK KK

goal (1 subgoal):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
K' = LtK KK

goal (1 subgoal):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
with Dec.IH(2)
[PROOF STATE]
proof (chain)
picking this:
K' \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})
K' = LtK KK
[PROOF STEP]
have "K' \<in> analz H"
[PROOF STATE]
proof (prove)
using this:
K' \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})
K' = LtK KK

goal (1 subgoal):
 1. K' \<in> analz H
[PROOF STEP]
by (auto simp add: Collect_disj_eq dest: synth_Int2)
[PROOF STATE]
proof (state)
this:
K' \<in> analz H

goal (1 subgoal):
 1. Enc Y K' \<in> EncSet G K \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Enc Y K' \<in> EncSet G K
K' \<in> K
K' = LtK KK
K' \<in> analz H
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Enc Y K' \<in> EncSet G K
K' \<in> K
K' = LtK KK
K' \<in> analz H

goal (1 subgoal):
 1. Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
using \<open>K \<inter> synth (analz H) = {}\<close>
[PROOF STATE]
proof (prove)
using this:
Enc Y K' \<in> EncSet G K
K' \<in> K
K' = LtK KK
K' \<in> analz H
K \<inter> synth (analz H) = {}

goal (1 subgoal):
 1. Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Y \<in> EncSet G K \<union> analz H

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Y \<in> EncSet G K \<union> analz H

goal (6 subgoals):
 1. \<And>X. X \<in> EncSet G K \<union> H \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 2. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 3. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
 4. \<And>X Y. \<lbrakk>Aenc X (pubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (pubK Y) \<in> EncSet G K \<union> analz H; priK Y \<in> analz (EncSet G K \<union> H); priK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 5. \<And>X Y. \<lbrakk>Aenc X (epubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (epubK Y) \<in> EncSet G K \<union> analz H; epriK Y \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 6. \<And>X Y. \<lbrakk>Sign X (priK Y) \<in> analz (EncSet G K \<union> H); Sign X (priK Y) \<in> EncSet G K \<union> analz H; pubK Y \<in> analz (EncSet G K \<union> H); pubK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>X. X \<in> EncSet G K \<union> H \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 2. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 3. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
 4. \<And>X Y. \<lbrakk>Aenc X (pubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (pubK Y) \<in> EncSet G K \<union> analz H; priK Y \<in> analz (EncSet G K \<union> H); priK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 5. \<And>X Y. \<lbrakk>Aenc X (epubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (epubK Y) \<in> EncSet G K \<union> analz H; epriK Y \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 6. \<And>X Y. \<lbrakk>Sign X (priK Y) \<in> analz (EncSet G K \<union> H); Sign X (priK Y) \<in> EncSet G K \<union> analz H; pubK Y \<in> analz (EncSet G K \<union> H); pubK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
[PROOF STEP]
case (Adec_eph Y K')
[PROOF STATE]
proof (state)
this:
Aenc Y (epubK K') \<in> analz (EncSet G K \<union> H)
Aenc Y (epubK K') \<in> EncSet G K \<union> analz H
epriK K' \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})

goal (6 subgoals):
 1. \<And>X. X \<in> EncSet G K \<union> H \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 2. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 3. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
 4. \<And>X Y. \<lbrakk>Aenc X (pubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (pubK Y) \<in> EncSet G K \<union> analz H; priK Y \<in> analz (EncSet G K \<union> H); priK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 5. \<And>X Y. \<lbrakk>Aenc X (epubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (epubK Y) \<in> EncSet G K \<union> analz H; epriK Y \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 6. \<And>X Y. \<lbrakk>Sign X (priK Y) \<in> analz (EncSet G K \<union> H); Sign X (priK Y) \<in> EncSet G K \<union> analz H; pubK Y \<in> analz (EncSet G K \<union> H); pubK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
Aenc Y (epubK K') \<in> analz (EncSet G K \<union> H)
Aenc Y (epubK K') \<in> EncSet G K \<union> analz H
epriK K' \<in> synth (analz (EncSet G K \<union> H) \<inter> {a. a \<in> EncSet G K \<union> analz H})

goal (1 subgoal):
 1. Y \<in> EncSet G K \<union> analz H
[PROOF STEP]
by (auto dest!: EpriK_synth)
[PROOF STATE]
proof (state)
this:
Y \<in> EncSet G K \<union> analz H

goal (5 subgoals):
 1. \<And>X. X \<in> EncSet G K \<union> H \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 2. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 3. \<And>X Y. \<lbrakk>\<langle>X, Y\<rangle> \<in> analz (EncSet G K \<union> H); \<langle>X, Y\<rangle> \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> Y \<in> EncSet G K \<union> analz H
 4. \<And>X Y. \<lbrakk>Aenc X (pubK Y) \<in> analz (EncSet G K \<union> H); Aenc X (pubK Y) \<in> EncSet G K \<union> analz H; priK Y \<in> analz (EncSet G K \<union> H); priK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
 5. \<And>X Y. \<lbrakk>Sign X (priK Y) \<in> analz (EncSet G K \<union> H); Sign X (priK Y) \<in> EncSet G K \<union> analz H; pubK Y \<in> analz (EncSet G K \<union> H); pubK Y \<in> EncSet G K \<union> analz H\<rbrakk> \<Longrightarrow> X \<in> EncSet G K \<union> analz H
[PROOF STEP]
qed (insert assms(2), auto)
[PROOF STATE]
proof (state)
this:
X \<in> EncSet G K \<union> analz H

goal:
No subgoals!
[PROOF STEP]
qed