[STATEMENT]
theorem Sat_complete:
  "Sat F \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sat F \<noteq> None
[PROOF STEP]
proof (induct F rule: Sat.induct)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. Sat sform.true \<noteq> None
 2. \<And>L. Sat (Label L) \<noteq> None
 3. \<And>F. Sat F \<noteq> None \<Longrightarrow> Sat (Neg F) \<noteq> None
 4. \<And>F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (And F1 F2) \<noteq> None
 5. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Prob rel r (X F)) \<noteq> None
 6. \<And>rel r k F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U k F1 F2)) \<noteq> None
 7. \<And>rel r F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U\<^sup>\<infinity> F1 F2)) \<noteq> None
 8. \<And>rel r k. Sat (Exp rel r (C\<^sup>\<le> k)) \<noteq> None
 9. \<And>rel r k. Sat (Exp rel r (I\<^sup>= k)) \<noteq> None
 10. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Exp rel r (Future F)) \<noteq> None
[PROOF STEP]
case (7 r rel \<Phi> \<Psi>)
[PROOF STATE]
proof (state)
this:
Sat \<Phi> \<noteq> None
Sat \<Phi> = Some ?a1 \<Longrightarrow> Sat \<Psi> \<noteq> None

goal (10 subgoals):
 1. Sat sform.true \<noteq> None
 2. \<And>L. Sat (Label L) \<noteq> None
 3. \<And>F. Sat F \<noteq> None \<Longrightarrow> Sat (Neg F) \<noteq> None
 4. \<And>F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (And F1 F2) \<noteq> None
 5. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Prob rel r (X F)) \<noteq> None
 6. \<And>rel r k F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U k F1 F2)) \<noteq> None
 7. \<And>rel r F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U\<^sup>\<infinity> F1 F2)) \<noteq> None
 8. \<And>rel r k. Sat (Exp rel r (C\<^sup>\<le> k)) \<noteq> None
 9. \<And>rel r k. Sat (Exp rel r (I\<^sup>= k)) \<noteq> None
 10. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Exp rel r (Future F)) \<noteq> None
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sat \<Phi> \<noteq> None
Sat \<Phi> = Some ?a1 \<Longrightarrow> Sat \<Psi> \<noteq> None
[PROOF STEP]
have F: "Sat \<Phi> = Some (svalid \<Phi>)" "Sat \<Psi> = Some (svalid \<Psi>)"
[PROOF STATE]
proof (prove)
using this:
Sat \<Phi> \<noteq> None
Sat \<Phi> = Some ?a1 \<Longrightarrow> Sat \<Psi> \<noteq> None

goal (1 subgoal):
 1. Sat \<Phi> = Some (svalid \<Phi>) &&& Sat \<Psi> = Some (svalid \<Psi>)
[PROOF STEP]
by (auto intro!: Sat_sound)
[PROOF STATE]
proof (state)
this:
Sat \<Phi> = Some (svalid \<Phi>)
Sat \<Psi> = Some (svalid \<Psi>)

goal (10 subgoals):
 1. Sat sform.true \<noteq> None
 2. \<And>L. Sat (Label L) \<noteq> None
 3. \<And>F. Sat F \<noteq> None \<Longrightarrow> Sat (Neg F) \<noteq> None
 4. \<And>F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (And F1 F2) \<noteq> None
 5. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Prob rel r (X F)) \<noteq> None
 6. \<And>rel r k F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U k F1 F2)) \<noteq> None
 7. \<And>rel r F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U\<^sup>\<infinity> F1 F2)) \<noteq> None
 8. \<And>rel r k. Sat (Exp rel r (C\<^sup>\<le> k)) \<noteq> None
 9. \<And>rel r k. Sat (Exp rel r (I\<^sup>= k)) \<noteq> None
 10. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Exp rel r (Future F)) \<noteq> None
[PROOF STEP]
define constants :: "'s \<Rightarrow> real" where "constants = (\<lambda>s. if s \<in> svalid \<Psi> then 1 else 0)"
[PROOF STATE]
proof (state)
this:
constants = (\<lambda>s. if s \<in> svalid \<Psi> then 1 else 0)

goal (10 subgoals):
 1. Sat sform.true \<noteq> None
 2. \<And>L. Sat (Label L) \<noteq> None
 3. \<And>F. Sat F \<noteq> None \<Longrightarrow> Sat (Neg F) \<noteq> None
 4. \<And>F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (And F1 F2) \<noteq> None
 5. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Prob rel r (X F)) \<noteq> None
 6. \<And>rel r k F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U k F1 F2)) \<noteq> None
 7. \<And>rel r F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U\<^sup>\<infinity> F1 F2)) \<noteq> None
 8. \<And>rel r k. Sat (Exp rel r (C\<^sup>\<le> k)) \<noteq> None
 9. \<And>rel r k. Sat (Exp rel r (I\<^sup>= k)) \<noteq> None
 10. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Exp rel r (Future F)) \<noteq> None
[PROOF STEP]
define distr where "distr = LES (Prob0 (svalid \<Phi>) (svalid \<Psi>) \<union> svalid \<Psi>)"
[PROOF STATE]
proof (state)
this:
distr = LES (Prob0 (svalid \<Phi>) (svalid \<Psi>) \<union> svalid \<Psi>)

goal (10 subgoals):
 1. Sat sform.true \<noteq> None
 2. \<And>L. Sat (Label L) \<noteq> None
 3. \<And>F. Sat F \<noteq> None \<Longrightarrow> Sat (Neg F) \<noteq> None
 4. \<And>F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (And F1 F2) \<noteq> None
 5. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Prob rel r (X F)) \<noteq> None
 6. \<And>rel r k F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U k F1 F2)) \<noteq> None
 7. \<And>rel r F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U\<^sup>\<infinity> F1 F2)) \<noteq> None
 8. \<And>rel r k. Sat (Exp rel r (C\<^sup>\<le> k)) \<noteq> None
 9. \<And>rel r k. Sat (Exp rel r (I\<^sup>= k)) \<noteq> None
 10. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Exp rel r (Future F)) \<noteq> None
