[STATEMENT]
lemma (in trace_top) liveness_dense_iff:
  assumes P: "P \<subseteq> A\<^sup>\<infinity>"
  shows "liveness A P = (P dense)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
have "liveness A P = (\<forall>r\<in>A\<^sup>\<star>. \<exists> s \<in> A\<^sup>\<infinity>. r @@ s \<in> P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liveness A P = (\<forall>r\<in>A\<^sup>\<star>. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P)
[PROOF STEP]
by (simp add: liveness_def)
[PROOF STATE]
proof (state)
this:
liveness A P = (\<forall>r\<in>A\<^sup>\<star>. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P)

goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
liveness A P = (\<forall>r\<in>A\<^sup>\<star>. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P)

goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
have "\<dots> = (\<forall>x\<in>A\<^sup>\<infinity>. \<forall> r \<in> finpref A x. \<exists> s \<in> A\<^sup>\<infinity>. r @@ s \<in> P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>r\<in>A\<^sup>\<star>. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P) = (\<forall>x\<in>A\<^sup>\<infinity>. \<forall>r\<in>finpref A x. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P)
[PROOF STEP]
by (auto simp: finpref_def dest: finsubsetall)
[PROOF STATE]
proof (state)
this:
(\<forall>r\<in>A\<^sup>\<star>. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P) = (\<forall>x\<in>A\<^sup>\<infinity>. \<forall>r\<in>finpref A x. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P)

goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>r\<in>A\<^sup>\<star>. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P) = (\<forall>x\<in>A\<^sup>\<infinity>. \<forall>r\<in>finpref A x. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P)

goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
have "\<dots> = (\<forall>x\<in>A\<^sup>\<infinity>. x adh P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>A\<^sup>\<infinity>. \<forall>r\<in>finpref A x. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P) = (\<forall>x\<in>A\<^sup>\<infinity>. x adh P)
[PROOF STEP]
using P
[PROOF STATE]
proof (prove)
using this:
P \<subseteq> A\<^sup>\<infinity>

goal (1 subgoal):
 1. (\<forall>x\<in>A\<^sup>\<infinity>. \<forall>r\<in>finpref A x. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P) = (\<forall>x\<in>A\<^sup>\<infinity>. x adh P)
[PROOF STEP]
by (simp add: adh_lemma)
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>A\<^sup>\<infinity>. \<forall>r\<in>finpref A x. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P) = (\<forall>x\<in>A\<^sup>\<infinity>. x adh P)

goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>A\<^sup>\<infinity>. \<forall>r\<in>finpref A x. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P) = (\<forall>x\<in>A\<^sup>\<infinity>. x adh P)

goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
have "\<dots> = (A\<^sup>\<infinity> \<subseteq> closure P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>A\<^sup>\<infinity>. x adh P) = (A\<^sup>\<infinity> \<subseteq> closure P)
[PROOF STEP]
using P
[PROOF STATE]
proof (prove)
using this:
P \<subseteq> A\<^sup>\<infinity>

goal (1 subgoal):
 1. (\<forall>x\<in>A\<^sup>\<infinity>. x adh P) = (A\<^sup>\<infinity> \<subseteq> closure P)
[PROOF STEP]
by (auto simp: adh_closure_iff ttop_carrier)
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>A\<^sup>\<infinity>. x adh P) = (A\<^sup>\<infinity> \<subseteq> closure P)

goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>A\<^sup>\<infinity>. x adh P) = (A\<^sup>\<infinity> \<subseteq> closure P)

goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
have "\<dots> = (P dense)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A\<^sup>\<infinity> \<subseteq> closure P) = (P dense)
[PROOF STEP]
by (simp add: liveness_def is_dense_def is_densein_def ttop_carrier)
[PROOF STATE]
proof (state)
this:
(A\<^sup>\<infinity> \<subseteq> closure P) = (P dense)

goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
liveness A P = (P dense)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
liveness A P = (P dense)

goal (1 subgoal):
 1. liveness A P = (P dense)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
liveness A P = (P dense)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem (in trace_top) alpern_schneider:
assumes Psub:     "P \<subseteq> A\<^sup>\<infinity>"
  shows "\<exists> S L. safety A S \<and> liveness A L \<and> P = S \<inter> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>S L. safety A S \<and> liveness A L \<and> P = S \<inter> L
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>S L. safety A S \<and> liveness A L \<and> P = S \<inter> L
[PROOF STEP]
from Psub
[PROOF STATE]
proof (chain)
picking this:
P \<subseteq> A\<^sup>\<infinity>
[PROOF STEP]
have "P \<subseteq> carrier"
[PROOF STATE]
proof (prove)
using this:
P \<subseteq> A\<^sup>\<infinity>

goal (1 subgoal):
 1. P \<subseteq> carrier
[PROOF STEP]
by (simp add: ttop_carrier)
[PROOF STATE]
proof (state)
this:
P \<subseteq> carrier

goal (1 subgoal):
 1. \<exists>S L. safety A S \<and> liveness A L \<and> P = S \<inter> L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<subseteq> carrier
[PROOF STEP]
obtain L S where
    Lsub: "L \<subseteq> carrier" and
    Ssub: "S \<subseteq> carrier" and
    Sclosed: "S closed" and
    Ldense: "L dense" and
    Pinter: "P = S \<inter> L"
[PROOF STATE]
proof (prove)
using this:
P \<subseteq> carrier

goal (1 subgoal):
 1. (\<And>L S. \<lbrakk>L \<subseteq> carrier; S \<subseteq> carrier; S closed; L dense; P = S \<inter> L\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (blast elim: topology.ex_dense_closure_interE [OF topology])
[PROOF STATE]
proof (state)
this:
L \<subseteq> carrier
S \<subseteq> carrier
S closed
L dense
P = S \<inter> L

goal (1 subgoal):
 1. \<exists>S L. safety A S \<and> liveness A L \<and> P = S \<inter> L
[PROOF STEP]
from Ssub Sclosed
[PROOF STATE]
proof (chain)
picking this:
S \<subseteq> carrier
S closed
[PROOF STEP]
have "safety A S"
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> carrier
S closed

goal (1 subgoal):
 1. safety A S
[PROOF STEP]
by (simp add: safety_closed_iff ttop_carrier)
[PROOF STATE]
proof (state)
this:
safety A S

goal (1 subgoal):
 1. \<exists>S L. safety A S \<and> liveness A L \<and> P = S \<inter> L
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
safety A S

goal (1 subgoal):
 1. \<exists>S L. safety A S \<and> liveness A L \<and> P = S \<inter> L
[PROOF STEP]
from Lsub Ldense
[PROOF STATE]
proof (chain)
picking this:
L \<subseteq> carrier
L dense
[PROOF STEP]
have "liveness A L"
[PROOF STATE]
proof (prove)
using this:
L \<subseteq> carrier
L dense

goal (1 subgoal):
 1. liveness A L
[PROOF STEP]
by (simp add: liveness_dense_iff ttop_carrier)
[PROOF STATE]
proof (state)
this:
liveness A L

goal (1 subgoal):
 1. \<exists>S L. safety A S \<and> liveness A L \<and> P = S \<inter> L
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
safety A S
liveness A L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
safety A S
liveness A L

goal (1 subgoal):
 1. \<exists>S L. safety A S \<and> liveness A L \<and> P = S \<inter> L
[PROOF STEP]
using Pinter
[PROOF STATE]
proof (prove)
using this:
safety A S
liveness A L
P = S \<inter> L

goal (1 subgoal):
 1. \<exists>S L. safety A S \<and> liveness A L \<and> P = S \<inter> L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>S L. safety A S \<and> liveness A L \<and> P = S \<inter> L

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in ptrace_top) suff_ptop_nhd_base:
  assumes unhd: "u \<in> nhds t"
  and H: "\<And>r. \<lbrakk> r \<in> pfinpref A t; suff A r \<subseteq> u \<rbrakk> \<Longrightarrow> R"
  shows "R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. R
[PROOF STEP]
from unhd
[PROOF STATE]
proof (chain)
picking this:
u \<in> nhds t
[PROOF STEP]
obtain m where
    uA: "u \<subseteq> A\<^sup>\<spadesuit>" and
    mopen: "m open" and
    tm: "t \<in> m" and
    mu: "m \<subseteq> u"
[PROOF STATE]
proof (prove)
using this:
u \<in> nhds t

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>u \<subseteq> A\<^sup>\<spadesuit>; m open; t \<in> m; m \<subseteq> u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: ptop_carrier)
[PROOF STATE]
proof (state)
this:
u \<subseteq> A\<^sup>\<spadesuit>
m open
t \<in> m
m \<subseteq> u

goal (1 subgoal):
 1. R
[PROOF STEP]
from mopen tm
[PROOF STATE]
proof (chain)
picking this:
m open
t \<in> m
[PROOF STEP]
have
    "\<exists>r \<in> pfinpref A t. suff A r \<subseteq> m"
[PROOF STATE]
proof (prove)
using this:
m open
t \<in> m

goal (1 subgoal):
 1. \<exists>r\<in>pfinpref A t. suff A r \<subseteq> m
[PROOF STEP]
proof (induct "m")
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<in> B; t \<in> x\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x
 2. \<And>x y. \<lbrakk>x open; t \<in> x \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x; y open; t \<in> y \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> y; t \<in> x \<inter> y\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x \<inter> y
 3. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
case (basic a)
[PROOF STATE]
proof (state)
this:
a \<in> B
t \<in> a

goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<in> B; t \<in> x\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x
 2. \<And>x y. \<lbrakk>x open; t \<in> x \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x; y open; t \<in> y \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> y; t \<in> x \<inter> y\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x \<inter> y
 3. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> B
