[STATEMENT]
lemma gauss_jordan'_complete:
  assumes exists: "\<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * x s') = a s"
  assumes unique: "\<And>y. \<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * y s') = a s \<Longrightarrow> \<forall>s\<in>S. y s = x s"
  shows "\<exists>y. gauss_jordan' M a = Some y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. gauss_jordan' M a = Some y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y. gauss_jordan' M a = Some y
[PROOF STEP]
define M' where "M' = (\<lambda>i j. if j = card S then
    a (order i) else M (order i) (order j))"
[PROOF STATE]
proof (state)
this:
M' = (\<lambda>i j. if j = card S then a (order i) else M (order i) (order j))

goal (1 subgoal):
 1. \<exists>y. gauss_jordan' M a = Some y
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
M' = (\<lambda>i j. if j = card S then a (order i) else M (order i) (order j))

goal (1 subgoal):
 1. \<exists>y. gauss_jordan' M a = Some y
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y. gauss_jordan' M a = Some y
[PROOF STEP]
have iorder_neq_card_S: "\<And>s. s \<in> S \<Longrightarrow> iorder s \<noteq> card S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> iorder s \<noteq> card S
[PROOF STEP]
using iorder_image_eq
[PROOF STATE]
proof (prove)
using this:
iorder ` S = {..<card S}

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> iorder s \<noteq> card S
[PROOF STEP]
by (auto simp: set_eq_iff less_le)
[PROOF STATE]
proof (state)
this:
?s1 \<in> S \<Longrightarrow> iorder ?s1 \<noteq> card S

goal (1 subgoal):
 1. \<exists>y. gauss_jordan' M a = Some y
[PROOF STEP]
have "solution2 M' (card S) (card S) x \<longleftrightarrow>
      (\<forall>s\<in>{..<card S}. (\<Sum>s'\<in>{..<card S}. M' s s' * x s') = M' s (card S))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution2 M' (card S) (card S) x = (\<forall>s\<in>{..<card S}. (\<Sum>s'<card S. M' s s' * x s') = M' s (card S))
[PROOF STEP]
unfolding solution2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i<card S. (\<Sum>j = 0..<card S. M' i j * x j) = M' i (card S)) = (\<forall>s\<in>{..<card S}. (\<Sum>s'<card S. M' s s' * x s') = M' s (card S))
[PROOF STEP]
by (auto simp: atLeast0LessThan)
[PROOF STATE]
proof (state)
this:
solution2 M' (card S) (card S) x = (\<forall>s\<in>{..<card S}. (\<Sum>s'<card S. M' s s' * x s') = M' s (card S))

goal (1 subgoal):
 1. \<exists>y. gauss_jordan' M a = Some y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
solution2 M' (card S) (card S) x = (\<forall>s\<in>{..<card S}. (\<Sum>s'<card S. M' s s' * x s') = M' s (card S))

goal (1 subgoal):
 1. \<exists>y. gauss_jordan' M a = Some y
[PROOF STEP]
have "\<dots> \<longleftrightarrow> (\<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * x (iorder s')) = a s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>s\<in>{..<card S}. (\<Sum>s'<card S. M' s s' * x s') = M' s (card S)) = (\<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * x (iorder s')) = a s)
[PROOF STEP]
unfolding iorder_image_eq[symmetric] M'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>s\<in>iorder ` S. (\<Sum>s'\<in>iorder ` S. (if s' = card S then a (order s) else M (order s) (order s')) * x s') = (if card S = card S then a (order s) else M (order s) (order (card S)))) = (\<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * x (iorder s')) = a s)
[PROOF STEP]
using inj_iorder iorder_neq_card_S
[PROOF STATE]
proof (prove)
using this:
inj_on iorder S
?s1 \<in> S \<Longrightarrow> iorder ?s1 \<noteq> card S

goal (1 subgoal):
 1. (\<forall>s\<in>iorder ` S. (\<Sum>s'\<in>iorder ` S. (if s' = card S then a (order s) else M (order s) (order s')) * x s') = (if card S = card S then a (order s) else M (order s) (order (card S)))) = (\<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * x (iorder s')) = a s)
[PROOF STEP]
by (simp add: sum.reindex order_iorder)
[PROOF STATE]
proof (state)
this:
(\<forall>s\<in>{..<card S}. (\<Sum>s'<card S. M' s s' * x s') = M' s (card S)) = (\<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * x (iorder s')) = a s)

goal (1 subgoal):
 1. \<exists>y. gauss_jordan' M a = Some y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
solution2 M' (card S) (card S) x = (\<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * x (iorder s')) = a s)
[PROOF STEP]
have "solution2 M' (card S) (card S) x \<longleftrightarrow>
      (\<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * x (iorder s')) = a s)"
[PROOF STATE]
proof (prove)
using this:
solution2 M' (card S) (card S) x = (\<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * x (iorder s')) = a s)

goal (1 subgoal):
 1. solution2 M' (card S) (card S) x = (\<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * x (iorder s')) = a s)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
solution2 M' (card S) (card S) x = (\<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * x (iorder s')) = a s)

goal (1 subgoal):
 1. \<exists>y. gauss_jordan' M a = Some y
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
solution2 M' (card S) (card S) ?xa3 = (\<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * ?xa3 (iorder s')) = a s)

goal (1 subgoal):
 1. \<exists>y. gauss_jordan' M a = Some y
[PROOF STEP]
note sol2_eq = this
[PROOF STATE]
proof (state)
this:
solution2 M' (card S) (card S) ?xa3 = (\<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * ?xa3 (iorder s')) = a s)

goal (1 subgoal):
 1. \<exists>y. gauss_jordan' M a = Some y