[PROOF STEP]
have "\<exists>l. gauss_jordan' distr constants = Some l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. gauss_jordan' distr constants = Some l
[PROOF STEP]
proof (rule gauss_jordan'_complete[OF _ uniqueness_of_ProbU])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>s\<in>S. (\<Sum>s'\<in>S. distr s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> ?F1.2 ?F2.3) (s' ## \<omega>))) = constants s
 2. \<And>l. \<forall>s\<in>S. (\<Sum>s'\<in>S. distr s s' * l s') = constants s \<Longrightarrow> \<forall>s\<in>S. (\<Sum>s'\<in>S. LES (Prob0 (svalid ?F1.2) (svalid ?F2.3) \<union> svalid ?F2.3) s s' * l s') = (if s \<in> svalid ?F2.3 then 1 else 0)
[PROOF STEP]
show "\<forall>s\<in>S. (\<Sum>s'\<in>S. distr s s' * \<P>(\<omega> in T s'. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = constants s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s\<in>S. (\<Sum>s'\<in>S. distr s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = constants s
[PROOF STEP]
apply (simp add: distr_def constants_def LES_def del: pvalid.simps space_T)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s\<in>S. (s \<in> svalid \<Psi> \<longrightarrow> (\<Sum>s'\<in>S. (if s' = s then 1 else 0) * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 1) \<and> (s \<notin> svalid \<Psi> \<longrightarrow> (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0)
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<in> svalid \<Psi>\<rbrakk> \<Longrightarrow> (\<Sum>s'\<in>S. (if s' = s then 1 else 0) * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 1
 2. \<And>s. \<lbrakk>s \<in> S; s \<notin> svalid \<Psi>\<rbrakk> \<Longrightarrow> (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<in> svalid \<Psi>\<rbrakk> \<Longrightarrow> (\<Sum>s'\<in>S. (if s' = s then 1 else 0) * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 1
 2. \<And>s. \<lbrakk>s \<in> S; s \<notin> svalid \<Psi>\<rbrakk> \<Longrightarrow> (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
assume "s \<in> svalid \<Psi>" "s \<in> S"
[PROOF STATE]
proof (state)
this:
s \<in> svalid \<Psi>
s \<in> S

goal (2 subgoals):
 1. \<And>s. \<lbrakk>s \<in> S; s \<in> svalid \<Psi>\<rbrakk> \<Longrightarrow> (\<Sum>s'\<in>S. (if s' = s then 1 else 0) * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 1
 2. \<And>s. \<lbrakk>s \<in> S; s \<notin> svalid \<Psi>\<rbrakk> \<Longrightarrow> (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> svalid \<Psi>
s \<in> S
[PROOF STEP]
show "(\<Sum>s'\<in>S. (if s' = s then 1 else 0) * \<P>(\<omega> in T s'. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 1"
[PROOF STATE]
proof (prove)
using this:
s \<in> svalid \<Psi>
s \<in> S

goal (1 subgoal):
 1. (\<Sum>s'\<in>S. (if s' = s then 1 else 0) * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 1
[PROOF STEP]
by (simp add: single_l suntil_Stream)
[PROOF STATE]
proof (state)
this:
(\<Sum>s'\<in>S. (if s' = s then 1 else 0) * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 1

goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> svalid \<Psi>\<rbrakk> \<Longrightarrow> (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> svalid \<Psi>\<rbrakk> \<Longrightarrow> (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> svalid \<Psi>\<rbrakk> \<Longrightarrow> (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
assume s: "s \<notin> svalid \<Psi>" "s \<in> S"
[PROOF STATE]
proof (state)
this:
s \<notin> svalid \<Psi>
s \<in> S

goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> svalid \<Psi>\<rbrakk> \<Longrightarrow> (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
let ?x = "\<lambda>s'. \<P>(\<omega> in T s'. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<in> S; s \<notin> svalid \<Psi>\<rbrakk> \<Longrightarrow> (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
show "(\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * ?x s') = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
 2. \<not> ?P \<Longrightarrow> (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
assume "s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>)"
[PROOF STATE]
proof (state)
this:
s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>)

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
 2. \<not> ?P \<Longrightarrow> (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
with s
[PROOF STATE]
proof (chain)
picking this:
s \<notin> svalid \<Psi>
s \<in> S
s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<notin> svalid \<Psi>
s \<in> S
s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>)

goal (1 subgoal):
 1. (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
by (simp add: single_l Prob0_iff svalid_subset_S T.prob_eq_0_AE del: space_T)
[PROOF STATE]
proof (state)
this:
(\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0

goal (1 subgoal):
 1. s \<notin> Prob0 (svalid \<Phi>) (svalid \<Psi>) \<Longrightarrow> (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<notin> Prob0 (svalid \<Phi>) (svalid \<Psi>) \<Longrightarrow> (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
assume s_not_0: "s \<notin> Prob0 (svalid \<Phi>) (svalid \<Psi>)"
[PROOF STATE]
proof (state)
this:
s \<notin> Prob0 (svalid \<Phi>) (svalid \<Psi>)

goal (1 subgoal):
 1. s \<notin> Prob0 (svalid \<Phi>) (svalid \<Psi>) \<Longrightarrow> (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
with s
[PROOF STATE]
proof (chain)
picking this:
s \<notin> svalid \<Psi>
s \<in> S
s \<notin> Prob0 (svalid \<Phi>) (svalid \<Psi>)
[PROOF STEP]
have *:"\<And>s' \<omega>. s' \<in> S \<Longrightarrow> pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s ## s' ## \<omega>) = pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>)"
[PROOF STATE]
proof (prove)
using this:
s \<notin> svalid \<Psi>
s \<in> S
s \<notin> Prob0 (svalid \<Phi>) (svalid \<Psi>)

goal (1 subgoal):
 1. \<And>s' \<omega>. s' \<in> S \<Longrightarrow> pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s ## s' ## \<omega>) = pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>)
[PROOF STEP]
by (auto simp: suntil_Stream Prob0_iff svalid_subset_S)
[PROOF STATE]
proof (state)
this:
?s'1 \<in> S \<Longrightarrow> pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s ## ?s'1 ## ?\<omega>1) = pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (?s'1 ## ?\<omega>1)

goal (1 subgoal):
 1. s \<notin> Prob0 (svalid \<Phi>) (svalid \<Psi>) \<Longrightarrow> (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
have "(\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * ?x s') =
          (\<Sum>s'\<in>S. \<tau> s s' * ?x s' - (if s' = s then 1 else 0) * ?x s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>)) - (if s' = s then 1 else 0) * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>)))
[PROOF STEP]
by (auto intro!: sum.cong simp: field_simps)
[PROOF STATE]
proof (state)
this:
(\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>)) - (if s' = s then 1 else 0) * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>)))

goal (1 subgoal):
 1. s \<notin> Prob0 (svalid \<Phi>) (svalid \<Psi>) \<Longrightarrow> (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>)) - (if s' = s then 1 else 0) * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>)))

goal (1 subgoal):
 1. s \<notin> Prob0 (svalid \<Phi>) (svalid \<Psi>) \<Longrightarrow> (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
have "\<dots> = (\<Sum>s'\<in>S. \<tau> s s' * ?x s') - ?x s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>)) - (if s' = s then 1 else 0) * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) - prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s ## \<omega>))
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
s \<notin> svalid \<Psi>
s \<in> S

goal (1 subgoal):
 1. (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>)) - (if s' = s then 1 else 0) * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) - prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s ## \<omega>))
[PROOF STEP]
by (simp add: single_l sum_subtractf)
[PROOF STATE]
proof (state)
this:
(\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>)) - (if s' = s then 1 else 0) * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) - prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s ## \<omega>))

goal (1 subgoal):
 1. s \<notin> Prob0 (svalid \<Phi>) (svalid \<Psi>) \<Longrightarrow> (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) - prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s ## \<omega>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) - prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s ## \<omega>))

goal (1 subgoal):
 1. (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
using * prob_sum[OF \<open>s \<in> S\<close>] s_not_0
[PROOF STATE]
proof (prove)
using this:
(\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = (\<Sum>s'\<in>S. \<tau> s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) - prob s (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s ## \<omega>))
?s'1 \<in> S \<Longrightarrow> pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s ## ?s'1 ## ?\<omega>1) = pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (?s'1 ## ?\<omega>1)
Measurable.pred (stream_space (count_space UNIV)) ?P \<Longrightarrow> prob s ?P = (\<Sum>t\<in>S. \<tau> s t * prob t (\<lambda>\<omega>. ?P (t ## \<omega>)))
s \<notin> Prob0 (svalid \<Phi>) (svalid \<Psi>)

goal (1 subgoal):
 1. (\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0
[PROOF STEP]
by (simp del: pvalid.simps)
[PROOF STATE]
proof (state)
this:
(\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>s'\<in>S. (if s \<in> Prob0 (svalid \<Phi>) (svalid \<Psi>) then if s' = s then 1 else 0 else if s' = s then \<tau> s s' - 1 else \<tau> s s') * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>s\<in>S. (\<Sum>s'\<in>S. distr s s' * prob s' (\<lambda>\<omega>. pvalid (U\<^sup>\<infinity> \<Phi> \<Psi>) (s' ## \<omega>))) = constants s

goal (1 subgoal):
 1. \<And>l. \<forall>s\<in>S. (\<Sum>s'\<in>S. distr s s' * l s') = constants s \<Longrightarrow> \<forall>s\<in>S. (\<Sum>s'\<in>S. LES (Prob0 (svalid \<Phi>) (svalid \<Psi>) \<union> svalid \<Psi>) s s' * l s') = (if s \<in> svalid \<Psi> then 1 else 0)
[PROOF STEP]
qed (simp add: distr_def constants_def)
[PROOF STATE]
proof (state)
this:
\<exists>l. gauss_jordan' distr constants = Some l

goal (10 subgoals):
 1. Sat sform.true \<noteq> None
 2. \<And>L. Sat (Label L) \<noteq> None
 3. \<And>F. Sat F \<noteq> None \<Longrightarrow> Sat (Neg F) \<noteq> None
 4. \<And>F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (And F1 F2) \<noteq> None
 5. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Prob rel r (X F)) \<noteq> None
 6. \<And>rel r k F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U k F1 F2)) \<noteq> None
 7. \<And>rel r F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U\<^sup>\<infinity> F1 F2)) \<noteq> None
 8. \<And>rel r k. Sat (Exp rel r (C\<^sup>\<le> k)) \<noteq> None
 9. \<And>rel r k. Sat (Exp rel r (I\<^sup>= k)) \<noteq> None
 10. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Exp rel r (Future F)) \<noteq> None
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l. gauss_jordan' distr constants = Some l
[PROOF STEP]
have P: "\<exists>l. ProbUinfty (svalid \<Phi>) (svalid \<Psi>) = Some l"
[PROOF STATE]
proof (prove)
using this:
\<exists>l. gauss_jordan' distr constants = Some l

goal (1 subgoal):
 1. \<exists>l. ProbUinfty (svalid \<Phi>) (svalid \<Psi>) = Some l
[PROOF STEP]
unfolding ProbUinfty_def constants_def distr_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l. gauss_jordan' (LES (Prob0 (svalid \<Phi>) (svalid \<Psi>) \<union> svalid \<Psi>)) (\<lambda>s. if s \<in> svalid \<Psi> then 1 else 0) = Some l

goal (1 subgoal):
 1. \<exists>l. gauss_jordan' (LES (Prob0 (svalid \<Phi>) (svalid \<Psi>) \<union> svalid \<Psi>)) (\<lambda>i. if i \<in> svalid \<Psi> then 1 else 0) = Some l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>l. ProbUinfty (svalid \<Phi>) (svalid \<Psi>) = Some l

goal (10 subgoals):
 1. Sat sform.true \<noteq> None
 2. \<And>L. Sat (Label L) \<noteq> None
 3. \<And>F. Sat F \<noteq> None \<Longrightarrow> Sat (Neg F) \<noteq> None
 4. \<And>F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (And F1 F2) \<noteq> None
 5. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Prob rel r (X F)) \<noteq> None
 6. \<And>rel r k F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U k F1 F2)) \<noteq> None
 7. \<And>rel r F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U\<^sup>\<infinity> F1 F2)) \<noteq> None
 8. \<And>rel r k. Sat (Exp rel r (C\<^sup>\<le> k)) \<noteq> None
 9. \<And>rel r k. Sat (Exp rel r (I\<^sup>= k)) \<noteq> None
 10. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Exp rel r (Future F)) \<noteq> None
[PROOF STEP]
with F
[PROOF STATE]
proof (chain)
picking this:
Sat \<Phi> = Some (svalid \<Phi>)
Sat \<Psi> = Some (svalid \<Psi>)
\<exists>l. ProbUinfty (svalid \<Phi>) (svalid \<Psi>) = Some l
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Sat \<Phi> = Some (svalid \<Phi>)
Sat \<Psi> = Some (svalid \<Psi>)
\<exists>l. ProbUinfty (svalid \<Phi>) (svalid \<Psi>) = Some l

goal (1 subgoal):
 1. Sat (Prob r rel (U\<^sup>\<infinity> \<Phi> \<Psi>)) \<noteq> None
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Sat (Prob r rel (U\<^sup>\<infinity> \<Phi> \<Psi>)) \<noteq> None

goal (9 subgoals):
 1. Sat sform.true \<noteq> None
 2. \<And>L. Sat (Label L) \<noteq> None
 3. \<And>F. Sat F \<noteq> None \<Longrightarrow> Sat (Neg F) \<noteq> None
 4. \<And>F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (And F1 F2) \<noteq> None
 5. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Prob rel r (X F)) \<noteq> None
 6. \<And>rel r k F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U k F1 F2)) \<noteq> None
 7. \<And>rel r k. Sat (Exp rel r (C\<^sup>\<le> k)) \<noteq> None
 8. \<And>rel r k. Sat (Exp rel r (I\<^sup>= k)) \<noteq> None
 9. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Exp rel r (Future F)) \<noteq> None
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. Sat sform.true \<noteq> None
 2. \<And>L. Sat (Label L) \<noteq> None
 3. \<And>F. Sat F \<noteq> None \<Longrightarrow> Sat (Neg F) \<noteq> None
 4. \<And>F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (And F1 F2) \<noteq> None
 5. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Prob rel r (X F)) \<noteq> None
 6. \<And>rel r k F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U k F1 F2)) \<noteq> None
 7. \<And>rel r k. Sat (Exp rel r (C\<^sup>\<le> k)) \<noteq> None
 8. \<And>rel r k. Sat (Exp rel r (I\<^sup>= k)) \<noteq> None
 9. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Exp rel r (Future F)) \<noteq> None
[PROOF STEP]
case (10 rel r \<Phi>)
[PROOF STATE]
proof (state)
this:
Sat \<Phi> \<noteq> None

goal (9 subgoals):
 1. Sat sform.true \<noteq> None
 2. \<And>L. Sat (Label L) \<noteq> None
 3. \<And>F. Sat F \<noteq> None \<Longrightarrow> Sat (Neg F) \<noteq> None
 4. \<And>F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (And F1 F2) \<noteq> None
 5. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Prob rel r (X F)) \<noteq> None
 6. \<And>rel r k F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U k F1 F2)) \<noteq> None
 7. \<And>rel r k. Sat (Exp rel r (C\<^sup>\<le> k)) \<noteq> None
 8. \<And>rel r k. Sat (Exp rel r (I\<^sup>= k)) \<noteq> None
 9. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Exp rel r (Future F)) \<noteq> None
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Sat \<Phi> \<noteq> None
[PROOF STEP]
have F: "Sat \<Phi> = Some (svalid \<Phi>)"
[PROOF STATE]
proof (prove)
using this:
Sat \<Phi> \<noteq> None

goal (1 subgoal):
 1. Sat \<Phi> = Some (svalid \<Phi>)
[PROOF STEP]
by (auto intro!: Sat_sound)
[PROOF STATE]
proof (state)
this:
Sat \<Phi> = Some (svalid \<Phi>)

goal (9 subgoals):
 1. Sat sform.true \<noteq> None
 2. \<And>L. Sat (Label L) \<noteq> None
 3. \<And>F. Sat F \<noteq> None \<Longrightarrow> Sat (Neg F) \<noteq> None
 4. \<And>F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (And F1 F2) \<noteq> None
 5. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Prob rel r (X F)) \<noteq> None
 6. \<And>rel r k F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U k F1 F2)) \<noteq> None
 7. \<And>rel r k. Sat (Exp rel r (C\<^sup>\<le> k)) \<noteq> None
 8. \<And>rel r k. Sat (Exp rel r (I\<^sup>= k)) \<noteq> None
 9. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Exp rel r (Future F)) \<noteq> None