t \<in> a
[PROOF STEP]
obtain s where sA: "s \<in> A\<^sup>\<clubsuit>" and as: "a = suff A s" and ta: "t \<in> a"
[PROOF STATE]
proof (prove)
using this:
a \<in> B
t \<in> a

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> A\<^sup>\<clubsuit>; a = suff A s; t \<in> a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<in> A\<^sup>\<clubsuit>
a = suff A s
t \<in> a

goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<in> B; t \<in> x\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x
 2. \<And>x y. \<lbrakk>x open; t \<in> x \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x; y open; t \<in> y \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> y; t \<in> x \<inter> y\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x \<inter> y
 3. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
from sA as ta
[PROOF STATE]
proof (chain)
picking this:
s \<in> A\<^sup>\<clubsuit>
a = suff A s
t \<in> a
[PROOF STEP]
have "s \<in> pfinpref A t"
[PROOF STATE]
proof (prove)
using this:
s \<in> A\<^sup>\<clubsuit>
a = suff A s
t \<in> a

goal (1 subgoal):
 1. s \<in> pfinpref A t
[PROOF STEP]
by (auto simp: pfinpref_def dest: suff_finpref)
[PROOF STATE]
proof (state)
this:
s \<in> pfinpref A t

goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<in> B; t \<in> x\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x
 2. \<And>x y. \<lbrakk>x open; t \<in> x \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x; y open; t \<in> y \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> y; t \<in> x \<inter> y\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x \<inter> y
 3. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
s \<in> pfinpref A t

goal (1 subgoal):
 1. \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a
[PROOF STEP]
using as
[PROOF STATE]
proof (prove)
using this:
s \<in> pfinpref A t
a = suff A s

goal (1 subgoal):
 1. \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r\<in>pfinpref A t. suff A r \<subseteq> a

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x open; t \<in> x \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x; y open; t \<in> y \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> y; t \<in> x \<inter> y\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x \<inter> y
 2. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x open; t \<in> x \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x; y open; t \<in> y \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> y; t \<in> x \<inter> y\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x \<inter> y
 2. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
case (inter a b)
[PROOF STATE]
proof (state)
this:
a open
t \<in> a \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a
b open
t \<in> b \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> b
t \<in> a \<inter> b

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x open; t \<in> x \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x; y open; t \<in> y \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> y; t \<in> x \<inter> y\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x \<inter> y
 2. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a open
t \<in> a \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a
b open
t \<in> b \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> b
t \<in> a \<inter> b
[PROOF STEP]
obtain r r' where
      rt: "r \<in> pfinpref A t" and ra: "suff A r \<subseteq> a" and
      r't: "r' \<in> pfinpref A t" and r'b: "suff A r' \<subseteq> b"
[PROOF STATE]
proof (prove)
using this:
a open
t \<in> a \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a
b open
t \<in> b \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> b
t \<in> a \<inter> b

goal (1 subgoal):
 1. (\<And>r r'. \<lbrakk>r \<in> pfinpref A t; suff A r \<subseteq> a; r' \<in> pfinpref A t; suff A r' \<subseteq> b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> pfinpref A t
suff A r \<subseteq> a
r' \<in> pfinpref A t
suff A r' \<subseteq> b

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x open; t \<in> x \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x; y open; t \<in> y \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> y; t \<in> x \<inter> y\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x \<inter> y
 2. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
from rt r't
[PROOF STATE]
proof (chain)
picking this:
r \<in> pfinpref A t
r' \<in> pfinpref A t
[PROOF STEP]
have "r \<le> r' \<or> r' \<le> r"
[PROOF STATE]
proof (prove)
using this:
r \<in> pfinpref A t
r' \<in> pfinpref A t

goal (1 subgoal):
 1. r \<le> r' \<or> r' \<le> r
[PROOF STEP]
by (auto simp: pfinpref_def finpref_def dest: pref_locally_linear)
[PROOF STATE]
proof (state)
this:
r \<le> r' \<or> r' \<le> r

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x open; t \<in> x \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x; y open; t \<in> y \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> y; t \<in> x \<inter> y\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> x \<inter> y
 2. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
r \<le> r' \<or> r' \<le> r

goal (1 subgoal):
 1. \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r \<le> r' \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
 2. r' \<le> r \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
assume "r \<le> r'"
[PROOF STATE]
proof (state)
this:
r \<le> r'

goal (2 subgoals):
 1. r \<le> r' \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
 2. r' \<le> r \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
hence "suff A r' \<subseteq> suff A r"
[PROOF STATE]
proof (prove)
using this:
r \<le> r'

goal (1 subgoal):
 1. suff A r' \<subseteq> suff A r
[PROOF STEP]
by (rule suff_mono2)
[PROOF STATE]
proof (state)
this:
suff A r' \<subseteq> suff A r

goal (2 subgoals):
 1. r \<le> r' \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
 2. r' \<le> r \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
suff A r' \<subseteq> suff A r

goal (1 subgoal):
 1. \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
using r't ra r'b
[PROOF STATE]
proof (prove)
using this:
suff A r' \<subseteq> suff A r
r' \<in> pfinpref A t
suff A r \<subseteq> a
suff A r' \<subseteq> b

goal (1 subgoal):
 1. \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b

goal (1 subgoal):
 1. r' \<le> r \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r' \<le> r \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
assume "r' \<le> r"
[PROOF STATE]
proof (state)
this:
r' \<le> r

goal (1 subgoal):
 1. r' \<le> r \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
hence "suff A r \<subseteq> suff A r'"
[PROOF STATE]
proof (prove)
using this:
r' \<le> r

goal (1 subgoal):
 1. suff A r \<subseteq> suff A r'
[PROOF STEP]
by (rule suff_mono2)
[PROOF STATE]
proof (state)
this:
suff A r \<subseteq> suff A r'

goal (1 subgoal):
 1. r' \<le> r \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
suff A r \<subseteq> suff A r'

goal (1 subgoal):
 1. \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
using rt r'b ra
[PROOF STATE]
proof (prove)
using this:
suff A r \<subseteq> suff A r'
r \<in> pfinpref A t
suff A r' \<subseteq> b
suff A r \<subseteq> a

goal (1 subgoal):
 1. \<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>r\<in>pfinpref A t. suff A r \<subseteq> a \<inter> b

goal (1 subgoal):
 1. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
case (union M)
[PROOF STATE]
proof (state)
this:
\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta))
t \<in> \<Union> M

goal (1 subgoal):
 1. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta))
t \<in> \<Union> M
[PROOF STEP]
obtain v where
      "t \<in> v" and vM: "v \<in> M"
[PROOF STATE]
proof (prove)
using this:
\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta))
t \<in> \<Union> M

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>t \<in> v; v \<in> M\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t \<in> v
v \<in> M

goal (1 subgoal):
 1. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> v
v \<in> M
[PROOF STEP]
obtain r where "r\<in>pfinpref A t" "suff A r \<subseteq> v"
[PROOF STATE]
proof (prove)
using this:
t \<in> v
v \<in> M

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>r \<in> pfinpref A t; suff A r \<subseteq> v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using union
[PROOF STATE]
proof (prove)
using this:
t \<in> v
v \<in> M
\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta))
t \<in> \<Union> M

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>r \<in> pfinpref A t; suff A r \<subseteq> v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> pfinpref A t
suff A r \<subseteq> v

goal (1 subgoal):
 1. \<And>M. \<lbrakk>\<forall>ta\<in>M. ta open \<and> (t \<in> ta \<longrightarrow> (\<exists>r\<in>pfinpref A t. suff A r \<subseteq> ta)); t \<in> \<Union> M\<rbrakk> \<Longrightarrow> \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
r \<in> pfinpref A t
suff A r \<subseteq> v

goal (1 subgoal):
 1. \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
using vM
[PROOF STATE]
proof (prove)
using this:
r \<in> pfinpref A t
suff A r \<subseteq> v
v \<in> M

goal (1 subgoal):
 1. \<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r\<in>pfinpref A t. suff A r \<subseteq> \<Union> M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>r\<in>pfinpref A t. suff A r \<subseteq> m

goal (1 subgoal):
 1. R
[PROOF STEP]
with mu
[PROOF STATE]
proof (chain)
picking this:
m \<subseteq> u
\<exists>r\<in>pfinpref A t. suff A r \<subseteq> m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m \<subseteq> u
\<exists>r\<in>pfinpref A t. suff A r \<subseteq> m

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inheritedJoinI[rule_format]: "[| inherited subs P; inherited subs Q; R = ( % x . P x & Q x) |] ==> inherited subs R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inherited subs P; inherited subs Q; R = (\<lambda>x. P x \<and> Q x)\<rbrakk> \<Longrightarrow> inherited subs R
[PROOF STEP]
by(blast intro!:inheritedI dest: inheritedUnEq inheritedIncLevelEq inheritedInsertEq inheritedEmpty)


[STATEMENT]
lemma R\<^sub>N_0 [simp]: "R\<^sub>N 0 u l = return_pmf 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R\<^sub>N 0 u l = return_pmf 0
[PROOF STEP]
unfolding R\<^sub>N_def R_def SL_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf (\<lambda>f. steps {..<0} f 0 u l) (Pi_pmf.Pi_pmf {..<0} 0 (\<lambda>_. geometric_pmf p)) = return_pmf 0
[PROOF STEP]
by (auto simp add: steps.simps)


[STATEMENT]
lemma in_kD_after_update [simp]:
  fixes rt nip dsn dsk flag hops nhip pre
  shows "kD (update rt nip (dsn, dsk, flag, hops, nhip, pre)) = insert nip (kD rt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kD (update rt nip (dsn, dsk, flag, hops, nhip, pre)) = insert nip (kD rt)
