[STATEMENT]
lemma grun_elim[elim?]:
    assumes "grun A w V s v"
    obtains r k p
    where "s = fromN (Suc k) ||| r" "v = (k, p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k r p. \<lbrakk>s = fromN (Suc k) ||| r; v = (k, p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>k r p. \<lbrakk>s = fromN (Suc k) ||| r; v = (k, p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain t r where 1: "s = t ||| r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t r. s = t ||| r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using szip_smap
[PROOF STATE]
proof (prove)
using this:
smap fst ?zs ||| smap snd ?zs = ?zs

goal (1 subgoal):
 1. (\<And>t r. s = t ||| r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s = t ||| r

goal (1 subgoal):
 1. (\<And>k r p. \<lbrakk>s = fromN (Suc k) ||| r; v = (k, p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain k p where 2: "v = (k, p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k p. v = (k, p) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
v = (k, p)

goal (1 subgoal):
 1. (\<And>k r p. \<lbrakk>s = fromN (Suc k) ||| r; v = (k, p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have 3: "t = fromN (Suc k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = fromN (Suc k)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
grun A w V s v

goal (1 subgoal):
 1. t = fromN (Suc k)
[PROOF STEP]
unfolding 1 2
[PROOF STATE]
proof (prove)
using this:
grun A w V (t ||| r) (k, p)

goal (1 subgoal):
 1. t = fromN (Suc k)
[PROOF STEP]
by (coinduction arbitrary: t r k p) (force iff: eq_scons elim: graph.run.cases)
[PROOF STATE]
proof (state)
this:
t = fromN (Suc k)

goal (1 subgoal):
 1. (\<And>k r p. \<lbrakk>s = fromN (Suc k) ||| r; v = (k, p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that 1 2 3
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>s = fromN (Suc ?k) ||| ?r; v = (?k, ?p)\<rbrakk> \<Longrightarrow> thesis
s = t ||| r
v = (k, p)
t = fromN (Suc k)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma run_grun:
    assumes "run A (sdrop k w ||| r) p"
    shows "gurun A w (fromN (Suc k) ||| r) (k, p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gurun A w (fromN (Suc k) ||| r) (k, p)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run A (sdrop k w ||| r) p

goal (1 subgoal):
 1. gurun A w (fromN (Suc k) ||| r) (k, p)
[PROOF STEP]
by (coinduction arbitrary: k p r) (auto elim: nba.run.cases)


[STATEMENT]
lemma grun_run:
    assumes "grun A w V (fromN (Suc k) ||| r) (k, p)"
    shows "run A (sdrop k w ||| r) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run A (sdrop k w ||| r) p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. run A (sdrop k w ||| r) p
[PROOF STEP]
have 2: "\<exists> ka wa. sdrop k (stl w :: 'a stream) = sdrop ka wa \<and> P ka wa" if "P (Suc k) w" for P k w
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>kaa waa. sdrop k (stl w) = sdrop kaa waa \<and> P kaa waa
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
P (Suc k) w

goal (1 subgoal):
 1. \<exists>kaa waa. sdrop k (stl w) = sdrop kaa waa \<and> P kaa waa
[PROOF STEP]
by (metis sdrop.simps(2))
[PROOF STATE]
proof (state)
this:
?P (Suc ?k) ?w \<Longrightarrow> \<exists>ka wa. sdrop ?k (stl ?w) = sdrop ka wa \<and> ?P ka wa

goal (1 subgoal):
 1. run A (sdrop k w ||| r) p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run A (sdrop k w ||| r) p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
grun A w V (fromN (Suc k) ||| r) (k, p)

goal (1 subgoal):
 1. run A (sdrop k w ||| r) p
[PROOF STEP]
by (coinduction arbitrary: k p w r) (auto intro!: 2 elim: graph.run.cases)
[PROOF STATE]
proof (state)
this:
run A (sdrop k w ||| r) p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma greachable_reachable:
    fixes l q k p
    defines "u \<equiv> (l, q)"
    defines "v \<equiv> (k, p)"
    assumes "u \<in> greachable A w V v"
    shows "q \<in> reachable A p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> reachable A p
[PROOF STEP]
using assms(3, 1, 2)
[PROOF STATE]
proof (prove)
using this:
u \<in> greachable A w V v
u \<equiv> (l, q)
v \<equiv> (k, p)

goal (1 subgoal):
 1. q \<in> reachable A p
[PROOF STEP]
proof (induct arbitrary: l q k p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l q k p. \<lbrakk>v = (l, q); v = (k, p)\<rbrakk> \<Longrightarrow> q \<in> reachable A p
 2. \<And>q l qa k p. \<lbrakk>q \<in> greachable A w V v; \<And>l qa k p. \<lbrakk>q = (l, qa); v = (k, p)\<rbrakk> \<Longrightarrow> qa \<in> reachable A p; case q of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> (l, qa) \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; v = (k, p)\<rbrakk> \<Longrightarrow> qa \<in> reachable A p
[PROOF STEP]
case reflexive
[PROOF STATE]
proof (state)
this:
v = (l, q)
v = (k, p)

goal (2 subgoals):
 1. \<And>l q k p. \<lbrakk>v = (l, q); v = (k, p)\<rbrakk> \<Longrightarrow> q \<in> reachable A p
 2. \<And>q l qa k p. \<lbrakk>q \<in> greachable A w V v; \<And>l qa k p. \<lbrakk>q = (l, qa); v = (k, p)\<rbrakk> \<Longrightarrow> qa \<in> reachable A p; case q of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> (l, qa) \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; v = (k, p)\<rbrakk> \<Longrightarrow> qa \<in> reachable A p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v = (l, q)
v = (k, p)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
v = (l, q)
v = (k, p)

goal (1 subgoal):
 1. q \<in> reachable A p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q \<in> reachable A p

goal (1 subgoal):
 1. \<And>q l qa k p. \<lbrakk>q \<in> greachable A w V v; \<And>l qa k p. \<lbrakk>q = (l, qa); v = (k, p)\<rbrakk> \<Longrightarrow> qa \<in> reachable A p; case q of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> (l, qa) \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; v = (k, p)\<rbrakk> \<Longrightarrow> qa \<in> reachable A p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q l qa k p. \<lbrakk>q \<in> greachable A w V v; \<And>l qa k p. \<lbrakk>q = (l, qa); v = (k, p)\<rbrakk> \<Longrightarrow> qa \<in> reachable A p; case q of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> (l, qa) \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; v = (k, p)\<rbrakk> \<Longrightarrow> qa \<in> reachable A p
[PROOF STEP]
case (execute u)
[PROOF STATE]
proof (state)
this:
u \<in> greachable A w V v
\<lbrakk>u = (?l, ?q); v = (?k, ?p)\<rbrakk> \<Longrightarrow> ?q \<in> reachable A ?p
case u of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> (l, q) \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V
v = (k, p)

goal (1 subgoal):
 1. \<And>q l qa k p. \<lbrakk>q \<in> greachable A w V v; \<And>l qa k p. \<lbrakk>q = (l, qa); v = (k, p)\<rbrakk> \<Longrightarrow> qa \<in> reachable A p; case q of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> (l, qa) \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; v = (k, p)\<rbrakk> \<Longrightarrow> qa \<in> reachable A p
[PROOF STEP]
have 1: "q \<in> successors A (snd u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> successors A (snd u)
[PROOF STEP]
using execute
[PROOF STATE]
proof (prove)
using this:
u \<in> greachable A w V v
\<lbrakk>u = (?l, ?q); v = (?k, ?p)\<rbrakk> \<Longrightarrow> ?q \<in> reachable A ?p
case u of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> (l, q) \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V
v = (k, p)

goal (1 subgoal):
 1. q \<in> successors A (snd u)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q \<in> successors A (snd u)

goal (1 subgoal):
 1. \<And>q l qa k p. \<lbrakk>q \<in> greachable A w V v; \<And>l qa k p. \<lbrakk>q = (l, qa); v = (k, p)\<rbrakk> \<Longrightarrow> qa \<in> reachable A p; case q of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> (l, qa) \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; v = (k, p)\<rbrakk> \<Longrightarrow> qa \<in> reachable A p
[PROOF STEP]
have "snd u \<in> reachable A p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd u \<in> reachable A p
[PROOF STEP]
using execute
[PROOF STATE]
proof (prove)
using this:
u \<in> greachable A w V v
\<lbrakk>u = (?l, ?q); v = (?k, ?p)\<rbrakk> \<Longrightarrow> ?q \<in> reachable A ?p
case u of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> (l, q) \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V
v = (k, p)

goal (1 subgoal):
 1. snd u \<in> reachable A p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
snd u \<in> reachable A p

goal (1 subgoal):
 1. \<And>q l qa k p. \<lbrakk>q \<in> greachable A w V v; \<And>l qa k p. \<lbrakk>q = (l, qa); v = (k, p)\<rbrakk> \<Longrightarrow> qa \<in> reachable A p; case q of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> (l, qa) \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; v = (k, p)\<rbrakk> \<Longrightarrow> qa \<in> reachable A p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
snd u \<in> reachable A p

goal (1 subgoal):
 1. \<And>q l qa k p. \<lbrakk>q \<in> greachable A w V v; \<And>l qa k p. \<lbrakk>q = (l, qa); v = (k, p)\<rbrakk> \<Longrightarrow> qa \<in> reachable A p; case q of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> (l, qa) \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; v = (k, p)\<rbrakk> \<Longrightarrow> qa \<in> reachable A p
[PROOF STEP]
have "q \<in> reachable A (snd u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> reachable A (snd u)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
q \<in> successors A (snd u)

goal (1 subgoal):
 1. q \<in> reachable A (snd u)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
q \<in> reachable A (snd u)

goal (1 subgoal):
 1. \<And>q l qa k p. \<lbrakk>q \<in> greachable A w V v; \<And>l qa k p. \<lbrakk>q = (l, qa); v = (k, p)\<rbrakk> \<Longrightarrow> qa \<in> reachable A p; case q of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> (l, qa) \<in> {Suc k} \<times> transition A (w !! k) p \<inter> V; v = (k, p)\<rbrakk> \<Longrightarrow> qa \<in> reachable A p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
q \<in> reachable A p
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
q \<in> reachable A p

goal (1 subgoal):
 1. q \<in> reachable A p
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
q \<in> reachable A p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gnodes_nodes: "gnodes A w V \<subseteq> UNIV \<times> nodes A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gnodes A w V \<subseteq> UNIV \<times> nodes A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> gnodes A w V \<Longrightarrow> x \<in> UNIV \<times> nodes A
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> gnodes A w V \<Longrightarrow> x \<in> UNIV \<times> nodes A
[PROOF STEP]
assume "v \<in> gnodes A w V"
[PROOF STATE]
proof (state)
this:
v \<in> gnodes A w V

goal (1 subgoal):
 1. \<And>x. x \<in> gnodes A w V \<Longrightarrow> x \<in> UNIV \<times> nodes A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> gnodes A w V
[PROOF STEP]
show "v \<in> UNIV \<times> nodes A"
[PROOF STATE]
proof (prove)
using this:
v \<in> gnodes A w V

goal (1 subgoal):
 1. v \<in> UNIV \<times> nodes A
[PROOF STEP]
by induct auto
[PROOF STATE]
proof (state)
this:
v \<in> UNIV \<times> nodes A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gpath_subset:
    assumes "gpath A w V r v"
    assumes "set (gstates r v) \<subseteq> U"
    shows "gpath A w U r v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gpath A w U r v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gpath A w V r v
set (gstates r v) \<subseteq> U

goal (1 subgoal):
 1. gpath A w U r v
[PROOF STEP]
by induct auto


[STATEMENT]
lemma grun_subset:
    assumes "grun A w V r v"
    assumes "sset (gtrace r v) \<subseteq> U"
    shows "grun A w U r v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. grun A w U r v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
grun A w V r v
sset (gtrace r v) \<subseteq> U

goal (1 subgoal):
 1. grun A w U r v
[PROOF STEP]
proof (coinduction arbitrary: r v)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a r ra v. \<lbrakk>a ## r = ra; grun A w V ra v; sset (gtrace ra v) \<subseteq> U\<rbrakk> \<Longrightarrow> (case v of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> a \<in> {Suc k} \<times> transition A (w !! k) p \<inter> U) \<and> (\<exists>ra v. r = ra \<and> a = v \<and> grun A w V ra v \<and> sset (gtrace ra v) \<subseteq> U)
[PROOF STEP]
case (run a s r v)
[PROOF STATE]
proof (state)
this:
a ## s = r
grun A w V r v
sset (gtrace r v) \<subseteq> U

goal (1 subgoal):
 1. \<And>a r ra v. \<lbrakk>a ## r = ra; grun A w V ra v; sset (gtrace ra v) \<subseteq> U\<rbrakk> \<Longrightarrow> (case v of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> a \<in> {Suc k} \<times> transition A (w !! k) p \<inter> U) \<and> (\<exists>ra v. r = ra \<and> a = v \<and> grun A w V ra v \<and> sset (gtrace ra v) \<subseteq> U)
[PROOF STEP]
have 1: "grun A w V s a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. grun A w V s a
[PROOF STEP]
using run(1, 2)
[PROOF STATE]
proof (prove)
using this:
a ## s = r
grun A w V r v

goal (1 subgoal):
 1. grun A w V s a
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
grun A w V s a

goal (1 subgoal):
 1. \<And>a r ra v. \<lbrakk>a ## r = ra; grun A w V ra v; sset (gtrace ra v) \<subseteq> U\<rbrakk> \<Longrightarrow> (case v of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> a \<in> {Suc k} \<times> transition A (w !! k) p \<inter> U) \<and> (\<exists>ra v. r = ra \<and> a = v \<and> grun A w V ra v \<and> sset (gtrace ra v) \<subseteq> U)
[PROOF STEP]
have 2: "a \<in> gusuccessors A w v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> gusuccessors A w v
[PROOF STEP]
using run(1, 2)
[PROOF STATE]
proof (prove)
using this:
a ## s = r
grun A w V r v

goal (1 subgoal):
 1. a \<in> gusuccessors A w v
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
a \<in> gusuccessors A w v

goal (1 subgoal):
 1. \<And>a r ra v. \<lbrakk>a ## r = ra; grun A w V ra v; sset (gtrace ra v) \<subseteq> U\<rbrakk> \<Longrightarrow> (case v of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> a \<in> {Suc k} \<times> transition A (w !! k) p \<inter> U) \<and> (\<exists>ra v. r = ra \<and> a = v \<and> grun A w V ra v \<and> sset (gtrace ra v) \<subseteq> U)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case v of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> a \<in> {Suc k} \<times> transition A (w !! k) p \<inter> U) \<and> (\<exists>r v. s = r \<and> a = v \<and> grun A w V r v \<and> sset (gtrace r v) \<subseteq> U)
[PROOF STEP]
using 1 2 run(1, 3)
[PROOF STATE]
proof (prove)
using this:
grun A w V s a
a \<in> gusuccessors A w v
a ## s = r
sset (gtrace r v) \<subseteq> U

goal (1 subgoal):
 1. (case v of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> a \<in> {Suc k} \<times> transition A (w !! k) p \<inter> U) \<and> (\<exists>r v. s = r \<and> a = v \<and> grun A w V r v \<and> sset (gtrace r v) \<subseteq> U)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(case v of (k, p) \<Rightarrow> w !! k \<in> alphabet A \<and> a \<in> {Suc k} \<times> transition A (w !! k) p \<inter> U) \<and> (\<exists>r v. s = r \<and> a = v \<and> grun A w V r v \<and> sset (gtrace r v) \<subseteq> U)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma greachable_subset: "greachable A w V v \<subseteq> insert v V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. greachable A w V v \<subseteq> insert v V
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> greachable A w V v \<Longrightarrow> x \<in> insert v V
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> greachable A w V v \<Longrightarrow> x \<in> insert v V
[PROOF STEP]
assume "u \<in> greachable A w V v"
[PROOF STATE]
proof (state)
this:
u \<in> greachable A w V v

goal (1 subgoal):
 1. \<And>x. x \<in> greachable A w V v \<Longrightarrow> x \<in> insert v V
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in> greachable A w V v
[PROOF STEP]
show "u \<in> insert v V"
[PROOF STATE]
proof (prove)
using this:
u \<in> greachable A w V v

goal (1 subgoal):
 1. u \<in> insert v V
[PROOF STEP]
by induct auto
[PROOF STATE]
proof (state)
this:
u \<in> insert v V

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gtrace_infinite:
    assumes "grun A w V r v"
    shows "infinite (sset (gtrace r v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (sset (gtrace r v))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
grun A w V r v

goal (1 subgoal):
 1. infinite (sset (gtrace r v))
[PROOF STEP]
by (metis grun_elim gtrace_alt_def infinite_Ici sset_fromN sset_szip_finite)


[STATEMENT]
lemma infinite_greachable_gtrace:
    assumes "grun A w V r v"
    assumes "u \<in> sset (gtrace r v)"
    shows "infinite (greachable A w V u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (greachable A w V u)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite (greachable A w V u)
[PROOF STEP]
obtain i where 1: "u = gtrace r v !! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. u = gtrace r v !! i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using sset_range imageE assms(2)
[PROOF STATE]
proof (prove)
using this:
sset ?s = range ((!!) ?s)
\<lbrakk>?b \<in> ?f ` ?A; \<And>x. \<lbrakk>?b = ?f x; x \<in> ?A\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
u \<in> sset (gtrace r v)

goal (1 subgoal):
 1. (\<And>i. u = gtrace r v !! i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
u = gtrace r v !! i

goal (1 subgoal):
 1. infinite (greachable A w V u)
[PROOF STEP]
have 2: "gtarget (stake (Suc i) r) v = u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gtarget (stake (Suc i) r) v = u
[PROOF STEP]
unfolding 1 sscan_snth
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gtarget (stake (Suc i) r) v = gtarget (stake (Suc i) r) v
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
gtarget (stake (Suc i) r) v = u

goal (1 subgoal):
 1. infinite (greachable A w V u)
[PROOF STEP]
have "infinite (sset (sdrop (Suc i) (gtrace r v)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (sset (sdrop (Suc i) (gtrace r v)))
[PROOF STEP]
using gtrace_infinite[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
infinite (sset (gtrace r v))

goal (1 subgoal):
 1. infinite (sset (sdrop (Suc i) (gtrace r v)))
[PROOF STEP]
by (metis List.finite_set finite_Un sset_shift stake_sdrop)
[PROOF STATE]
proof (state)
this:
infinite (sset (sdrop (Suc i) (gtrace r v)))

goal (1 subgoal):
 1. infinite (greachable A w V u)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
infinite (sset (sdrop (Suc i) (gtrace r v)))

goal (1 subgoal):
 1. infinite (greachable A w V u)
[PROOF STEP]
have "sdrop (Suc i) (gtrace r v) = gtrace (sdrop (Suc i) r) (gtarget (stake (Suc i) r) v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sdrop (Suc i) (gtrace r v) = gtrace (sdrop (Suc i) r) (gtarget (stake (Suc i) r) v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sdrop (Suc i) (gtrace r v) = gtrace (sdrop (Suc i) r) (gtarget (stake (Suc i) r) v)

goal (1 subgoal):
 1. infinite (greachable A w V u)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sdrop (Suc i) (gtrace r v) = gtrace (sdrop (Suc i) r) (gtarget (stake (Suc i) r) v)

goal (1 subgoal):
 1. infinite (greachable A w V u)
[PROOF STEP]
have "sset \<dots> \<subseteq> greachable A w V u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sset (gtrace (sdrop (Suc i) r) (gtarget (stake (Suc i) r) v)) \<subseteq> greachable A w V u
[PROOF STEP]
using assms(1) 2
[PROOF STATE]
proof (prove)
using this:
grun A w V r v
gtarget (stake (Suc i) r) v = u

goal (1 subgoal):
 1. sset (gtrace (sdrop (Suc i) r) (gtarget (stake (Suc i) r) v)) \<subseteq> greachable A w V u
[PROOF STEP]
by (metis graph.reachable.reflexive graph.reachable_trace graph.run_sdrop)
[PROOF STATE]
proof (state)
this:
sset (gtrace (sdrop (Suc i) r) (gtarget (stake (Suc i) r) v)) \<subseteq> greachable A w V u

goal (1 subgoal):
 1. infinite (greachable A w V u)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
infinite (greachable A w V u)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
infinite (greachable A w V u)

goal (1 subgoal):
 1. infinite (greachable A w V u)
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
infinite (greachable A w V u)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_nodes_gsuccessors:
    assumes "finite (nodes A)"
    assumes "v \<in> gunodes A w"
    shows "finite (gusuccessors A w v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (gusuccessors A w v)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (gusuccessors A w v)
[PROOF STEP]
have "gusuccessors A w v \<subseteq> gureachable A w v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gusuccessors A w v \<subseteq> gureachable A w v
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
gusuccessors A w v \<subseteq> gureachable A w v

goal (1 subgoal):
 1. finite (gusuccessors A w v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gusuccessors A w v \<subseteq> gureachable A w v

goal (1 subgoal):
 1. finite (gusuccessors A w v)
[PROOF STEP]
have "\<dots> \<subseteq> gunodes A w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gureachable A w v \<subseteq> gunodes A w
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
v \<in> gunodes A w

goal (1 subgoal):
 1. gureachable A w v \<subseteq> gunodes A w
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
gureachable A w v \<subseteq> gunodes A w

goal (1 subgoal):
 1. finite (gusuccessors A w v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gureachable A w v \<subseteq> gunodes A w

goal (1 subgoal):
 1. finite (gusuccessors A w v)
[PROOF STEP]
have "\<dots> \<subseteq> UNIV \<times> nodes A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gunodes A w \<subseteq> UNIV \<times> nodes A
[PROOF STEP]
using gnodes_nodes
[PROOF STATE]
proof (prove)
using this:
gnodes ?A ?w ?V \<subseteq> UNIV \<times> nodes ?A

goal (1 subgoal):
 1. gunodes A w \<subseteq> UNIV \<times> nodes A
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
gunodes A w \<subseteq> UNIV \<times> nodes A

goal (1 subgoal):
 1. finite (gusuccessors A w v)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
gusuccessors A w v \<subseteq> UNIV \<times> nodes A
[PROOF STEP]
have 3: "gusuccessors A w v \<subseteq> UNIV \<times> nodes A"
[PROOF STATE]
proof (prove)
using this:
gusuccessors A w v \<subseteq> UNIV \<times> nodes A

goal (1 subgoal):
 1. gusuccessors A w v \<subseteq> UNIV \<times> nodes A
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
gusuccessors A w v \<subseteq> UNIV \<times> nodes A

goal (1 subgoal):
 1. finite (gusuccessors A w v)
[PROOF STEP]
have "gusuccessors A w v \<subseteq> {Suc (fst v)} \<times> nodes A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gusuccessors A w v \<subseteq> {Suc (fst v)} \<times> nodes A
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
gusuccessors A w v \<subseteq> UNIV \<times> nodes A

goal (1 subgoal):
 1. gusuccessors A w v \<subseteq> {Suc (fst v)} \<times> nodes A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gusuccessors A w v \<subseteq> {Suc (fst v)} \<times> nodes A

goal (1 subgoal):
 1. finite (gusuccessors A w v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gusuccessors A w v \<subseteq> {Suc (fst v)} \<times> nodes A

goal (1 subgoal):
 1. finite (gusuccessors A w v)
[PROOF STEP]
have "finite \<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ({Suc (fst v)} \<times> nodes A)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
finite (nodes A)

goal (1 subgoal):
 1. finite ({Suc (fst v)} \<times> nodes A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite ({Suc (fst v)} \<times> nodes A)

goal (1 subgoal):
 1. finite (gusuccessors A w v)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
finite (gusuccessors A w v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (gusuccessors A w v)

goal (1 subgoal):
 1. finite (gusuccessors A w v)
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
finite (gusuccessors A w v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem knowledge_equiv:
 "\<lbrakk> X \<in> knows A evs; Notes A X \<notin> set evs;
   X \<notin> {Key (priEK A), Key (priSK A), Key (shrK A)} \<rbrakk>
 \<Longrightarrow> X \<in> knows B evs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<in> knows A evs; Notes A X \<notin> set evs; X \<notin> {Key (priEK A), Key (priSK A), Key (shrK A)}\<rbrakk> \<Longrightarrow> X \<in> knows B evs
[PROOF STEP]
apply (erule rev_mp, erule rev_mp, erule rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<notin> {Key (priEK A), Key (priSK A), Key (shrK A)} \<longrightarrow> Notes A X \<notin> set evs \<longrightarrow> X \<in> knows A evs \<longrightarrow> X \<in> knows B evs
[PROOF STEP]
apply (induct_tac "A", induct_tac "B", induct_tac "evs")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa xaa. X \<notin> {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<longrightarrow> Notes (Friend xa) X \<notin> set [] \<longrightarrow> X \<in> knows (Friend xa) [] \<longrightarrow> X \<in> knows (Friend xaa) []
 2. \<And>xa xaa a list. X \<notin> {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<longrightarrow> Notes (Friend xa) X \<notin> set list \<longrightarrow> X \<in> knows (Friend xa) list \<longrightarrow> X \<in> knows (Friend xaa) list \<Longrightarrow> X \<notin> {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<longrightarrow> Notes (Friend xa) X \<notin> set (a # list) \<longrightarrow> X \<in> knows (Friend xa) (a # list) \<longrightarrow> X \<in> knows (Friend xaa) (a # list)
[PROOF STEP]
apply (induct_tac [2] "a")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>xa xaa. X \<notin> {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<longrightarrow> Notes (Friend xa) X \<notin> set [] \<longrightarrow> X \<in> knows (Friend xa) [] \<longrightarrow> X \<in> knows (Friend xaa) []
 2. \<And>xa xaa a list x1 x2 x3. X \<notin> {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<longrightarrow> Notes (Friend xa) X \<notin> set list \<longrightarrow> X \<in> knows (Friend xa) list \<longrightarrow> X \<in> knows (Friend xaa) list \<Longrightarrow> X \<notin> {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<longrightarrow> Notes (Friend xa) X \<notin> set (Says x1 x2 x3 # list) \<longrightarrow> X \<in> knows (Friend xa) (Says x1 x2 x3 # list) \<longrightarrow> X \<in> knows (Friend xaa) (Says x1 x2 x3 # list)
 3. \<And>xa xaa a list x1 x2. X \<notin> {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<longrightarrow> Notes (Friend xa) X \<notin> set list \<longrightarrow> X \<in> knows (Friend xa) list \<longrightarrow> X \<in> knows (Friend xaa) list \<Longrightarrow> X \<notin> {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<longrightarrow> Notes (Friend xa) X \<notin> set (Gets x1 x2 # list) \<longrightarrow> X \<in> knows (Friend xa) (Gets x1 x2 # list) \<longrightarrow> X \<in> knows (Friend xaa) (Gets x1 x2 # list)
 4. \<And>xa xaa a list x1 x2. X \<notin> {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<longrightarrow> Notes (Friend xa) X \<notin> set list \<longrightarrow> X \<in> knows (Friend xa) list \<longrightarrow> X \<in> knows (Friend xaa) list \<Longrightarrow> X \<notin> {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<longrightarrow> Notes (Friend xa) X \<notin> set (Notes x1 x2 # list) \<longrightarrow> X \<in> knows (Friend xa) (Notes x1 x2 # list) \<longrightarrow> X \<in> knows (Friend xaa) (Notes x1 x2 # list)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma knowledge_equiv_bis:
 "\<lbrakk> X \<in> knows A evs; Notes A X \<notin> set evs \<rbrakk>
 \<Longrightarrow> X \<in> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> knows B evs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<in> knows A evs; Notes A X \<notin> set evs\<rbrakk> \<Longrightarrow> X \<in> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> knows B evs
[PROOF STEP]
apply (blast dest: knowledge_equiv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma knowledge_equiv_ter:
 "\<lbrakk> X \<in> knows A evs; X \<notin> {Key (priEK A), Key (priSK A), Key (shrK A)} \<rbrakk>
\<Longrightarrow> X \<in> knows B evs \<or> Notes A X \<in> set evs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<in> knows A evs; X \<notin> {Key (priEK A), Key (priSK A), Key (shrK A)}\<rbrakk> \<Longrightarrow> X \<in> knows B evs \<or> Notes A X \<in> set evs
[PROOF STEP]
apply (blast dest: knowledge_equiv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma knowledge_equiv_quater:
 " X \<in> knows A evs
\<Longrightarrow> X \<in> knows B evs \<or> Notes A X \<in> set evs \<or>
   X \<in> {Key (priEK A), Key (priSK A), Key (shrK A)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> knows A evs \<Longrightarrow> X \<in> knows B evs \<or> Notes A X \<in> set evs \<or> X \<in> {Key (priEK A), Key (priSK A), Key (shrK A)}
[PROOF STEP]
apply (blast dest: knowledge_equiv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "A-B-C=D-E-F \<Longrightarrow> insert m A-B-C = insert m D-E-F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A - B - C = D - E - F \<Longrightarrow> insert m A - B - C = insert m D - E - F
[PROOF STEP]
oops


[STATEMENT]
lemma knowledge_equiv_eq_setdiff:
 "knows A evs  -
   {Key (priEK A), Key (priSK A), Key (shrK A)} -
     {X. Notes A X \<in> set evs}
  =
  knows B evs -
   {Key (priEK B), Key (priSK B), Key (shrK B)} -
     {X. Notes B X \<in> set evs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. knows A evs - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set evs} = knows B evs - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set evs}
[PROOF STEP]
apply (induct_tac "evs", induct_tac "A", induct_tac "B")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa xaa. knows (Friend xa) [] - {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} - {X. Notes (Friend xa) X \<in> set []} = knows (Friend xaa) [] - {Key (priEK (Friend xaa)), Key (priSK (Friend xaa)), Key (shrK (Friend xaa))} - {X. Notes (Friend xaa) X \<in> set []}
 2. \<And>a list. knows A list - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set list} = knows B list - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set list} \<Longrightarrow> knows A (a # list) - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set (a # list)} = knows B (a # list) - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set (a # list)}
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. knows A list - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set list} = knows B list - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set list} \<Longrightarrow> knows A (a # list) - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set (a # list)} = knows B (a # list) - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set (a # list)}
[PROOF STEP]
apply (induct_tac "a")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a list x1 x2 x3. knows A list - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set list} = knows B list - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set list} \<Longrightarrow> knows A (Says x1 x2 x3 # list) - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set (Says x1 x2 x3 # list)} = knows B (Says x1 x2 x3 # list) - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set (Says x1 x2 x3 # list)}
 2. \<And>a list x1 x2. knows A list - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set list} = knows B list - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set list} \<Longrightarrow> knows A (Gets x1 x2 # list) - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set (Gets x1 x2 # list)} = knows B (Gets x1 x2 # list) - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set (Gets x1 x2 # list)}
 3. \<And>a list x1 x2. knows A list - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set list} = knows B list - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set list} \<Longrightarrow> knows A (Notes x1 x2 # list) - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set (Notes x1 x2 # list)} = knows B (Notes x1 x2 # list) - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set (Notes x1 x2 # list)}
[PROOF STEP]
(*Gets case solves because this event doesn't touch any agent knowledge*)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a list x1 x2 x3. knows A list - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set list} = knows B list - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set list} \<Longrightarrow> knows A (Says x1 x2 x3 # list) - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set (Says x1 x2 x3 # list)} = knows B (Says x1 x2 x3 # list) - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set (Says x1 x2 x3 # list)}
 2. \<And>a list x1 x2. knows A list - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set list} = knows B list - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set list} \<Longrightarrow> knows A (Gets x1 x2 # list) - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set (Gets x1 x2 # list)} = knows B (Gets x1 x2 # list) - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set (Gets x1 x2 # list)}
 3. \<And>a list x1 x2. knows A list - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set list} = knows B list - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set list} \<Longrightarrow> knows A (Notes x1 x2 # list) - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set (Notes x1 x2 # list)} = knows B (Notes x1 x2 # list) - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set (Notes x1 x2 # list)}
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>list x3. knows A list - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set list} = knows B list - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set list} \<Longrightarrow> insert x3 (knows A list) - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set list} = insert x3 (knows B list) - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set list}
 2. \<And>list x1 x2. knows A list - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set list} = knows B list - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set list} \<Longrightarrow> (A = x1 \<longrightarrow> B \<noteq> x1 \<longrightarrow> insert x2 (knows x1 list) - {Key (priEK x1), Key (priSK x1), Key (shrK x1)} - {X. X = x2 \<or> Notes x1 X \<in> set list} = knows B list - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set list}) \<and> (A \<noteq> x1 \<longrightarrow> B = x1 \<longrightarrow> knows x1 list - {Key (priEK x1), Key (priSK x1), Key (shrK x1)} - {X. Notes x1 X \<in> set list} = insert x2 (knows x1 list) - {Key (priEK x1), Key (priSK x1), Key (shrK x1)} - {X. X = x2 \<or> Notes x1 X \<in> set list})
[PROOF STEP]
(*Says case fails because both agents extract the said message, plus
discussion on lemma setdiff_diff_insert*)

(*Notes case solves in case neither of the two agents is the agent of the
  current step, because no notes are extracted and inductive premise applies;
  it fails in the two subcases when either of them is the agent of the current
  step, because a note would be extracted i.e. inserted in his knowledge, and
  hence falsification by discussion on lemma setdiff_diff_insert*)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>list x3. knows A list - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set list} = knows B list - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set list} \<Longrightarrow> insert x3 (knows A list) - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set list} = insert x3 (knows B list) - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set list}
 2. \<And>list x1 x2. knows A list - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set list} = knows B list - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set list} \<Longrightarrow> (A = x1 \<longrightarrow> B \<noteq> x1 \<longrightarrow> insert x2 (knows x1 list) - {Key (priEK x1), Key (priSK x1), Key (shrK x1)} - {X. X = x2 \<or> Notes x1 X \<in> set list} = knows B list - {Key (priEK B), Key (priSK B), Key (shrK B)} - {X. Notes B X \<in> set list}) \<and> (A \<noteq> x1 \<longrightarrow> B = x1 \<longrightarrow> knows x1 list - {Key (priEK x1), Key (priSK x1), Key (shrK x1)} - {X. Notes x1 X \<in> set list} = insert x2 (knows x1 list) - {Key (priEK x1), Key (priSK x1), Key (shrK x1)} - {X. X = x2 \<or> Notes x1 X \<in> set list})
[PROOF STEP]
oops


[STATEMENT]
lemma knowledge_equiv_eq_old:
 "knows A evs  \<union>
   {Key (priEK B), Key (priSK B), Key (shrK B)} \<union>
     {X. Notes B X \<in> set evs}
  =
  knows B evs \<union>
   {Key (priEK A), Key (priSK A), Key (shrK A)} \<union>
     {X. Notes A X \<in> set evs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. knows A evs \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> {X. Notes B X \<in> set evs} = knows B evs \<union> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> {X. Notes A X \<in> set evs}
[PROOF STEP]
apply (induct_tac "evs", induct_tac "A", induct_tac "B")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa xaa. knows (Friend xa) [] \<union> {Key (priEK (Friend xaa)), Key (priSK (Friend xaa)), Key (shrK (Friend xaa))} \<union> {X. Notes (Friend xaa) X \<in> set []} = knows (Friend xaa) [] \<union> {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<union> {X. Notes (Friend xa) X \<in> set []}
 2. \<And>a list. knows A list \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> {X. Notes B X \<in> set list} = knows B list \<union> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> {X. Notes A X \<in> set list} \<Longrightarrow> knows A (a # list) \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> {X. Notes B X \<in> set (a # list)} = knows B (a # list) \<union> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> {X. Notes A X \<in> set (a # list)}
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. knows A list \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> {X. Notes B X \<in> set list} = knows B list \<union> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> {X. Notes A X \<in> set list} \<Longrightarrow> knows A (a # list) \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> {X. Notes B X \<in> set (a # list)} = knows B (a # list) \<union> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> {X. Notes A X \<in> set (a # list)}
[PROOF STEP]
apply (induct_tac "a")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a list x1 x2 x3. knows A list \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> {X. Notes B X \<in> set list} = knows B list \<union> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> {X. Notes A X \<in> set list} \<Longrightarrow> knows A (Says x1 x2 x3 # list) \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> {X. Notes B X \<in> set (Says x1 x2 x3 # list)} = knows B (Says x1 x2 x3 # list) \<union> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> {X. Notes A X \<in> set (Says x1 x2 x3 # list)}
 2. \<And>a list x1 x2. knows A list \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> {X. Notes B X \<in> set list} = knows B list \<union> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> {X. Notes A X \<in> set list} \<Longrightarrow> knows A (Gets x1 x2 # list) \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> {X. Notes B X \<in> set (Gets x1 x2 # list)} = knows B (Gets x1 x2 # list) \<union> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> {X. Notes A X \<in> set (Gets x1 x2 # list)}
 3. \<And>a list x1 x2. knows A list \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> {X. Notes B X \<in> set list} = knows B list \<union> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> {X. Notes A X \<in> set list} \<Longrightarrow> knows A (Notes x1 x2 # list) \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> {X. Notes B X \<in> set (Notes x1 x2 # list)} = knows B (Notes x1 x2 # list) \<union> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> {X. Notes A X \<in> set (Notes x1 x2 # list)}
[PROOF STEP]
txt\<open>Gets case solves because this event doesn't touch any agent knowledge\<close>
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a list x1 x2 x3. knows A list \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> {X. Notes B X \<in> set list} = knows B list \<union> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> {X. Notes A X \<in> set list} \<Longrightarrow> knows A (Says x1 x2 x3 # list) \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> {X. Notes B X \<in> set (Says x1 x2 x3 # list)} = knows B (Says x1 x2 x3 # list) \<union> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> {X. Notes A X \<in> set (Says x1 x2 x3 # list)}
 2. \<And>a list x1 x2. knows A list \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> {X. Notes B X \<in> set list} = knows B list \<union> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> {X. Notes A X \<in> set list} \<Longrightarrow> knows A (Gets x1 x2 # list) \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> {X. Notes B X \<in> set (Gets x1 x2 # list)} = knows B (Gets x1 x2 # list) \<union> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> {X. Notes A X \<in> set (Gets x1 x2 # list)}
 3. \<And>a list x1 x2. knows A list \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> {X. Notes B X \<in> set list} = knows B list \<union> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> {X. Notes A X \<in> set list} \<Longrightarrow> knows A (Notes x1 x2 # list) \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> {X. Notes B X \<in> set (Notes x1 x2 # list)} = knows B (Notes x1 x2 # list) \<union> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> {X. Notes A X \<in> set (Notes x1 x2 # list)}
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>list x3. insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))) \<Longrightarrow> insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (insert x3 (knows A list \<union> {X. Notes B X \<in> set list})))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (insert x3 (knows B list \<union> {X. Notes A X \<in> set list}))))
 2. \<And>list x1 x2. insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))) \<Longrightarrow> (A = x1 \<longrightarrow> B \<noteq> x1 \<longrightarrow> insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (insert x2 (knows x1 list \<union> {X. Notes B X \<in> set list})))) = insert (Key (priEK x1)) (insert (Key (priSK x1)) (insert (Key (shrK x1)) (knows B list \<union> {X. X = x2 \<or> Notes x1 X \<in> set list})))) \<and> (A \<noteq> x1 \<longrightarrow> B = x1 \<longrightarrow> insert (Key (priEK x1)) (insert (Key (priSK x1)) (insert (Key (shrK x1)) (knows A list \<union> {X. X = x2 \<or> Notes x1 X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (insert x2 (knows x1 list \<union> {X. Notes A X \<in> set list})))))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (24 subgoals):
 1. \<And>list x3 x. \<lbrakk>insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))); Key (priEK B) \<noteq> x3; Key (priEK B) \<notin> knows B list; Notes A (Key (priEK B)) \<notin> set list; priEK B \<noteq> priEK A; priEK B \<noteq> priSK A\<rbrakk> \<Longrightarrow> priEK B = shrK A
 2. \<And>list x3 x. \<lbrakk>insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))); Key (priSK B) \<noteq> x3; Key (priSK B) \<notin> knows B list; Notes A (Key (priSK B)) \<notin> set list; priSK B \<noteq> priEK A; priSK B \<noteq> priSK A\<rbrakk> \<Longrightarrow> priSK B = shrK A
 3. \<And>list x3 x. \<lbrakk>insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))); x \<noteq> Key (priEK A); x \<noteq> Key (priSK A); x \<noteq> Key (shrK A); x \<noteq> x3; x \<notin> knows B list; x \<in> knows A list\<rbrakk> \<Longrightarrow> Notes A x \<in> set list
 4. \<And>list x3 x. \<lbrakk>insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))); x \<noteq> Key (priEK A); x \<noteq> Key (priSK A); x \<noteq> Key (shrK A); x \<noteq> x3; x \<notin> knows B list; Notes B x \<in> set list\<rbrakk> \<Longrightarrow> Notes A x \<in> set list
 5. \<And>list x3 x. \<lbrakk>insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))); Key (priEK A) \<noteq> x3; Key (priEK A) \<notin> knows A list; Notes B (Key (priEK A)) \<notin> set list; priEK A \<noteq> priEK B; priEK A \<noteq> priSK B\<rbrakk> \<Longrightarrow> priEK A = shrK B
 6. \<And>list x3 x. \<lbrakk>insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))); Key (priSK A) \<noteq> x3; Key (priSK A) \<notin> knows A list; Notes B (Key (priSK A)) \<notin> set list; priSK A \<noteq> priEK B; priSK A \<noteq> priSK B\<rbrakk> \<Longrightarrow> priSK A = shrK B
 7. \<And>list x3 x. \<lbrakk>insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))); x \<noteq> Key (priEK B); x \<noteq> Key (priSK B); x \<noteq> Key (shrK B); x \<noteq> x3; x \<notin> knows A list; x \<in> knows B list\<rbrakk> \<Longrightarrow> Notes B x \<in> set list
 8. \<And>list x3 x. \<lbrakk>insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))); x \<noteq> Key (priEK B); x \<noteq> Key (priSK B); x \<noteq> Key (shrK B); x \<noteq> x3; x \<notin> knows A list; Notes A x \<in> set list\<rbrakk> \<Longrightarrow> Notes B x \<in> set list
 9. \<And>list x1 x2 x. \<lbrakk>insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))); B \<noteq> A; Key (priEK B) \<notin> knows B list; Notes A (Key (priEK B)) \<notin> set list; Key (priEK B) \<noteq> x2; priEK B \<noteq> priEK A; priEK B \<noteq> priSK A\<rbrakk> \<Longrightarrow> priEK B = shrK A
 10. \<And>list x1 x2 x. \<lbrakk>insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))); B \<noteq> A; Key (priSK B) \<notin> knows B list; Notes A (Key (priSK B)) \<notin> set list; Key (priSK B) \<noteq> x2; priSK B \<noteq> priEK A; priSK B \<noteq> priSK A\<rbrakk> \<Longrightarrow> priSK B = shrK A
A total of 24 subgoals...
[PROOF STEP]
txt\<open>speeds up subsequent blasting\<close>
[PROOF STATE]
proof (prove)
goal (24 subgoals):
 1. \<And>list x3 x. \<lbrakk>insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))); Key (priEK B) \<noteq> x3; Key (priEK B) \<notin> knows B list; Notes A (Key (priEK B)) \<notin> set list; priEK B \<noteq> priEK A; priEK B \<noteq> priSK A\<rbrakk> \<Longrightarrow> priEK B = shrK A
 2. \<And>list x3 x. \<lbrakk>insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))); Key (priSK B) \<noteq> x3; Key (priSK B) \<notin> knows B list; Notes A (Key (priSK B)) \<notin> set list; priSK B \<noteq> priEK A; priSK B \<noteq> priSK A\<rbrakk> \<Longrightarrow> priSK B = shrK A
 3. \<And>list x3 x. \<lbrakk>insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))); x \<noteq> Key (priEK A); x \<noteq> Key (priSK A); x \<noteq> Key (shrK A); x \<noteq> x3; x \<notin> knows B list; x \<in> knows A list\<rbrakk> \<Longrightarrow> Notes A x \<in> set list
 4. \<And>list x3 x. \<lbrakk>insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))); x \<noteq> Key (priEK A); x \<noteq> Key (priSK A); x \<noteq> Key (shrK A); x \<noteq> x3; x \<notin> knows B list; Notes B x \<in> set list\<rbrakk> \<Longrightarrow> Notes A x \<in> set list
 5. \<And>list x3 x. \<lbrakk>insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))); Key (priEK A) \<noteq> x3; Key (priEK A) \<notin> knows A list; Notes B (Key (priEK A)) \<notin> set list; priEK A \<noteq> priEK B; priEK A \<noteq> priSK B\<rbrakk> \<Longrightarrow> priEK A = shrK B
 6. \<And>list x3 x. \<lbrakk>insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))); Key (priSK A) \<noteq> x3; Key (priSK A) \<notin> knows A list; Notes B (Key (priSK A)) \<notin> set list; priSK A \<noteq> priEK B; priSK A \<noteq> priSK B\<rbrakk> \<Longrightarrow> priSK A = shrK B
 7. \<And>list x3 x. \<lbrakk>insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))); x \<noteq> Key (priEK B); x \<noteq> Key (priSK B); x \<noteq> Key (shrK B); x \<noteq> x3; x \<notin> knows A list; x \<in> knows B list\<rbrakk> \<Longrightarrow> Notes B x \<in> set list
 8. \<And>list x3 x. \<lbrakk>insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))); x \<noteq> Key (priEK B); x \<noteq> Key (priSK B); x \<noteq> Key (shrK B); x \<noteq> x3; x \<notin> knows A list; Notes A x \<in> set list\<rbrakk> \<Longrightarrow> Notes B x \<in> set list
 9. \<And>list x1 x2 x. \<lbrakk>insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))); B \<noteq> A; Key (priEK B) \<notin> knows B list; Notes A (Key (priEK B)) \<notin> set list; Key (priEK B) \<noteq> x2; priEK B \<noteq> priEK A; priEK B \<noteq> priSK A\<rbrakk> \<Longrightarrow> priEK B = shrK A
 10. \<And>list x1 x2 x. \<lbrakk>insert (Key (priEK B)) (insert (Key (priSK B)) (insert (Key (shrK B)) (knows A list \<union> {X. Notes B X \<in> set list}))) = insert (Key (priEK A)) (insert (Key (priSK A)) (insert (Key (shrK A)) (knows B list \<union> {X. Notes A X \<in> set list}))); B \<noteq> A; Key (priSK B) \<notin> knows B list; Notes A (Key (priSK B)) \<notin> set list; Key (priSK B) \<noteq> x2; priSK B \<noteq> priEK A; priSK B \<noteq> priSK A\<rbrakk> \<Longrightarrow> priSK B = shrK A
A total of 24 subgoals...
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
txt\<open>very very slow\<close>
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem knowledge_eval: "knows A evs =
       {Key (priEK A), Key (priSK A), Key (shrK A)} \<union>
       (Key ` range pubEK) \<union> (Key ` range pubSK) \<union>
       {X. \<exists> S R. Says S R X \<in> set evs} \<union>
       {X. Notes A X \<in> set evs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. knows A evs = {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> Key ` range pubK \<union> Key ` range pubSK \<union> {X. \<exists>S R. Says S R X \<in> set evs} \<union> {X. Notes A X \<in> set evs}
[PROOF STEP]
apply (induct_tac "A", induct_tac "evs")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. knows (Friend xa) [] = {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<union> Key ` range pubK \<union> Key ` range pubSK \<union> {X. \<exists>S R. Says S R X \<in> set []} \<union> {X. Notes (Friend xa) X \<in> set []}
 2. \<And>xa a list. knows (Friend xa) list = {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<union> Key ` range pubK \<union> Key ` range pubSK \<union> {X. \<exists>S R. Says S R X \<in> set list} \<union> {X. Notes (Friend xa) X \<in> set list} \<Longrightarrow> knows (Friend xa) (a # list) = {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<union> Key ` range pubK \<union> Key ` range pubSK \<union> {X. \<exists>S R. Says S R X \<in> set (a # list)} \<union> {X. Notes (Friend xa) X \<in> set (a # list)}
[PROOF STEP]
apply (induct_tac [2] "a")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>xa. knows (Friend xa) [] = {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<union> Key ` range pubK \<union> Key ` range pubSK \<union> {X. \<exists>S R. Says S R X \<in> set []} \<union> {X. Notes (Friend xa) X \<in> set []}
 2. \<And>xa a list x1 x2 x3. knows (Friend xa) list = {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<union> Key ` range pubK \<union> Key ` range pubSK \<union> {X. \<exists>S R. Says S R X \<in> set list} \<union> {X. Notes (Friend xa) X \<in> set list} \<Longrightarrow> knows (Friend xa) (Says x1 x2 x3 # list) = {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<union> Key ` range pubK \<union> Key ` range pubSK \<union> {X. \<exists>S R. Says S R X \<in> set (Says x1 x2 x3 # list)} \<union> {X. Notes (Friend xa) X \<in> set (Says x1 x2 x3 # list)}
 3. \<And>xa a list x1 x2. knows (Friend xa) list = {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<union> Key ` range pubK \<union> Key ` range pubSK \<union> {X. \<exists>S R. Says S R X \<in> set list} \<union> {X. Notes (Friend xa) X \<in> set list} \<Longrightarrow> knows (Friend xa) (Gets x1 x2 # list) = {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<union> Key ` range pubK \<union> Key ` range pubSK \<union> {X. \<exists>S R. Says S R X \<in> set (Gets x1 x2 # list)} \<union> {X. Notes (Friend xa) X \<in> set (Gets x1 x2 # list)}
 4. \<And>xa a list x1 x2. knows (Friend xa) list = {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<union> Key ` range pubK \<union> Key ` range pubSK \<union> {X. \<exists>S R. Says S R X \<in> set list} \<union> {X. Notes (Friend xa) X \<in> set list} \<Longrightarrow> knows (Friend xa) (Notes x1 x2 # list) = {Key (priEK (Friend xa)), Key (priSK (Friend xa)), Key (shrK (Friend xa))} \<union> Key ` range pubK \<union> Key ` range pubSK \<union> {X. \<exists>S R. Says S R X \<in> set (Notes x1 x2 # list)} \<union> {X. Notes (Friend xa) X \<in> set (Notes x1 x2 # list)}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma knowledge_eval_setdiff:
 "knows A evs  -
   {Key (priEK A), Key (priSK A), Key (shrK A)} -
     {X. Notes A X \<in> set evs}
  =
       (Key ` range pubEK) \<union> (Key ` range pubSK) \<union>
       {X. \<exists> S R. Says S R X \<in> set evs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. knows A evs - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set evs} = Key ` range pubK \<union> Key ` range pubSK \<union> {X. \<exists>S R. Says S R X \<in> set evs}
[PROOF STEP]
apply (simp only: knowledge_eval)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> Key ` range pubK \<union> Key ` range pubSK \<union> {X. \<exists>S R. Says S R X \<in> set evs} \<union> {X. Notes A X \<in> set evs} - {Key (priEK A), Key (priSK A), Key (shrK A)} - {X. Notes A X \<in> set evs} = Key ` range pubK \<union> Key ` range pubSK \<union> {X. \<exists>S R. Says S R X \<in> set evs}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>S R. Says S R (Key (priEK A)) \<in> set evs \<Longrightarrow> False
 2. \<And>S R. Says S R (Key (priSK A)) \<in> set evs \<Longrightarrow> False
 3. \<And>S R. Says S R (Key (shrK A)) \<in> set evs \<Longrightarrow> False
 4. \<And>xb. Notes A (Key (pubK xb)) \<in> set evs \<Longrightarrow> False
 5. \<And>xb. Notes A (Key (pubSK xb)) \<in> set evs \<Longrightarrow> False
 6. \<And>x S R. \<lbrakk>Notes A x \<in> set evs; Says S R x \<in> set evs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
oops


[STATEMENT]
theorem knowledge_equiv_eq: "knows A evs  \<union>
   {Key (priEK B), Key (priSK B), Key (shrK B)} \<union>
     {X. Notes B X \<in> set evs}
  =
  knows B evs \<union>
   {Key (priEK A), Key (priSK A), Key (shrK A)} \<union>
     {X. Notes A X \<in> set evs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. knows A evs \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> {X. Notes B X \<in> set evs} = knows B evs \<union> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> {X. Notes A X \<in> set evs}
[PROOF STEP]
apply (force simp only: knowledge_eval)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "knows A evs  \<union>
   {Key (priEK B), Key (priSK B), Key (shrK B)} \<union>
     {X. Notes B X \<in> set evs} -
(  {Key (priEK B), Key (priSK B), Key (shrK B)} \<union>
     {X. Notes B X \<in> set evs} ) = knows A evs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. knows A evs \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> {X. Notes B X \<in> set evs} - ({Key (priEK B), Key (priSK B), Key (shrK B)} \<union> {X. Notes B X \<in> set evs}) = knows A evs
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. Key (priEK B) \<in> knows A evs \<Longrightarrow> False
 2. Key (priSK B) \<in> knows A evs \<Longrightarrow> False
 3. Key (shrK B) \<in> knows A evs \<Longrightarrow> False
 4. \<And>x. \<lbrakk>x \<in> knows A evs; Notes B x \<in> set evs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
oops


[STATEMENT]
theorem parts_knowledge_equiv_eq: "
parts(knows A evs)  \<union>
   {Key (priEK B), Key (priSK B), Key (shrK B)} \<union>
     parts({X. Notes B X \<in> set evs})
  =
parts(knows B evs) \<union>
   {Key (priEK A), Key (priSK A), Key (shrK A)} \<union>
     parts({X. Notes A X \<in> set evs})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (knows A evs) \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> parts {X. Notes B X \<in> set evs} = parts (knows B evs) \<union> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> parts {X. Notes A X \<in> set evs}
[PROOF STEP]
apply (simp only: knowledge_eval parts_Un)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> parts (Key ` range pubK) \<union> parts (Key ` range pubSK) \<union> parts {X. \<exists>S R. Says S R X \<in> set evs} \<union> parts {X. Notes A X \<in> set evs} \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> parts {X. Notes B X \<in> set evs} = parts {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> parts (Key ` range pubK) \<union> parts (Key ` range pubSK) \<union> parts {X. \<exists>S R. Says S R X \<in> set evs} \<union> parts {X. Notes B X \<in> set evs} \<union> {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> parts {X. Notes A X \<in> set evs}
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem noprishr_parts_knowledge_equiv: "
\<lbrakk> X \<notin> {Key (priEK A), Key (priSK A), Key (shrK A)};
  X \<in> parts(knows A evs) \<rbrakk>
\<Longrightarrow>  X \<in> parts(knows B evs) \<union>
      parts({X. Notes A X \<in> set evs})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<notin> {Key (priEK A), Key (priSK A), Key (shrK A)}; X \<in> parts (knows A evs)\<rbrakk> \<Longrightarrow> X \<in> parts (knows B evs) \<union> parts {X. Notes A X \<in> set evs}
[PROOF STEP]
apply (force dest: UnI1 [THEN UnI1, THEN parts_knowledge_equiv])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma knowledge_equiv_eq_NS: "
  evs \<in> ns_public \<Longrightarrow>
  knows A evs  \<union> {Key (priEK B), Key (priSK B), Key (shrK B)}  =
  knows B evs \<union> {Key (priEK A), Key (priSK A), Key (shrK A)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evs \<in> ns_public \<Longrightarrow> knows A evs \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} = knows B evs \<union> {Key (priEK A), Key (priSK A), Key (shrK A)}
[PROOF STEP]
apply (force simp only: knowledge_eval NS_no_Notes)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma parts_knowledge_equiv_eq_NS: "
  evs \<in> ns_public \<Longrightarrow>
  parts(knows A evs) \<union> {Key (priEK B), Key (priSK B), Key (shrK B)}  =
  parts(knows B evs) \<union> {Key (priEK A), Key (priSK A), Key (shrK A)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evs \<in> ns_public \<Longrightarrow> parts (knows A evs) \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} = parts (knows B evs) \<union> {Key (priEK A), Key (priSK A), Key (shrK A)}
[PROOF STEP]
apply (simp only: knowledge_eval NS_no_Notes parts_Un)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evs \<in> ns_public \<Longrightarrow> parts {Key (priEK A), Key (priSK A), Key (shrK A)} \<union> parts (Key ` range pubK) \<union> parts (Key ` range pubSK) \<union> parts {X. \<exists>S R. Says S R X \<in> set evs} \<union> parts {X. False} \<union> {Key (priEK B), Key (priSK B), Key (shrK B)} = parts {Key (priEK B), Key (priSK B), Key (shrK B)} \<union> parts (Key ` range pubK) \<union> parts (Key ` range pubSK) \<union> parts {X. \<exists>S R. Says S R X \<in> set evs} \<union> parts {X. False} \<union> {Key (priEK A), Key (priSK A), Key (shrK A)}
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem noprishr_parts_knowledge_equiv_NS: "
\<lbrakk> X \<notin> {Key (priEK A), Key (priSK A), Key (shrK A)};
  X \<in> parts(knows A evs); evs \<in> ns_public \<rbrakk>
\<Longrightarrow>  X \<in> parts(knows B evs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<notin> {Key (priEK A), Key (priSK A), Key (shrK A)}; X \<in> parts (knows A evs); evs \<in> ns_public\<rbrakk> \<Longrightarrow> X \<in> parts (knows B evs)
[PROOF STEP]
apply (drule noprishr_parts_knowledge_equiv, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<in> parts (knows A evs); evs \<in> ns_public; X \<in> parts (knows ?B evs) \<union> parts {X. Notes A X \<in> set evs}\<rbrakk> \<Longrightarrow> X \<in> parts (knows B evs)
[PROOF STEP]
apply (simp add: NS_no_Notes)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem Agent_not_analz_N:
"\<lbrakk> Nonce N \<notin> parts(knows A evs); evs \<in> ns_public \<rbrakk>
 \<Longrightarrow> Nonce N \<notin> analz(knows B evs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Nonce N \<notin> parts (knows A evs); evs \<in> ns_public\<rbrakk> \<Longrightarrow> Nonce N \<notin> analz (knows B evs)
[PROOF STEP]
apply (force intro: noprishr_parts_knowledge_equiv_NS analz_into_parts)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "match_tcp_flags ipt_tcp_syn {TCP_SYN, TCP_URG, TCP_PSH}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match_tcp_flags ipt_tcp_syn {TCP_SYN, TCP_URG, TCP_PSH}
[PROOF STEP]
by eval


[STATEMENT]
lemma match_tcp_flags_nomatch: "\<not> c \<subseteq> fmask \<Longrightarrow> \<not> match_tcp_flags (TCP_Flags fmask c) pkt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> c \<subseteq> fmask \<Longrightarrow> \<not> match_tcp_flags (TCP_Flags fmask c) pkt
[PROOF STEP]
by auto


[STATEMENT]
lemma ipt_tcp_flags_NoMatch: "\<not> match_tcp_flags ipt_tcp_flags_NoMatch pkt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> match_tcp_flags ipt_tcp_flags_NoMatch pkt
[PROOF STEP]
by(simp add: ipt_tcp_flags_NoMatch_def)


[STATEMENT]
lemma ipt_tcp_flags_Any_isUNIV: "fmask = {} \<and> c = {} \<longleftrightarrow> (\<forall>pkt. match_tcp_flags (TCP_Flags fmask c) pkt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fmask = {} \<and> c = {}) = (\<forall>pkt. match_tcp_flags (TCP_Flags fmask c) pkt)
[PROOF STEP]
by auto


[STATEMENT]
lemma match_tcp_flags_conjunct: "match_tcp_flags (match_tcp_flags_conjunct f1 f2) pkt \<longleftrightarrow> match_tcp_flags f1 pkt \<and> match_tcp_flags f2 pkt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match_tcp_flags (match_tcp_flags_conjunct f1 f2) pkt = (match_tcp_flags f1 pkt \<and> match_tcp_flags f2 pkt)
[PROOF STEP]
apply(cases f1, cases f2, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>f1 = TCP_Flags x1 x2; f2 = TCP_Flags x1a x2a\<rbrakk> \<Longrightarrow> (x2 \<subseteq> x1 \<and> x2a \<subseteq> x1a \<and> x1 \<inter> x1a \<inter> x2 = x1 \<inter> x1a \<inter> x2a \<longrightarrow> (pkt \<inter> (x1 \<union> x1a) = x2 \<union> x2a) = (pkt \<inter> x1 = x2 \<and> pkt \<inter> x1a = x2a)) \<and> ((x2a \<subseteq> x1a \<longrightarrow> x2 \<subseteq> x1 \<longrightarrow> x1 \<inter> x1a \<inter> x2 \<noteq> x1 \<inter> x1a \<inter> x2a) \<longrightarrow> match_tcp_flags ipt_tcp_flags_NoMatch pkt = (pkt \<inter> x1 = x2 \<and> pkt \<inter> x1a = x2a))
[PROOF STEP]
apply(rename_tac fmask1 c1 fmask2 c2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fmask1 c1 fmask2 c2. \<lbrakk>f1 = TCP_Flags fmask1 c1; f2 = TCP_Flags fmask2 c2\<rbrakk> \<Longrightarrow> (c1 \<subseteq> fmask1 \<and> c2 \<subseteq> fmask2 \<and> fmask1 \<inter> fmask2 \<inter> c1 = fmask1 \<inter> fmask2 \<inter> c2 \<longrightarrow> (pkt \<inter> (fmask1 \<union> fmask2) = c1 \<union> c2) = (pkt \<inter> fmask1 = c1 \<and> pkt \<inter> fmask2 = c2)) \<and> ((c2 \<subseteq> fmask2 \<longrightarrow> c1 \<subseteq> fmask1 \<longrightarrow> fmask1 \<inter> fmask2 \<inter> c1 \<noteq> fmask1 \<inter> fmask2 \<inter> c2) \<longrightarrow> match_tcp_flags ipt_tcp_flags_NoMatch pkt = (pkt \<inter> fmask1 = c1 \<and> pkt \<inter> fmask2 = c2))
[PROOF STEP]
apply(intro conjI impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fmask1 c1 fmask2 c2. \<lbrakk>f1 = TCP_Flags fmask1 c1; f2 = TCP_Flags fmask2 c2; c1 \<subseteq> fmask1 \<and> c2 \<subseteq> fmask2 \<and> fmask1 \<inter> fmask2 \<inter> c1 = fmask1 \<inter> fmask2 \<inter> c2\<rbrakk> \<Longrightarrow> (pkt \<inter> (fmask1 \<union> fmask2) = c1 \<union> c2) = (pkt \<inter> fmask1 = c1 \<and> pkt \<inter> fmask2 = c2)
 2. \<And>fmask1 c1 fmask2 c2. \<lbrakk>f1 = TCP_Flags fmask1 c1; f2 = TCP_Flags fmask2 c2; c2 \<subseteq> fmask2 \<longrightarrow> c1 \<subseteq> fmask1 \<longrightarrow> fmask1 \<inter> fmask2 \<inter> c1 \<noteq> fmask1 \<inter> fmask2 \<inter> c2\<rbrakk> \<Longrightarrow> match_tcp_flags ipt_tcp_flags_NoMatch pkt = (pkt \<inter> fmask1 = c1 \<and> pkt \<inter> fmask2 = c2)
[PROOF STEP]
apply(elim conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fmask1 c1 fmask2 c2. \<lbrakk>f1 = TCP_Flags fmask1 c1; f2 = TCP_Flags fmask2 c2; c1 \<subseteq> fmask1; c2 \<subseteq> fmask2; fmask1 \<inter> fmask2 \<inter> c1 = fmask1 \<inter> fmask2 \<inter> c2\<rbrakk> \<Longrightarrow> (pkt \<inter> (fmask1 \<union> fmask2) = c1 \<union> c2) = (pkt \<inter> fmask1 = c1 \<and> pkt \<inter> fmask2 = c2)
 2. \<And>fmask1 c1 fmask2 c2. \<lbrakk>f1 = TCP_Flags fmask1 c1; f2 = TCP_Flags fmask2 c2; c2 \<subseteq> fmask2 \<longrightarrow> c1 \<subseteq> fmask1 \<longrightarrow> fmask1 \<inter> fmask2 \<inter> c1 \<noteq> fmask1 \<inter> fmask2 \<inter> c2\<rbrakk> \<Longrightarrow> match_tcp_flags ipt_tcp_flags_NoMatch pkt = (pkt \<inter> fmask1 = c1 \<and> pkt \<inter> fmask2 = c2)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fmask1 c1 fmask2 c2. \<lbrakk>f1 = TCP_Flags fmask1 c1; f2 = TCP_Flags fmask2 c2; c2 \<subseteq> fmask2 \<longrightarrow> c1 \<subseteq> fmask1 \<longrightarrow> fmask1 \<inter> fmask2 \<inter> c1 \<noteq> fmask1 \<inter> fmask2 \<inter> c2\<rbrakk> \<Longrightarrow> match_tcp_flags ipt_tcp_flags_NoMatch pkt = (pkt \<inter> fmask1 = c1 \<and> pkt \<inter> fmask2 = c2)
[PROOF STEP]
apply(simp add: ipt_tcp_flags_NoMatch)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fmask1 c1 fmask2 c2. \<lbrakk>f1 = TCP_Flags fmask1 c1; f2 = TCP_Flags fmask2 c2; c2 \<subseteq> fmask2 \<longrightarrow> c1 \<subseteq> fmask1 \<longrightarrow> fmask1 \<inter> fmask2 \<inter> c1 \<noteq> fmask1 \<inter> fmask2 \<inter> c2\<rbrakk> \<Longrightarrow> pkt \<inter> fmask1 = c1 \<longrightarrow> pkt \<inter> fmask2 \<noteq> c2
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "match_tcp_flags_conjunct_option ipt_tcp_syn (TCP_Flags {TCP_RST,TCP_ACK} {TCP_RST}) = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match_tcp_flags_conjunct_option ipt_tcp_syn (TCP_Flags {TCP_RST, TCP_ACK} {TCP_RST}) = None
[PROOF STEP]
by eval


[STATEMENT]
lemma match_tcp_flags_conjunct_option_Some: "match_tcp_flags_conjunct_option f1 f2 = Some f3 \<Longrightarrow>
      match_tcp_flags f1 pkt \<and> match_tcp_flags f2 pkt \<longleftrightarrow> match_tcp_flags f3 pkt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match_tcp_flags_conjunct_option f1 f2 = Some f3 \<Longrightarrow> (match_tcp_flags f1 pkt \<and> match_tcp_flags f2 pkt) = match_tcp_flags f3 pkt
[PROOF STEP]
apply(simp add: match_tcp_flags_conjunct_option_def split: ipt_tcp_flags.split_asm if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>match_tcp_flags_conjunct f1 f2 = f3; x2 \<subseteq> x1; TCP_Flags x1 x2 = f3\<rbrakk> \<Longrightarrow> (match_tcp_flags f1 pkt \<and> match_tcp_flags f2 pkt) = match_tcp_flags f3 pkt
[PROOF STEP]
using match_tcp_flags_conjunct
[PROOF STATE]
proof (prove)
using this:
match_tcp_flags (match_tcp_flags_conjunct ?f1.0 ?f2.0) ?pkt = (match_tcp_flags ?f1.0 ?pkt \<and> match_tcp_flags ?f2.0 ?pkt)

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>match_tcp_flags_conjunct f1 f2 = f3; x2 \<subseteq> x1; TCP_Flags x1 x2 = f3\<rbrakk> \<Longrightarrow> (match_tcp_flags f1 pkt \<and> match_tcp_flags f2 pkt) = match_tcp_flags f3 pkt
[PROOF STEP]
by blast


[STATEMENT]
lemma match_tcp_flags_conjunct_option_None: "match_tcp_flags_conjunct_option f1 f2 = None \<Longrightarrow>
      \<not>(match_tcp_flags f1 pkt \<and> match_tcp_flags f2 pkt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match_tcp_flags_conjunct_option f1 f2 = None \<Longrightarrow> \<not> (match_tcp_flags f1 pkt \<and> match_tcp_flags f2 pkt)
[PROOF STEP]
apply(simp add: match_tcp_flags_conjunct_option_def split: ipt_tcp_flags.split_asm if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>match_tcp_flags_conjunct f1 f2 = TCP_Flags x1 x2; \<not> x2 \<subseteq> x1\<rbrakk> \<Longrightarrow> match_tcp_flags f1 pkt \<longrightarrow> \<not> match_tcp_flags f2 pkt
[PROOF STEP]
using match_tcp_flags_conjunct match_tcp_flags_nomatch
[PROOF STATE]
proof (prove)
using this:
match_tcp_flags (match_tcp_flags_conjunct ?f1.0 ?f2.0) ?pkt = (match_tcp_flags ?f1.0 ?pkt \<and> match_tcp_flags ?f2.0 ?pkt)
\<not> ?c \<subseteq> ?fmask \<Longrightarrow> \<not> match_tcp_flags (TCP_Flags ?fmask ?c) ?pkt

goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>match_tcp_flags_conjunct f1 f2 = TCP_Flags x1 x2; \<not> x2 \<subseteq> x1\<rbrakk> \<Longrightarrow> match_tcp_flags f1 pkt \<longrightarrow> \<not> match_tcp_flags f2 pkt
[PROOF STEP]
by metis


[STATEMENT]
lemma match_tcp_flags_conjunct_option: "(case match_tcp_flags_conjunct_option f1 f2 of None \<Rightarrow> False | Some f3 \<Rightarrow> match_tcp_flags f3 pkt) \<longleftrightarrow> match_tcp_flags f1 pkt \<and> match_tcp_flags f2 pkt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case match_tcp_flags_conjunct_option f1 f2 of None \<Rightarrow> False | Some f3 \<Rightarrow> match_tcp_flags f3 pkt) = (match_tcp_flags f1 pkt \<and> match_tcp_flags f2 pkt)
[PROOF STEP]
apply(simp split: option.split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (match_tcp_flags_conjunct_option f1 f2 = None \<longrightarrow> match_tcp_flags f1 pkt \<longrightarrow> \<not> match_tcp_flags f2 pkt) \<and> (\<forall>x2. match_tcp_flags_conjunct_option f1 f2 = Some x2 \<longrightarrow> match_tcp_flags x2 pkt = (match_tcp_flags f1 pkt \<and> match_tcp_flags f2 pkt))
[PROOF STEP]
using match_tcp_flags_conjunct_option_Some match_tcp_flags_conjunct_option_None
[PROOF STATE]
proof (prove)
using this:
match_tcp_flags_conjunct_option ?f1.0 ?f2.0 = Some ?f3.0 \<Longrightarrow> (match_tcp_flags ?f1.0 ?pkt \<and> match_tcp_flags ?f2.0 ?pkt) = match_tcp_flags ?f3.0 ?pkt
match_tcp_flags_conjunct_option ?f1.0 ?f2.0 = None \<Longrightarrow> \<not> (match_tcp_flags ?f1.0 ?pkt \<and> match_tcp_flags ?f2.0 ?pkt)

goal (1 subgoal):
 1. (match_tcp_flags_conjunct_option f1 f2 = None \<longrightarrow> match_tcp_flags f1 pkt \<longrightarrow> \<not> match_tcp_flags f2 pkt) \<and> (\<forall>x2. match_tcp_flags_conjunct_option f1 f2 = Some x2 \<longrightarrow> match_tcp_flags x2 pkt = (match_tcp_flags f1 pkt \<and> match_tcp_flags f2 pkt))
[PROOF STEP]
by blast


[STATEMENT]
lemma funny_set_falg_fmask_helper: "c2 \<subseteq> fmask2 \<Longrightarrow> (c1 = c2 \<and> fmask1 = fmask2) = (\<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c2 \<subseteq> fmask2 \<Longrightarrow> (c1 = c2 \<and> fmask1 = fmask2) = (\<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c2 \<subseteq> fmask2; c1 = c2 \<and> fmask1 = fmask2\<rbrakk> \<Longrightarrow> \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)
 2. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> c1 = c2 \<and> fmask1 = fmask2
[PROOF STEP]
apply presburger
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> c1 = c2 \<and> fmask1 = fmask2
[PROOF STEP]
apply(subgoal_tac "fmask1 = fmask2")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2); fmask1 = fmask2\<rbrakk> \<Longrightarrow> c1 = c2 \<and> fmask1 = fmask2
 2. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
(*"e": Try this: by (metis Diff_Compl Diff_eq Int_lower2 Un_Diff_Int compl_sup disjoint_eq_subset_Compl inf_assoc inf_commute inf_sup_absorb) (> 1.0 s, timed out).
      Isar proof (300 ms):*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
assume a1: "c2 \<subseteq> fmask2"
[PROOF STATE]
proof (state)
this:
c2 \<subseteq> fmask2

goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
assume a2: "\<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)"
[PROOF STATE]
proof (state)
this:
\<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)

goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
have f3: "\<And>A Aa. (A::'a set) - - Aa = Aa - - A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A Aa. A - - Aa = Aa - - A
[PROOF STEP]
by (simp add: inf_commute)
[PROOF STATE]
proof (state)
this:
?A - - ?Aa = ?Aa - - ?A

goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
have f4: "\<And>A Aa. (A::'a set) - - (- Aa) = A - Aa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A Aa. A - - (- Aa) = A - Aa
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?A - - (- ?Aa) = ?A - ?Aa

goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
have f5: "\<And>A Aa Ab. (A::'a set) - - Aa - - Ab = A - - (Aa - - Ab)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A Aa Ab. A - - Aa - - Ab = A - - (Aa - - Ab)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?A - - ?Aa - - ?Ab = ?A - - (?Aa - - ?Ab)

goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
have f6: "\<And>A Aa. (A::'a set) - (- A - Aa) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A Aa. A - (- A - Aa) = A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?A - (- ?A - ?Aa) = ?A

goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
have f7: "\<And>A Aa. - (A::'a set) - - Aa = Aa - A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A Aa. - A - - Aa = Aa - A
[PROOF STEP]
using f4 f3
[PROOF STATE]
proof (prove)
using this:
?A - - (- ?Aa) = ?A - ?Aa
?A - - ?Aa = ?Aa - - ?A

goal (1 subgoal):
 1. \<And>A Aa. - A - - Aa = Aa - A
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
- ?A - - ?Aa = ?Aa - ?A

goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
have f8: "\<And>A Aa. - (A::'a set) = - (A - Aa) - (A - - Aa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A Aa. - A = - (A - Aa) - (A - - Aa)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
- ?A = - (?A - ?Aa) - (?A - - ?Aa)

goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
have f9: "c1 = - (- c1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c1 = - (- c1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c1 = - (- c1)

goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
have f10: "\<And>A. A - c1 - c1 = A - c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A. A - c1 - c1 = A - c1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?A - c1 - c1 = ?A - c1

goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
have "\<And>A. A - - (fmask1 - - fmask2) = c2 \<or> A - - fmask1 \<noteq> c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A. A - - (fmask1 - - fmask2) = c2 \<or> A - - fmask1 \<noteq> c1
[PROOF STEP]
using f6 f5 a2
[PROOF STATE]
proof (prove)
using this:
?A - (- ?A - ?Aa) = ?A
?A - - ?Aa - - ?Ab = ?A - - (?Aa - - ?Ab)
\<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)

goal (1 subgoal):
 1. \<And>A. A - - (fmask1 - - fmask2) = c2 \<or> A - - fmask1 \<noteq> c1
[PROOF STEP]
by (metis (no_types) Diff_Compl)
[PROOF STATE]
proof (state)
this:
?A - - (fmask1 - - fmask2) = c2 \<or> ?A - - fmask1 \<noteq> c1

goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
hence f11: "\<And>A. - A - - (fmask1 - - fmask2) = c2 \<or> fmask1 - A \<noteq> c1"
[PROOF STATE]
proof (prove)
using this:
?A - - (fmask1 - - fmask2) = c2 \<or> ?A - - fmask1 \<noteq> c1

goal (1 subgoal):
 1. \<And>A. - A - - (fmask1 - - fmask2) = c2 \<or> fmask1 - A \<noteq> c1
[PROOF STEP]
using f7
[PROOF STATE]
proof (prove)
using this:
?A - - (fmask1 - - fmask2) = c2 \<or> ?A - - fmask1 \<noteq> c1
- ?A - - ?Aa = ?Aa - ?A

goal (1 subgoal):
 1. \<And>A. - A - - (fmask1 - - fmask2) = c2 \<or> fmask1 - A \<noteq> c1
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
- ?A - - (fmask1 - - fmask2) = c2 \<or> fmask1 - ?A \<noteq> c1

goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
have "c2 - fmask2 = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c2 - fmask2 = {}
[PROOF STEP]
using a1
[PROOF STATE]
proof (prove)
using this:
c2 \<subseteq> fmask2

goal (1 subgoal):
 1. c2 - fmask2 = {}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
c2 - fmask2 = {}

goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
hence f12: "- c2 - (fmask2 - c2) = - fmask2"
[PROOF STATE]
proof (prove)
using this:
c2 - fmask2 = {}

goal (1 subgoal):
 1. - c2 - (fmask2 - c2) = - fmask2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
- c2 - (fmask2 - c2) = - fmask2

goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
hence "fmask2 - - c2 = c2"
[PROOF STATE]
proof (prove)
using this:
- c2 - (fmask2 - c2) = - fmask2

goal (1 subgoal):
 1. fmask2 - - c2 = c2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fmask2 - - c2 = c2

goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
hence f13: "fmask1 - - c2 = c1"
[PROOF STATE]
proof (prove)
using this:
fmask2 - - c2 = c2

goal (1 subgoal):
 1. fmask1 - - c2 = c1
[PROOF STEP]
using f3 a2
[PROOF STATE]
proof (prove)
using this:
fmask2 - - c2 = c2
?A - - ?Aa = ?Aa - - ?A
\<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)

goal (1 subgoal):
 1. fmask1 - - c2 = c1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fmask1 - - c2 = c1

goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
hence f14: "c1 = c2"
[PROOF STATE]
proof (prove)
using this:
fmask1 - - c2 = c1

goal (1 subgoal):
 1. c1 = c2
[PROOF STEP]
using f11
[PROOF STATE]
proof (prove)
using this:
fmask1 - - c2 = c1
- ?A - - (fmask1 - - fmask2) = c2 \<or> fmask1 - ?A \<noteq> c1

goal (1 subgoal):
 1. c1 = c2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c1 = c2

goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
hence f15: "fmask2 - (fmask1 - c1) = c1"
[PROOF STATE]
proof (prove)
using this:
c1 = c2

goal (1 subgoal):
 1. fmask2 - (fmask1 - c1) = c1
[PROOF STEP]
using f13 f10 f9 f8 f7 f3 a2
[PROOF STATE]
proof (prove)
using this:
c1 = c2
fmask1 - - c2 = c1
?A - c1 - c1 = ?A - c1
c1 = - (- c1)
- ?A = - (?A - ?Aa) - (?A - - ?Aa)
- ?A - - ?Aa = ?Aa - ?A
?A - - ?Aa = ?Aa - - ?A
\<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)

goal (1 subgoal):
 1. fmask2 - (fmask1 - c1) = c1
[PROOF STEP]
by (metis Diff_Compl)
[PROOF STATE]
proof (state)
this:
fmask2 - (fmask1 - c1) = c1

goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
have "fmask1 - (fmask2 - c1) = c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmask1 - (fmask2 - c1) = c1
[PROOF STEP]
using f14 f12 f10 f9 f8 f4 f3 a2
[PROOF STATE]
proof (prove)
using this:
c1 = c2
- c2 - (fmask2 - c2) = - fmask2
?A - c1 - c1 = ?A - c1
c1 = - (- c1)
- ?A = - (?A - ?Aa) - (?A - - ?Aa)
?A - - (- ?Aa) = ?A - ?Aa
?A - - ?Aa = ?Aa - - ?A
\<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)

goal (1 subgoal):
 1. fmask1 - (fmask2 - c1) = c1
[PROOF STEP]
by (metis Diff_Compl)
[PROOF STATE]
proof (state)
this:
fmask1 - (fmask2 - c1) = c1

goal (1 subgoal):
 1. \<lbrakk>c2 \<subseteq> fmask2; \<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)\<rbrakk> \<Longrightarrow> fmask1 = fmask2
[PROOF STEP]
thus "fmask1 = fmask2"
[PROOF STATE]
proof (prove)
using this:
fmask1 - (fmask2 - c1) = c1

goal (1 subgoal):
 1. fmask1 = fmask2
[PROOF STEP]
using f15
[PROOF STATE]
proof (prove)
using this:
fmask1 - (fmask2 - c1) = c1
fmask2 - (fmask1 - c1) = c1

goal (1 subgoal):
 1. fmask1 = fmask2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fmask1 = fmask2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ipt_tcp_flags_equal: "ipt_tcp_flags_equal f1 f2 \<longleftrightarrow> (\<forall>pkt. match_tcp_flags f1 pkt = match_tcp_flags f2 pkt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipt_tcp_flags_equal f1 f2 = (\<forall>pkt. match_tcp_flags f1 pkt = match_tcp_flags f2 pkt)
[PROOF STEP]
apply(cases f1, cases f2, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>f1 = TCP_Flags x1 x2; f2 = TCP_Flags x1a x2a\<rbrakk> \<Longrightarrow> (x2 \<subseteq> x1 \<and> x2a \<subseteq> x1a \<longrightarrow> (x2 = x2a \<and> x1 = x1a) = (\<forall>pkt. (pkt \<inter> x1 = x2) = (pkt \<inter> x1a = x2a))) \<and> ((x2 \<subseteq> x1 \<longrightarrow> \<not> x2a \<subseteq> x1a) \<longrightarrow> (\<not> x2 \<subseteq> x1 \<and> \<not> x2a \<subseteq> x1a) = (\<forall>pkt. (pkt \<inter> x1 = x2) = (pkt \<inter> x1a = x2a)))
[PROOF STEP]
apply(rename_tac fmask1 c1 fmask2 c2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fmask1 c1 fmask2 c2. \<lbrakk>f1 = TCP_Flags fmask1 c1; f2 = TCP_Flags fmask2 c2\<rbrakk> \<Longrightarrow> (c1 \<subseteq> fmask1 \<and> c2 \<subseteq> fmask2 \<longrightarrow> (c1 = c2 \<and> fmask1 = fmask2) = (\<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2))) \<and> ((c1 \<subseteq> fmask1 \<longrightarrow> \<not> c2 \<subseteq> fmask2) \<longrightarrow> (\<not> c1 \<subseteq> fmask1 \<and> \<not> c2 \<subseteq> fmask2) = (\<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2)))
[PROOF STEP]
apply(intro conjI impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>fmask1 c1 fmask2 c2. \<lbrakk>f1 = TCP_Flags fmask1 c1; f2 = TCP_Flags fmask2 c2; c1 \<subseteq> fmask1 \<and> c2 \<subseteq> fmask2\<rbrakk> \<Longrightarrow> (c1 = c2 \<and> fmask1 = fmask2) = (\<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2))
 2. \<And>fmask1 c1 fmask2 c2. \<lbrakk>f1 = TCP_Flags fmask1 c1; f2 = TCP_Flags fmask2 c2; c1 \<subseteq> fmask1 \<longrightarrow> \<not> c2 \<subseteq> fmask2\<rbrakk> \<Longrightarrow> (\<not> c1 \<subseteq> fmask1 \<and> \<not> c2 \<subseteq> fmask2) = (\<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2))
[PROOF STEP]
using funny_set_falg_fmask_helper
[PROOF STATE]
proof (prove)
using this:
?c2.0 \<subseteq> ?fmask2.0 \<Longrightarrow> (?c1.0 = ?c2.0 \<and> ?fmask1.0 = ?fmask2.0) = (\<forall>pkt. (pkt \<inter> ?fmask1.0 = ?c1.0) = (pkt \<inter> ?fmask2.0 = ?c2.0))

goal (2 subgoals):
 1. \<And>fmask1 c1 fmask2 c2. \<lbrakk>f1 = TCP_Flags fmask1 c1; f2 = TCP_Flags fmask2 c2; c1 \<subseteq> fmask1 \<and> c2 \<subseteq> fmask2\<rbrakk> \<Longrightarrow> (c1 = c2 \<and> fmask1 = fmask2) = (\<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2))
 2. \<And>fmask1 c1 fmask2 c2. \<lbrakk>f1 = TCP_Flags fmask1 c1; f2 = TCP_Flags fmask2 c2; c1 \<subseteq> fmask1 \<longrightarrow> \<not> c2 \<subseteq> fmask2\<rbrakk> \<Longrightarrow> (\<not> c1 \<subseteq> fmask1 \<and> \<not> c2 \<subseteq> fmask2) = (\<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2))
[PROOF STEP]
apply metis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>fmask1 c1 fmask2 c2. \<lbrakk>f1 = TCP_Flags fmask1 c1; f2 = TCP_Flags fmask2 c2; c1 \<subseteq> fmask1 \<longrightarrow> \<not> c2 \<subseteq> fmask2\<rbrakk> \<Longrightarrow> (\<not> c1 \<subseteq> fmask1 \<and> \<not> c2 \<subseteq> fmask2) = (\<forall>pkt. (pkt \<inter> fmask1 = c1) = (pkt \<inter> fmask2 = c2))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma protectRefl: "PROP Pure.prop (PROP C) \<Longrightarrow> PROP Pure.prop (PROP C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (PROP C) \<Longrightarrow> (PROP C)
[PROOF STEP]
by (simp add: prop_def)


[STATEMENT]
lemma protectImp:
 assumes i: "PROP Pure.prop (PROP P \<Longrightarrow> PROP Q)"
 shows "PROP Pure.prop (PROP Pure.prop P \<Longrightarrow> PROP Pure.prop Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (PROP P) \<Longrightarrow> (PROP Q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (PROP P) \<Longrightarrow> (PROP Q)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (PROP P) \<Longrightarrow> (PROP Q)
[PROOF STEP]
assume P: "PROP Pure.prop P"
[PROOF STATE]
proof (state)
this:
PROP P

goal (1 subgoal):
 1. (PROP P) \<Longrightarrow> (PROP Q)
[PROOF STEP]
from i [unfolded prop_def, OF P [unfolded prop_def]]
[PROOF STATE]
proof (chain)
picking this:
PROP Q
[PROOF STEP]
have "PROP Pure.prop Q"
[PROOF STATE]
proof (prove)
using this:
PROP Q

goal (1 subgoal):
 1. PROP Q
[PROOF STEP]
by (simp add: prop_def)
[PROOF STATE]
proof (state)
this:
PROP Q

goal (1 subgoal):
 1. (PROP P) \<Longrightarrow> (PROP Q)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(PROP P) \<Longrightarrow> (PROP Q)

goal (1 subgoal):
 1. (PROP P) \<Longrightarrow> (PROP Q)
[PROOF STEP]
note i' = this
[PROOF STATE]
proof (state)
this:
(PROP P) \<Longrightarrow> (PROP Q)

goal (1 subgoal):
 1. (PROP P) \<Longrightarrow> (PROP Q)
[PROOF STEP]
show "PROP ?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (PROP P) \<Longrightarrow> (PROP Q)
[PROOF STEP]
apply (rule protectI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (PROP P) \<Longrightarrow> (PROP Q)
[PROOF STEP]
apply (rule i')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (PROP P) \<Longrightarrow> (PROP P)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(PROP P) \<Longrightarrow> (PROP Q)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma generaliseConj:
  assumes i1: "PROP Pure.prop (PROP Pure.prop (Trueprop P) \<Longrightarrow> PROP Pure.prop (Trueprop Q))"
  assumes i2: "PROP Pure.prop (PROP Pure.prop (Trueprop P') \<Longrightarrow> PROP Pure.prop (Trueprop Q'))"
  shows "PROP Pure.prop (PROP Pure.prop (Trueprop (P \<and> P')) \<Longrightarrow> (PROP Pure.prop (Trueprop (Q \<and> Q'))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<and> P') \<Longrightarrow> (Q \<and> Q')
[PROOF STEP]
using i1 i2
[PROOF STATE]
proof (prove)
using this:
(P) \<Longrightarrow> (Q)
(P') \<Longrightarrow> (Q')

goal (1 subgoal):
 1. (P \<and> P') \<Longrightarrow> (Q \<and> Q')
[PROOF STEP]
by (auto simp add: prop_def)


[STATEMENT]
lemma generaliseAll:
 assumes i: "PROP Pure.prop (\<And>s. PROP Pure.prop (Trueprop (P s)) \<Longrightarrow> PROP Pure.prop (Trueprop (Q s)))"
 shows "PROP Pure.prop (PROP Pure.prop (Trueprop (\<forall>s. P s)) \<Longrightarrow> PROP Pure.prop (Trueprop (\<forall>s. Q s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>s. P s) \<Longrightarrow> (\<forall>s. Q s)
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
\<And>s. (P s) \<Longrightarrow> (Q s)

goal (1 subgoal):
 1. (\<forall>s. P s) \<Longrightarrow> (\<forall>s. Q s)
[PROOF STEP]
by (auto simp add: prop_def)


[STATEMENT]
lemma generalise_all:
 assumes i: "PROP Pure.prop (\<And>s. PROP Pure.prop (PROP P s) \<Longrightarrow> PROP Pure.prop (PROP Q s))"
 shows "PROP Pure.prop ((PROP Pure.prop (\<And>s. PROP P s)) \<Longrightarrow> (PROP Pure.prop (\<And>s. PROP Q s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. PROP P s) \<Longrightarrow> (\<And>s. PROP Q s)
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
\<And>s. (PROP P s) \<Longrightarrow> (PROP Q s)

goal (1 subgoal):
 1. (\<And>s. PROP P s) \<Longrightarrow> (\<And>s. PROP Q s)
[PROOF STEP]
proof (unfold prop_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. PROP P s \<Longrightarrow> PROP Q s; Pure.all P\<rbrakk> \<Longrightarrow> Pure.all Q
[PROOF STEP]
assume i1: "\<And>s. (PROP P s) \<Longrightarrow> (PROP Q s)"
[PROOF STATE]
proof (state)
this:
PROP P ?s \<Longrightarrow> PROP Q ?s

goal (1 subgoal):
 1. \<lbrakk>\<And>s. PROP P s \<Longrightarrow> PROP Q s; Pure.all P\<rbrakk> \<Longrightarrow> Pure.all Q
[PROOF STEP]
assume i2: "\<And>s. PROP P s"
[PROOF STATE]
proof (state)
this:
PROP P ?s

goal (1 subgoal):
 1. \<lbrakk>\<And>s. PROP P s \<Longrightarrow> PROP Q s; Pure.all P\<rbrakk> \<Longrightarrow> Pure.all Q
[PROOF STEP]
show "\<And>s. PROP Q s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. PROP Q s
[PROOF STEP]
by (rule i1) (rule i2)
[PROOF STATE]
proof (state)
this:
PROP Q ?s

goal:
No subgoals!
[PROOF STEP]
qed