[PROOF STEP]
let ?F = "svalid \<Phi>"
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. Sat sform.true \<noteq> None
 2. \<And>L. Sat (Label L) \<noteq> None
 3. \<And>F. Sat F \<noteq> None \<Longrightarrow> Sat (Neg F) \<noteq> None
 4. \<And>F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (And F1 F2) \<noteq> None
 5. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Prob rel r (X F)) \<noteq> None
 6. \<And>rel r k F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U k F1 F2)) \<noteq> None
 7. \<And>rel r k. Sat (Exp rel r (C\<^sup>\<le> k)) \<noteq> None
 8. \<And>rel r k. Sat (Exp rel r (I\<^sup>= k)) \<noteq> None
 9. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Exp rel r (Future F)) \<noteq> None
[PROOF STEP]
define N where "N \<equiv> Prob0 S ?F"
[PROOF STATE]
proof (state)
this:
N \<equiv> Prob0 S (svalid \<Phi>)

goal (9 subgoals):
 1. Sat sform.true \<noteq> None
 2. \<And>L. Sat (Label L) \<noteq> None
 3. \<And>F. Sat F \<noteq> None \<Longrightarrow> Sat (Neg F) \<noteq> None
 4. \<And>F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (And F1 F2) \<noteq> None
 5. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Prob rel r (X F)) \<noteq> None
 6. \<And>rel r k F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U k F1 F2)) \<noteq> None
 7. \<And>rel r k. Sat (Exp rel r (C\<^sup>\<le> k)) \<noteq> None
 8. \<And>rel r k. Sat (Exp rel r (I\<^sup>= k)) \<noteq> None
 9. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Exp rel r (Future F)) \<noteq> None