[PROOF STEP]
unfolding update_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kD (case rt nip of None \<Rightarrow> rt(nip \<mapsto> (dsn, dsk, flag, hops, nhip, pre)) | Some s \<Rightarrow> if \<pi>\<^sub>2 s < \<pi>\<^sub>2 (dsn, dsk, flag, hops, nhip, pre) then rt(nip \<mapsto> addpre (dsn, dsk, flag, hops, nhip, pre) (\<pi>\<^sub>7 s)) else if \<pi>\<^sub>2 s = \<pi>\<^sub>2 (dsn, dsk, flag, hops, nhip, pre) \<and> (\<pi>\<^sub>5 (dsn, dsk, flag, hops, nhip, pre) < \<pi>\<^sub>5 s \<or> \<pi>\<^sub>4 s = Aodv_Basic.inv) then rt(nip \<mapsto> addpre (dsn, dsk, flag, hops, nhip, pre) (\<pi>\<^sub>7 s)) else if \<pi>\<^sub>3 (dsn, dsk, flag, hops, nhip, pre) = unk then rt(nip \<mapsto> (\<pi>\<^sub>2 s, snd (addpre (dsn, dsk, flag, hops, nhip, pre) (\<pi>\<^sub>7 s)))) else rt(nip \<mapsto> addpre s (\<pi>\<^sub>7 (dsn, dsk, flag, hops, nhip, pre)))) = insert nip (kD rt)
[PROOF STEP]
by (cases "rt nip") auto


[STATEMENT]
lemma hom_graph_compl:
  "hom_graph f S x a \<Longrightarrow> hom_graph f S (- x) (- a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hom_graph f S x a \<Longrightarrow> hom_graph f S (- x) (- a)
[PROOF STEP]
by (induct set: hom_graph, simp_all add: hom_graph.intros compl_ifte)


[STATEMENT]
lemma max_pos_imp_Interp:
  assumes "C \<in> N" and "C \<noteq> {#}" and "Max_mset C = Pos A" and "S C = {#}"
  shows "Interp C \<Turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Interp C \<Turnstile> C
[PROOF STEP]
proof (cases "productive C")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. production C \<noteq> {} \<Longrightarrow> Interp C \<Turnstile> C
 2. \<not> production C \<noteq> {} \<Longrightarrow> Interp C \<Turnstile> C
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
production C \<noteq> {}

goal (2 subgoals):
 1. production C \<noteq> {} \<Longrightarrow> Interp C \<Turnstile> C
 2. \<not> production C \<noteq> {} \<Longrightarrow> Interp C \<Turnstile> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