[PROOF STEP]
have "usolution M' (card S) (card S) (\<lambda>i. x (order i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. usolution M' (card S) (card S) (\<lambda>i. x (order i))
[PROOF STEP]
unfolding usolution_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution2 M' (card S) (card S) (\<lambda>i. x (order i)) \<and> (\<forall>y. solution2 M' (card S) (card S) y \<longrightarrow> (\<forall>j<card S. y j = x (order j)))
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. solution2 M' (card S) (card S) (\<lambda>i. x (order i))
 2. \<And>y j. \<lbrakk>solution2 M' (card S) (card S) y; j < card S\<rbrakk> \<Longrightarrow> y j = x (order j)
[PROOF STEP]
from exists
[PROOF STATE]
proof (chain)
picking this:
\<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * x s') = a s
[PROOF STEP]
show "solution2 M' (card S) (card S) (\<lambda>i. x (order i))"
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * x s') = a s

goal (1 subgoal):
 1. solution2 M' (card S) (card S) (\<lambda>i. x (order i))
[PROOF STEP]
by (simp add: sol2_eq order_iorder)
[PROOF STATE]
proof (state)
this:
solution2 M' (card S) (card S) (\<lambda>i. x (order i))

goal (1 subgoal):
 1. \<And>y j. \<lbrakk>solution2 M' (card S) (card S) y; j < card S\<rbrakk> \<Longrightarrow> y j = x (order j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y j. \<lbrakk>solution2 M' (card S) (card S) y; j < card S\<rbrakk> \<Longrightarrow> y j = x (order j)
[PROOF STEP]
fix y j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y j. \<lbrakk>solution2 M' (card S) (card S) y; j < card S\<rbrakk> \<Longrightarrow> y j = x (order j)
[PROOF STEP]
assume y: "solution2 M' (card S) (card S) y" and "j < card S"
[PROOF STATE]
proof (state)
this:
solution2 M' (card S) (card S) y
j < card S

goal (1 subgoal):
 1. \<And>y j. \<lbrakk>solution2 M' (card S) (card S) y; j < card S\<rbrakk> \<Longrightarrow> y j = x (order j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
solution2 M' (card S) (card S) y
j < card S
[PROOF STEP]
have "\<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * y (iorder s')) = a s"
[PROOF STATE]
proof (prove)
using this:
solution2 M' (card S) (card S) y
j < card S