[PROOF STEP]
define Y where "Y \<equiv> Prob1 N S ?F"
[PROOF STATE]
proof (state)
this:
Y \<equiv> Prob1 N S (svalid \<Phi>)

goal (9 subgoals):
 1. Sat sform.true \<noteq> None
 2. \<And>L. Sat (Label L) \<noteq> None
 3. \<And>F. Sat F \<noteq> None \<Longrightarrow> Sat (Neg F) \<noteq> None
 4. \<And>F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (And F1 F2) \<noteq> None
 5. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Prob rel r (X F)) \<noteq> None
 6. \<And>rel r k F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U k F1 F2)) \<noteq> None
 7. \<And>rel r k. Sat (Exp rel r (C\<^sup>\<le> k)) \<noteq> None
 8. \<And>rel r k. Sat (Exp rel r (I\<^sup>= k)) \<noteq> None
 9. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Exp rel r (Future F)) \<noteq> None
[PROOF STEP]
define const where "const \<equiv> (\<lambda>s. if s \<in> Y \<and> s \<notin> ?F then - \<rho> s - (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s') else 0)"
[PROOF STATE]
proof (state)
this:
const \<equiv> \<lambda>s. if s \<in> Y \<and> s \<notin> svalid \<Phi> then - \<rho> s - (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s') else 0

goal (9 subgoals):
 1. Sat sform.true \<noteq> None
 2. \<And>L. Sat (Label L) \<noteq> None
 3. \<And>F. Sat F \<noteq> None \<Longrightarrow> Sat (Neg F) \<noteq> None
 4. \<And>F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (And F1 F2) \<noteq> None
 5. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Prob rel r (X F)) \<noteq> None
 6. \<And>rel r k F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U k F1 F2)) \<noteq> None
 7. \<And>rel r k. Sat (Exp rel r (C\<^sup>\<le> k)) \<noteq> None
 8. \<And>rel r k. Sat (Exp rel r (I\<^sup>= k)) \<noteq> None
 9. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Exp rel r (Future F)) \<noteq> None
[PROOF STEP]
let ?E = "\<lambda>s'. \<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s'"
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. Sat sform.true \<noteq> None
 2. \<And>L. Sat (Label L) \<noteq> None
 3. \<And>F. Sat F \<noteq> None \<Longrightarrow> Sat (Neg F) \<noteq> None
 4. \<And>F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (And F1 F2) \<noteq> None
 5. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Prob rel r (X F)) \<noteq> None
 6. \<And>rel r k F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U k F1 F2)) \<noteq> None
 7. \<And>rel r k. Sat (Exp rel r (C\<^sup>\<le> k)) \<noteq> None
 8. \<And>rel r k. Sat (Exp rel r (I\<^sup>= k)) \<noteq> None
 9. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Exp rel r (Future F)) \<noteq> None
[PROOF STEP]
have "\<exists>l. gauss_jordan' (LES (S - Y \<union> ?F)) const = Some l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. gauss_jordan' (LES (S - Y \<union> svalid \<Phi>)) const = Some l
[PROOF STEP]
proof (rule gauss_jordan'_complete[OF _ uniqueness_of_ExpFuture[OF N_def Y_def const_def]])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>s\<in>S. (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
 2. \<And>l s. \<lbrakk>\<forall>s\<in>S. (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * l s') = const s; s \<in> S\<rbrakk> \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * l s') = const s
[PROOF STEP]
show "\<forall>s\<in>S. (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (?E s')) = const s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s\<in>S. (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
assume "s \<in> S"
[PROOF STATE]
proof (state)
this:
s \<in> S

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
show "(\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (?E s')) = const s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
 2. \<not> ?P \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
assume s: "s \<in> S - (Y - svalid \<Phi>)"
[PROOF STATE]
proof (state)
this:
s \<in> S - (Y - svalid \<Phi>)

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
 2. \<not> ?P \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
 2. \<not> ?P \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
assume "s \<in> Y"
[PROOF STATE]
proof (state)
this:
s \<in> Y

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
 2. \<not> ?P \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
with \<open>s \<in> S\<close> s \<open>s \<in> Y\<close>
[PROOF STATE]
proof (chain)
picking this:
s \<in> S
s \<in> S - (Y - svalid \<Phi>)
s \<in> Y
s \<in> Y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<in> S
s \<in> S - (Y - svalid \<Phi>)
s \<in> Y
s \<in> Y

goal (1 subgoal):
 1. (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
by (simp add: LES_def const_def single_l ev_Stream)
[PROOF STATE]
proof (state)
this:
(\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s

goal (1 subgoal):
 1. s \<notin> Y \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<notin> Y \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
assume "s \<notin> Y"
[PROOF STATE]
proof (state)
this:
s \<notin> Y

goal (1 subgoal):
 1. s \<notin> Y \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
with infinite_reward[of s \<Phi>] Y_def N_def s \<open>s \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>s \<in> S; s \<notin> Prob1 (Prob0 S (svalid \<Phi>)) S (svalid \<Phi>)\<rbrakk> \<Longrightarrow> \<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s ## \<omega>) \<partial>T s = \<infinity>
Y \<equiv> Prob1 N S (svalid \<Phi>)
N \<equiv> Prob0 S (svalid \<Phi>)
s \<in> S - (Y - svalid \<Phi>)
s \<in> S
s \<notin> Y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>s \<in> S; s \<notin> Prob1 (Prob0 S (svalid \<Phi>)) S (svalid \<Phi>)\<rbrakk> \<Longrightarrow> \<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s ## \<omega>) \<partial>T s = \<infinity>
Y \<equiv> Prob1 N S (svalid \<Phi>)
N \<equiv> Prob0 S (svalid \<Phi>)
s \<in> S - (Y - svalid \<Phi>)
s \<in> S
s \<notin> Y

goal (1 subgoal):
 1. (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
by (simp add: const_def LES_def single_l del: reward.simps)
[PROOF STATE]
proof (state)
this:
(\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s

goal (1 subgoal):
 1. s \<notin> S - (Y - svalid \<Phi>) \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<notin> S - (Y - svalid \<Phi>) \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
assume s: "s \<notin> S - (Y - svalid \<Phi>)"
[PROOF STATE]
proof (state)
this:
s \<notin> S - (Y - svalid \<Phi>)

goal (1 subgoal):
 1. s \<notin> S - (Y - svalid \<Phi>) \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
have "(\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * enn2real (?E s')) =
          (\<Sum>s'\<in>S. \<tau> s s' * enn2real (?E s') - (if s' = s then 1 else 0) * enn2real (?E s'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s') - (if s' = s then 1 else 0) * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s'))
[PROOF STEP]
by (auto intro!: sum.cong simp: field_simps)
[PROOF STATE]
proof (state)
this:
(\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s') - (if s' = s then 1 else 0) * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s'))

goal (1 subgoal):
 1. s \<notin> S - (Y - svalid \<Phi>) \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s') - (if s' = s then 1 else 0) * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s'))

goal (1 subgoal):
 1. s \<notin> S - (Y - svalid \<Phi>) \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
have "\<dots> = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (?E s')) - enn2real (?E s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s') - (if s' = s then 1 else 0) * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) - enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
using \<open>s \<in> S\<close>
[PROOF STATE]
proof (prove)
using this:
s \<in> S

goal (1 subgoal):
 1. (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s') - (if s' = s then 1 else 0) * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) - enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
by (simp add: sum_subtractf single_l)
[PROOF STATE]
proof (state)
this:
(\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s') - (if s' = s then 1 else 0) * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) - enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s ## \<omega>) \<partial>T s)

goal (1 subgoal):
 1. s \<notin> S - (Y - svalid \<Phi>) \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) - enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s ## \<omega>) \<partial>T s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) - enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s ## \<omega>) \<partial>T s)

goal (1 subgoal):
 1. (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
using s \<open>s \<in> S\<close> existence_of_ExpFuture[OF N_def Y_def \<open>s \<in> S\<close> s]
[PROOF STATE]
proof (prove)
using this:
(\<Sum>s'\<in>S. (if s' = s then \<tau> s s' - 1 else \<tau> s s') * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) - enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s ## \<omega>) \<partial>T s)
s \<notin> S - (Y - svalid \<Phi>)
s \<in> S
enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s ## \<omega>) \<partial>T s) - (\<rho> s + (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s')) = (\<Sum>s'\<in>S. \<tau> s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s'))

goal (1 subgoal):
 1. (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s
[PROOF STEP]
by (simp add: LES_def const_def del: reward.simps)
[PROOF STATE]
proof (state)
this:
(\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>s\<in>S. (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * enn2real (\<integral>\<^sup>+ \<omega>. reward (Future \<Phi>) (s' ## \<omega>) \<partial>T s')) = const s

goal (1 subgoal):
 1. \<And>l s. \<lbrakk>\<forall>s\<in>S. (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * l s') = const s; s \<in> S\<rbrakk> \<Longrightarrow> (\<Sum>s'\<in>S. LES (S - Y \<union> svalid \<Phi>) s s' * l s') = const s
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
\<exists>l. gauss_jordan' (LES (S - Y \<union> svalid \<Phi>)) const = Some l

goal (9 subgoals):
 1. Sat sform.true \<noteq> None
 2. \<And>L. Sat (Label L) \<noteq> None
 3. \<And>F. Sat F \<noteq> None \<Longrightarrow> Sat (Neg F) \<noteq> None
 4. \<And>F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (And F1 F2) \<noteq> None
 5. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Prob rel r (X F)) \<noteq> None
 6. \<And>rel r k F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U k F1 F2)) \<noteq> None
 7. \<And>rel r k. Sat (Exp rel r (C\<^sup>\<le> k)) \<noteq> None
 8. \<And>rel r k. Sat (Exp rel r (I\<^sup>= k)) \<noteq> None
 9. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Exp rel r (Future F)) \<noteq> None
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l. gauss_jordan' (LES (S - Y \<union> svalid \<Phi>)) const = Some l
[PROOF STEP]
have P: "\<exists>l. ExpFuture (svalid \<Phi>) = Some l"
[PROOF STATE]
proof (prove)
using this:
\<exists>l. gauss_jordan' (LES (S - Y \<union> svalid \<Phi>)) const = Some l