production C \<noteq> {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
production C \<noteq> {}

goal (1 subgoal):
 1. Interp C \<Turnstile> C
[PROOF STEP]
by (fast intro: productive_imp_Interp)
[PROOF STATE]
proof (state)
this:
Interp C \<Turnstile> C

goal (1 subgoal):
 1. \<not> production C \<noteq> {} \<Longrightarrow> Interp C \<Turnstile> C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> production C \<noteq> {} \<Longrightarrow> Interp C \<Turnstile> C
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> production C \<noteq> {}

goal (1 subgoal):
 1. \<not> production C \<noteq> {} \<Longrightarrow> Interp C \<Turnstile> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> production C \<noteq> {}
[PROOF STEP]
have "interp C \<Turnstile> C"
[PROOF STATE]
proof (prove)
using this:
\<not> production C \<noteq> {}

goal (1 subgoal):
 1. interp C \<Turnstile> C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> production C \<noteq> {}
C \<in> N
C \<noteq> {#}
Max_mset C = Pos A
S C = {#}

goal (1 subgoal):
 1. interp C \<Turnstile> C
[PROOF STEP]
unfolding production_unfold
[PROOF STATE]
proof (prove)
using this:
\<not> {A. C \<in> N \<and> C \<noteq> {#} \<and> Max_mset C = Pos A \<and> \<not> interp C \<Turnstile> C \<and> S C = {#}} \<noteq> {}
C \<in> N
C \<noteq> {#}
Max_mset C = Pos A
S C = {#}

goal (1 subgoal):
 1. interp C \<Turnstile> C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
interp C \<Turnstile> C

goal (1 subgoal):
 1. \<not> production C \<noteq> {} \<Longrightarrow> Interp C \<Turnstile> C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
interp C \<Turnstile> C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
interp C \<Turnstile> C

goal (1 subgoal):
 1. Interp C \<Turnstile> C
[PROOF STEP]
unfolding Interp_def
[PROOF STATE]
proof (prove)
using this:
interp C \<Turnstile> C

goal (1 subgoal):
 1. interp C \<union> production C \<Turnstile> C
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
interp C \<Turnstile> C
\<not> production C \<noteq> {}

goal (1 subgoal):
 1. interp C \<union> production C \<Turnstile> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Interp C \<Turnstile> C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Group) rcs_sub_smult:"\<lbrakk>G \<guillemotright> H; G \<guillemotright> N; a \<in> H\<rbrakk> \<Longrightarrow> N \<bullet> a \<subseteq> N \<diamondop>\<^bsub>G\<^esub> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G \<guillemotright> H ; G \<guillemotright> N ; a \<in> H\<rbrakk> \<Longrightarrow> N \<bullet> a \<subseteq> N \<diamondop> H
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>G \<guillemotright> H ; G \<guillemotright> N ; a \<in> H; x \<in> N \<bullet> a\<rbrakk> \<Longrightarrow> x \<in> N \<diamondop> H
[PROOF STEP]
apply (simp add:rcs_def s_top_def, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Group) joint_D_gchains:"\<lbrakk>D_gchain G n f; D_gchain G m g;
       g 0 \<subset> f n \<rbrakk> \<Longrightarrow>  D_gchain G (Suc (n + m)) (jointfun n f m g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n\<rbrakk> \<Longrightarrow> D_gchain G (Suc (n + m)) (jointfun n f m g)
[PROOF STEP]
apply (simp add:D_gchain_def [of "G" "Suc (n + m)" _])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n\<rbrakk> \<Longrightarrow> d_gchain G (Suc (n + m)) (jointfun n f m g) \<and> (\<forall>l\<le>n + m. jointfun n f m g (Suc l) \<subset> jointfun n f m g l)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n\<rbrakk> \<Longrightarrow> d_gchain G (Suc (n + m)) (jointfun n f m g)
 2. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n\<rbrakk> \<Longrightarrow> \<forall>l\<le>n + m. jointfun n f m g (Suc l) \<subset> jointfun n f m g l
[PROOF STEP]
apply (rule joint_d_gchains[of n f m g],
       simp add:D_gchain_is_d_gchain,
       simp add:D_gchain_is_d_gchain,
       simp add:psubset_imp_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n\<rbrakk> \<Longrightarrow> \<forall>l\<le>n + m. jointfun n f m g (Suc l) \<subset> jointfun n f m g l
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m\<rbrakk> \<Longrightarrow> jointfun n f m g (Suc l) \<subset> jointfun n f m g l
[PROOF STEP]
apply (case_tac "Suc l \<le> n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; Suc l \<le> n\<rbrakk> \<Longrightarrow> jointfun n f m g (Suc l) \<subset> jointfun n f m g l
 2. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; \<not> Suc l \<le> n\<rbrakk> \<Longrightarrow> jointfun n f m g (Suc l) \<subset> jointfun n f m g l
[PROOF STEP]
apply (simp add:jointfun_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; Suc l \<le> n\<rbrakk> \<Longrightarrow> f (Suc l) \<subset> f l
 2. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; \<not> Suc l \<le> n\<rbrakk> \<Longrightarrow> jointfun n f m g (Suc l) \<subset> jointfun n f m g l
[PROOF STEP]
apply (rule_tac i = l and j = "Suc l" in D_gchain0[of n f], assumption,
        cut_tac x = l and y = "Suc l" and z = n in less_le_trans)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; Suc l \<le> n\<rbrakk> \<Longrightarrow> l < Suc l
 2. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; Suc l \<le> n\<rbrakk> \<Longrightarrow> Suc l \<le> n
 3. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; Suc l \<le> n; l < n\<rbrakk> \<Longrightarrow> l \<le> n
 4. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; Suc l \<le> n\<rbrakk> \<Longrightarrow> Suc l \<le> n
 5. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; Suc l \<le> n\<rbrakk> \<Longrightarrow> l < Suc l
 6. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; \<not> Suc l \<le> n\<rbrakk> \<Longrightarrow> jointfun n f m g (Suc l) \<subset> jointfun n f m g l
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; \<not> Suc l \<le> n\<rbrakk> \<Longrightarrow> jointfun n f m g (Suc l) \<subset> jointfun n f m g l
[PROOF STEP]
apply (simp add:nat_not_le_less,
        frule_tac m = n and n = "Suc l" in Suc_leI, thin_tac "n < Suc l", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; n \<le> l\<rbrakk> \<Longrightarrow> jointfun n f m g (Suc l) \<subset> jointfun n f m g l
[PROOF STEP]
apply (case_tac "l = n", simp add:jointfun_def sliden_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; n \<le> l; l \<noteq> n\<rbrakk> \<Longrightarrow> jointfun n f m g (Suc l) \<subset> jointfun n f m g l
[PROOF STEP]
apply (frule not_sym, thin_tac "l \<noteq> n",
        frule_tac x = n and y = l in le_imp_less_or_eq,
        thin_tac "n \<le> l", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; n < l\<rbrakk> \<Longrightarrow> jointfun n f m g (Suc l) \<subset> jointfun n f m g l
[PROOF STEP]
apply (simp add:jointfun_def sliden_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; n < l\<rbrakk> \<Longrightarrow> g (l - n) \<subset> g (l - Suc n)
[PROOF STEP]
apply (frule_tac m = l and n = "n + m" and l = n in  diff_le_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; n < l; l - n \<le> n + m - n\<rbrakk> \<Longrightarrow> g (l - n) \<subset> g (l - Suc n)
[PROOF STEP]
apply (simp add:diff_add_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; n < l; l - n \<le> m\<rbrakk> \<Longrightarrow> g (l - n) \<subset> g (l - Suc n)
[PROOF STEP]
apply (rule_tac i = "l - Suc n" and j = "l - n" in D_gchain0[of m g],
         assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; n < l; l - n \<le> m\<rbrakk> \<Longrightarrow> l - Suc n \<le> m
 2. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; n < l; l - n \<le> m\<rbrakk> \<Longrightarrow> l - n \<le> m
 3. \<And>l. \<lbrakk>D_gchain G n f; D_gchain G m g; g 0 \<subset> f n; l \<le> n + m; n < l; l - n \<le> m\<rbrakk> \<Longrightarrow> l - Suc n < l - n
[PROOF STEP]
apply (arith, assumption, arith)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Group) Nset_Suc_im:"\<forall>l \<le> (Suc n). G \<guillemotright> (f l) \<Longrightarrow>
                 insert (f (Suc n)) (f ` {i. i \<le> n}) = f ` {i. i \<le> (Suc n)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l\<le>Suc n. G \<guillemotright> f l  \<Longrightarrow> insert (f (Suc n)) (f ` {i. i \<le> n}) = f ` {i. i \<le> Suc n}
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>l\<le>Suc n. G \<guillemotright> f l  \<Longrightarrow> insert (f (Suc n)) (f ` {i. i \<le> n}) \<subseteq> f ` {i. i \<le> Suc n}
 2. \<forall>l\<le>Suc n. G \<guillemotright> f l  \<Longrightarrow> f ` {i. i \<le> Suc n} \<subseteq> insert (f (Suc n)) (f ` {i. i \<le> n})
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>l\<le>Suc n. G \<guillemotright> f l ; x \<in> insert (f (Suc n)) (f ` {i. i \<le> n})\<rbrakk> \<Longrightarrow> x \<in> f ` {i. i \<le> Suc n}
 2. \<forall>l\<le>Suc n. G \<guillemotright> f l  \<Longrightarrow> f ` {i. i \<le> Suc n} \<subseteq> insert (f (Suc n)) (f ` {i. i \<le> n})
[PROOF STEP]
apply (simp add:image_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>l\<le>Suc n. G \<guillemotright> f l ; x = f (Suc n) \<or> (\<exists>xa\<le>n. x = f xa)\<rbrakk> \<Longrightarrow> \<exists>xa\<le>Suc n. x = f xa
 2. \<forall>l\<le>Suc n. G \<guillemotright> f l  \<Longrightarrow> f ` {i. i \<le> Suc n} \<subseteq> insert (f (Suc n)) (f ` {i. i \<le> n})
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<forall>l\<le>Suc n. G \<guillemotright> f l ; x = f (Suc n)\<rbrakk> \<Longrightarrow> \<exists>xa\<le>Suc n. x = f xa
 2. \<And>x. \<lbrakk>\<forall>l\<le>Suc n. G \<guillemotright> f l ; \<exists>xa\<le>n. x = f xa\<rbrakk> \<Longrightarrow> \<exists>xa\<le>Suc n. x = f xa
 3. \<forall>l\<le>Suc n. G \<guillemotright> f l  \<Longrightarrow> f ` {i. i \<le> Suc n} \<subseteq> insert (f (Suc n)) (f ` {i. i \<le> n})
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>l\<le>Suc n. G \<guillemotright> f l ; \<exists>xa\<le>n. x = f xa\<rbrakk> \<Longrightarrow> \<exists>xa\<le>Suc n. x = f xa
 2. \<forall>l\<le>Suc n. G \<guillemotright> f l  \<Longrightarrow> f ` {i. i \<le> Suc n} \<subseteq> insert (f (Suc n)) (f ` {i. i \<le> n})
[PROOF STEP]
apply (erule exE, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>\<forall>l\<le>Suc n. G \<guillemotright> f l ; xa \<le> n; x = f xa\<rbrakk> \<Longrightarrow> \<exists>xa\<le>Suc n. x = f xa
 2. \<forall>l\<le>Suc n. G \<guillemotright> f l  \<Longrightarrow> f ` {i. i \<le> Suc n} \<subseteq> insert (f (Suc n)) (f ` {i. i \<le> n})
[PROOF STEP]
apply (frule_tac x = xa and y = n and z = "Suc n" in le_less_trans,
         simp,
         frule_tac x = xa and y = "Suc n" in less_imp_le, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l\<le>Suc n. G \<guillemotright> f l  \<Longrightarrow> f ` {i. i \<le> Suc n} \<subseteq> insert (f (Suc n)) (f ` {i. i \<le> n})
[PROOF STEP]
apply (cut_tac Nset_Suc [of "n"], simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Qw_cmpser:"\<lbrakk>Group G; w_cmpser G (Suc n) f \<rbrakk> \<Longrightarrow>
                               Gchain n (Qw_cmpser G f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Group G; w_cmpser G (Suc n) f\<rbrakk> \<Longrightarrow> Gchain n (Qw_cmpser G f)
[PROOF STEP]
apply (simp add:Gchain_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Group G; w_cmpser G (Suc n) f\<rbrakk> \<Longrightarrow> \<forall>l\<le>n. Group (Qw_cmpser G f l)
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>Group G; w_cmpser G (Suc n) f; l \<le> n\<rbrakk> \<Longrightarrow> Group (Qw_cmpser G f l)
[PROOF STEP]
apply (simp  add:Qw_cmpser_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>Group G; w_cmpser G (Suc n) f; l \<le> n\<rbrakk> \<Longrightarrow> Group (\<natural>\<^bsub>G\<^esub>f l / f (Suc l))
[PROOF STEP]
apply (simp add:w_cmpser_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>Group G; d_gchain G (Suc n) f \<and> (\<forall>l\<le>n. \<natural>\<^bsub>G\<^esub>f l \<triangleright> f (Suc l)); l \<le> n\<rbrakk> \<Longrightarrow> Group (\<natural>\<^bsub>G\<^esub>f l / f (Suc l))
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>Group G; l \<le> n; d_gchain G (Suc n) f; \<forall>l\<le>n. \<natural>\<^bsub>G\<^esub>f l \<triangleright> f (Suc l)\<rbrakk> \<Longrightarrow> Group (\<natural>\<^bsub>G\<^esub>f l / f (Suc l))
[PROOF STEP]
apply (simp add:d_gchain_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>Group G; l \<le> n; \<forall>l\<le>Suc n. G \<guillemotright> f l  \<and> (\<forall>l\<le>n. f (Suc l) \<subseteq> f l); \<forall>l\<le>n. \<natural>\<^bsub>G\<^esub>f l \<triangleright> f (Suc l)\<rbrakk> \<Longrightarrow> Group (\<natural>\<^bsub>G\<^esub>f l / f (Suc l))
[PROOF STEP]
apply (cut_tac c = l in subsetD[of "{i. i \<le> n}" "{i. i \<le> (Suc n)}"],
        rule subsetI, simp, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>Group G; l \<le> n; \<forall>l\<le>Suc n. G \<guillemotright> f l  \<and> (\<forall>l\<le>n. f (Suc l) \<subseteq> f l); \<forall>l\<le>n. \<natural>\<^bsub>G\<^esub>f l \<triangleright> f (Suc l); l \<in> {i. i \<le> Suc n}\<rbrakk> \<Longrightarrow> Group (\<natural>\<^bsub>G\<^esub>f l / f (Suc l))
[PROOF STEP]
apply (frule_tac H = "f l" in Group.Group_Gp[of "G"],
        frule_tac a = l in forall_spec, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>Group G; l \<le> n; \<forall>l\<le>Suc n. G \<guillemotright> f l  \<and> (\<forall>l\<le>n. f (Suc l) \<subseteq> f l); \<forall>l\<le>n. \<natural>\<^bsub>G\<^esub>f l \<triangleright> f (Suc l); Group (\<natural>\<^bsub>G\<^esub>f l)\<rbrakk> \<Longrightarrow> Group (\<natural>\<^bsub>G\<^esub>f l / f (Suc l))
[PROOF STEP]
apply (frule_tac G = "Gp G (f l)" and N = "f (Suc l)" in Group.Group_Qg)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l. \<lbrakk>Group G; l \<le> n; \<forall>l\<le>Suc n. G \<guillemotright> f l  \<and> (\<forall>l\<le>n. f (Suc l) \<subseteq> f l); \<forall>l\<le>n. \<natural>\<^bsub>G\<^esub>f l \<triangleright> f (Suc l); Group (\<natural>\<^bsub>G\<^esub>f l)\<rbrakk> \<Longrightarrow> \<natural>\<^bsub>G\<^esub>f l \<triangleright> f (Suc l)
 2. \<And>l. \<lbrakk>Group G; l \<le> n; \<forall>l\<le>Suc n. G \<guillemotright> f l  \<and> (\<forall>l\<le>n. f (Suc l) \<subseteq> f l); \<forall>l\<le>n. \<natural>\<^bsub>G\<^esub>f l \<triangleright> f (Suc l); Group (\<natural>\<^bsub>G\<^esub>f l); Group (\<natural>\<^bsub>G\<^esub>f l / f (Suc l))\<rbrakk> \<Longrightarrow> Group (\<natural>\<^bsub>G\<^esub>f l / f (Suc l))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>Group G; l \<le> n; \<forall>l\<le>Suc n. G \<guillemotright> f l  \<and> (\<forall>l\<le>n. f (Suc l) \<subseteq> f l); \<forall>l\<le>n. \<natural>\<^bsub>G\<^esub>f l \<triangleright> f (Suc l); Group (\<natural>\<^bsub>G\<^esub>f l); Group (\<natural>\<^bsub>G\<^esub>f l / f (Suc l))\<rbrakk> \<Longrightarrow> Group (\<natural>\<^bsub>G\<^esub>f l / f (Suc l))
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma WTrt_binop_widen_mono:
  "\<lbrakk> P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 : T; P \<turnstile> T1' \<le> T1; P \<turnstile> T2' \<le> T2 \<rbrakk> \<Longrightarrow> \<exists>T'. P \<turnstile> T1'\<guillemotleft>bop\<guillemotright>T2' : T' \<and> P \<turnstile> T' \<le> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> T1\<guillemotleft>bop\<guillemotright>T2 : T; P \<turnstile> T1' \<le> T1; P \<turnstile> T2' \<le> T2\<rbrakk> \<Longrightarrow> \<exists>T'. P \<turnstile> T1'\<guillemotleft>bop\<guillemotright>T2' : T' \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
by(cases bop)(auto elim!: WTrt_binop_cases)


[STATEMENT]
lemma symvars_of_adapt_bexp :
  "Bexp.vars (adapt_bexp e s) \<subseteq> symvars s" (is "Bexp.vars ?e' \<subseteq> ?SV")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bexp.vars (adapt_bexp e s) \<subseteq> symvars s
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Bexp.vars (adapt_bexp e s) \<Longrightarrow> x \<in> symvars s
[PROOF STEP]
fix sv
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Bexp.vars (adapt_bexp e s) \<Longrightarrow> x \<in> symvars s
[PROOF STEP]
assume "sv \<in> Bexp.vars ?e'"
[PROOF STATE]
proof (state)
this:
sv \<in> Bexp.vars (adapt_bexp e s)

goal (1 subgoal):
 1. \<And>x. x \<in> Bexp.vars (adapt_bexp e s) \<Longrightarrow> x \<in> symvars s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sv \<in> Bexp.vars (adapt_bexp e s)
[PROOF STEP]
obtain \<sigma>\<^sub>s\<^sub>y\<^sub>m val
  where "?e' (\<sigma>\<^sub>s\<^sub>y\<^sub>m (sv := val)) \<noteq> ?e' \<sigma>\<^sub>s\<^sub>y\<^sub>m"
[PROOF STATE]
proof (prove)
using this:
sv \<in> Bexp.vars (adapt_bexp e s)

goal (1 subgoal):
 1. (\<And>\<sigma>\<^sub>s\<^sub>y\<^sub>m val. adapt_bexp e s (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) \<noteq> adapt_bexp e s \<sigma>\<^sub>s\<^sub>y\<^sub>m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp add : Bexp.vars_def, blast)
[PROOF STATE]
proof (state)
this:
adapt_bexp e s (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) \<noteq> adapt_bexp e s \<sigma>\<^sub>s\<^sub>y\<^sub>m

goal (1 subgoal):
 1. \<And>x. x \<in> Bexp.vars (adapt_bexp e s) \<Longrightarrow> x \<in> symvars s
[PROOF STEP]
hence "(\<lambda> x. (\<sigma>\<^sub>s\<^sub>y\<^sub>m (sv := val)) (symvar x s)) \<noteq> (\<lambda> x. \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar x s))"
[PROOF STATE]
proof (prove)
using this:
adapt_bexp e s (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) \<noteq> adapt_bexp e s \<sigma>\<^sub>s\<^sub>y\<^sub>m

goal (1 subgoal):
 1. (\<lambda>x. (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) (symvar x s)) \<noteq> (\<lambda>x. \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar x s))
[PROOF STEP]
by (auto simp add : adapt_bexp_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) (symvar x s)) \<noteq> (\<lambda>x. \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar x s))

goal (1 subgoal):
 1. \<And>x. x \<in> Bexp.vars (adapt_bexp e s) \<Longrightarrow> x \<in> symvars s
[PROOF STEP]
hence "\<exists> v. (\<sigma>\<^sub>s\<^sub>y\<^sub>m (sv := val)) (symvar v s) \<noteq> \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar v s)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) (symvar x s)) \<noteq> (\<lambda>x. \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar x s))

goal (1 subgoal):
 1. \<exists>v. (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) (symvar v s) \<noteq> \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar v s)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>v. (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) (symvar v s) \<noteq> \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar v s)

goal (1 subgoal):
 1. \<And>x. x \<in> Bexp.vars (adapt_bexp e s) \<Longrightarrow> x \<in> symvars s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>v. (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) (symvar v s) \<noteq> \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar v s)
[PROOF STEP]
obtain v
  where "(\<sigma>\<^sub>s\<^sub>y\<^sub>m (sv := val)) (symvar v s) \<noteq> \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar v s)"
[PROOF STATE]
proof (prove)
using this:
\<exists>v. (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) (symvar v s) \<noteq> \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar v s)

goal (1 subgoal):
 1. (\<And>v. (\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) (symvar v s) \<noteq> \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar v s) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) (symvar v s) \<noteq> \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar v s)

goal (1 subgoal):
 1. \<And>x. x \<in> Bexp.vars (adapt_bexp e s) \<Longrightarrow> x \<in> symvars s
[PROOF STEP]
hence "sv = symvar v s"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>\<^sub>s\<^sub>y\<^sub>m(sv := val)) (symvar v s) \<noteq> \<sigma>\<^sub>s\<^sub>y\<^sub>m (symvar v s)

goal (1 subgoal):
 1. sv = symvar v s
[PROOF STEP]
by (case_tac "sv = symvar v s", simp_all)
[PROOF STATE]
proof (state)
this:
sv = symvar v s

goal (1 subgoal):
 1. \<And>x. x \<in> Bexp.vars (adapt_bexp e s) \<Longrightarrow> x \<in> symvars s
[PROOF STEP]
thus "sv \<in> symvars s"
[PROOF STATE]
proof (prove)
using this:
sv = symvar v s

goal (1 subgoal):
 1. sv \<in> symvars s
[PROOF STEP]
by (simp add : symvars_def)
[PROOF STATE]
proof (state)
this:
sv \<in> symvars s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chop_transfer [transfer_rule]:
  "((=) ===> list_all2 R ===> list_all2 (list_all2 R)) chop chop"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> list_all2 R ===> list_all2 (list_all2 R)) chop chop
[PROOF STEP]
proof (intro rel_funI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>x = y; list_all2 R xa ya\<rbrakk> \<Longrightarrow> list_all2 (list_all2 R) (chop x xa) (chop y ya)
[PROOF STEP]
fix m n ::nat and xs :: "'a list" and ys :: "'b list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>x = y; list_all2 R xa ya\<rbrakk> \<Longrightarrow> list_all2 (list_all2 R) (chop x xa) (chop y ya)
[PROOF STEP]
assume "m = n" "list_all2 R xs ys"
[PROOF STATE]
proof (state)
this:
m = n
list_all2 R xs ys

goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>x = y; list_all2 R xa ya\<rbrakk> \<Longrightarrow> list_all2 (list_all2 R) (chop x xa) (chop y ya)
[PROOF STEP]
from this(2)
[PROOF STATE]
proof (chain)
picking this:
list_all2 R xs ys
[PROOF STEP]
have "list_all2 (list_all2 R) (chop n xs) (chop n ys)"
[PROOF STATE]
proof (prove)
using this:
list_all2 R xs ys

goal (1 subgoal):
 1. list_all2 (list_all2 R) (chop n xs) (chop n ys)
[PROOF STEP]
proof (induction n xs arbitrary: ys rule: chop.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n ys. list_all2 R [] ys \<Longrightarrow> list_all2 (list_all2 R) (chop n []) (chop n ys)
 2. \<And>xs ys. list_all2 R xs ys \<Longrightarrow> list_all2 (list_all2 R) (chop 0 xs) (chop 0 ys)
 3. \<And>n xs ys. \<lbrakk>0 < n; xs \<noteq> []; \<And>ys. list_all2 R (drop n xs) ys \<Longrightarrow> list_all2 (list_all2 R) (chop n (drop n xs)) (chop n ys); list_all2 R xs ys\<rbrakk> \<Longrightarrow> list_all2 (list_all2 R) (chop n xs) (chop n ys)
[PROOF STEP]
case (3 n xs ys)
[PROOF STATE]
proof (state)
this:
0 < n
xs \<noteq> []
list_all2 R (drop n xs) ?ys \<Longrightarrow> list_all2 (list_all2 R) (chop n (drop n xs)) (chop n ?ys)
list_all2 R xs ys

goal (3 subgoals):
 1. \<And>n ys. list_all2 R [] ys \<Longrightarrow> list_all2 (list_all2 R) (chop n []) (chop n ys)
 2. \<And>xs ys. list_all2 R xs ys \<Longrightarrow> list_all2 (list_all2 R) (chop 0 xs) (chop 0 ys)
 3. \<And>n xs ys. \<lbrakk>0 < n; xs \<noteq> []; \<And>ys. list_all2 R (drop n xs) ys \<Longrightarrow> list_all2 (list_all2 R) (chop n (drop n xs)) (chop n ys); list_all2 R xs ys\<rbrakk> \<Longrightarrow> list_all2 (list_all2 R) (chop n xs) (chop n ys)
[PROOF STEP]
hence "ys \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
0 < n
xs \<noteq> []
list_all2 R (drop n xs) ?ys \<Longrightarrow> list_all2 (list_all2 R) (chop n (drop n xs)) (chop n ?ys)
list_all2 R xs ys

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

goal (3 subgoals):
 1. \<And>n ys. list_all2 R [] ys \<Longrightarrow> list_all2 (list_all2 R) (chop n []) (chop n ys)
 2. \<And>xs ys. list_all2 R xs ys \<Longrightarrow> list_all2 (list_all2 R) (chop 0 xs) (chop 0 ys)
 3. \<And>n xs ys. \<lbrakk>0 < n; xs \<noteq> []; \<And>ys. list_all2 R (drop n xs) ys \<Longrightarrow> list_all2 (list_all2 R) (chop n (drop n xs)) (chop n ys); list_all2 R xs ys\<rbrakk> \<Longrightarrow> list_all2 (list_all2 R) (chop n xs) (chop n ys)
[PROOF STEP]
with 3
[PROOF STATE]
proof (chain)
picking this:
0 < n
xs \<noteq> []
list_all2 R (drop n xs) ?ys \<Longrightarrow> list_all2 (list_all2 R) (chop n (drop n xs)) (chop n ?ys)
list_all2 R xs ys
ys \<noteq> []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 < n
xs \<noteq> []
list_all2 R (drop n xs) ?ys \<Longrightarrow> list_all2 (list_all2 R) (chop n (drop n xs)) (chop n ?ys)
list_all2 R xs ys
ys \<noteq> []

goal (1 subgoal):
 1. list_all2 (list_all2 R) (chop n xs) (chop n ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
list_all2 (list_all2 R) (chop n xs) (chop n ys)

goal (2 subgoals):
 1. \<And>n ys. list_all2 R [] ys \<Longrightarrow> list_all2 (list_all2 R) (chop n []) (chop n ys)
 2. \<And>xs ys. list_all2 R xs ys \<Longrightarrow> list_all2 (list_all2 R) (chop 0 xs) (chop 0 ys)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
list_all2 (list_all2 R) (chop n xs) (chop n ys)

goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>x = y; list_all2 R xa ya\<rbrakk> \<Longrightarrow> list_all2 (list_all2 R) (chop x xa) (chop y ya)
[PROOF STEP]
with \<open>m = n\<close>
[PROOF STATE]
proof (chain)
picking this:
m = n
list_all2 (list_all2 R) (chop n xs) (chop n ys)
[PROOF STEP]
show "list_all2 (list_all2 R) (chop m xs) (chop n ys)"
[PROOF STATE]
proof (prove)
using this:
m = n
list_all2 (list_all2 R) (chop n xs) (chop n ys)

goal (1 subgoal):
 1. list_all2 (list_all2 R) (chop m xs) (chop n ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
list_all2 (list_all2 R) (chop m xs) (chop n ys)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma blocksOf_nonInitBlks:
  "(\<forall>p bk. bk \<in> blocksOf s p \<longrightarrow> P bk)
       \<Longrightarrow> bk \<in> nonInitBlks s p \<longrightarrow> P bk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p bk. bk \<in> blocksOf s p \<longrightarrow> P bk \<Longrightarrow> bk \<in> nonInitBlks s p \<longrightarrow> P bk
[PROOF STEP]
by(auto simp add: allRdBlks_def blocksOf_def nonInitBlks_def
                    blocksSeen_def allBlocksRead_def rdBy_def,
    blast)


[STATEMENT]
theorem HInit_Inv2b: "HInit s \<longrightarrow> Inv2b s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HInit s \<longrightarrow> Inv2b s
[PROOF STEP]
by (auto simp add: HInit_def Init_def Inv2b_def
                   Inv2b_inner_def InitDB_def)


[STATEMENT]
lemma take_n:
  fixes n :: nat and l :: "'a list" and g :: "'a list"
  assumes "take n l = take n g" and "Suc n \<le> length g" and "length l = length g"
  shows "take (Suc n) (l[n := g!n]) = take (Suc n) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take (Suc n) (l[n := g ! n]) = take (Suc n) g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. take (Suc n) (l[n := g ! n]) = take (Suc n) g
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
Suc n \<le> length g
[PROOF STEP]
have ng: "n < length g"
[PROOF STATE]
proof (prove)
using this:
Suc n \<le> length g

goal (1 subgoal):
 1. n < length g
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n < length g

goal (1 subgoal):
 1. take (Suc n) (l[n := g ! n]) = take (Suc n) g
[PROOF STEP]
with assms(3)
[PROOF STATE]
proof (chain)
picking this:
length l = length g
n < length g
[PROOF STEP]
have nlupd: "n < length (l[n := g!n])"
[PROOF STATE]
proof (prove)
using this:
length l = length g
n < length g

goal (1 subgoal):
 1. n < length (l[n := g ! n])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n < length (l[n := g ! n])

goal (1 subgoal):
 1. take (Suc n) (l[n := g ! n]) = take (Suc n) g
[PROOF STEP]
hence nl: "n < length l"
[PROOF STATE]
proof (prove)
using this:
n < length (l[n := g ! n])

goal (1 subgoal):
 1. n < length l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n < length l

goal (1 subgoal):
 1. take (Suc n) (l[n := g ! n]) = take (Suc n) g
[PROOF STEP]
from
    sym[OF assms(1)] id_take_nth_drop[OF ng] take_Suc_conv_app_nth[OF nlupd]
    nth_list_update_eq[OF nl] take_Suc_conv_app_nth[OF ng]
    upd_conv_take_nth_drop[OF nl] assms(2-3)
[PROOF STATE]
proof (chain)
picking this:
take n g = take n l
g = take n g @ g ! n # drop (Suc n) g
take (Suc n) (l[n := g ! n]) = take n (l[n := g ! n]) @ [l[n := g ! n] ! n]
l[n := ?x] ! n = ?x
take (Suc n) g = take n g @ [g ! n]
l[n := ?a] = take n l @ ?a # drop (Suc n) l
Suc n \<le> length g
length l = length g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
take n g = take n l
g = take n g @ g ! n # drop (Suc n) g
take (Suc n) (l[n := g ! n]) = take n (l[n := g ! n]) @ [l[n := g ! n] ! n]
l[n := ?x] ! n = ?x
take (Suc n) g = take n g @ [g ! n]
l[n := ?a] = take n l @ ?a # drop (Suc n) l
Suc n \<le> length g
length l = length g

goal (1 subgoal):
 1. take (Suc n) (l[n := g ! n]) = take (Suc n) g
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
take (Suc n) (l[n := g ! n]) = take (Suc n) g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma actions_min_mdpc_Inr: "actions min_mdpc (Inr b) = {return_pmf (Inr b)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. actions local.min_mdpc (Inr b) = {return_pmf (Inr b)}
[PROOF STEP]
by (simp add: min_mdpc_def map_min_state_R)


[STATEMENT]
lemma sqUn_lem3: "\<lbrakk> A \<sqsubseteq> A'; B \<sqsubseteq> B' \<rbrakk> \<Longrightarrow> A \<squnion> B \<sqsubseteq> A' \<squnion> B'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<sqsubseteq> A'; B \<sqsubseteq> B'\<rbrakk> \<Longrightarrow> A \<squnion> B \<sqsubseteq> A' \<squnion> B'
[PROOF STEP]
by(auto simp add: hyperset_defs)


[STATEMENT]
lemma a0i_anyP_observable [iff]: "observable (obs a0i) P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. observable (obs a0i) P
[PROOF STEP]
by (auto)


[STATEMENT]
lemma enat_coexhaust:
  obtains (0) "n = 0"
     | (eSuc) n' where "n = eSuc n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = 0 \<Longrightarrow> thesis; \<And>n'. n = eSuc n' \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>n = 0 \<Longrightarrow> thesis; \<And>n'. n = eSuc n' \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "n \<in> enat_set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> enat_set
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<in> enat_set

goal (1 subgoal):
 1. \<lbrakk>n = 0 \<Longrightarrow> thesis; \<And>n'. n = eSuc n' \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus thesis
[PROOF STATE]
proof (prove)
using this:
n \<in> enat_set

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by cases (erule that)+
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma foldli_card: "det_fold_set X (\<lambda>_. True) (\<lambda>_ n. Suc n) 0 card"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det_fold_set X (\<lambda>_. True) (\<lambda>_. Suc) 0 card
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>distinct l; sorted_wrt X l\<rbrakk> \<Longrightarrow> foldli l (\<lambda>_. True) (\<lambda>_. Suc) 0 = card (set l)
[PROOF STEP]
using foldli_card_aux[where n=0]
[PROOF STATE]
proof (prove)
using this:
distinct ?l \<Longrightarrow> foldli ?l (\<lambda>_. True) (\<lambda>_. Suc) 0 = 0 + card (set ?l)

goal (1 subgoal):
 1. \<And>l. \<lbrakk>distinct l; sorted_wrt X l\<rbrakk> \<Longrightarrow> foldli l (\<lambda>_. True) (\<lambda>_. Suc) 0 = card (set l)
[PROOF STEP]
by simp


[STATEMENT]
lemma init_fin_silent_movesD:
  assumes "\<tau>trsys.silent_moves (init_fin t) init_fin_\<tau>move ((s, x), m) ((s', x'), m')"
  shows "silent_moves t (x, m) (x', m') \<and> s = s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. silent_moves t (x, m) (x', m') \<and> s = s'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<tau>trsys.silent_move (init_fin t) init_fin_\<tau>move)\<^sup>*\<^sup>* ((s, x), m) ((s', x'), m')

goal (1 subgoal):
 1. silent_moves t (x, m) (x', m') \<and> s = s'
[PROOF STEP]
by(induct "((s, x), m)" "((s', x'), m')" arbitrary: s' x' m')
  (auto 7 2 simp only: dest!: init_fin_silent_moveD intro: rtranclp.rtrancl_into_rtrancl)


[STATEMENT]
lemma unitary_gen_inv:
  assumes "unitary_gen M"
  shows "unitary_gen (mat_inv M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary_gen (mat_inv M)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. unitary_gen (mat_inv M)
[PROOF STEP]
obtain k M' where "0 < k" "unitary M'" "M = cor k *\<^sub>s\<^sub>m eye *\<^sub>m\<^sub>m M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k M'. \<lbrakk>0 < k; unitary M'; M = cor k *\<^sub>s\<^sub>m eye *\<^sub>m\<^sub>m M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using unitary_gen_unitary[of M] assms
[PROOF STATE]
proof (prove)
using this:
unitary_gen M = (\<exists>k M'. 0 < k \<and> unitary M' \<and> M = cor k *\<^sub>s\<^sub>m eye *\<^sub>m\<^sub>m M')
unitary_gen M

goal (1 subgoal):
 1. (\<And>k M'. \<lbrakk>0 < k; unitary M'; M = cor k *\<^sub>s\<^sub>m eye *\<^sub>m\<^sub>m M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < k
unitary M'
M = cor k *\<^sub>s\<^sub>m eye *\<^sub>m\<^sub>m M'

goal (1 subgoal):
 1. unitary_gen (mat_inv M)
[PROOF STEP]
hence "mat_inv M = cor (1/k) *\<^sub>s\<^sub>m mat_inv M'"
[PROOF STATE]
proof (prove)
using this:
0 < k
unitary M'
M = cor k *\<^sub>s\<^sub>m eye *\<^sub>m\<^sub>m M'

goal (1 subgoal):
 1. mat_inv M = cor (1 / k) *\<^sub>s\<^sub>m mat_inv M'
[PROOF STEP]
by (metis mat_inv_mult_sm mult_sm_eye_mm norm_not_less_zero of_real_1 of_real_divide of_real_eq_0_iff sgn_1_neg sgn_greater sgn_if sgn_pos sgn_sgn)
[PROOF STATE]
proof (state)
this:
mat_inv M = cor (1 / k) *\<^sub>s\<^sub>m mat_inv M'

goal (1 subgoal):
 1. unitary_gen (mat_inv M)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
mat_inv M = cor (1 / k) *\<^sub>s\<^sub>m mat_inv M'

goal (1 subgoal):
 1. unitary_gen (mat_inv M)
[PROOF STEP]
using \<open>k > 0\<close> \<open>unitary M'\<close>
[PROOF STATE]
proof (prove)
using this:
mat_inv M = cor (1 / k) *\<^sub>s\<^sub>m mat_inv M'
0 < k
unitary M'

goal (1 subgoal):
 1. unitary_gen (mat_inv M)
[PROOF STEP]
by (subst unitary_gen_unitary[of "mat_inv M"]) (rule_tac x="1/k" in exI, rule_tac x="mat_inv M'" in exI, metis divide_pos_pos mult_sm_eye_mm unitary_inv zero_less_one)
[PROOF STATE]
proof (state)
this:
unitary_gen (mat_inv M)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iprop11a': "Fr_1 \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<Rightarrow> (a \<^bold>\<Rightarrow> b)) \<^bold>\<preceq> (a \<^bold>\<Rightarrow> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fr_1 \<F> \<Longrightarrow> \<forall>a b. contains (b \<^bold>\<Leftarrow> a) ((b \<^bold>\<Leftarrow> a) \<^bold>\<Leftarrow> a)
[PROOF STEP]
by (smt MONO_def PF1 imp_rel monI conn)


[STATEMENT]
lemma pos_oriented_opposite_ocircline_cmat [simp]:
  assumes "hermitean H \<and> H \<noteq> mat_zero"
  shows  "pos_oriented_cmat (opposite_ocircline_cmat H) \<longleftrightarrow> \<not> pos_oriented_cmat H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)
[PROOF STEP]
obtain A B C D where HH: "H = (A, B, C, D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A B C D. H = (A, B, C, D) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases H) auto
[PROOF STATE]
proof (state)
this:
H = (A, B, C, D)

goal (1 subgoal):
 1. pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
H = (A, B, C, D)

goal (1 subgoal):
 1. pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)
[PROOF STEP]
hence "Re A = 0 \<and> Re D = 0 \<longrightarrow> B \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
H = (A, B, C, D)

goal (1 subgoal):
 1. is_imag A \<and> is_imag D \<longrightarrow> B \<noteq> 0
[PROOF STEP]
using assms hermitean_elems[of A B C D]
[PROOF STATE]
proof (prove)
using this:
H = (A, B, C, D)
hermitean H \<and> H \<noteq> mat_zero
hermitean (A, B, C, D) \<Longrightarrow> is_real A
hermitean (A, B, C, D) \<Longrightarrow> is_real D
hermitean (A, B, C, D) \<Longrightarrow> B = cnj C
hermitean (A, B, C, D) \<Longrightarrow> cnj B = C

goal (1 subgoal):
 1. is_imag A \<and> is_imag D \<longrightarrow> B \<noteq> 0
[PROOF STEP]
by (cases A, cases D) (auto simp add: Complex_eq)
[PROOF STATE]
proof (state)
this:
is_imag A \<and> is_imag D \<longrightarrow> B \<noteq> 0

goal (1 subgoal):
 1. pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_imag A \<and> is_imag D \<longrightarrow> B \<noteq> 0

goal (1 subgoal):
 1. pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)
[PROOF STEP]
have "B \<noteq> 0 \<and> \<not> 0 < Arg B \<longrightarrow> 0 < Arg (- B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<noteq> 0 \<and> \<not> 0 < Arg B \<longrightarrow> 0 < Arg (- B)
[PROOF STEP]
using canon_ang_plus_pi2[of "Arg B"] Arg_bounded[of B]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>- 2 * pi < Arg B; Arg B \<le> 0\<rbrakk> \<Longrightarrow> \<downharpoonright>Arg B + pi\<downharpoonleft> = Arg B + pi
- pi < Arg B \<and> Arg B \<le> pi

goal (1 subgoal):
 1. B \<noteq> 0 \<and> \<not> 0 < Arg B \<longrightarrow> 0 < Arg (- B)
[PROOF STEP]
by (auto simp add: arg_uminus)
[PROOF STATE]
proof (state)
this:
B \<noteq> 0 \<and> \<not> 0 < Arg B \<longrightarrow> 0 < Arg (- B)

goal (1 subgoal):
 1. pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
B \<noteq> 0 \<and> \<not> 0 < Arg B \<longrightarrow> 0 < Arg (- B)

goal (1 subgoal):
 1. pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)
[PROOF STEP]
have "B \<noteq> 0 \<and> 0 < Arg B \<longrightarrow> \<not> 0 < Arg (- B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<noteq> 0 \<and> 0 < Arg B \<longrightarrow> \<not> 0 < Arg (- B)
[PROOF STEP]
using canon_ang_plus_pi1[of "Arg B"] Arg_bounded[of B]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < Arg B; Arg B \<le> 2 * pi\<rbrakk> \<Longrightarrow> \<downharpoonright>Arg B + pi\<downharpoonleft> = Arg B - pi
- pi < Arg B \<and> Arg B \<le> pi

goal (1 subgoal):
 1. B \<noteq> 0 \<and> 0 < Arg B \<longrightarrow> \<not> 0 < Arg (- B)
[PROOF STEP]
by (auto simp add: arg_uminus)
[PROOF STATE]
proof (state)
this:
B \<noteq> 0 \<and> 0 < Arg B \<longrightarrow> \<not> 0 < Arg (- B)

goal (1 subgoal):
 1. pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
H = (A, B, C, D)
is_imag A \<and> is_imag D \<longrightarrow> B \<noteq> 0
B \<noteq> 0 \<and> \<not> 0 < Arg B \<longrightarrow> 0 < Arg (- B)
B \<noteq> 0 \<and> 0 < Arg B \<longrightarrow> \<not> 0 < Arg (- B)
[PROOF STEP]
show "pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)"
[PROOF STATE]
proof (prove)
using this:
H = (A, B, C, D)
is_imag A \<and> is_imag D \<longrightarrow> B \<noteq> 0
B \<noteq> 0 \<and> \<not> 0 < Arg B \<longrightarrow> 0 < Arg (- B)
B \<noteq> 0 \<and> 0 < Arg B \<longrightarrow> \<not> 0 < Arg (- B)

goal (1 subgoal):
 1. pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)
[PROOF STEP]
by simp (metis not_less_iff_gr_or_eq)
[PROOF STATE]
proof (state)
this:
pos_oriented_cmat (opposite_ocircline_cmat H) = (\<not> pos_oriented_cmat H)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_ocircline_ounit_circle_conjugate [simp]:
  assumes "in_ocircline ounit_circle z"
  shows "in_ocircline ounit_circle (conjugate z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_ocircline ounit_circle (conjugate z)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
in_ocircline ounit_circle z

goal (1 subgoal):
 1. in_ocircline ounit_circle (conjugate z)
[PROOF STEP]
by (transfer, transfer, auto simp add: vec_cnj_def)


[STATEMENT]
lemma pr_ext_agrk_user_1 [rule_format]:
 "(evs, S, A, U) \<in> protocol \<Longrightarrow>
    User m \<noteq> Spy \<longrightarrow>
    Says n run 4 (User m) (Card n) (Crypt (sesK K) (pubAK e)) \<in> set evs \<longrightarrow>
  ExtAgrK (S (User m, n, run)) \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (evs, S, A, U) \<in> protocol \<Longrightarrow> User m \<noteq> Spy \<longrightarrow> Says n run 4 (User m) (Card n) (Crypt (sesK K) (pubAK e)) \<in> set evs \<longrightarrow> ExtAgrK (S (User m, n, run)) \<noteq> None
[PROOF STEP]
by (erule protocol.induct, simp_all, (rule_tac [!] impI)+, simp_all)


[STATEMENT]
theorem ccard_diff_lgth:
    shows "n'\<ge>n \<Longrightarrow> bc n' - bc n \<ge> ccard n n' (\<lambda>n. mining n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> n' \<Longrightarrow> card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n
[PROOF STEP]
proof (induction n' rule: dec_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. card {i. n < i \<and> i \<le> n \<and> mining i} \<le> bc n - bc n
 2. \<And>na. \<lbrakk>n \<le> na; na < n'; card {i. n < i \<and> i \<le> na \<and> mining i} \<le> bc na - bc n\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc na \<and> mining i} \<le> bc (Suc na) - bc n
[PROOF STEP]
case base
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. card {i. n < i \<and> i \<le> n \<and> mining i} \<le> bc n - bc n
 2. \<And>na. \<lbrakk>n \<le> na; na < n'; card {i. n < i \<and> i \<le> na \<and> mining i} \<le> bc na - bc n\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc na \<and> mining i} \<le> bc (Suc na) - bc n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> n \<and> mining i} \<le> bc n - bc n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> n \<and> mining i} \<le> bc n - bc n

goal (1 subgoal):
 1. \<And>na. \<lbrakk>n \<le> na; na < n'; card {i. n < i \<and> i \<le> na \<and> mining i} \<le> bc na - bc n\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc na \<and> mining i} \<le> bc (Suc na) - bc n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>n \<le> na; na < n'; card {i. n < i \<and> i \<le> na \<and> mining i} \<le> bc na - bc n\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc na \<and> mining i} \<le> bc (Suc na) - bc n
[PROOF STEP]
case (step n')
[PROOF STATE]
proof (state)
this:
n \<le> n'
n' < n'
card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n

goal (1 subgoal):
 1. \<And>na. \<lbrakk>n \<le> na; na < n'; card {i. n < i \<and> i \<le> na \<and> mining i} \<le> bc na - bc n\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc na \<and> mining i} \<le> bc (Suc na) - bc n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<le> n'
n' < n'
card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n \<le> n'
n' < n'
card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
 2. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
assume "mining (Suc n')"
[PROOF STATE]
proof (state)
this:
mining (Suc n')

goal (2 subgoals):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
 2. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
with as2
[PROOF STATE]
proof (chain)
picking this:
mining (Suc ?n) \<Longrightarrow> bc ?n < bc (Suc ?n)
mining (Suc n')
[PROOF STEP]
have "bc (Suc n') > bc n'"
[PROOF STATE]
proof (prove)
using this:
mining (Suc ?n) \<Longrightarrow> bc ?n < bc (Suc ?n)
mining (Suc n')

goal (1 subgoal):
 1. bc n' < bc (Suc n')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bc n' < bc (Suc n')

goal (2 subgoals):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
 2. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bc n' < bc (Suc n')

goal (2 subgoals):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
 2. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
from step.hyps
[PROOF STATE]
proof (chain)
picking this:
n \<le> n'
n' < n'
[PROOF STEP]
have "bc n'\<ge>bc n"
[PROOF STATE]
proof (prove)
using this:
n \<le> n'
n' < n'

goal (1 subgoal):
 1. bc n \<le> bc n'
[PROOF STEP]
using grow_mono
[PROOF STATE]
proof (prove)
using this:
n \<le> n'
n' < n'
?n \<le> ?n' \<Longrightarrow> bc ?n \<le> bc ?n'

goal (1 subgoal):
 1. bc n \<le> bc n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bc n \<le> bc n'

goal (2 subgoals):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
 2. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bc n' < bc (Suc n')
bc n \<le> bc n'
[PROOF STEP]
have "bc (Suc n') - bc n > bc n' - bc n"
[PROOF STATE]
proof (prove)
using this:
bc n' < bc (Suc n')
bc n \<le> bc n'

goal (1 subgoal):
 1. bc n' - bc n < bc (Suc n') - bc n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bc n' - bc n < bc (Suc n') - bc n

goal (2 subgoals):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
 2. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bc n' - bc n < bc (Suc n') - bc n

goal (2 subgoals):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
 2. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
from as1
[PROOF STATE]
proof (chain)
picking this:
bc ?n \<le> bc (Suc ?n)
[PROOF STEP]
have "bc (Suc n') - bc n \<ge> bc n' - bc n"
[PROOF STATE]
proof (prove)
using this:
bc ?n \<le> bc (Suc ?n)

goal (1 subgoal):
 1. bc n' - bc n \<le> bc (Suc n') - bc n
[PROOF STEP]
by (simp add: diff_le_mono)
[PROOF STATE]
proof (state)
this:
bc n' - bc n \<le> bc (Suc n') - bc n

goal (2 subgoals):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
 2. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bc n' - bc n \<le> bc (Suc n') - bc n

goal (2 subgoals):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
 2. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
from \<open>mining (Suc n')\<close> step.hyps
[PROOF STATE]
proof (chain)
picking this:
mining (Suc n')
n \<le> n'
n' < n'
[PROOF STEP]
have "ccard n (Suc n') (\<lambda>n. mining n) \<le> Suc (ccard n n' (\<lambda>n. mining n))"
[PROOF STATE]
proof (prove)
using this:
mining (Suc n')
n \<le> n'
n' < n'

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> Suc (card {i. n < i \<and> i \<le> n' \<and> mining i})
[PROOF STEP]
using ccard_inc
[PROOF STATE]
proof (prove)
using this:
mining (Suc n')
n \<le> n'
n' < n'
\<lbrakk>?p (Suc ?n'); ?n \<le> ?n'\<rbrakk> \<Longrightarrow> card {i. ?n < i \<and> i \<le> Suc ?n' \<and> ?p i} = Suc (card {i. ?n < i \<and> i \<le> ?n' \<and> ?p i})

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> Suc (card {i. n < i \<and> i \<le> n' \<and> mining i})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> Suc (card {i. n < i \<and> i \<le> n' \<and> mining i})

goal (2 subgoals):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
 2. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bc n' - bc n < bc (Suc n') - bc n
bc n' - bc n \<le> bc (Suc n') - bc n
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> Suc (card {i. n < i \<and> i \<le> n' \<and> mining i})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bc n' - bc n < bc (Suc n') - bc n
bc n' - bc n \<le> bc (Suc n') - bc n
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> Suc (card {i. n < i \<and> i \<le> n' \<and> mining i})

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
using step.IH
[PROOF STATE]
proof (prove)
using this:
bc n' - bc n < bc (Suc n') - bc n
bc n' - bc n \<le> bc (Suc n') - bc n
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> Suc (card {i. n < i \<and> i \<le> n' \<and> mining i})
card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n

goal (1 subgoal):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> mining (Suc n')\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> mining (Suc n')\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
assume "\<not> mining (Suc n')"
[PROOF STATE]
proof (state)
this:
\<not> mining (Suc n')

goal (1 subgoal):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> mining (Suc n')\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
hence "ccard n (Suc n') (\<lambda>n. mining n) \<le> (ccard n n' (\<lambda>n. mining n))"
[PROOF STATE]
proof (prove)
using this:
\<not> mining (Suc n')

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> card {i. n < i \<and> i \<le> n' \<and> mining i}
[PROOF STEP]
using ccard_same
[PROOF STATE]
proof (prove)
using this:
\<not> mining (Suc n')
\<not> ?p (Suc ?n') \<Longrightarrow> card {i. ?n < i \<and> i \<le> ?n' \<and> ?p i} = card {i. ?n < i \<and> i \<le> Suc ?n' \<and> ?p i}

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> card {i. n < i \<and> i \<le> n' \<and> mining i}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> card {i. n < i \<and> i \<le> n' \<and> mining i}

goal (1 subgoal):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> mining (Suc n')\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> card {i. n < i \<and> i \<le> n' \<and> mining i}

goal (1 subgoal):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> mining (Suc n')\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
from as1
[PROOF STATE]
proof (chain)
picking this:
bc ?n \<le> bc (Suc ?n)
[PROOF STEP]
have "bc (Suc n') - bc n \<ge> bc n' - bc n"
[PROOF STATE]
proof (prove)
using this:
bc ?n \<le> bc (Suc ?n)

goal (1 subgoal):
 1. bc n' - bc n \<le> bc (Suc n') - bc n
[PROOF STEP]
by (simp add: diff_le_mono)
[PROOF STATE]
proof (state)
this:
bc n' - bc n \<le> bc (Suc n') - bc n

goal (1 subgoal):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> mining (Suc n')\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> card {i. n < i \<and> i \<le> n' \<and> mining i}
bc n' - bc n \<le> bc (Suc n') - bc n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> card {i. n < i \<and> i \<le> n' \<and> mining i}
bc n' - bc n \<le> bc (Suc n') - bc n

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
using step.IH
[PROOF STATE]
proof (prove)
using this:
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> card {i. n < i \<and> i \<le> n' \<and> mining i}
bc n' - bc n \<le> bc (Suc n') - bc n
card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n

goal:
No subgoals!
[PROOF STEP]
qed