goal (1 subgoal):
 1. \<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * y (iorder s')) = a s
[PROOF STEP]
by (simp add: sol2_eq)
[PROOF STATE]
proof (state)
this:
\<forall>s\<in>S. (\<Sum>s'\<in>S. M s s' * y (iorder s')) = a s

goal (1 subgoal):
 1. \<And>y j. \<lbrakk>solution2 M' (card S) (card S) y; j < card S\<rbrakk> \<Longrightarrow> y j = x (order j)
[PROOF STEP]
from unique[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<forall>s\<in>S. y (iorder s) = x s
[PROOF STEP]
have "\<forall>i\<in>{..<card S}. y i = x (order i)"
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<in>S. y (iorder s) = x s

goal (1 subgoal):
 1. \<forall>i\<in>{..<card S}. y i = x (order i)
[PROOF STEP]
unfolding iorder_image_eq[symmetric]
[PROOF STATE]
proof (prove)
using this:
\<forall>s\<in>S. y (iorder s) = x s

goal (1 subgoal):
 1. \<forall>i\<in>iorder ` S. y i = x (order i)
[PROOF STEP]
by (simp add: order_iorder)
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>{..<card S}. y i = x (order i)

goal (1 subgoal):
 1. \<And>y j. \<lbrakk>solution2 M' (card S) (card S) y; j < card S\<rbrakk> \<Longrightarrow> y j = x (order j)
[PROOF STEP]
with \<open>j < card S\<close>
[PROOF STATE]
proof (chain)
picking this:
j < card S
\<forall>i\<in>{..<card S}. y i = x (order i)
[PROOF STEP]
show "y j = x (order j)"
[PROOF STATE]
proof (prove)
using this:
j < card S
\<forall>i\<in>{..<card S}. y i = x (order i)

goal (1 subgoal):
 1. y j = x (order j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y j = x (order j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
usolution M' (card S) (card S) (\<lambda>i. x (order i))

goal (1 subgoal):
 1. \<exists>y. gauss_jordan' M a = Some y
[PROOF STEP]
from gauss_jordan_complete[OF _ this]
[PROOF STATE]
proof (chain)
picking this:
card S \<le> card S \<Longrightarrow> \<exists>B. gauss_jordan M' (card S) = Some B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card S \<le> card S \<Longrightarrow> \<exists>B. gauss_jordan M' (card S) = Some B

goal (1 subgoal):
 1. \<exists>y. gauss_jordan' M a = Some y
[PROOF STEP]
by (auto simp: gauss_jordan'_def simp: M'_def)
[PROOF STATE]
proof (state)
this:
\<exists>y. gauss_jordan' M a = Some y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma measurable_bound_until[measurable]:
  assumes [measurable]: "Measurable.pred (stream_space M) \<phi>" "Measurable.pred (stream_space M) \<psi>"
  shows "Measurable.pred (stream_space M) (bound_until n \<phi> \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Measurable.pred (stream_space M) (bound_until n \<phi> \<psi>)
[PROOF STEP]
by (induct n) simp_all


[STATEMENT]
lemma svalid_subset_S: "svalid F \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. svalid F \<subseteq> S
[PROOF STEP]
by (induct F) auto


[STATEMENT]
lemma finite_svalid[simp, intro]: "finite (svalid F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (svalid F)
[PROOF STEP]
using svalid_subset_S finite_S
[PROOF STATE]
proof (prove)
using this:
svalid ?F \<subseteq> S
finite S

goal (1 subgoal):
 1. finite (svalid F)
[PROOF STEP]
by (blast intro: finite_subset)


[STATEMENT]
lemma svalid_sets[measurable]: "svalid F \<in> sets (count_space S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. svalid F \<in> sets (count_space S)
[PROOF STEP]
using svalid_subset_S
[PROOF STATE]
proof (prove)
using this:
svalid ?F \<subseteq> S

goal (1 subgoal):
 1. svalid F \<in> sets (count_space S)
[PROOF STEP]
by auto


[STATEMENT]
lemma reward_measurable[measurable]: "reward F \<in> borel_measurable R.S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reward F \<in> borel_measurable (stream_space (count_space UNIV))
[PROOF STEP]
by (cases F) auto


[STATEMENT]
lemma Prob0_subset_S: "Prob0 \<Phi> \<Psi> \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prob0 \<Phi> \<Psi> \<subseteq> S
[PROOF STEP]
unfolding Prob0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S - while (\<lambda>R. \<exists>s\<in>\<Phi>. R \<inter> E s \<noteq> {} \<and> s \<notin> R) (\<lambda>R. R \<union> {s \<in> \<Phi>. R \<inter> E s \<noteq> {}}) \<Psi> \<subseteq> S
[PROOF STEP]
by auto


[STATEMENT]
lemma Prob0_iff_reachable:
  assumes "\<Phi> \<subseteq> S" "\<Psi> \<subseteq> S"
  shows "Prob0 \<Phi> \<Psi> = {s \<in> S. ((SIGMA x:\<Phi>. E x)\<^sup>* `` {s}) \<inter> \<Psi> = {}}" (is "_ = ?U")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prob0 \<Phi> \<Psi> = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
unfolding Prob0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S - while (\<lambda>R. \<exists>s\<in>\<Phi>. R \<inter> E s \<noteq> {} \<and> s \<notin> R) (\<lambda>R. R \<union> {s \<in> \<Phi>. R \<inter> E s \<noteq> {}}) \<Psi> = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
proof (intro while_rule[where Q="\<lambda>R. S - R = ?U" and P="\<lambda>R. \<Psi> \<subseteq> R \<and> R \<subseteq> S - ?U"] conjI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<Psi> \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 3. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> \<Psi> \<subseteq> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}}
 4. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 5. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 6. wf ?r
 7. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> (s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}}, s) \<in> ?r
[PROOF STEP]
show "wf {(B, A). A \<subset> B \<and> B \<subseteq> S}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(B, A). A \<subset> B \<and> B \<subseteq> S}
[PROOF STEP]
by (rule wf_bounded_set[where ub="\<lambda>_. S" and f="\<lambda>x. x"]) auto
[PROOF STATE]
proof (state)
this:
wf {(B, A). A \<subset> B \<and> B \<subseteq> S}

goal (6 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<Psi> \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 3. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> \<Psi> \<subseteq> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}}
 4. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 5. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 6. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> (s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}}, s) \<in> {(B, A). A \<subset> B \<and> B \<subseteq> S}
[PROOF STEP]
show "\<Psi> \<subseteq> S - ?U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Phi> \<subseteq> S
\<Psi> \<subseteq> S

goal (1 subgoal):
 1. \<Psi> \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Psi> \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}

goal (5 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> \<Psi> \<subseteq> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}}
 3. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 4. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 5. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> (s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}}, s) \<in> {(B, A). A \<subset> B \<and> B \<subseteq> S}
[PROOF STEP]
let ?\<Delta> = "\<lambda>R. {s\<in>\<Phi>. R \<inter> E s \<noteq> {}}"
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> \<Psi> \<subseteq> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}}
 3. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 4. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 5. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> (s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}}, s) \<in> {(B, A). A \<subset> B \<and> B \<subseteq> S}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> \<Psi> \<subseteq> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}}
 3. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 4. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 5. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> (s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}}, s) \<in> {(B, A). A \<subset> B \<and> B \<subseteq> S}
[PROOF STEP]
fix R
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> \<Psi> \<subseteq> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}}
 3. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 4. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 5. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> (s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}}, s) \<in> {(B, A). A \<subset> B \<and> B \<subseteq> S}
[PROOF STEP]
assume R: "\<Psi> \<subseteq> R \<and> R \<subseteq> S - ?U" and "\<exists>s\<in>\<Phi>. R \<inter> E s \<noteq> {} \<and> s \<notin> R"
[PROOF STATE]
proof (state)
this:
\<Psi> \<subseteq> R \<and> R \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
\<exists>s\<in>\<Phi>. R \<inter> E s \<noteq> {} \<and> s \<notin> R

goal (5 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> \<Psi> \<subseteq> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}}
 3. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 4. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 5. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> (s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}}, s) \<in> {(B, A). A \<subset> B \<and> B \<subseteq> S}
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<Phi> \<subseteq> S
\<Psi> \<subseteq> S
\<Psi> \<subseteq> R \<and> R \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
\<exists>s\<in>\<Phi>. R \<inter> E s \<noteq> {} \<and> s \<notin> R
[PROOF STEP]
show "(R \<union> ?\<Delta> R, R) \<in> {(B, A). A \<subset> B \<and> B \<subseteq> S}" "\<Psi> \<subseteq> R \<union> ?\<Delta> R"
[PROOF STATE]
proof (prove)
using this:
\<Phi> \<subseteq> S
\<Psi> \<subseteq> S
\<Psi> \<subseteq> R \<and> R \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
\<exists>s\<in>\<Phi>. R \<inter> E s \<noteq> {} \<and> s \<notin> R

goal (1 subgoal):
 1. (R \<union> {s \<in> \<Phi>. R \<inter> E s \<noteq> {}}, R) \<in> {(B, A). A \<subset> B \<and> B \<subseteq> S} &&& \<Psi> \<subseteq> R \<union> {s \<in> \<Phi>. R \<inter> E s \<noteq> {}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(R \<union> {s \<in> \<Phi>. R \<inter> E s \<noteq> {}}, R) \<in> {(B, A). A \<subset> B \<and> B \<subseteq> S}
\<Psi> \<subseteq> R \<union> {s \<in> \<Phi>. R \<inter> E s \<noteq> {}}

goal (3 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 3. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(R \<union> {s \<in> \<Phi>. R \<inter> E s \<noteq> {}}, R) \<in> {(B, A). A \<subset> B \<and> B \<subseteq> S}
\<Psi> \<subseteq> R \<union> {s \<in> \<Phi>. R \<inter> E s \<noteq> {}}

goal (3 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 3. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
fix s s'
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 3. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
assume s: "s \<in> \<Phi>" "s' \<in> R" "s' \<in> E s" and r: "(Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}"
[PROOF STATE]
proof (state)
this:
s \<in> \<Phi>
s' \<in> R
s' \<in> E s
(Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}

goal (3 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 3. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
with R
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<subseteq> R \<and> R \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
s \<in> \<Phi>
s' \<in> R
s' \<in> E s
(Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
[PROOF STEP]
have "(s, s') \<in> (Sigma \<Phi> E)\<^sup>*" "s' \<in> \<Phi> - \<Psi>"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<subseteq> R \<and> R \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
s \<in> \<Phi>
s' \<in> R
s' \<in> E s
(Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}

goal (1 subgoal):
 1. (s, s') \<in> (Sigma \<Phi> E)\<^sup>* &&& s' \<in> \<Phi> - \<Psi>
[PROOF STEP]
by (auto elim: converse_rtranclE)
[PROOF STATE]
proof (state)
this:
(s, s') \<in> (Sigma \<Phi> E)\<^sup>*
s' \<in> \<Phi> - \<Psi>

goal (3 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 3. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(s, s') \<in> (Sigma \<Phi> E)\<^sup>*
s' \<in> \<Phi> - \<Psi>

goal (3 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 3. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
with \<open>s' \<in> R\<close> R
[PROOF STATE]
proof (chain)
picking this:
s' \<in> R
\<Psi> \<subseteq> R \<and> R \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
(s, s') \<in> (Sigma \<Phi> E)\<^sup>*
s' \<in> \<Phi> - \<Psi>
[PROOF STEP]
obtain s'' where "(s', s'') \<in> (Sigma \<Phi> E)\<^sup>*" "s'' \<in> \<Psi>"
[PROOF STATE]
proof (prove)
using this:
s' \<in> R
\<Psi> \<subseteq> R \<and> R \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
(s, s') \<in> (Sigma \<Phi> E)\<^sup>*
s' \<in> \<Phi> - \<Psi>

goal (1 subgoal):
 1. (\<And>s''. \<lbrakk>(s', s'') \<in> (Sigma \<Phi> E)\<^sup>*; s'' \<in> \<Psi>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(s', s'') \<in> (Sigma \<Phi> E)\<^sup>*
s'' \<in> \<Psi>

goal (3 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 3. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(s, s') \<in> (Sigma \<Phi> E)\<^sup>*
s' \<in> \<Phi> - \<Psi>
(s', s'') \<in> (Sigma \<Phi> E)\<^sup>*
s'' \<in> \<Psi>
[PROOF STEP]
have "(s, s'') \<in> (Sigma \<Phi> E)\<^sup>*" "s'' \<in> \<Psi>"
[PROOF STATE]
proof (prove)
using this:
(s, s') \<in> (Sigma \<Phi> E)\<^sup>*
s' \<in> \<Phi> - \<Psi>
(s', s'') \<in> (Sigma \<Phi> E)\<^sup>*
s'' \<in> \<Psi>

goal (1 subgoal):
 1. (s, s'') \<in> (Sigma \<Phi> E)\<^sup>* &&& s'' \<in> \<Psi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(s, s'') \<in> (Sigma \<Phi> E)\<^sup>*
s'' \<in> \<Psi>

goal (3 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 3. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
with r
[PROOF STATE]
proof (chain)
picking this:
(Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
(s, s'') \<in> (Sigma \<Phi> E)\<^sup>*
s'' \<in> \<Psi>
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
(Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
(s, s'') \<in> (Sigma \<Phi> E)\<^sup>*
s'' \<in> \<Psi>

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

goal (3 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 3. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?s3 \<in> \<Phi>; ?s'3 \<in> R; ?s'3 \<in> E ?s3; (Sigma \<Phi> E)\<^sup>* `` {?s3} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False

goal (3 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s\<rbrakk> \<Longrightarrow> s \<union> {sa \<in> \<Phi>. s \<inter> E sa \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
 3. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
with \<open>\<Phi> \<subseteq> S\<close> R
[PROOF STATE]
proof (chain)
picking this:
\<Phi> \<subseteq> S
\<Psi> \<subseteq> R \<and> R \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
\<lbrakk>?s3 \<in> \<Phi>; ?s'3 \<in> R; ?s'3 \<in> E ?s3; (Sigma \<Phi> E)\<^sup>* `` {?s3} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show "R \<union> ?\<Delta> R \<subseteq> S - ?U"
[PROOF STATE]
proof (prove)
using this:
\<Phi> \<subseteq> S
\<Psi> \<subseteq> R \<and> R \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
\<lbrakk>?s3 \<in> \<Phi>; ?s'3 \<in> R; ?s'3 \<in> E ?s3; (Sigma \<Phi> E)\<^sup>* `` {?s3} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. R \<union> {s \<in> \<Phi>. R \<inter> E s \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
R \<union> {s \<in> \<Phi>. R \<inter> E s \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}

goal (2 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<Psi> \<subseteq> ?R3 \<and> ?R3 \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>s\<in>\<Phi>. ?R3 \<inter> E s \<noteq> {} \<and> s \<notin> ?R3\<rbrakk> \<Longrightarrow> ?R3 \<union> {s \<in> \<Phi>. ?R3 \<inter> E s \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}

goal (2 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<Psi> \<subseteq> ?R3 \<and> ?R3 \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<exists>s\<in>\<Phi>. ?R3 \<inter> E s \<noteq> {} \<and> s \<notin> ?R3\<rbrakk> \<Longrightarrow> ?R3 \<union> {s \<in> \<Phi>. ?R3 \<inter> E s \<noteq> {}} \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}

goal (2 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
fix R
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
assume R: "\<Psi> \<subseteq> R \<and> R \<subseteq> S - ?U" and dR: "\<not> (\<exists>s\<in>\<Phi>. R \<inter> E s \<noteq> {} \<and> s \<notin> R)"
[PROOF STATE]
proof (state)
this:
\<Psi> \<subseteq> R \<and> R \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
\<not> (\<exists>s\<in>\<Phi>. R \<inter> E s \<noteq> {} \<and> s \<notin> R)

goal (2 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<Psi> \<subseteq> R \<and> R \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
\<not> (\<exists>s\<in>\<Phi>. R \<inter> E s \<noteq> {} \<and> s \<notin> R)

goal (2 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
fix s t
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
assume s: "s \<in> S - R"
[PROOF STATE]
proof (state)
this:
s \<in> S - R

goal (2 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
assume s_t: "(s, t) \<in> (Sigma \<Phi> E)\<^sup>*"
[PROOF STATE]
proof (state)
this:
(s, t) \<in> (Sigma \<Phi> E)\<^sup>*

goal (2 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(s, t) \<in> (Sigma \<Phi> E)\<^sup>*
[PROOF STEP]
have "t \<in> S - R"
[PROOF STATE]
proof (prove)
using this:
(s, t) \<in> (Sigma \<Phi> E)\<^sup>*

goal (1 subgoal):
 1. t \<in> S - R
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s \<in> S - R
 2. \<And>y z. \<lbrakk>(s, y) \<in> (Sigma \<Phi> E)\<^sup>*; (y, z) \<in> Sigma \<Phi> E; y \<in> S - R\<rbrakk> \<Longrightarrow> z \<in> S - R
[PROOF STEP]
case (step t u)
[PROOF STATE]
proof (state)
this:
(s, t) \<in> (Sigma \<Phi> E)\<^sup>*
(t, u) \<in> Sigma \<Phi> E
t \<in> S - R

goal (2 subgoals):
 1. s \<in> S - R
 2. \<And>y z. \<lbrakk>(s, y) \<in> (Sigma \<Phi> E)\<^sup>*; (y, z) \<in> Sigma \<Phi> E; y \<in> S - R\<rbrakk> \<Longrightarrow> z \<in> S - R
[PROOF STEP]
with R dR E_closed
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<subseteq> R \<and> R \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
\<not> (\<exists>s\<in>\<Phi>. R \<inter> E s \<noteq> {} \<and> s \<notin> R)
\<Union> (E ` S) \<subseteq> S
(s, t) \<in> (Sigma \<Phi> E)\<^sup>*
(t, u) \<in> Sigma \<Phi> E
t \<in> S - R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<subseteq> R \<and> R \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
\<not> (\<exists>s\<in>\<Phi>. R \<inter> E s \<noteq> {} \<and> s \<notin> R)
\<Union> (E ` S) \<subseteq> S
(s, t) \<in> (Sigma \<Phi> E)\<^sup>*
(t, u) \<in> Sigma \<Phi> E
t \<in> S - R

goal (1 subgoal):
 1. u \<in> S - R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> S - R

goal (1 subgoal):
 1. s \<in> S - R
[PROOF STEP]
qed fact
[PROOF STATE]
proof (state)
this:
t \<in> S - R

goal (2 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> S - R
[PROOF STEP]
have "t \<notin> \<Psi>"
[PROOF STATE]
proof (prove)
using this:
t \<in> S - R

goal (1 subgoal):
 1. t \<notin> \<Psi>
[PROOF STEP]
using R
[PROOF STATE]
proof (prove)
using this:
t \<in> S - R
\<Psi> \<subseteq> R \<and> R \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}

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

goal (2 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?s3 \<in> S - R; (?s3, ?t3) \<in> (Sigma \<Phi> E)\<^sup>*\<rbrakk> \<Longrightarrow> ?t3 \<notin> \<Psi>

goal (2 subgoals):
 1. \<Psi> \<subseteq> \<Psi>
 2. \<And>s. \<lbrakk>\<Psi> \<subseteq> s \<and> s \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>sa\<in>\<Phi>. s \<inter> E sa \<noteq> {} \<and> sa \<notin> s)\<rbrakk> \<Longrightarrow> S - s = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
with R
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<subseteq> R \<and> R \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
\<lbrakk>?s3 \<in> S - R; (?s3, ?t3) \<in> (Sigma \<Phi> E)\<^sup>*\<rbrakk> \<Longrightarrow> ?t3 \<notin> \<Psi>
[PROOF STEP]
show "S - R = ?U"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<subseteq> R \<and> R \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
\<lbrakk>?s3 \<in> S - R; (?s3, ?t3) \<in> (Sigma \<Phi> E)\<^sup>*\<rbrakk> \<Longrightarrow> ?t3 \<notin> \<Psi>

goal (1 subgoal):
 1. S - R = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S - R = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}

goal (1 subgoal):
 1. \<Psi> \<subseteq> \<Psi>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<Psi> \<subseteq> ?R3 \<and> ?R3 \<subseteq> S - {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}; \<not> (\<exists>s\<in>\<Phi>. ?R3 \<inter> E s \<noteq> {} \<and> s \<notin> ?R3)\<rbrakk> \<Longrightarrow> S - ?R3 = {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}}

goal (1 subgoal):
 1. \<Psi> \<subseteq> \<Psi>
[PROOF STEP]
qed rule


[STATEMENT]
lemma Prob0_iff:
  assumes "\<Phi> \<subseteq> S" "\<Psi> \<subseteq> S"
  shows "Prob0 \<Phi> \<Psi> = {s\<in>S. AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)}" (is "_ = ?U")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prob0 \<Phi> \<Psi> = {s \<in> S. AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)}
[PROOF STEP]
unfolding Prob0_iff_reachable[OF assms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s \<in> S. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}} = {s \<in> S. AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)}
[PROOF STEP]
proof (intro Collect_cong conj_cong refl iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
 2. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
 2. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
[PROOF STEP]
assume s: "s \<in> S" "(Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}"
[PROOF STATE]
proof (state)
this:
s \<in> S
(Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
 2. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
s \<in> S
(Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
 2. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
[PROOF STEP]
fix \<omega>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
 2. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
[PROOF STEP]
assume "(HLD \<Phi> suntil HLD \<Psi>) \<omega>" "enabled (shd \<omega>) (stl \<omega>)" "(Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}"
[PROOF STATE]
proof (state)
this:
(HLD \<Phi> suntil HLD \<Psi>) \<omega>
enabled (shd \<omega>) (stl \<omega>)
(Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
 2. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(HLD \<Phi> suntil HLD \<Psi>) \<omega>
enabled (shd \<omega>) (stl \<omega>)
(Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
(HLD \<Phi> suntil HLD \<Psi>) \<omega>
enabled (shd \<omega>) (stl \<omega>)
(Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}

goal (1 subgoal):
 1. False
[PROOF STEP]
proof induction
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<omega>. \<lbrakk>HLD \<Psi> \<omega>; enabled (shd \<omega>) (stl \<omega>); (Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>\<omega>. \<lbrakk>HLD \<Phi> \<omega>; (HLD \<Phi> suntil HLD \<Psi>) (stl \<omega>); \<lbrakk>enabled (shd (stl \<omega>)) (stl (stl \<omega>)); (Sigma \<Phi> E)\<^sup>* `` {shd (stl \<omega>)} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False; enabled (shd \<omega>) (stl \<omega>); (Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (step \<omega>)
[PROOF STATE]
proof (state)
this:
HLD \<Phi> \<omega>
(HLD \<Phi> suntil HLD \<Psi>) (stl \<omega>)
\<lbrakk>enabled (shd (stl \<omega>)) (stl (stl \<omega>)); (Sigma \<Phi> E)\<^sup>* `` {shd (stl \<omega>)} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False
enabled (shd \<omega>) (stl \<omega>)
(Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}

goal (2 subgoals):
 1. \<And>\<omega>. \<lbrakk>HLD \<Psi> \<omega>; enabled (shd \<omega>) (stl \<omega>); (Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>\<omega>. \<lbrakk>HLD \<Phi> \<omega>; (HLD \<Phi> suntil HLD \<Psi>) (stl \<omega>); \<lbrakk>enabled (shd (stl \<omega>)) (stl (stl \<omega>)); (Sigma \<Phi> E)\<^sup>* `` {shd (stl \<omega>)} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False; enabled (shd \<omega>) (stl \<omega>); (Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
HLD \<Phi> \<omega>
(HLD \<Phi> suntil HLD \<Psi>) (stl \<omega>)
\<lbrakk>enabled (shd (stl \<omega>)) (stl (stl \<omega>)); (Sigma \<Phi> E)\<^sup>* `` {shd (stl \<omega>)} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False
enabled (shd \<omega>) (stl \<omega>)
(Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}

goal (2 subgoals):
 1. \<And>\<omega>. \<lbrakk>HLD \<Psi> \<omega>; enabled (shd \<omega>) (stl \<omega>); (Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>\<omega>. \<lbrakk>HLD \<Phi> \<omega>; (HLD \<Phi> suntil HLD \<Psi>) (stl \<omega>); \<lbrakk>enabled (shd (stl \<omega>)) (stl (stl \<omega>)); (Sigma \<Phi> E)\<^sup>* `` {shd (stl \<omega>)} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False; enabled (shd \<omega>) (stl \<omega>); (Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
HLD \<Phi> \<omega>
(HLD \<Phi> suntil HLD \<Psi>) (stl \<omega>)
\<lbrakk>enabled (shd (stl \<omega>)) (stl (stl \<omega>)); (Sigma \<Phi> E)\<^sup>* `` {shd (stl \<omega>)} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False
enabled (shd \<omega>) (stl \<omega>)
(Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}
[PROOF STEP]
have "(shd \<omega>, shd (stl \<omega>)) \<in> (Sigma \<Phi> E)\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
HLD \<Phi> \<omega>
(HLD \<Phi> suntil HLD \<Psi>) (stl \<omega>)
\<lbrakk>enabled (shd (stl \<omega>)) (stl (stl \<omega>)); (Sigma \<Phi> E)\<^sup>* `` {shd (stl \<omega>)} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False
enabled (shd \<omega>) (stl \<omega>)
(Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}

goal (1 subgoal):
 1. (shd \<omega>, shd (stl \<omega>)) \<in> (Sigma \<Phi> E)\<^sup>*
[PROOF STEP]
by (auto simp: enabled.simps[of _ "stl \<omega>"] HLD_iff)
[PROOF STATE]
proof (state)
this:
(shd \<omega>, shd (stl \<omega>)) \<in> (Sigma \<Phi> E)\<^sup>*

goal (2 subgoals):
 1. \<And>\<omega>. \<lbrakk>HLD \<Psi> \<omega>; enabled (shd \<omega>) (stl \<omega>); (Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>\<omega>. \<lbrakk>HLD \<Phi> \<omega>; (HLD \<Phi> suntil HLD \<Psi>) (stl \<omega>); \<lbrakk>enabled (shd (stl \<omega>)) (stl (stl \<omega>)); (Sigma \<Phi> E)\<^sup>* `` {shd (stl \<omega>)} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False; enabled (shd \<omega>) (stl \<omega>); (Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(shd \<omega>, shd (stl \<omega>)) \<in> (Sigma \<Phi> E)\<^sup>*
[PROOF STEP]
have "(Sigma \<Phi> E)\<^sup>* `` {shd (stl \<omega>)} \<subseteq> (Sigma \<Phi> E)\<^sup>* `` {shd \<omega>}"
[PROOF STATE]
proof (prove)
using this:
(shd \<omega>, shd (stl \<omega>)) \<in> (Sigma \<Phi> E)\<^sup>*

goal (1 subgoal):
 1. (Sigma \<Phi> E)\<^sup>* `` {shd (stl \<omega>)} \<subseteq> (Sigma \<Phi> E)\<^sup>* `` {shd \<omega>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Sigma \<Phi> E)\<^sup>* `` {shd (stl \<omega>)} \<subseteq> (Sigma \<Phi> E)\<^sup>* `` {shd \<omega>}

goal (2 subgoals):
 1. \<And>\<omega>. \<lbrakk>HLD \<Psi> \<omega>; enabled (shd \<omega>) (stl \<omega>); (Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>\<omega>. \<lbrakk>HLD \<Phi> \<omega>; (HLD \<Phi> suntil HLD \<Psi>) (stl \<omega>); \<lbrakk>enabled (shd (stl \<omega>)) (stl (stl \<omega>)); (Sigma \<Phi> E)\<^sup>* `` {shd (stl \<omega>)} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False; enabled (shd \<omega>) (stl \<omega>); (Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
HLD \<Phi> \<omega>
(HLD \<Phi> suntil HLD \<Psi>) (stl \<omega>)
\<lbrakk>enabled (shd (stl \<omega>)) (stl (stl \<omega>)); (Sigma \<Phi> E)\<^sup>* `` {shd (stl \<omega>)} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False
enabled (shd \<omega>) (stl \<omega>)
(Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}
(Sigma \<Phi> E)\<^sup>* `` {shd (stl \<omega>)} \<subseteq> (Sigma \<Phi> E)\<^sup>* `` {shd \<omega>}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
HLD \<Phi> \<omega>
(HLD \<Phi> suntil HLD \<Psi>) (stl \<omega>)
\<lbrakk>enabled (shd (stl \<omega>)) (stl (stl \<omega>)); (Sigma \<Phi> E)\<^sup>* `` {shd (stl \<omega>)} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False
enabled (shd \<omega>) (stl \<omega>)
(Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}
(Sigma \<Phi> E)\<^sup>* `` {shd (stl \<omega>)} \<subseteq> (Sigma \<Phi> E)\<^sup>* `` {shd \<omega>}

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto simp add: enabled.simps[of _ "stl \<omega>"])
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<And>\<omega>. \<lbrakk>HLD \<Psi> \<omega>; enabled (shd \<omega>) (stl \<omega>); (Sigma \<Phi> E)\<^sup>* `` {shd \<omega>} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
qed (auto simp: HLD_iff)
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
 2. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(HLD \<Phi> suntil HLD \<Psi>) ?\<omega>3; enabled (shd ?\<omega>3) (stl ?\<omega>3); (Sigma \<Phi> E)\<^sup>* `` {shd ?\<omega>3} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
 2. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
[PROOF STEP]
from s this[of "s ## \<omega>" for \<omega>]
[PROOF STATE]
proof (chain)
picking this:
s \<in> S
(Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
\<lbrakk>(HLD \<Phi> suntil HLD \<Psi>) (s ## ?\<omega>3); enabled (shd (s ## ?\<omega>3)) (stl (s ## ?\<omega>3)); (Sigma \<Phi> E)\<^sup>* `` {shd (s ## ?\<omega>3)} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show "AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)"
[PROOF STATE]
proof (prove)
using this:
s \<in> S
(Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
\<lbrakk>(HLD \<Phi> suntil HLD \<Psi>) (s ## ?\<omega>3); enabled (shd (s ## ?\<omega>3)) (stl (s ## ?\<omega>3)); (Sigma \<Phi> E)\<^sup>* `` {shd (s ## ?\<omega>3)} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
[PROOF STEP]
using AE_T_enabled[of s]
[PROOF STATE]
proof (prove)
using this:
s \<in> S
(Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
\<lbrakk>(HLD \<Phi> suntil HLD \<Psi>) (s ## ?\<omega>3); enabled (shd (s ## ?\<omega>3)) (stl (s ## ?\<omega>3)); (Sigma \<Phi> E)\<^sup>* `` {shd (s ## ?\<omega>3)} \<inter> \<Psi> = {}\<rbrakk> \<Longrightarrow> False
almost_everywhere (T s) (enabled s)

goal (1 subgoal):
 1. AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)

goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
[PROOF STEP]
assume s: "AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)"
[PROOF STATE]
proof (state)
this:
AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)

goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)

goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
[PROOF STEP]
assume "(s, t) \<in> (Sigma \<Phi> E)\<^sup>*"
[PROOF STATE]
proof (state)
this:
(s, t) \<in> (Sigma \<Phi> E)\<^sup>*

goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
[PROOF STEP]
from this s
[PROOF STATE]
proof (chain)
picking this:
(s, t) \<in> (Sigma \<Phi> E)\<^sup>*
AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
[PROOF STEP]
have "t \<notin> \<Psi>"
[PROOF STATE]
proof (prove)
using this:
(s, t) \<in> (Sigma \<Phi> E)\<^sup>*
AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)

goal (1 subgoal):
 1. t \<notin> \<Psi>
[PROOF STEP]
proof (induction rule: converse_rtrancl_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. AE \<omega> in T t. \<not> (HLD \<Phi> suntil HLD \<Psi>) (t ## \<omega>) \<Longrightarrow> t \<notin> \<Psi>
 2. \<And>y z. \<lbrakk>(y, z) \<in> Sigma \<Phi> E; (z, t) \<in> (Sigma \<Phi> E)\<^sup>*; AE \<omega> in T z. \<not> (HLD \<Phi> suntil HLD \<Psi>) (z ## \<omega>) \<Longrightarrow> t \<notin> \<Psi>; AE \<omega> in T y. \<not> (HLD \<Phi> suntil HLD \<Psi>) (y ## \<omega>)\<rbrakk> \<Longrightarrow> t \<notin> \<Psi>
[PROOF STEP]
case (step s u)
[PROOF STATE]
proof (state)
this:
(s, u) \<in> Sigma \<Phi> E
(u, t) \<in> (Sigma \<Phi> E)\<^sup>*
AE \<omega> in T u. \<not> (HLD \<Phi> suntil HLD \<Psi>) (u ## \<omega>) \<Longrightarrow> t \<notin> \<Psi>
AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)

goal (2 subgoals):
 1. AE \<omega> in T t. \<not> (HLD \<Phi> suntil HLD \<Psi>) (t ## \<omega>) \<Longrightarrow> t \<notin> \<Psi>
 2. \<And>y z. \<lbrakk>(y, z) \<in> Sigma \<Phi> E; (z, t) \<in> (Sigma \<Phi> E)\<^sup>*; AE \<omega> in T z. \<not> (HLD \<Phi> suntil HLD \<Psi>) (z ## \<omega>) \<Longrightarrow> t \<notin> \<Psi>; AE \<omega> in T y. \<not> (HLD \<Phi> suntil HLD \<Psi>) (y ## \<omega>)\<rbrakk> \<Longrightarrow> t \<notin> \<Psi>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(s, u) \<in> Sigma \<Phi> E
(u, t) \<in> (Sigma \<Phi> E)\<^sup>*
AE \<omega> in T u. \<not> (HLD \<Phi> suntil HLD \<Psi>) (u ## \<omega>) \<Longrightarrow> t \<notin> \<Psi>
AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(s, u) \<in> Sigma \<Phi> E
(u, t) \<in> (Sigma \<Phi> E)\<^sup>*
AE \<omega> in T u. \<not> (HLD \<Phi> suntil HLD \<Psi>) (u ## \<omega>) \<Longrightarrow> t \<notin> \<Psi>
AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)

goal (1 subgoal):
 1. t \<notin> \<Psi>
[PROOF STEP]
by (simp add: AE_T_iff[where x=s] suntil_Stream[of _ _ s])
[PROOF STATE]
proof (state)
this:
t \<notin> \<Psi>

goal (1 subgoal):
 1. AE \<omega> in T t. \<not> (HLD \<Phi> suntil HLD \<Psi>) (t ## \<omega>) \<Longrightarrow> t \<notin> \<Psi>
[PROOF STEP]
qed (simp add: suntil_Stream)
[PROOF STATE]
proof (state)
this:
t \<notin> \<Psi>

goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(s, ?t3) \<in> (Sigma \<Phi> E)\<^sup>* \<Longrightarrow> ?t3 \<notin> \<Psi>

goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; AE \<omega> in T s. \<not> (HLD \<Phi> suntil HLD \<Psi>) (s ## \<omega>)\<rbrakk> \<Longrightarrow> (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(s, ?t3) \<in> (Sigma \<Phi> E)\<^sup>* \<Longrightarrow> ?t3 \<notin> \<Psi>
[PROOF STEP]
show "(Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}"
[PROOF STATE]
proof (prove)
using this:
(s, ?t3) \<in> (Sigma \<Phi> E)\<^sup>* \<Longrightarrow> ?t3 \<notin> \<Psi>

goal (1 subgoal):
 1. (Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Sigma \<Phi> E)\<^sup>* `` {s} \<inter> \<Psi> = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma E_rtrancl_closed:
  assumes "s \<in> S" "(s, t) \<in> (SIGMA x:A. B x)\<^sup>*" "\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> E x" shows "t \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> S
[PROOF STEP]
using assms(2,3,1) E_closed
[PROOF STATE]
proof (prove)
using this:
(s, t) \<in> (Sigma A B)\<^sup>*
?x1 \<in> A \<Longrightarrow> B ?x1 \<subseteq> E ?x1
s \<in> S
\<Union> (E ` S) \<subseteq> S

goal (1 subgoal):
 1. t \<in> S
[PROOF STEP]
by induction force+