goal (1 subgoal):
 1. \<exists>l. ExpFuture (svalid \<Phi>) = Some l
[PROOF STEP]
unfolding ExpFuture_def const_def N_def Y_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l. gauss_jordan' (LES (S - Prob1 (Prob0 S (svalid \<Phi>)) S (svalid \<Phi>) \<union> svalid \<Phi>)) (\<lambda>s. if s \<in> Prob1 (Prob0 S (svalid \<Phi>)) S (svalid \<Phi>) \<and> s \<notin> svalid \<Phi> then - \<rho> s - (\<Sum>s'\<in>S. \<tau> s s' * \<iota> s s') else 0) = Some l

goal (1 subgoal):
 1. \<exists>l. (let N = Prob0 S (svalid \<Phi>); Y = Prob1 N S (svalid \<Phi>) in gauss_jordan' (LES (S - Y \<union> svalid \<Phi>)) (\<lambda>i. if i \<in> Y \<and> i \<notin> svalid \<Phi> then - \<rho> i - (\<Sum>s'\<in>S. \<tau> i s' * \<iota> i s') else 0) \<bind> (\<lambda>sol. Some (\<lambda>s. if s \<in> Y then ennreal (sol s) else \<infinity>))) = Some l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>l. ExpFuture (svalid \<Phi>) = Some l

goal (9 subgoals):
 1. Sat sform.true \<noteq> None
 2. \<And>L. Sat (Label L) \<noteq> None
 3. \<And>F. Sat F \<noteq> None \<Longrightarrow> Sat (Neg F) \<noteq> None
 4. \<And>F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (And F1 F2) \<noteq> None
 5. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Prob rel r (X F)) \<noteq> None
 6. \<And>rel r k F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U k F1 F2)) \<noteq> None
 7. \<And>rel r k. Sat (Exp rel r (C\<^sup>\<le> k)) \<noteq> None
 8. \<And>rel r k. Sat (Exp rel r (I\<^sup>= k)) \<noteq> None
 9. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Exp rel r (Future F)) \<noteq> None
[PROOF STEP]
with F
[PROOF STATE]
proof (chain)
picking this:
Sat \<Phi> = Some (svalid \<Phi>)
\<exists>l. ExpFuture (svalid \<Phi>) = Some l
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Sat \<Phi> = Some (svalid \<Phi>)
\<exists>l. ExpFuture (svalid \<Phi>) = Some l

goal (1 subgoal):
 1. Sat (Exp rel r (Future \<Phi>)) \<noteq> None
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Sat (Exp rel r (Future \<Phi>)) \<noteq> None

goal (8 subgoals):
 1. Sat sform.true \<noteq> None
 2. \<And>L. Sat (Label L) \<noteq> None
 3. \<And>F. Sat F \<noteq> None \<Longrightarrow> Sat (Neg F) \<noteq> None
 4. \<And>F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (And F1 F2) \<noteq> None
 5. \<And>rel r F. Sat F \<noteq> None \<Longrightarrow> Sat (Prob rel r (X F)) \<noteq> None
 6. \<And>rel r k F1 F2. \<lbrakk>Sat F1 \<noteq> None; \<And>a. Sat F1 = Some a \<Longrightarrow> Sat F2 \<noteq> None\<rbrakk> \<Longrightarrow> Sat (Prob rel r (U k F1 F2)) \<noteq> None
 7. \<And>rel r k. Sat (Exp rel r (C\<^sup>\<le> k)) \<noteq> None
 8. \<And>rel r k. Sat (Exp rel r (I\<^sup>= k)) \<noteq> None
[PROOF STEP]
qed (force split: bind_split)+


[STATEMENT]
lemma weakTransitionI:
  fixes P  :: pi
  and   \<alpha>  :: freeRes
  and   P' :: pi

  shows "P \<Longrightarrow>\<alpha> \<prec> P' \<Longrightarrow> P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'"
  and   "P \<Longrightarrow>\<^sup>^\<tau> \<prec> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow>\<alpha> \<prec> P' \<Longrightarrow> P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P') &&& P \<Longrightarrow>\<^sup>^\<tau> \<prec> P
[PROOF STEP]
by(auto simp add: weakFreeTransition_def)


[STATEMENT]
lemma transitionCases[consumes 1, case_names Step Stay]:
  fixes P  :: pi
  and   \<alpha>  :: freeRes
  and   P' :: pi

  assumes "P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'"
  and     "P \<Longrightarrow>\<alpha> \<prec> P' \<Longrightarrow> F \<alpha> P'"
  and     "F (\<tau>) P"

  shows "F \<alpha> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<alpha> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'
P \<Longrightarrow>\<alpha> \<prec> P' \<Longrightarrow> F \<alpha> P'
F (\<tau>) P

goal (1 subgoal):
 1. F \<alpha> P'
[PROOF STEP]
by(auto simp add: weakFreeTransition_def)


[STATEMENT]
lemma singleActionChain:
  fixes P  :: pi
  and   \<alpha>  :: freeRes
  and   P' :: pi

  assumes "P \<longmapsto>\<alpha> \<prec> P'"

  shows "P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> \<alpha> \<prec> P'

goal (1 subgoal):
 1. P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'
[PROOF STEP]
by(auto dest: singleActionChain intro: weakTransitionI)


[STATEMENT]
lemma Tau:
  fixes P :: pi

  shows "\<tau>.(P) \<Longrightarrow>\<^sup>^ \<tau> \<prec>  P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>.P \<Longrightarrow>\<^sup>^\<tau> \<prec> P
[PROOF STEP]
by(auto intro: Weak_Early_Step_Semantics.Tau
   simp add: weakFreeTransition_def)


[STATEMENT]
lemma Input:
  fixes a :: name
  and   x :: name
  and   u :: name
  and   P :: pi

  shows "a<x>.P \<Longrightarrow>\<^sup>^ a<u> \<prec> P[x::=u]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a<x>.P \<Longrightarrow>\<^sup>^a<u> \<prec> P[x::=u]
[PROOF STEP]
by(auto intro: Weak_Early_Step_Semantics.Input
   simp add: weakFreeTransition_def)


[STATEMENT]
lemma Output:
  fixes a :: name
  and   b :: name
  and   P :: pi

  shows "a{b}.P \<Longrightarrow>\<^sup>^a[b] \<prec> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a{b}.P \<Longrightarrow>\<^sup>^a[b] \<prec> P
[PROOF STEP]
by(auto intro: Weak_Early_Step_Semantics.Output
   simp add: weakFreeTransition_def)


[STATEMENT]
lemma Par1F:
  fixes P  :: pi
  and   \<alpha>  :: freeRes
  and   P' :: pi
  and   Q  :: pi

  assumes "P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'"

  shows "P \<parallel> Q \<Longrightarrow>\<^sup>^\<alpha> \<prec> (P' \<parallel> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sup>^\<alpha> \<prec> P' \<parallel> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'

goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sup>^\<alpha> \<prec> P' \<parallel> Q
[PROOF STEP]
by(auto intro: Weak_Early_Step_Semantics.Par1F
   simp add: weakFreeTransition_def residual.inject)


[STATEMENT]
lemma Par2F:
  fixes Q :: pi
  and   \<alpha>  :: freeRes
  and   Q' :: pi
  and   P  :: pi

  assumes QTrans: "Q \<Longrightarrow>\<^sup>^\<alpha> \<prec> Q'"

  shows "P \<parallel> Q \<Longrightarrow>\<^sup>^\<alpha> \<prec> (P \<parallel> Q')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sup>^\<alpha> \<prec> P \<parallel> Q'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Q \<Longrightarrow>\<^sup>^\<alpha> \<prec> Q'

goal (1 subgoal):
 1. P \<parallel> Q \<Longrightarrow>\<^sup>^\<alpha> \<prec> P \<parallel> Q'
[PROOF STEP]
by(auto intro: Weak_Early_Step_Semantics.Par2F
   simp add: weakFreeTransition_def residual.inject)


[STATEMENT]
lemma ResF:
  fixes P  :: pi
  and   \<alpha>  :: freeRes
  and   P' :: pi
  and   x  :: name

  assumes "P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'"
  and     "x \<sharp> \<alpha>"

  shows "<\<nu>x>P \<Longrightarrow>\<^sup>^\<alpha> \<prec> <\<nu>x>P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<nu>x>P \<Longrightarrow>\<^sup>^\<alpha> \<prec> <\<nu>x>P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'
x \<sharp> \<alpha>

goal (1 subgoal):
 1. <\<nu>x>P \<Longrightarrow>\<^sup>^\<alpha> \<prec> <\<nu>x>P'
[PROOF STEP]
by(auto intro: Weak_Early_Step_Semantics.ResF
   simp add: weakFreeTransition_def residual.inject)


[STATEMENT]
lemma Bang:
  fixes P  :: pi
  and   Rs :: residual

  assumes "P \<parallel> !P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'"
  and     "P' \<noteq> P \<parallel> !P"

  shows "!P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. !P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<parallel> !P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'
P' \<noteq> P \<parallel> !P

goal (1 subgoal):
 1. !P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'
[PROOF STEP]
by(auto intro: Weak_Early_Step_Semantics.Bang
   simp add: weakFreeTransition_def residual.inject)


[STATEMENT]
lemma tauTransitionChain[simp]:
  fixes P  :: pi
  and   P' :: pi

  shows "P \<Longrightarrow>\<^sup>^\<tau> \<prec> P' = P \<Longrightarrow>\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sup>^\<tau> \<prec> P' = P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
apply(auto dest: Weak_Early_Step_Semantics.tauTransitionChain
      simp add: weakFreeTransition_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(P, P') \<in> {(P, P'). P \<longmapsto> \<tau> \<prec> P'}\<^sup>*; P \<noteq> P'\<rbrakk> \<Longrightarrow> P \<Longrightarrow>\<tau> \<prec> P'
[PROOF STEP]
by(erule rtrancl.cases) (auto intro: transitionI)


[STATEMENT]
lemma tauStepTransitionChain[simp]:
  fixes P  :: pi
  and   P' :: pi

  assumes "P \<noteq> P'"

  shows "P \<Longrightarrow>\<tau> \<prec> P' = P \<Longrightarrow>\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<tau> \<prec> P' = P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<noteq> P'

goal (1 subgoal):
 1. P \<Longrightarrow>\<tau> \<prec> P' = P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
apply(auto dest: Weak_Early_Step_Semantics.tauTransitionChain
      simp add: weakFreeTransition_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<noteq> P'; (P, P') \<in> {(P, P'). P \<longmapsto> \<tau> \<prec> P'}\<^sup>*\<rbrakk> \<Longrightarrow> P \<Longrightarrow>\<tau> \<prec> P'
[PROOF STEP]
by(erule rtrancl.cases) (auto intro: transitionI)


[STATEMENT]
lemma chainTransitionAppend:
  fixes P   :: pi
  and   P'  :: pi
  and   Rs  :: residual
  and   a   :: name
  and   x   :: name
  and   P'' :: pi
  and   \<alpha>   :: freeRes

  shows "P \<Longrightarrow>\<^sub>\<tau> P'' \<Longrightarrow> P'' \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'  \<Longrightarrow> P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'"
  and   "P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'' \<Longrightarrow> P'' \<Longrightarrow>\<^sub>\<tau> P' \<Longrightarrow> P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>P \<Longrightarrow>\<^sub>\<tau> P''; P'' \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'\<rbrakk> \<Longrightarrow> P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P') &&& (\<lbrakk>P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P''; P'' \<Longrightarrow>\<^sub>\<tau> P'\<rbrakk> \<Longrightarrow> P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P')
[PROOF STEP]
by(auto intro: chainTransitionAppend simp add: weakFreeTransition_def dest: Weak_Early_Step_Semantics.tauTransitionChain)


[STATEMENT]
lemma freshTauTransition:
  fixes P :: pi
  and   c :: name

  assumes "P \<Longrightarrow>\<^sup>^\<tau> \<prec> P'"
  and     "c \<sharp> P"

  shows "c \<sharp> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<sharp> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sup>^\<tau> \<prec> P'
c \<sharp> P

goal (1 subgoal):
 1. c \<sharp> P'
[PROOF STEP]
by(auto intro: Weak_Early_Step_Semantics.freshTauTransition
   simp add: weakFreeTransition_def residual.inject)


[STATEMENT]
lemma freshOutputTransition:
  fixes P  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi
  and   c  :: name

  assumes "P \<Longrightarrow>\<^sup>^a[b] \<prec> P'"
  and     "c \<sharp> P"

  shows "c \<sharp> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<sharp> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sup>^a[b] \<prec> P'
c \<sharp> P

goal (1 subgoal):
 1. c \<sharp> P'
[PROOF STEP]
by(auto intro: Weak_Early_Step_Semantics.freshOutputTransition
   simp add: weakFreeTransition_def residual.inject)


[STATEMENT]
lemma eqvtI:
  fixes P  :: pi
  and   \<alpha>  :: freeRes
  and   P' :: pi
  and   p  :: "name prm"

  assumes "P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'"

  shows "(p \<bullet> P) \<Longrightarrow>\<^sup>^(p \<bullet> \<alpha>) \<prec> (p \<bullet> P')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> P \<Longrightarrow>\<^sup>^p \<bullet> \<alpha> \<prec> p \<bullet> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sup>^\<alpha> \<prec> P'

goal (1 subgoal):
 1. p \<bullet> P \<Longrightarrow>\<^sup>^p \<bullet> \<alpha> \<prec> p \<bullet> P'
[PROOF STEP]
by(auto intro: Weak_Early_Step_Semantics.eqvtI
   simp add: weakFreeTransition_def residual.inject)


[STATEMENT]
lemma freshInputTransition:
  fixes P  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi
  and   c  :: name

  assumes "P \<Longrightarrow>\<^sup>^a<b> \<prec> P'"
  and     "c \<sharp> P"
  and     "c \<noteq> b"

  shows "c \<sharp> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<sharp> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sup>^a<b> \<prec> P'
c \<sharp> P
c \<noteq> b

goal (1 subgoal):
 1. c \<sharp> P'
[PROOF STEP]
by(auto intro: Weak_Early_Step_Semantics.freshInputTransition
   simp add: weakFreeTransition_def residual.inject)


[STATEMENT]
lemma sunflower_remove_element_lift:
  assumes S: "S \<subseteq> { A - {a} | A . A \<in> F \<and> a \<in> A}"
    and sf: "sunflower S"
  shows "\<exists> Sa. sunflower Sa \<and> Sa \<subseteq> F \<and> card Sa = card S \<and> Sa = insert a ` S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Sa. sunflower Sa \<and> Sa \<subseteq> F \<and> card Sa = card S \<and> Sa = insert a ` S
[PROOF STEP]
proof (intro exI[of _ "insert a ` S"] conjI refl)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sunflower (insert a ` S)
 2. insert a ` S \<subseteq> F
 3. card (insert a ` S) = card S
[PROOF STEP]
let ?Sa = "insert a ` S"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sunflower (insert a ` S)
 2. insert a ` S \<subseteq> F
 3. card (insert a ` S) = card S
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sunflower (insert a ` S)
 2. insert a ` S \<subseteq> F
 3. card (insert a ` S) = card S
[PROOF STEP]
fix B
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sunflower (insert a ` S)
 2. insert a ` S \<subseteq> F
 3. card (insert a ` S) = card S
[PROOF STEP]
assume "B \<in> ?Sa"
[PROOF STATE]
proof (state)
this:
B \<in> insert a ` S

goal (3 subgoals):
 1. sunflower (insert a ` S)
 2. insert a ` S \<subseteq> F
 3. card (insert a ` S) = card S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B \<in> insert a ` S
[PROOF STEP]
obtain C where C: "C \<in> S" and B: "B = insert a C"
[PROOF STATE]
proof (prove)
using this:
B \<in> insert a ` S

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>C \<in> S; B = insert a C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C \<in> S
B = insert a C

goal (3 subgoals):
 1. sunflower (insert a ` S)
 2. insert a ` S \<subseteq> F
 3. card (insert a ` S) = card S
[PROOF STEP]
from C S
[PROOF STATE]
proof (chain)
picking this:
C \<in> S
S \<subseteq> {A - {a} |A. A \<in> F \<and> a \<in> A}
[PROOF STEP]
obtain T where "T \<in> F" "a \<in> T" "C = T - {a}"
[PROOF STATE]
proof (prove)
using this:
C \<in> S
S \<subseteq> {A - {a} |A. A \<in> F \<and> a \<in> A}

goal (1 subgoal):
 1. (\<And>T. \<lbrakk>T \<in> F; a \<in> T; C = T - {a}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T \<in> F
a \<in> T
C = T - {a}

goal (3 subgoals):
 1. sunflower (insert a ` S)
 2. insert a ` S \<subseteq> F
 3. card (insert a ` S) = card S
[PROOF STEP]
with B
[PROOF STATE]
proof (chain)
picking this:
B = insert a C
T \<in> F
a \<in> T
C = T - {a}
[PROOF STEP]
have "B = T"
[PROOF STATE]
proof (prove)
using this:
B = insert a C
T \<in> F
a \<in> T
C = T - {a}

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

goal (3 subgoals):
 1. sunflower (insert a ` S)
 2. insert a ` S \<subseteq> F
 3. card (insert a ` S) = card S
[PROOF STEP]
with \<open>T \<in> F\<close>
[PROOF STATE]
proof (chain)
picking this:
T \<in> F
B = T
[PROOF STEP]
have "B \<in> F"
[PROOF STATE]
proof (prove)
using this:
T \<in> F
B = T

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

goal (3 subgoals):
 1. sunflower (insert a ` S)
 2. insert a ` S \<subseteq> F
 3. card (insert a ` S) = card S
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?B2 \<in> insert a ` S \<Longrightarrow> ?B2 \<in> F

goal (3 subgoals):
 1. sunflower (insert a ` S)
 2. insert a ` S \<subseteq> F
 3. card (insert a ` S) = card S
[PROOF STEP]
thus SaF: "?Sa \<subseteq> F"
[PROOF STATE]
proof (prove)
using this:
?B2 \<in> insert a ` S \<Longrightarrow> ?B2 \<in> F

goal (1 subgoal):
 1. insert a ` S \<subseteq> F
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert a ` S \<subseteq> F

goal (2 subgoals):
 1. sunflower (insert a ` S)
 2. card (insert a ` S) = card S
[PROOF STEP]
have inj: "inj_on (insert a) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (insert a) S
[PROOF STEP]
using S
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> {A - {a} |A. A \<in> F \<and> a \<in> A}

goal (1 subgoal):
 1. inj_on (insert a) S
[PROOF STEP]
by (intro inj_on_inverseI[of _ "\<lambda> B. B - {a}"], auto)
[PROOF STATE]
proof (state)
this:
inj_on (insert a) S

goal (2 subgoals):
 1. sunflower (insert a ` S)
 2. card (insert a ` S) = card S
[PROOF STEP]
thus "card ?Sa = card S"
[PROOF STATE]
proof (prove)
using this:
inj_on (insert a) S

goal (1 subgoal):
 1. card (insert a ` S) = card S
[PROOF STEP]
by (rule card_image)
[PROOF STATE]
proof (state)
this:
card (insert a ` S) = card S

goal (1 subgoal):
 1. sunflower (insert a ` S)
[PROOF STEP]
show "sunflower ?Sa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sunflower (insert a ` S)
[PROOF STEP]
unfolding sunflower_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (\<exists>A B. A \<in> insert a ` S \<and> B \<in> insert a ` S \<and> A \<noteq> B \<and> x \<in> A \<and> x \<in> B) \<longrightarrow> (\<forall>A. A \<in> insert a ` S \<longrightarrow> x \<in> A)
[PROOF STEP]
proof (intro allI, intro impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<exists>A B. A \<in> insert a ` S \<and> B \<in> insert a ` S \<and> A \<noteq> B \<and> x \<in> A \<and> x \<in> B \<Longrightarrow> \<forall>A. A \<in> insert a ` S \<longrightarrow> x \<in> A
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<exists>A B. A \<in> insert a ` S \<and> B \<in> insert a ` S \<and> A \<noteq> B \<and> x \<in> A \<and> x \<in> B \<Longrightarrow> \<forall>A. A \<in> insert a ` S \<longrightarrow> x \<in> A
[PROOF STEP]
assume "\<exists>C D. C \<in> ?Sa \<and> D \<in> ?Sa \<and> C \<noteq> D \<and> x \<in> C \<and> x \<in> D"
[PROOF STATE]
proof (state)
this:
\<exists>C D. C \<in> insert a ` S \<and> D \<in> insert a ` S \<and> C \<noteq> D \<and> x \<in> C \<and> x \<in> D

goal (1 subgoal):
 1. \<And>x. \<exists>A B. A \<in> insert a ` S \<and> B \<in> insert a ` S \<and> A \<noteq> B \<and> x \<in> A \<and> x \<in> B \<Longrightarrow> \<forall>A. A \<in> insert a ` S \<longrightarrow> x \<in> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>C D. C \<in> insert a ` S \<and> D \<in> insert a ` S \<and> C \<noteq> D \<and> x \<in> C \<and> x \<in> D
[PROOF STEP]
obtain C D where *: "C \<in> ?Sa" "D \<in> ?Sa" "C \<noteq> D" "x \<in> C" "x \<in> D"
[PROOF STATE]
proof (prove)
using this:
\<exists>C D. C \<in> insert a ` S \<and> D \<in> insert a ` S \<and> C \<noteq> D \<and> x \<in> C \<and> x \<in> D

goal (1 subgoal):
 1. (\<And>C D. \<lbrakk>C \<in> insert a ` S; D \<in> insert a ` S; C \<noteq> D; x \<in> C; x \<in> D\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C \<in> insert a ` S
D \<in> insert a ` S
C \<noteq> D
x \<in> C
x \<in> D

goal (1 subgoal):
 1. \<And>x. \<exists>A B. A \<in> insert a ` S \<and> B \<in> insert a ` S \<and> A \<noteq> B \<and> x \<in> A \<and> x \<in> B \<Longrightarrow> \<forall>A. A \<in> insert a ` S \<longrightarrow> x \<in> A
[PROOF STEP]
from *(1-2)
[PROOF STATE]
proof (chain)
picking this:
C \<in> insert a ` S
D \<in> insert a ` S
[PROOF STEP]
obtain C' D' where
      **: "C' \<in> S" "D' \<in> S" "C = insert a C'" "D = insert a D'"
[PROOF STATE]
proof (prove)
using this:
C \<in> insert a ` S
D \<in> insert a ` S

goal (1 subgoal):
 1. (\<And>C' D'. \<lbrakk>C' \<in> S; D' \<in> S; C = insert a C'; D = insert a D'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C' \<in> S
D' \<in> S
C = insert a C'
D = insert a D'

goal (1 subgoal):
 1. \<And>x. \<exists>A B. A \<in> insert a ` S \<and> B \<in> insert a ` S \<and> A \<noteq> B \<and> x \<in> A \<and> x \<in> B \<Longrightarrow> \<forall>A. A \<in> insert a ` S \<longrightarrow> x \<in> A
[PROOF STEP]
with \<open>C \<noteq> D\<close> inj
[PROOF STATE]
proof (chain)
picking this:
C \<noteq> D
inj_on (insert a) S
C' \<in> S
D' \<in> S
C = insert a C'
D = insert a D'
[PROOF STEP]
have CD': "C' \<noteq> D'"
[PROOF STATE]
proof (prove)
using this:
C \<noteq> D
inj_on (insert a) S
C' \<in> S
D' \<in> S
C = insert a C'
D = insert a D'

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

goal (1 subgoal):
 1. \<And>x. \<exists>A B. A \<in> insert a ` S \<and> B \<in> insert a ` S \<and> A \<noteq> B \<and> x \<in> A \<and> x \<in> B \<Longrightarrow> \<forall>A. A \<in> insert a ` S \<longrightarrow> x \<in> A
[PROOF STEP]
show "\<forall>E. E \<in> ?Sa \<longrightarrow> x \<in> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>E. E \<in> insert a ` S \<longrightarrow> x \<in> E
[PROOF STEP]
proof (cases "x = a")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = a \<Longrightarrow> \<forall>E. E \<in> insert a ` S \<longrightarrow> x \<in> E
 2. x \<noteq> a \<Longrightarrow> \<forall>E. E \<in> insert a ` S \<longrightarrow> x \<in> E
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> a

goal (2 subgoals):
 1. x = a \<Longrightarrow> \<forall>E. E \<in> insert a ` S \<longrightarrow> x \<in> E
 2. x \<noteq> a \<Longrightarrow> \<forall>E. E \<in> insert a ` S \<longrightarrow> x \<in> E
[PROOF STEP]
with * **
[PROOF STATE]
proof (chain)
picking this:
C \<in> insert a ` S
D \<in> insert a ` S
C \<noteq> D
x \<in> C
x \<in> D
C' \<in> S
D' \<in> S
C = insert a C'
D = insert a D'
x \<noteq> a
[PROOF STEP]
have "x \<in> C'" "x \<in> D'"
[PROOF STATE]
proof (prove)
using this:
C \<in> insert a ` S
D \<in> insert a ` S
C \<noteq> D
x \<in> C
x \<in> D
C' \<in> S
D' \<in> S
C = insert a C'
D = insert a D'
x \<noteq> a

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

goal (2 subgoals):
 1. x = a \<Longrightarrow> \<forall>E. E \<in> insert a ` S \<longrightarrow> x \<in> E
 2. x \<noteq> a \<Longrightarrow> \<forall>E. E \<in> insert a ` S \<longrightarrow> x \<in> E
[PROOF STEP]
with ** CD'
[PROOF STATE]
proof (chain)
picking this:
C' \<in> S
D' \<in> S
C = insert a C'
D = insert a D'
C' \<noteq> D'
x \<in> C'
x \<in> D'
[PROOF STEP]
have "\<exists>C D. C \<in> S \<and> D \<in> S \<and> C \<noteq> D \<and> x \<in> C \<and> x \<in> D"
[PROOF STATE]
proof (prove)
using this:
C' \<in> S
D' \<in> S
C = insert a C'
D = insert a D'
C' \<noteq> D'
x \<in> C'
x \<in> D'

goal (1 subgoal):
 1. \<exists>C D. C \<in> S \<and> D \<in> S \<and> C \<noteq> D \<and> x \<in> C \<and> x \<in> D
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>C D. C \<in> S \<and> D \<in> S \<and> C \<noteq> D \<and> x \<in> C \<and> x \<in> D

goal (2 subgoals):
 1. x = a \<Longrightarrow> \<forall>E. E \<in> insert a ` S \<longrightarrow> x \<in> E
 2. x \<noteq> a \<Longrightarrow> \<forall>E. E \<in> insert a ` S \<longrightarrow> x \<in> E
[PROOF STEP]
from sf[unfolded sunflower_def, rule_format, OF this]
[PROOF STATE]
proof (chain)
picking this:
?A \<in> S \<Longrightarrow> x \<in> ?A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?A \<in> S \<Longrightarrow> x \<in> ?A

goal (1 subgoal):
 1. \<forall>E. E \<in> insert a ` S \<longrightarrow> x \<in> E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>E. E \<in> insert a ` S \<longrightarrow> x \<in> E

goal (1 subgoal):
 1. x = a \<Longrightarrow> \<forall>E. E \<in> insert a ` S \<longrightarrow> x \<in> E
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<forall>E. E \<in> insert a ` S \<longrightarrow> x \<in> E

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sunflower (insert a ` S)

goal:
No subgoals!
[PROOF STEP]
qed