[STATEMENT]
lemma rept_ex:
  assumes "\<mu> \<in> \<K> (abss s)"
  shows "rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<mu> \<in> \<K> (abss s)

goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
case prems: (delay l R R')
[PROOF STATE]
proof (state)
this:
\<mu> = return_pmf (l, R')
abss s \<in> \<S>
abss s = (l, R)
R' \<in> Succ \<R> R
R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}

goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<mu> = return_pmf (l, R')
abss s \<in> \<S>
abss s = (l, R)
R' \<in> Succ \<R> R
R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
[PROOF STEP]
have "R \<in> \<R>"
[PROOF STATE]
proof (prove)
using this:
\<mu> = return_pmf (l, R')
abss s \<in> \<S>
abss s = (l, R)
R' \<in> Succ \<R> R
R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}

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

goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
from prems(2)
[PROOF STATE]
proof (chain)
picking this:
abss s \<in> \<S>
[PROOF STEP]
have "s \<in> S"
[PROOF STATE]
proof (prove)
using this:
abss s \<in> \<S>

goal (1 subgoal):
 1. s \<in> S
[PROOF STEP]
by (auto intro: \<S>_abss_S)
[PROOF STATE]
proof (state)
this:
s \<in> S

goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
from abss_\<S>D[OF prems(2)]
[PROOF STATE]
proof (chain)
picking this:
(\<And>l u. \<lbrakk>s = (l, u); u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain l' u' where "s = (l', u')" "u' \<in> [u']\<^sub>\<R>"
[PROOF STATE]
proof (prove)
using this:
(\<And>l u. \<lbrakk>s = (l, u); u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>l' u'. \<lbrakk>s = (l', u'); u' \<in> [u']\<^sub>\<R>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s = (l', u')
u' \<in> [u']\<^sub>\<R>

goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with prems(3)
[PROOF STATE]
proof (chain)
picking this:
abss s = (l, R)
s = (l', u')
u' \<in> [u']\<^sub>\<R>
[PROOF STEP]
have *: "s = (l, u') \<and> u' \<in> R"
[PROOF STATE]
proof (prove)
using this:
abss s = (l, R)
s = (l', u')
u' \<in> [u']\<^sub>\<R>

goal (1 subgoal):
 1. s = (l, u') \<and> u' \<in> R
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>abss (l', u') = (l, R); s = (l', u'); u' \<in> [u']\<^sub>\<R>\<rbrakk> \<Longrightarrow> l' = l \<and> u' \<in> R
[PROOF STEP]
apply (subst (asm) abss_S[OF \<S>_abss_S])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s = (l', u'); u' \<in> [u']\<^sub>\<R>\<rbrakk> \<Longrightarrow> abss (l', u') \<in> \<S>
 2. \<lbrakk>(l', [u']\<^sub>\<R>) = (l, R); s = (l', u'); u' \<in> [u']\<^sub>\<R>\<rbrakk> \<Longrightarrow> l' = l \<and> u' \<in> R
[PROOF STEP]
using prems(2)
[PROOF STATE]
proof (prove)
using this:
abss s \<in> \<S>

goal (2 subgoals):
 1. \<lbrakk>s = (l', u'); u' \<in> [u']\<^sub>\<R>\<rbrakk> \<Longrightarrow> abss (l', u') \<in> \<S>
 2. \<lbrakk>(l', [u']\<^sub>\<R>) = (l, R); s = (l', u'); u' \<in> [u']\<^sub>\<R>\<rbrakk> \<Longrightarrow> l' = l \<and> u' \<in> R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = (l, u') \<and> u' \<in> R

goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with prems(4) alpha_interp.set_of_regions_spec[OF \<open>R \<in> \<R>\<close>]
[PROOF STATE]
proof (chain)
picking this:
R' \<in> Succ \<R> R
\<lbrakk>?v \<in> R; ?R' \<in> Succ \<R> R\<rbrakk> \<Longrightarrow> \<exists>t\<ge>0. [?v \<oplus> t]\<^sub>\<R> = ?R'
s = (l, u') \<and> u' \<in> R
[PROOF STEP]
obtain t where R':
    "t \<ge> 0" "R' = [u' \<oplus> t]\<^sub>\<R>"
[PROOF STATE]
proof (prove)
using this:
R' \<in> Succ \<R> R
\<lbrakk>?v \<in> R; ?R' \<in> Succ \<R> R\<rbrakk> \<Longrightarrow> \<exists>t\<ge>0. [?v \<oplus> t]\<^sub>\<R> = ?R'
s = (l, u') \<and> u' \<in> R

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>0 \<le> t; R' = [u' \<oplus> t]\<^sub>\<R>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> t
R' = [u' \<oplus> t]\<^sub>\<R>

goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with \<open>s \<in> S\<close> *
[PROOF STATE]
proof (chain)
picking this:
s \<in> S
s = (l, u') \<and> u' \<in> R
0 \<le> t
R' = [u' \<oplus> t]\<^sub>\<R>
[PROOF STEP]
have "u' \<oplus> t \<in> R'" "u' \<oplus> t \<in> V" "l \<in> L"
[PROOF STATE]
proof (prove)
using this:
s \<in> S
s = (l, u') \<and> u' \<in> R
0 \<le> t
R' = [u' \<oplus> t]\<^sub>\<R>

goal (1 subgoal):
 1. u' \<oplus> t \<in> R' &&& u' \<oplus> t \<in> V &&& l \<in> L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u' \<oplus> t \<in> R'
u' \<oplus> t \<in> V
l \<in> L

goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with prems(5)
[PROOF STATE]
proof (chain)
picking this:
R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
u' \<oplus> t \<in> R'
u' \<oplus> t \<in> V
l \<in> L
[PROOF STEP]
have "(l, u' \<oplus> t) \<in> S"
[PROOF STATE]
proof (prove)
using this:
R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
u' \<oplus> t \<in> R'
u' \<oplus> t \<in> V
l \<in> L

goal (1 subgoal):
 1. (l, u' \<oplus> t) \<in> S
[PROOF STEP]
unfolding S_def V_def
[PROOF STATE]
proof (prove)
using this:
R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
u' \<oplus> t \<in> R'
u' \<oplus> t \<in> {v. \<forall>x\<in>\<X>. 0 \<le> v x}
l \<in> L

goal (1 subgoal):
 1. (l, u' \<oplus> t) \<in> {(l, u). l \<in> L \<and> (\<forall>x\<in>\<X>. 0 \<le> u x) \<and> u \<turnstile> PTA.inv_of A l}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(l, u' \<oplus> t) \<in> S

goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with \<open>R' = [u' \<oplus> t]\<^sub>\<R>\<close>
[PROOF STATE]
proof (chain)
picking this:
R' = [u' \<oplus> t]\<^sub>\<R>
(l, u' \<oplus> t) \<in> S
[PROOF STEP]
have **: "abss (l, u' \<oplus> t) = (l, R')"
[PROOF STATE]
proof (prove)
using this:
R' = [u' \<oplus> t]\<^sub>\<R>
(l, u' \<oplus> t) \<in> S

goal (1 subgoal):
 1. abss (l, u' \<oplus> t) = (l, R')
[PROOF STEP]
by (auto simp: abss_S)
[PROOF STATE]
proof (state)
this:
abss (l, u' \<oplus> t) = (l, R')

goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
let ?\<mu> = "return_pmf (l, u' \<oplus> t)"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
have "?\<mu> \<in> K s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return_pmf (l, u' \<oplus> t) \<in> K s
[PROOF STEP]
using * \<open>s \<in> S\<close> \<open>t \<ge> 0\<close> \<open>u' \<oplus> t \<in> R'\<close> prems
[PROOF STATE]
proof (prove)
using this:
s = (l, u') \<and> u' \<in> R
s \<in> S
0 \<le> t
u' \<oplus> t \<in> R'
\<mu> = return_pmf (l, R')
abss s \<in> \<S>
abss s = (l, R)
R' \<in> Succ \<R> R
R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}

goal (1 subgoal):
 1. return_pmf (l, u' \<oplus> t) \<in> K s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
return_pmf (l, u' \<oplus> t) \<in> K s

goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
return_pmf (l, u' \<oplus> t) \<in> K s

goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
have "abst ?\<mu> = \<mu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abst (return_pmf (l, u' \<oplus> t)) = \<mu>
[PROOF STEP]
by (simp add: ** abst_def prems(1))
[PROOF STATE]
proof (state)
this:
abst (return_pmf (l, u' \<oplus> t)) = \<mu>

goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
abst (return_pmf (l, u' \<oplus> t)) = \<mu>

goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
note default = calculation
[PROOF STATE]
proof (state)
this:
return_pmf (l, u' \<oplus> t) \<in> K s
abst (return_pmf (l, u' \<oplus> t)) = \<mu>

goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
have "R' \<in> \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R' \<in> \<R>
[PROOF STEP]
using prems(4)
[PROOF STATE]
proof (prove)
using this:
R' \<in> Succ \<R> R

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

goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
have R: "[u']\<^sub>\<R> = R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [u']\<^sub>\<R> = R
[PROOF STEP]
by (simp add: * \<open>R \<in> \<R>\<close> alpha_interp.region_unique_spec)
[PROOF STATE]
proof (state)
this:
[u']\<^sub>\<R> = R

goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
from \<open>R' \<in> \<R>\<close>
[PROOF STATE]
proof (chain)
picking this:
R' \<in> \<R>
[PROOF STEP]
obtain I r where R':
    "R' = region \<X> I r" "valid_region \<X> k I r"
[PROOF STATE]
proof (prove)
using this:
R' \<in> \<R>

goal (1 subgoal):
 1. (\<And>I r. \<lbrakk>R' = Regions.region \<X> I r; Regions.valid_region \<X> k I r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding \<R>_def
[PROOF STATE]
proof (prove)
using this:
R' \<in> {Regions.region \<X> I r |I r. Regions.valid_region \<X> k I r}

goal (1 subgoal):
 1. (\<And>I r. \<lbrakk>R' = Regions.region \<X> I r; Regions.valid_region \<X> k I r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
R' = Regions.region \<X> I r
Regions.valid_region \<X> k I r

goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
have "u' \<in> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u' \<in> V
[PROOF STEP]
using * prems \<R>_V
[PROOF STATE]
proof (prove)
using this:
s = (l, u') \<and> u' \<in> R
\<mu> = return_pmf (l, R')
abss s \<in> \<S>
abss s = (l, R)
R' \<in> Succ \<R> R
R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
\<Union> \<R> = V

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

goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
let ?\<mu>' = "return_pmf (l, u' \<oplus> 0.5)"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
have elapsed: "abst (return_pmf (l, u' \<oplus> t)) = \<mu>" "return_pmf (l, u' \<oplus> t) \<in> K s"
    if "u' \<oplus> t \<in> R'" "t \<ge> 0" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abst (return_pmf (l, u' \<oplus> t)) = \<mu> &&& return_pmf (l, u' \<oplus> t) \<in> K s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. abst (return_pmf (l, u' \<oplus> t)) = \<mu>
 2. return_pmf (l, u' \<oplus> t) \<in> K s
[PROOF STEP]
let ?u = "u' \<oplus> t"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. abst (return_pmf (l, u' \<oplus> t)) = \<mu>
 2. return_pmf (l, u' \<oplus> t) \<in> K s
[PROOF STEP]
let ?\<mu>' = "return_pmf (l, u' \<oplus> t)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. abst (return_pmf (l, u' \<oplus> t)) = \<mu>
 2. return_pmf (l, u' \<oplus> t) \<in> K s
[PROOF STEP]
from \<open>?u \<in> R'\<close> \<open>R' \<in> \<R>\<close> \<R>_V
[PROOF STATE]
proof (chain)
picking this:
u' \<oplus> t \<in> R'
R' \<in> \<R>
\<Union> \<R> = V
[PROOF STEP]
have "?u \<in> V"
[PROOF STATE]
proof (prove)
using this:
u' \<oplus> t \<in> R'
R' \<in> \<R>
\<Union> \<R> = V

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

goal (2 subgoals):
 1. abst (return_pmf (l, u' \<oplus> t)) = \<mu>
 2. return_pmf (l, u' \<oplus> t) \<in> K s
[PROOF STEP]
with \<open>?u \<in> R'\<close> \<open>R' \<in> \<R>\<close>
[PROOF STATE]
proof (chain)
picking this:
u' \<oplus> t \<in> R'
R' \<in> \<R>
u' \<oplus> t \<in> V
[PROOF STEP]
have "[?u]\<^sub>\<R> = R'"
[PROOF STATE]
proof (prove)
using this:
u' \<oplus> t \<in> R'
R' \<in> \<R>
u' \<oplus> t \<in> V

goal (1 subgoal):
 1. [u' \<oplus> t]\<^sub>\<R> = R'
[PROOF STEP]
using alpha_interp.region_unique_spec
[PROOF STATE]
proof (prove)
using this:
u' \<oplus> t \<in> R'
R' \<in> \<R>
u' \<oplus> t \<in> V
\<lbrakk>?u \<in> ?R; ?R \<in> \<R>\<rbrakk> \<Longrightarrow> [?u]\<^sub>\<R> = ?R

goal (1 subgoal):
 1. [u' \<oplus> t]\<^sub>\<R> = R'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[u' \<oplus> t]\<^sub>\<R> = R'

goal (2 subgoals):
 1. abst (return_pmf (l, u' \<oplus> t)) = \<mu>
 2. return_pmf (l, u' \<oplus> t) \<in> K s
[PROOF STEP]
with \<open>?u \<in> V\<close> \<open>?u \<in> R'\<close> \<open>l \<in> L\<close> prems(4,5)
[PROOF STATE]
proof (chain)
picking this:
u' \<oplus> t \<in> V
u' \<oplus> t \<in> R'
l \<in> L
R' \<in> Succ \<R> R
R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
[u' \<oplus> t]\<^sub>\<R> = R'
[PROOF STEP]
have "abss (l, ?u) = (l, R')"
[PROOF STATE]
proof (prove)
using this:
u' \<oplus> t \<in> V
u' \<oplus> t \<in> R'
l \<in> L
R' \<in> Succ \<R> R
R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
[u' \<oplus> t]\<^sub>\<R> = R'

goal (1 subgoal):
 1. abss (l, u' \<oplus> t) = (l, R')
[PROOF STEP]
by (subst abss_S) auto
[PROOF STATE]
proof (state)
this:
abss (l, u' \<oplus> t) = (l, R')

goal (2 subgoals):
 1. abst (return_pmf (l, u' \<oplus> t)) = \<mu>
 2. return_pmf (l, u' \<oplus> t) \<in> K s
[PROOF STEP]
with prems(1)
[PROOF STATE]
proof (chain)
picking this:
\<mu> = return_pmf (l, R')
abss (l, u' \<oplus> t) = (l, R')
[PROOF STEP]
have "abst ?\<mu>' = \<mu>"
[PROOF STATE]
proof (prove)
using this:
\<mu> = return_pmf (l, R')
abss (l, u' \<oplus> t) = (l, R')

goal (1 subgoal):
 1. abst (return_pmf (l, u' \<oplus> t)) = \<mu>
[PROOF STEP]
by (auto simp: abst_def)
[PROOF STATE]
proof (state)
this:
abst (return_pmf (l, u' \<oplus> t)) = \<mu>

goal (2 subgoals):
 1. abst (return_pmf (l, u' \<oplus> t)) = \<mu>
 2. return_pmf (l, u' \<oplus> t) \<in> K s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
abst (return_pmf (l, u' \<oplus> t)) = \<mu>

goal (2 subgoals):
 1. abst (return_pmf (l, u' \<oplus> t)) = \<mu>
 2. return_pmf (l, u' \<oplus> t) \<in> K s
[PROOF STEP]
from * \<open>?u \<in> R'\<close> \<open>s \<in> S\<close> prems \<open>t \<ge> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
s = (l, u') \<and> u' \<in> R
u' \<oplus> t \<in> R'
s \<in> S
\<mu> = return_pmf (l, R')
abss s \<in> \<S>
abss s = (l, R)
R' \<in> Succ \<R> R
R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
0 \<le> t
[PROOF STEP]
have "?\<mu>' \<in> K s"
[PROOF STATE]
proof (prove)
using this:
s = (l, u') \<and> u' \<in> R
u' \<oplus> t \<in> R'
s \<in> S
\<mu> = return_pmf (l, R')
abss s \<in> \<S>
abss s = (l, R)
R' \<in> Succ \<R> R
R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
0 \<le> t

goal (1 subgoal):
 1. return_pmf (l, u' \<oplus> t) \<in> K s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
return_pmf (l, u' \<oplus> t) \<in> K s

goal (2 subgoals):
 1. abst (return_pmf (l, u' \<oplus> t)) = \<mu>
 2. return_pmf (l, u' \<oplus> t) \<in> K s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
abst (return_pmf (l, u' \<oplus> t)) = \<mu>
return_pmf (l, u' \<oplus> t) \<in> K s
[PROOF STEP]
show "abst ?\<mu>' = \<mu>" "?\<mu>' \<in> K s"
[PROOF STATE]
proof (prove)
using this:
abst (return_pmf (l, u' \<oplus> t)) = \<mu>
return_pmf (l, u' \<oplus> t) \<in> K s

goal (1 subgoal):
 1. abst (return_pmf (l, u' \<oplus> t)) = \<mu> &&& return_pmf (l, u' \<oplus> t) \<in> K s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
abst (return_pmf (l, u' \<oplus> t)) = \<mu>
return_pmf (l, u' \<oplus> t) \<in> K s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>u' \<oplus> ?t5 \<in> R'; 0 \<le> ?t5\<rbrakk> \<Longrightarrow> abst (return_pmf (l, u' \<oplus> ?t5)) = \<mu>
\<lbrakk>u' \<oplus> ?t5 \<in> R'; 0 \<le> ?t5\<rbrakk> \<Longrightarrow> return_pmf (l, u' \<oplus> ?t5) \<in> K s

goal (3 subgoals):
 1. \<And>l R R'. \<lbrakk>\<mu> = return_pmf (l, R'); abss s \<in> \<S>; abss s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 3. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
proof (cases "R = R'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. R = R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. R \<noteq> R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
case T: True
[PROOF STATE]
proof (state)
this:
R = R'

goal (2 subgoals):
 1. R = R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. R \<noteq> R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
proof (cases "\<forall> c \<in> \<X>. u' c > k c")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>c\<in>\<X>. real (k c) < u' c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<not> (\<forall>c\<in>\<X>. real (k c) < u' c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>\<X>. real (k c) < u' c

goal (2 subgoals):
 1. \<forall>c\<in>\<X>. real (k c) < u' c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<not> (\<forall>c\<in>\<X>. real (k c) < u' c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with T * R prems(1,4) \<open>s \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
R = R'
s = (l, u') \<and> u' \<in> R
[u']\<^sub>\<R> = R
\<mu> = return_pmf (l, R')
R' \<in> Succ \<R> R
s \<in> S
\<forall>c\<in>\<X>. real (k c) < u' c
[PROOF STEP]
have
        "rept s \<mu> = return_pmf (l, u' \<oplus> 0.5)" (is "_ = ?\<mu>")
[PROOF STATE]
proof (prove)
using this:
R = R'
s = (l, u') \<and> u' \<in> R
[u']\<^sub>\<R> = R
\<mu> = return_pmf (l, R')
R' \<in> Succ \<R> R
s \<in> S
\<forall>c\<in>\<X>. real (k c) < u' c

goal (1 subgoal):
 1. rept s \<mu> = return_pmf (l, u' \<oplus> 5 / 10)
[PROOF STEP]
unfolding rept_def
[PROOF STATE]
proof (prove)
using this:
R = R'
s = (l, u') \<and> u' \<in> R
[u']\<^sub>\<R> = R
\<mu> = return_pmf (l, R')
R' \<in> Succ \<R> R
s \<in> S
\<forall>c\<in>\<X>. real (k c) < u' c

goal (1 subgoal):
 1. (let (l, u) = s in if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> [u]\<^sub>\<R> = R' \<and> (\<forall>c\<in>\<X>. real (k c) < u c) then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u) else SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) = return_pmf (l, u' \<oplus> 5 / 10)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rept s \<mu> = return_pmf (l, u' \<oplus> 5 / 10)

goal (2 subgoals):
 1. \<forall>c\<in>\<X>. real (k c) < u' c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<not> (\<forall>c\<in>\<X>. real (k c) < u' c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
from upper_right_closed[OF True] * \<open>R' \<in> \<R>\<close> T
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>u' \<in> ?R; ?R \<in> \<R>; 0 \<le> ?t\<rbrakk> \<Longrightarrow> u' \<oplus> ?t \<in> ?R
s = (l, u') \<and> u' \<in> R
R' \<in> \<R>
R = R'
[PROOF STEP]
have "u' \<oplus> 0.5 \<in> R'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>u' \<in> ?R; ?R \<in> \<R>; 0 \<le> ?t\<rbrakk> \<Longrightarrow> u' \<oplus> ?t \<in> ?R
s = (l, u') \<and> u' \<in> R
R' \<in> \<R>
R = R'

goal (1 subgoal):
 1. u' \<oplus> 5 / 10 \<in> R'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u' \<oplus> 5 / 10 \<in> R'

goal (2 subgoals):
 1. \<forall>c\<in>\<X>. real (k c) < u' c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<not> (\<forall>c\<in>\<X>. real (k c) < u' c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with elapsed \<open>rept _ _ = _\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>u' \<oplus> ?t5 \<in> R'; 0 \<le> ?t5\<rbrakk> \<Longrightarrow> abst (return_pmf (l, u' \<oplus> ?t5)) = \<mu>
\<lbrakk>u' \<oplus> ?t5 \<in> R'; 0 \<le> ?t5\<rbrakk> \<Longrightarrow> return_pmf (l, u' \<oplus> ?t5) \<in> K s
rept s \<mu> = return_pmf (l, u' \<oplus> 5 / 10)
u' \<oplus> 5 / 10 \<in> R'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>u' \<oplus> ?t5 \<in> R'; 0 \<le> ?t5\<rbrakk> \<Longrightarrow> abst (return_pmf (l, u' \<oplus> ?t5)) = \<mu>
\<lbrakk>u' \<oplus> ?t5 \<in> R'; 0 \<le> ?t5\<rbrakk> \<Longrightarrow> return_pmf (l, u' \<oplus> ?t5) \<in> K s
rept s \<mu> = return_pmf (l, u' \<oplus> 5 / 10)
u' \<oplus> 5 / 10 \<in> R'

goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>

goal (1 subgoal):
 1. \<not> (\<forall>c\<in>\<X>. real (k c) < u' c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>c\<in>\<X>. real (k c) < u' c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>c\<in>\<X>. real (k c) < u' c)

goal (1 subgoal):
 1. \<not> (\<forall>c\<in>\<X>. real (k c) < u' c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with T * R prems(1)
[PROOF STATE]
proof (chain)
picking this:
R = R'
s = (l, u') \<and> u' \<in> R
[u']\<^sub>\<R> = R
\<mu> = return_pmf (l, R')
\<not> (\<forall>c\<in>\<X>. real (k c) < u' c)
[PROOF STEP]
have
        "rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)"
[PROOF STATE]
proof (prove)
using this:
R = R'
s = (l, u') \<and> u' \<in> R
[u']\<^sub>\<R> = R
\<mu> = return_pmf (l, R')
\<not> (\<forall>c\<in>\<X>. real (k c) < u' c)

goal (1 subgoal):
 1. rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
unfolding rept_def
[PROOF STATE]
proof (prove)
using this:
R = R'
s = (l, u') \<and> u' \<in> R
[u']\<^sub>\<R> = R
\<mu> = return_pmf (l, R')
\<not> (\<forall>c\<in>\<X>. real (k c) < u' c)

goal (1 subgoal):
 1. (let (l, u) = s in if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> [u]\<^sub>\<R> = R' \<and> (\<forall>c\<in>\<X>. real (k c) < u c) then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u) else SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)

goal (1 subgoal):
 1. \<not> (\<forall>c\<in>\<X>. real (k c) < u' c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with default
[PROOF STATE]
proof (chain)
picking this:
return_pmf (l, u' \<oplus> t) \<in> K s
abst (return_pmf (l, u' \<oplus> t)) = \<mu>
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
return_pmf (l, u' \<oplus> t) \<in> K s
abst (return_pmf (l, u' \<oplus> t)) = \<mu>
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)

goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
by simp (rule someI; auto)
[PROOF STATE]
proof (state)
this:
rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>

goal (1 subgoal):
 1. R \<noteq> R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. R \<noteq> R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
case F: False
[PROOF STATE]
proof (state)
this:
R \<noteq> R'

goal (1 subgoal):
 1. R \<noteq> R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
proof (cases "\<forall> u \<in> R'. \<forall> c \<in> \<X>. \<nexists> d. d \<le> k c \<and> u c = real d")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<not> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d))

goal (2 subgoals):
 1. \<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<not> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with F * R prems(1)
[PROOF STATE]
proof (chain)
picking this:
R \<noteq> R'
s = (l, u') \<and> u' \<in> R
[u']\<^sub>\<R> = R
\<mu> = return_pmf (l, R')
\<not> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d))
[PROOF STEP]
have
        "rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)"
[PROOF STATE]
proof (prove)
using this:
R \<noteq> R'
s = (l, u') \<and> u' \<in> R
[u']\<^sub>\<R> = R
\<mu> = return_pmf (l, R')
\<not> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d))

goal (1 subgoal):
 1. rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
unfolding rept_def
[PROOF STATE]
proof (prove)
using this:
R \<noteq> R'
s = (l, u') \<and> u' \<in> R
[u']\<^sub>\<R> = R
\<mu> = return_pmf (l, R')
\<not> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d))

goal (1 subgoal):
 1. (let (l, u) = s in if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> [u]\<^sub>\<R> = R' \<and> (\<forall>c\<in>\<X>. real (k c) < u c) then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u) else SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)

goal (2 subgoals):
 1. \<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<not> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with default
[PROOF STATE]
proof (chain)
picking this:
return_pmf (l, u' \<oplus> t) \<in> K s
abst (return_pmf (l, u' \<oplus> t)) = \<mu>
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
return_pmf (l, u' \<oplus> t) \<in> K s
abst (return_pmf (l, u' \<oplus> t)) = \<mu>
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)

goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
by simp (rule someI; auto)
[PROOF STATE]
proof (state)
this:
rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>

goal (1 subgoal):
 1. \<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)

goal (1 subgoal):
 1. \<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
from True F * R prems(1,4) \<open>s \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)
R \<noteq> R'
s = (l, u') \<and> u' \<in> R
[u']\<^sub>\<R> = R
\<mu> = return_pmf (l, R')
R' \<in> Succ \<R> R
s \<in> S
[PROOF STEP]
have
        "rept s \<mu> = return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u')"
        (is "_ = return_pmf (l, delayedR ?R u')")
[PROOF STATE]
proof (prove)
using this:
\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)
R \<noteq> R'
s = (l, u') \<and> u' \<in> R
[u']\<^sub>\<R> = R
\<mu> = return_pmf (l, R')
R' \<in> Succ \<R> R
s \<in> S

goal (1 subgoal):
 1. rept s \<mu> = return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u')
[PROOF STEP]
unfolding rept_def
[PROOF STATE]
proof (prove)
using this:
\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)
R \<noteq> R'
s = (l, u') \<and> u' \<in> R
[u']\<^sub>\<R> = R
\<mu> = return_pmf (l, R')
R' \<in> Succ \<R> R
s \<in> S

goal (1 subgoal):
 1. (let (l, u) = s in if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> [u]\<^sub>\<R> = R' \<and> (\<forall>c\<in>\<X>. real (k c) < u c) then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u) else SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) = return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rept s \<mu> = return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u')

goal (1 subgoal):
 1. \<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
let ?u = "delayedR ?R u'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
from prems(1)
[PROOF STATE]
proof (chain)
picking this:
\<mu> = return_pmf (l, R')
[PROOF STEP]
have "\<mu> = return_pmf (l, ?R)"
[PROOF STATE]
proof (prove)
using this:
\<mu> = return_pmf (l, R')

goal (1 subgoal):
 1. \<mu> = return_pmf (l, SOME R'. \<mu> = return_pmf (l, R'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<mu> = return_pmf (l, SOME R'. \<mu> = return_pmf (l, R'))

goal (1 subgoal):
 1. \<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with prems(1)
[PROOF STATE]
proof (chain)
picking this:
\<mu> = return_pmf (l, R')
\<mu> = return_pmf (l, SOME R'. \<mu> = return_pmf (l, R'))
[PROOF STEP]
have "?R = R'"
[PROOF STATE]
proof (prove)
using this:
\<mu> = return_pmf (l, R')
\<mu> = return_pmf (l, SOME R'. \<mu> = return_pmf (l, R'))

goal (1 subgoal):
 1. (SOME R'. \<mu> = return_pmf (l, R')) = R'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(SOME R'. \<mu> = return_pmf (l, R')) = R'

goal (1 subgoal):
 1. \<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(SOME R'. \<mu> = return_pmf (l, R')) = R'

goal (1 subgoal):
 1. \<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
from R' True \<open>_ \<in> R'\<close>
[PROOF STATE]
proof (chain)
picking this:
R' = Regions.region \<X> I r
Regions.valid_region \<X> k I r
\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)
u' \<oplus> t \<in> R'
[PROOF STEP]
have "\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)"
[PROOF STATE]
proof (prove)
using this:
R' = Regions.region \<X> I r
Regions.valid_region \<X> k I r
\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)
u' \<oplus> t \<in> R'

goal (1 subgoal):
 1. \<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)

goal (1 subgoal):
 1. \<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)

goal (1 subgoal):
 1. \<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
note delayedR_correct[of u' R I r] * \<open>R \<in> \<R>\<close> R' True \<open>R' \<in> Succ \<R> R\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>u' \<in> R; R \<in> \<R>; Regions.valid_region \<X> k I r; \<forall>c\<in>\<X>. \<not> Regions.isConst (I c); Regions.region \<X> I r \<in> Succ \<R> R\<rbrakk> \<Longrightarrow> delayedR (Regions.region \<X> I r) u' \<in> Regions.region \<X> I r
\<lbrakk>u' \<in> R; R \<in> \<R>; Regions.valid_region \<X> k I r; \<forall>c\<in>\<X>. \<not> Regions.isConst (I c); Regions.region \<X> I r \<in> Succ \<R> R\<rbrakk> \<Longrightarrow> \<exists>t\<ge>0. delayedR (Regions.region \<X> I r) u' = u' \<oplus> t \<and> (1 - Max ({frac (u' c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
s = (l, u') \<and> u' \<in> R
R \<in> \<R>
R' = Regions.region \<X> I r
Regions.valid_region \<X> k I r
\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)
R' \<in> Succ \<R> R

goal (1 subgoal):
 1. \<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(SOME R'. \<mu> = return_pmf (l, R')) = R'
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
\<lbrakk>u' \<in> R; R \<in> \<R>; Regions.valid_region \<X> k I r; \<forall>c\<in>\<X>. \<not> Regions.isConst (I c); Regions.region \<X> I r \<in> Succ \<R> R\<rbrakk> \<Longrightarrow> delayedR (Regions.region \<X> I r) u' \<in> Regions.region \<X> I r
\<lbrakk>u' \<in> R; R \<in> \<R>; Regions.valid_region \<X> k I r; \<forall>c\<in>\<X>. \<not> Regions.isConst (I c); Regions.region \<X> I r \<in> Succ \<R> R\<rbrakk> \<Longrightarrow> \<exists>t\<ge>0. delayedR (Regions.region \<X> I r) u' = u' \<oplus> t \<and> (1 - Max ({frac (u' c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
s = (l, u') \<and> u' \<in> R
R \<in> \<R>
R' = Regions.region \<X> I r
Regions.valid_region \<X> k I r
\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)
R' \<in> Succ \<R> R
[PROOF STEP]
obtain t where **: "delayedR R' u' \<in> R'" "t \<ge> 0" "delayedR R' u' = u' \<oplus> t"
[PROOF STATE]
proof (prove)
using this:
(SOME R'. \<mu> = return_pmf (l, R')) = R'
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
\<lbrakk>u' \<in> R; R \<in> \<R>; Regions.valid_region \<X> k I r; \<forall>c\<in>\<X>. \<not> Regions.isConst (I c); Regions.region \<X> I r \<in> Succ \<R> R\<rbrakk> \<Longrightarrow> delayedR (Regions.region \<X> I r) u' \<in> Regions.region \<X> I r
\<lbrakk>u' \<in> R; R \<in> \<R>; Regions.valid_region \<X> k I r; \<forall>c\<in>\<X>. \<not> Regions.isConst (I c); Regions.region \<X> I r \<in> Succ \<R> R\<rbrakk> \<Longrightarrow> \<exists>t\<ge>0. delayedR (Regions.region \<X> I r) u' = u' \<oplus> t \<and> (1 - Max ({frac (u' c) |c. c \<in> \<X> \<and> Regions.isIntv (I c)} \<union> {0})) / 2 \<le> t
s = (l, u') \<and> u' \<in> R
R \<in> \<R>
R' = Regions.region \<X> I r
Regions.valid_region \<X> k I r
\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)
R' \<in> Succ \<R> R

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>delayedR R' u' \<in> R'; 0 \<le> t; delayedR R' u' = u' \<oplus> t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
delayedR R' u' \<in> R'
0 \<le> t
delayedR R' u' = u' \<oplus> t

goal (1 subgoal):
 1. \<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
delayedR R' u' \<in> R'
0 \<le> t
delayedR R' u' = u' \<oplus> t

goal (1 subgoal):
 1. \<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
from \<open>?R =_ \<close>\<open>rept _ _ = _\<close>
[PROOF STATE]
proof (chain)
picking this:
(SOME R'. \<mu> = return_pmf (l, R')) = R'
rept s \<mu> = return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u')
[PROOF STEP]
have "rept s \<mu> = return_pmf (l, delayedR R' u')"
[PROOF STATE]
proof (prove)
using this:
(SOME R'. \<mu> = return_pmf (l, R')) = R'
rept s \<mu> = return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u')

goal (1 subgoal):
 1. rept s \<mu> = return_pmf (l, delayedR R' u')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rept s \<mu> = return_pmf (l, delayedR R' u')

goal (1 subgoal):
 1. \<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
delayedR R' u' \<in> R'
0 \<le> t
delayedR R' u' = u' \<oplus> t
rept s \<mu> = return_pmf (l, delayedR R' u')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
delayedR R' u' \<in> R'
0 \<le> t
delayedR R' u' = u' \<oplus> t
rept s \<mu> = return_pmf (l, delayedR R' u')

goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
using elapsed
[PROOF STATE]
proof (prove)
using this:
delayedR R' u' \<in> R'
0 \<le> t
delayedR R' u' = u' \<oplus> t
rept s \<mu> = return_pmf (l, delayedR R' u')
\<lbrakk>u' \<oplus> ?t5 \<in> R'; 0 \<le> ?t5\<rbrakk> \<Longrightarrow> abst (return_pmf (l, u' \<oplus> ?t5)) = \<mu>
\<lbrakk>u' \<oplus> ?t5 \<in> R'; 0 \<le> ?t5\<rbrakk> \<Longrightarrow> return_pmf (l, u' \<oplus> ?t5) \<in> K s

goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>

goal (2 subgoals):
 1. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
case prems: (action l R \<tau> \<mu>')
[PROOF STATE]
proof (state)
this:
\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'
abss s \<in> \<S>
abss s = (l, R)
(l, \<tau>, \<mu>') \<in> PTA.trans_of A
R \<subseteq> {v. v \<turnstile> \<tau>}

goal (2 subgoals):
 1. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
from abss_\<S>D'[OF prems(2,3)]
[PROOF STATE]
proof (chain)
picking this:
(\<And>u. \<lbrakk>s = (l, u); u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>; R = [u]\<^sub>\<R>\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain u where u:
    "s = (l, u)" "u \<in> [u]\<^sub>\<R>" "[u]\<^sub>\<R> \<in> \<R>" "R = [u]\<^sub>\<R>"
[PROOF STATE]
proof (prove)
using this:
(\<And>u. \<lbrakk>s = (l, u); u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>; R = [u]\<^sub>\<R>\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>s = (l, u); u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>; R = [u]\<^sub>\<R>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = (l, u)
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
R = [u]\<^sub>\<R>

goal (2 subgoals):
 1. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with \<open>_ \<in> \<S>\<close>
[PROOF STATE]
proof (chain)
picking this:
abss s \<in> \<S>
s = (l, u)
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
R = [u]\<^sub>\<R>
[PROOF STEP]
have "(l, u) \<in> S"
[PROOF STATE]
proof (prove)
using this:
abss s \<in> \<S>
s = (l, u)
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
R = [u]\<^sub>\<R>

goal (1 subgoal):
 1. (l, u) \<in> S
[PROOF STEP]
by (auto intro: \<S>_abss_S)
[PROOF STATE]
proof (state)
this:
(l, u) \<in> S

goal (2 subgoals):
 1. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
let ?\<mu> = "map_pmf (\<lambda>(X, l). (l, [X:=0]u)) \<mu>'"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
from u prems
[PROOF STATE]
proof (chain)
picking this:
s = (l, u)
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
R = [u]\<^sub>\<R>
\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'
abss s \<in> \<S>
abss s = (l, R)
(l, \<tau>, \<mu>') \<in> PTA.trans_of A
R \<subseteq> {v. v \<turnstile> \<tau>}
[PROOF STEP]
have "?\<mu> \<in> K s"
[PROOF STATE]
proof (prove)
using this:
s = (l, u)
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
R = [u]\<^sub>\<R>
\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'
abss s \<in> \<S>
abss s = (l, R)
(l, \<tau>, \<mu>') \<in> PTA.trans_of A
R \<subseteq> {v. v \<turnstile> \<tau>}

goal (1 subgoal):
 1. map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>' \<in> K s
[PROOF STEP]
by (fastforce intro: \<S>_abss_S)
[PROOF STATE]
proof (state)
this:
map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>' \<in> K s

goal (2 subgoals):
 1. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>' \<in> K s

goal (2 subgoals):
 1. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
have "abst ?\<mu> = \<mu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abst (map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>') = \<mu>
[PROOF STEP]
unfolding prems(1) abst_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf abss (map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>') = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'
[PROOF STEP]
proof (subst map_pmf_comp, rule pmf.map_cong, safe, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set_pmf \<mu>' \<Longrightarrow> abss (b, [(SOME r. set r = a)\<rightarrow>0]u) = (b, [a::=0]R)
[PROOF STEP]
case A: (1 X l')
[PROOF STATE]
proof (state)
this:
(X, l') \<in> set_pmf \<mu>'

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set_pmf \<mu>' \<Longrightarrow> abss (b, [(SOME r. set r = a)\<rightarrow>0]u) = (b, [a::=0]R)
[PROOF STEP]
from u
[PROOF STATE]
proof (chain)
picking this:
s = (l, u)
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
R = [u]\<^sub>\<R>
[PROOF STEP]
have "u \<in> V"
[PROOF STATE]
proof (prove)
using this:
s = (l, u)
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
R = [u]\<^sub>\<R>

goal (1 subgoal):
 1. u \<in> V
[PROOF STEP]
using \<R>_V
[PROOF STATE]
proof (prove)
using this:
s = (l, u)
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
R = [u]\<^sub>\<R>
\<Union> \<R> = V

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

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set_pmf \<mu>' \<Longrightarrow> abss (b, [(SOME r. set r = a)\<rightarrow>0]u) = (b, [a::=0]R)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in> V
[PROOF STEP]
have "[X:=0]u \<in> V"
[PROOF STATE]
proof (prove)
using this:
u \<in> V

goal (1 subgoal):
 1. [(SOME r. set r = X)\<rightarrow>0]u \<in> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[(SOME r. set r = X)\<rightarrow>0]u \<in> V

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set_pmf \<mu>' \<Longrightarrow> abss (b, [(SOME r. set r = a)\<rightarrow>0]u) = (b, [a::=0]R)
[PROOF STEP]
from prems(1) A
[PROOF STATE]
proof (chain)
picking this:
\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'
(X, l') \<in> set_pmf \<mu>'
[PROOF STEP]
have "(l', region_set' R (SOME r. set r = X) 0) \<in> \<mu>"
[PROOF STATE]
proof (prove)
using this:
\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'
(X, l') \<in> set_pmf \<mu>'

goal (1 subgoal):
 1. (l', [X::=0]R) \<in> set_pmf \<mu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(l', [X::=0]R) \<in> set_pmf \<mu>

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set_pmf \<mu>' \<Longrightarrow> abss (b, [(SOME r. set r = a)\<rightarrow>0]u) = (b, [a::=0]R)
[PROOF STEP]
from A prems R_G.K_closed \<open>\<mu> \<in> _\<close>
[PROOF STATE]
proof (chain)
picking this:
(X, l') \<in> set_pmf \<mu>'
\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'
abss s \<in> \<S>
abss s = (l, R)
(l, \<tau>, \<mu>') \<in> PTA.trans_of A
R \<subseteq> {v. v \<turnstile> \<tau>}
?s \<in> \<S> \<Longrightarrow> \<Union> (set_pmf ` \<K> ?s) \<subseteq> \<S>
\<mu> \<in> \<K> (abss s)
[PROOF STEP]
have
        "l' \<in> L" "region_set' R (SOME r. set r = X) 0 \<subseteq> \<lbrace>inv_of A l'\<rbrace>"
[PROOF STATE]
proof (prove)
using this:
(X, l') \<in> set_pmf \<mu>'
\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'
abss s \<in> \<S>
abss s = (l, R)
(l, \<tau>, \<mu>') \<in> PTA.trans_of A
R \<subseteq> {v. v \<turnstile> \<tau>}
?s \<in> \<S> \<Longrightarrow> \<Union> (set_pmf ` \<K> ?s) \<subseteq> \<S>
\<mu> \<in> \<K> (abss s)

goal (1 subgoal):
 1. l' \<in> L &&& [X::=0]R \<subseteq> {v. v \<turnstile> PTA.inv_of A l'}
[PROOF STEP]
by (force dest: \<S>_L \<S>_inv)+
[PROOF STATE]
proof (state)
this:
l' \<in> L
[X::=0]R \<subseteq> {v. v \<turnstile> PTA.inv_of A l'}

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set_pmf \<mu>' \<Longrightarrow> abss (b, [(SOME r. set r = a)\<rightarrow>0]u) = (b, [a::=0]R)
[PROOF STEP]
with u
[PROOF STATE]
proof (chain)
picking this:
s = (l, u)
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
R = [u]\<^sub>\<R>
l' \<in> L
[X::=0]R \<subseteq> {v. v \<turnstile> PTA.inv_of A l'}
[PROOF STEP]
have "[X:=0]u \<turnstile> inv_of A l'"
[PROOF STATE]
proof (prove)
using this:
s = (l, u)
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
R = [u]\<^sub>\<R>
l' \<in> L
[X::=0]R \<subseteq> {v. v \<turnstile> PTA.inv_of A l'}

goal (1 subgoal):
 1. [(SOME r. set r = X)\<rightarrow>0]u \<turnstile> PTA.inv_of A l'
[PROOF STEP]
unfolding region_set'_def
[PROOF STATE]
proof (prove)
using this:
s = (l, u)
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
R = [u]\<^sub>\<R>
l' \<in> L
{[(SOME r. set r = X)\<rightarrow>0]v |v. v \<in> R} \<subseteq> {v. v \<turnstile> PTA.inv_of A l'}

goal (1 subgoal):
 1. [(SOME r. set r = X)\<rightarrow>0]u \<turnstile> PTA.inv_of A l'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[(SOME r. set r = X)\<rightarrow>0]u \<turnstile> PTA.inv_of A l'

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set_pmf \<mu>' \<Longrightarrow> abss (b, [(SOME r. set r = a)\<rightarrow>0]u) = (b, [a::=0]R)
[PROOF STEP]
with \<open>l' \<in> L\<close> \<open>[X:=0]u \<in> V\<close>
[PROOF STATE]
proof (chain)
picking this:
l' \<in> L
[(SOME r. set r = X)\<rightarrow>0]u \<in> V
[(SOME r. set r = X)\<rightarrow>0]u \<turnstile> PTA.inv_of A l'
[PROOF STEP]
have "(l', [X:=0]u) \<in> S"
[PROOF STATE]
proof (prove)
using this:
l' \<in> L
[(SOME r. set r = X)\<rightarrow>0]u \<in> V
[(SOME r. set r = X)\<rightarrow>0]u \<turnstile> PTA.inv_of A l'

goal (1 subgoal):
 1. (l', [(SOME r. set r = X)\<rightarrow>0]u) \<in> S
[PROOF STEP]
unfolding S_def V_def
[PROOF STATE]
proof (prove)
using this:
l' \<in> L
[(SOME r. set r = X)\<rightarrow>0]u \<in> {v. \<forall>x\<in>\<X>. 0 \<le> v x}
[(SOME r. set r = X)\<rightarrow>0]u \<turnstile> PTA.inv_of A l'

goal (1 subgoal):
 1. (l', [(SOME r. set r = X)\<rightarrow>0]u) \<in> {(l, u). l \<in> L \<and> (\<forall>x\<in>\<X>. 0 \<le> u x) \<and> u \<turnstile> PTA.inv_of A l}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(l', [(SOME r. set r = X)\<rightarrow>0]u) \<in> S

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set_pmf \<mu>' \<Longrightarrow> abss (b, [(SOME r. set r = a)\<rightarrow>0]u) = (b, [a::=0]R)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(l', [(SOME r. set r = X)\<rightarrow>0]u) \<in> S
[PROOF STEP]
have "abss (l', [X:=0]u) = (l', [[X:=0]u]\<^sub>\<R>)"
[PROOF STATE]
proof (prove)
using this:
(l', [(SOME r. set r = X)\<rightarrow>0]u) \<in> S

goal (1 subgoal):
 1. abss (l', [(SOME r. set r = X)\<rightarrow>0]u) = (l', [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
abss (l', [(SOME r. set r = X)\<rightarrow>0]u) = (l', [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R>)

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set_pmf \<mu>' \<Longrightarrow> abss (b, [(SOME r. set r = a)\<rightarrow>0]u) = (b, [a::=0]R)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
abss (l', [(SOME r. set r = X)\<rightarrow>0]u) = (l', [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R>)

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set_pmf \<mu>' \<Longrightarrow> abss (b, [(SOME r. set r = a)\<rightarrow>0]u) = (b, [a::=0]R)
[PROOF STEP]
have
       "\<dots> = (l', region_set' R (SOME r. set r = X) 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l', [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R>) = (l', [X::=0]R)
[PROOF STEP]
using region_set'_eq(1)[unfolded transition_def] prems A u
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?R \<in> \<R>; ?u \<in> ?R; (?l, ?g, ?\<mu>) \<in> PTA.trans_of A \<and> (?X, ?l') \<in> set_pmf ?\<mu>\<rbrakk> \<Longrightarrow> [[(SOME r. set r = ?X)\<rightarrow>0]?u]\<^sub>\<R> = [?X::=0]?R
\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'
abss s \<in> \<S>
abss s = (l, R)
(l, \<tau>, \<mu>') \<in> PTA.trans_of A
R \<subseteq> {v. v \<turnstile> \<tau>}
(X, l') \<in> set_pmf \<mu>'
s = (l, u)
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
R = [u]\<^sub>\<R>

goal (1 subgoal):
 1. (l', [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R>) = (l', [X::=0]R)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(l', [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R>) = (l', [X::=0]R)

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set_pmf \<mu>' \<Longrightarrow> abss (b, [(SOME r. set r = a)\<rightarrow>0]u) = (b, [a::=0]R)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
abss (l', [(SOME r. set r = X)\<rightarrow>0]u) = (l', [X::=0]R)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
abss (l', [(SOME r. set r = X)\<rightarrow>0]u) = (l', [X::=0]R)

goal (1 subgoal):
 1. abss (l', [(SOME r. set r = X)\<rightarrow>0]u) = (l', [X::=0]R)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
abss (l', [(SOME r. set r = X)\<rightarrow>0]u) = (l', [X::=0]R)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
abst (map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>') = \<mu>

goal (2 subgoals):
 1. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>' \<in> K s
abst (map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>') = \<mu>
[PROOF STEP]
have default: ?thesis if "rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)"
[PROOF STATE]
proof (prove)
using this:
map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>' \<in> K s
abst (map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>') = \<mu>

goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>' \<in> K s
abst (map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>') = \<mu>
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)

goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
by simp (rule someI; auto)
[PROOF STATE]
proof (state)
this:
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>

goal (2 subgoals):
 1. \<And>l R g \<mu>'. \<lbrakk>\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'; abss s \<in> \<S>; abss s = (l, R); (l, g, \<mu>') \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
proof (cases "\<exists> R. \<mu> = return_pmf (l, R)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>R. \<mu> = return_pmf (l, R) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<nexists>R. \<mu> = return_pmf (l, R) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>R. \<mu> = return_pmf (l, R)

goal (2 subgoals):
 1. \<exists>R. \<mu> = return_pmf (l, R) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<nexists>R. \<mu> = return_pmf (l, R) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with \<open>s = (l, u)\<close>
[PROOF STATE]
proof (chain)
picking this:
s = (l, u)
\<nexists>R. \<mu> = return_pmf (l, R)
[PROOF STEP]
have "rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)"
[PROOF STATE]
proof (prove)
using this:
s = (l, u)
\<nexists>R. \<mu> = return_pmf (l, R)

goal (1 subgoal):
 1. rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
unfolding rept_def
[PROOF STATE]
proof (prove)
using this:
s = (l, u)
\<nexists>R. \<mu> = return_pmf (l, R)

goal (1 subgoal):
 1. (let (l, u) = s in if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> [u]\<^sub>\<R> = R' \<and> (\<forall>c\<in>\<X>. real (k c) < u c) then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u) else SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)

goal (2 subgoals):
 1. \<exists>R. \<mu> = return_pmf (l, R) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<nexists>R. \<mu> = return_pmf (l, R) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with default
[PROOF STATE]
proof (chain)
picking this:
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)

goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>

goal (1 subgoal):
 1. \<exists>R. \<mu> = return_pmf (l, R) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>R. \<mu> = return_pmf (l, R) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>R. \<mu> = return_pmf (l, R)

goal (1 subgoal):
 1. \<exists>R. \<mu> = return_pmf (l, R) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>R. \<mu> = return_pmf (l, R)
[PROOF STEP]
obtain R' where R': "\<mu> = return_pmf (l, R')"
[PROOF STATE]
proof (prove)
using this:
\<exists>R. \<mu> = return_pmf (l, R)

goal (1 subgoal):
 1. (\<And>R'. \<mu> = return_pmf (l, R') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<mu> = return_pmf (l, R')

goal (1 subgoal):
 1. \<exists>R. \<mu> = return_pmf (l, R) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
proof (cases "R = R'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. R = R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. R \<noteq> R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
R \<noteq> R'

goal (2 subgoals):
 1. R = R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. R \<noteq> R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
from R' prems(1)
[PROOF STATE]
proof (chain)
picking this:
\<mu> = return_pmf (l, R')
\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'
[PROOF STEP]
have
        "\<forall> (X, l') \<in> \<mu>'. (l', region_set' R (SOME r. set r = X) 0) = (l, R')"
[PROOF STATE]
proof (prove)
using this:
\<mu> = return_pmf (l, R')
\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'

goal (1 subgoal):
 1. \<forall>(X, l')\<in>set_pmf \<mu>'. (l', [X::=0]R) = (l, R')
[PROOF STEP]
by (auto simp: map_pmf_eq_return_pmf_iff[of _ \<mu>' "(l, R')"])
[PROOF STATE]
proof (state)
this:
\<forall>(X, l')\<in>set_pmf \<mu>'. (l', [X::=0]R) = (l, R')

goal (2 subgoals):
 1. R = R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. R \<noteq> R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>(X, l')\<in>set_pmf \<mu>'. (l', [X::=0]R) = (l, R')
[PROOF STEP]
obtain X where
        "region_set' R (SOME r. set r = X) 0 = R'" "(X, l) \<in> \<mu>'"
[PROOF STATE]
proof (prove)
using this:
\<forall>(X, l')\<in>set_pmf \<mu>'. (l', [X::=0]R) = (l, R')

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>[X::=0]R = R'; (X, l) \<in> set_pmf \<mu>'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using set_pmf_not_empty
[PROOF STATE]
proof (prove)
using this:
\<forall>(X, l')\<in>set_pmf \<mu>'. (l', [X::=0]R) = (l, R')
set_pmf ?M \<noteq> {}

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>[X::=0]R = R'; (X, l) \<in> set_pmf \<mu>'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
[X::=0]R = R'
(X, l) \<in> set_pmf \<mu>'

goal (2 subgoals):
 1. R = R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. R \<noteq> R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with prems(4)
[PROOF STATE]
proof (chain)
picking this:
(l, \<tau>, \<mu>') \<in> PTA.trans_of A
[X::=0]R = R'
(X, l) \<in> set_pmf \<mu>'
[PROOF STEP]
have "X \<subseteq> \<X>"
[PROOF STATE]
proof (prove)
using this:
(l, \<tau>, \<mu>') \<in> PTA.trans_of A
[X::=0]R = R'
(X, l) \<in> set_pmf \<mu>'

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

goal (2 subgoals):
 1. R = R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. R \<noteq> R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
X \<subseteq> \<X>

goal (2 subgoals):
 1. R = R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. R \<noteq> R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X \<subseteq> \<X>
[PROOF STEP]
have
        "set (SOME r. set r = X) = X"
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<X>

goal (1 subgoal):
 1. set (SOME r. set r = X) = X
[PROOF STEP]
by - (rule someI_ex, metis finite_list finite(1) finite_subset)
[PROOF STATE]
proof (state)
this:
set (SOME r. set r = X) = X

goal (2 subgoals):
 1. R = R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. R \<noteq> R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
X \<subseteq> \<X>
set (SOME r. set r = X) = X
[PROOF STEP]
have "set (SOME r. set r = X) \<subseteq> \<X>"
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<X>
set (SOME r. set r = X) = X

goal (1 subgoal):
 1. set (SOME r. set r = X) \<subseteq> \<X>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (SOME r. set r = X) \<subseteq> \<X>

goal (2 subgoals):
 1. R = R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. R \<noteq> R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with alpha_interp.region_reset_not_Succ False \<open>_ = R'\<close> u(3,4)
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?R \<in> \<R>; set ?r \<subseteq> \<X>\<rbrakk> \<Longrightarrow> region_set' ?R ?r 0 = ?R \<or> region_set' ?R ?r 0 \<notin> Succ \<R> ?R
R \<noteq> R'
[X::=0]R = R'
[u]\<^sub>\<R> \<in> \<R>
R = [u]\<^sub>\<R>
set (SOME r. set r = X) \<subseteq> \<X>
[PROOF STEP]
have "R' \<notin> Succ \<R> R"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?R \<in> \<R>; set ?r \<subseteq> \<X>\<rbrakk> \<Longrightarrow> region_set' ?R ?r 0 = ?R \<or> region_set' ?R ?r 0 \<notin> Succ \<R> ?R
R \<noteq> R'
[X::=0]R = R'
[u]\<^sub>\<R> \<in> \<R>
R = [u]\<^sub>\<R>
set (SOME r. set r = X) \<subseteq> \<X>

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

goal (2 subgoals):
 1. R = R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. R \<noteq> R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with \<open>s = (l, u)\<close> R' u(4) False
[PROOF STATE]
proof (chain)
picking this:
s = (l, u)
\<mu> = return_pmf (l, R')
R = [u]\<^sub>\<R>
R \<noteq> R'
R' \<notin> Succ \<R> R
[PROOF STEP]
have
        "rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)"
[PROOF STATE]
proof (prove)
using this:
s = (l, u)
\<mu> = return_pmf (l, R')
R = [u]\<^sub>\<R>
R \<noteq> R'
R' \<notin> Succ \<R> R

goal (1 subgoal):
 1. rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
unfolding rept_def
[PROOF STATE]
proof (prove)
using this:
s = (l, u)
\<mu> = return_pmf (l, R')
R = [u]\<^sub>\<R>
R \<noteq> R'
R' \<notin> Succ \<R> R

goal (1 subgoal):
 1. (let (l, u) = s in if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> [u]\<^sub>\<R> = R' \<and> (\<forall>c\<in>\<X>. real (k c) < u c) then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u) else SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)

goal (2 subgoals):
 1. R = R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. R \<noteq> R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with default
[PROOF STATE]
proof (chain)
picking this:
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)

goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>

goal (1 subgoal):
 1. R = R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. R = R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
case T: True
[PROOF STATE]
proof (state)
this:
R = R'

goal (1 subgoal):
 1. R = R' \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
proof (cases "\<forall>c\<in>\<X>. real (k c) < u c")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<not> (\<forall>c\<in>\<X>. real (k c) < u c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>c\<in>\<X>. real (k c) < u c)

goal (2 subgoals):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<not> (\<forall>c\<in>\<X>. real (k c) < u c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with T \<open>s = (l, u)\<close> R' u(4)
[PROOF STATE]
proof (chain)
picking this:
R = R'
s = (l, u)
\<mu> = return_pmf (l, R')
R = [u]\<^sub>\<R>
\<not> (\<forall>c\<in>\<X>. real (k c) < u c)
[PROOF STEP]
have
          "rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)"
[PROOF STATE]
proof (prove)
using this:
R = R'
s = (l, u)
\<mu> = return_pmf (l, R')
R = [u]\<^sub>\<R>
\<not> (\<forall>c\<in>\<X>. real (k c) < u c)

goal (1 subgoal):
 1. rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
unfolding rept_def
[PROOF STATE]
proof (prove)
using this:
R = R'
s = (l, u)
\<mu> = return_pmf (l, R')
R = [u]\<^sub>\<R>
\<not> (\<forall>c\<in>\<X>. real (k c) < u c)

goal (1 subgoal):
 1. (let (l, u) = s in if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> [u]\<^sub>\<R> = R' \<and> (\<forall>c\<in>\<X>. real (k c) < u c) then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u) else SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)

goal (2 subgoals):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<not> (\<forall>c\<in>\<X>. real (k c) < u c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with default
[PROOF STATE]
proof (chain)
picking this:
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)

goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>

goal (1 subgoal):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>\<X>. real (k c) < u c

goal (1 subgoal):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with T \<open>s = (l, u)\<close> R' u(4) \<open>(l, u) \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
R = R'
s = (l, u)
\<mu> = return_pmf (l, R')
R = [u]\<^sub>\<R>
(l, u) \<in> S
\<forall>c\<in>\<X>. real (k c) < u c
[PROOF STEP]
have
          "rept s \<mu> = return_pmf (l, u \<oplus> 0.5)"
[PROOF STATE]
proof (prove)
using this:
R = R'
s = (l, u)
\<mu> = return_pmf (l, R')
R = [u]\<^sub>\<R>
(l, u) \<in> S
\<forall>c\<in>\<X>. real (k c) < u c

goal (1 subgoal):
 1. rept s \<mu> = return_pmf (l, u \<oplus> 5 / 10)
[PROOF STEP]
unfolding rept_def
[PROOF STATE]
proof (prove)
using this:
R = R'
s = (l, u)
\<mu> = return_pmf (l, R')
R = [u]\<^sub>\<R>
(l, u) \<in> S
\<forall>c\<in>\<X>. real (k c) < u c

goal (1 subgoal):
 1. (let (l, u) = s in if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> [u]\<^sub>\<R> = R' \<and> (\<forall>c\<in>\<X>. real (k c) < u c) then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u) else SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) = return_pmf (l, u \<oplus> 5 / 10)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rept s \<mu> = return_pmf (l, u \<oplus> 5 / 10)

goal (1 subgoal):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
from upper_right_closed[OF True] T u \<R>_V
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>u \<in> ?R; ?R \<in> \<R>; 0 \<le> ?t\<rbrakk> \<Longrightarrow> u \<oplus> ?t \<in> ?R
R = R'
s = (l, u)
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
R = [u]\<^sub>\<R>
\<Union> \<R> = V
[PROOF STEP]
have "u \<oplus> 0.5 \<in> R'" "u \<oplus> 0.5 \<in> V"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>u \<in> ?R; ?R \<in> \<R>; 0 \<le> ?t\<rbrakk> \<Longrightarrow> u \<oplus> ?t \<in> ?R
R = R'
s = (l, u)
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
R = [u]\<^sub>\<R>
\<Union> \<R> = V

goal (1 subgoal):
 1. u \<oplus> 5 / 10 \<in> R' &&& u \<oplus> 5 / 10 \<in> V
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
u \<oplus> 5 / 10 \<in> R'
u \<oplus> 5 / 10 \<in> V

goal (1 subgoal):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u \<oplus> 5 / 10 \<in> R'
u \<oplus> 5 / 10 \<in> V

goal (1 subgoal):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<oplus> 5 / 10 \<in> R'
u \<oplus> 5 / 10 \<in> V
[PROOF STEP]
have "[u \<oplus> 0.5]\<^sub>\<R> = R'"
[PROOF STATE]
proof (prove)
using this:
u \<oplus> 5 / 10 \<in> R'
u \<oplus> 5 / 10 \<in> V

goal (1 subgoal):
 1. [u \<oplus> 5 / 10]\<^sub>\<R> = R'
[PROOF STEP]
using T alpha_interp.region_unique_spec u(3,4)
[PROOF STATE]
proof (prove)
using this:
u \<oplus> 5 / 10 \<in> R'
u \<oplus> 5 / 10 \<in> V
R = R'
\<lbrakk>?u \<in> ?R; ?R \<in> \<R>\<rbrakk> \<Longrightarrow> [?u]\<^sub>\<R> = ?R
[u]\<^sub>\<R> \<in> \<R>
R = [u]\<^sub>\<R>

goal (1 subgoal):
 1. [u \<oplus> 5 / 10]\<^sub>\<R> = R'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[u \<oplus> 5 / 10]\<^sub>\<R> = R'

goal (1 subgoal):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[u \<oplus> 5 / 10]\<^sub>\<R> = R'

goal (1 subgoal):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
note * = \<open>rept _ _ = _\<close> R' \<open>abss s \<in> \<S>\<close> \<open>abss s = _\<close> prems(5)
[PROOF STATE]
proof (state)
this:
rept s \<mu> = return_pmf (l, u \<oplus> 5 / 10)
\<mu> = return_pmf (l, R')
abss s \<in> \<S>
abss s = (l, R)
R \<subseteq> {v. v \<turnstile> \<tau>}

goal (1 subgoal):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
u \<oplus> 5 / 10 \<in> R'
u \<oplus> 5 / 10 \<in> V
[u \<oplus> 5 / 10]\<^sub>\<R> = R'
rept s \<mu> = return_pmf (l, u \<oplus> 5 / 10)
\<mu> = return_pmf (l, R')
abss s \<in> \<S>
abss s = (l, R)
R \<subseteq> {v. v \<turnstile> \<tau>}
[PROOF STEP]
have "abst (rept s \<mu>) = \<mu>"
[PROOF STATE]
proof (prove)
using this:
u \<oplus> 5 / 10 \<in> R'
u \<oplus> 5 / 10 \<in> V
[u \<oplus> 5 / 10]\<^sub>\<R> = R'
rept s \<mu> = return_pmf (l, u \<oplus> 5 / 10)
\<mu> = return_pmf (l, R')
abss s \<in> \<S>
abss s = (l, R)
R \<subseteq> {v. v \<turnstile> \<tau>}

goal (1 subgoal):
 1. abst (rept s \<mu>) = \<mu>
[PROOF STEP]
apply (simp add: abst_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u \<oplus> 1 / 2 \<in> R'; u \<oplus> 1 / 2 \<in> V; [u \<oplus> 1 / 2]\<^sub>\<R> = R'; rept s (return_pmf (l, R')) = return_pmf (l, u \<oplus> 1 / 2); \<mu> = return_pmf (l, R'); (l, R) \<in> \<S>; abss s = (l, R); R \<subseteq> {v. v \<turnstile> \<tau>}\<rbrakk> \<Longrightarrow> abss (l, u \<oplus> 1 / 2) = (l, R')
[PROOF STEP]
apply (subst abss_S)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>u \<oplus> 1 / 2 \<in> R'; u \<oplus> 1 / 2 \<in> V; [u \<oplus> 1 / 2]\<^sub>\<R> = R'; rept s (return_pmf (l, R')) = return_pmf (l, u \<oplus> 1 / 2); \<mu> = return_pmf (l, R'); (l, R) \<in> \<S>; abss s = (l, R); R \<subseteq> {v. v \<turnstile> \<tau>}\<rbrakk> \<Longrightarrow> (l, u \<oplus> 1 / 2) \<in> S
 2. \<lbrakk>u \<oplus> 1 / 2 \<in> R'; u \<oplus> 1 / 2 \<in> V; [u \<oplus> 1 / 2]\<^sub>\<R> = R'; rept s (return_pmf (l, R')) = return_pmf (l, u \<oplus> 1 / 2); \<mu> = return_pmf (l, R'); (l, R) \<in> \<S>; abss s = (l, R); R \<subseteq> {v. v \<turnstile> \<tau>}\<rbrakk> \<Longrightarrow> (l, [u \<oplus> 1 / 2]\<^sub>\<R>) = (l, R')
[PROOF STEP]
by (auto simp: \<S>_L S_def V_def T dest: \<S>_inv)
[PROOF STATE]
proof (state)
this:
abst (rept s \<mu>) = \<mu>

goal (1 subgoal):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
abst (rept s \<mu>) = \<mu>

goal (1 subgoal):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
from * \<open>s = _\<close> \<open>(l, u) \<in> S\<close> \<open>_ \<in> R'\<close>
[PROOF STATE]
proof (chain)
picking this:
rept s \<mu> = return_pmf (l, u \<oplus> 5 / 10)
\<mu> = return_pmf (l, R')
abss s \<in> \<S>
abss s = (l, R)
R \<subseteq> {v. v \<turnstile> \<tau>}
s = (l, u)
(l, u) \<in> S
u \<oplus> 5 / 10 \<in> R'
[PROOF STEP]
have
          "rept s \<mu> \<in> K s"
[PROOF STATE]
proof (prove)
using this:
rept s \<mu> = return_pmf (l, u \<oplus> 5 / 10)
\<mu> = return_pmf (l, R')
abss s \<in> \<S>
abss s = (l, R)
R \<subseteq> {v. v \<turnstile> \<tau>}
s = (l, u)
(l, u) \<in> S
u \<oplus> 5 / 10 \<in> R'

goal (1 subgoal):
 1. rept s \<mu> \<in> K s
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rept (l, u) (return_pmf (l, R')) = return_pmf (l, u \<oplus> 1 / 2); \<mu> = return_pmf (l, R'); (l, R) \<in> \<S>; abss (l, u) = (l, R); R \<subseteq> {v. v \<turnstile> \<tau>}; s = (l, u); (l, u) \<in> S; u \<oplus> 1 / 2 \<in> R'\<rbrakk> \<Longrightarrow> return_pmf (l, u \<oplus> 1 / 2) \<in> K (l, u)
[PROOF STEP]
apply (rule K.delay)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>rept (l, u) (return_pmf (l, R')) = return_pmf (l, u \<oplus> 1 / 2); \<mu> = return_pmf (l, R'); (l, R) \<in> \<S>; abss (l, u) = (l, R); R \<subseteq> {v. v \<turnstile> \<tau>}; s = (l, u); (l, u) \<in> S; u \<oplus> 1 / 2 \<in> R'\<rbrakk> \<Longrightarrow> (l, u) \<in> S
 2. \<lbrakk>rept (l, u) (return_pmf (l, R')) = return_pmf (l, u \<oplus> 1 / 2); \<mu> = return_pmf (l, R'); (l, R) \<in> \<S>; abss (l, u) = (l, R); R \<subseteq> {v. v \<turnstile> \<tau>}; s = (l, u); (l, u) \<in> S; u \<oplus> 1 / 2 \<in> R'\<rbrakk> \<Longrightarrow> (l, u) = (l, u)
 3. \<lbrakk>rept (l, u) (return_pmf (l, R')) = return_pmf (l, u \<oplus> 1 / 2); \<mu> = return_pmf (l, R'); (l, R) \<in> \<S>; abss (l, u) = (l, R); R \<subseteq> {v. v \<turnstile> \<tau>}; s = (l, u); (l, u) \<in> S; u \<oplus> 1 / 2 \<in> R'\<rbrakk> \<Longrightarrow> 0 \<le> 1 / 2
 4. \<lbrakk>rept (l, u) (return_pmf (l, R')) = return_pmf (l, u \<oplus> 1 / 2); \<mu> = return_pmf (l, R'); (l, R) \<in> \<S>; abss (l, u) = (l, R); R \<subseteq> {v. v \<turnstile> \<tau>}; s = (l, u); (l, u) \<in> S; u \<oplus> 1 / 2 \<in> R'\<rbrakk> \<Longrightarrow> u \<oplus> 1 / 2 \<turnstile> PTA.inv_of A l
[PROOF STEP]
by (auto simp: T dest: \<S>_inv)
[PROOF STATE]
proof (state)
this:
rept s \<mu> \<in> K s

goal (1 subgoal):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
abst (rept s \<mu>) = \<mu>
rept s \<mu> \<in> K s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
abst (rept s \<mu>) = \<mu>
rept s \<mu> \<in> K s

goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>

goal (1 subgoal):
 1. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
case loop
[PROOF STATE]
proof (state)
this:
\<mu> = return_pmf (abss s)

goal (1 subgoal):
 1. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
obtain l u where "s = (l, u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l u. s = (l, u) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
s = (l, u)

goal (1 subgoal):
 1. \<mu> = return_pmf (abss s) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
proof (cases "s \<in> S")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s \<in> S \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. s \<notin> S \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
case T: True
[PROOF STATE]
proof (state)
this:
s \<in> S

goal (2 subgoals):
 1. s \<in> S \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. s \<notin> S \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with \<open>s = _\<close>
[PROOF STATE]
proof (chain)
picking this:
s = (l, u)
s \<in> S
[PROOF STEP]
have *: "l \<in> L" "u \<in> [u]\<^sub>\<R>" "[u]\<^sub>\<R> \<in> \<R>" "abss s = (l, [u]\<^sub>\<R>)"
[PROOF STATE]
proof (prove)
using this:
s = (l, u)
s \<in> S

goal (1 subgoal):
 1. (l \<in> L &&& u \<in> [u]\<^sub>\<R>) &&& [u]\<^sub>\<R> \<in> \<R> &&& abss s = (l, [u]\<^sub>\<R>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l \<in> L
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
abss s = (l, [u]\<^sub>\<R>)

goal (2 subgoals):
 1. s \<in> S \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. s \<notin> S \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<in> L
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
abss s = (l, [u]\<^sub>\<R>)
[PROOF STEP]
have "abss s = (l, [u]\<^sub>\<R>)"
[PROOF STATE]
proof (prove)
using this:
l \<in> L
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
abss s = (l, [u]\<^sub>\<R>)

goal (1 subgoal):
 1. abss s = (l, [u]\<^sub>\<R>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
abss s = (l, [u]\<^sub>\<R>)

goal (2 subgoals):
 1. s \<in> S \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. s \<notin> S \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with \<open>s \<in> S\<close> S_abss_\<S>
[PROOF STATE]
proof (chain)
picking this:
s \<in> S
?s \<in> S \<Longrightarrow> abss ?s \<in> \<S>
abss s = (l, [u]\<^sub>\<R>)
[PROOF STEP]
have "(l, [u]\<^sub>\<R>) \<in> \<S>"
[PROOF STATE]
proof (prove)
using this:
s \<in> S
?s \<in> S \<Longrightarrow> abss ?s \<in> \<S>
abss s = (l, [u]\<^sub>\<R>)

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

goal (2 subgoals):
 1. s \<in> S \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. s \<notin> S \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with \<S>_inv
[PROOF STATE]
proof (chain)
picking this:
(?l, ?R) \<in> \<S> \<Longrightarrow> ?R \<subseteq> {v. v \<turnstile> PTA.inv_of A ?l}
(l, [u]\<^sub>\<R>) \<in> \<S>
[PROOF STEP]
have "[u]\<^sub>\<R> \<subseteq> {u. u \<turnstile> inv_of A l}"
[PROOF STATE]
proof (prove)
using this:
(?l, ?R) \<in> \<S> \<Longrightarrow> ?R \<subseteq> {v. v \<turnstile> PTA.inv_of A ?l}
(l, [u]\<^sub>\<R>) \<in> \<S>

goal (1 subgoal):
 1. [u]\<^sub>\<R> \<subseteq> {u. u \<turnstile> PTA.inv_of A l}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[u]\<^sub>\<R> \<subseteq> {u. u \<turnstile> PTA.inv_of A l}

goal (2 subgoals):
 1. s \<in> S \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. s \<notin> S \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
proof (cases "\<forall>c\<in>\<X>. real (k c) < u c")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<not> (\<forall>c\<in>\<X>. real (k c) < u c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>\<X>. real (k c) < u c

goal (2 subgoals):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<not> (\<forall>c\<in>\<X>. real (k c) < u c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with * \<open>\<mu> = _\<close> \<open>s = _\<close> \<open>s \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
l \<in> L
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
abss s = (l, [u]\<^sub>\<R>)
\<mu> = return_pmf (abss s)
s = (l, u)
s \<in> S
\<forall>c\<in>\<X>. real (k c) < u c
[PROOF STEP]
have
        "rept s \<mu> = return_pmf (l, u \<oplus> 0.5)"
[PROOF STATE]
proof (prove)
using this:
l \<in> L
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
abss s = (l, [u]\<^sub>\<R>)
\<mu> = return_pmf (abss s)
s = (l, u)
s \<in> S
\<forall>c\<in>\<X>. real (k c) < u c

goal (1 subgoal):
 1. rept s \<mu> = return_pmf (l, u \<oplus> 5 / 10)
[PROOF STEP]
unfolding rept_def
[PROOF STATE]
proof (prove)
using this:
l \<in> L
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
abss s = (l, [u]\<^sub>\<R>)
\<mu> = return_pmf (abss s)
s = (l, u)
s \<in> S
\<forall>c\<in>\<X>. real (k c) < u c

goal (1 subgoal):
 1. (let (l, u) = s in if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> [u]\<^sub>\<R> = R' \<and> (\<forall>c\<in>\<X>. real (k c) < u c) then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u) else SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) = return_pmf (l, u \<oplus> 5 / 10)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rept s \<mu> = return_pmf (l, u \<oplus> 5 / 10)

goal (2 subgoals):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<not> (\<forall>c\<in>\<X>. real (k c) < u c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
from upper_right_closed[OF True] *
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>u \<in> ?R; ?R \<in> \<R>; 0 \<le> ?t\<rbrakk> \<Longrightarrow> u \<oplus> ?t \<in> ?R
l \<in> L
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
abss s = (l, [u]\<^sub>\<R>)
[PROOF STEP]
have "u \<oplus> 0.5 \<in> [u]\<^sub>\<R>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>u \<in> ?R; ?R \<in> \<R>; 0 \<le> ?t\<rbrakk> \<Longrightarrow> u \<oplus> ?t \<in> ?R
l \<in> L
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
abss s = (l, [u]\<^sub>\<R>)

goal (1 subgoal):
 1. u \<oplus> 5 / 10 \<in> [u]\<^sub>\<R>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<oplus> 5 / 10 \<in> [u]\<^sub>\<R>

goal (2 subgoals):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<not> (\<forall>c\<in>\<X>. real (k c) < u c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u \<oplus> 5 / 10 \<in> [u]\<^sub>\<R>

goal (2 subgoals):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<not> (\<forall>c\<in>\<X>. real (k c) < u c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with * \<R>_V
[PROOF STATE]
proof (chain)
picking this:
l \<in> L
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
abss s = (l, [u]\<^sub>\<R>)
\<Union> \<R> = V
u \<oplus> 5 / 10 \<in> [u]\<^sub>\<R>
[PROOF STEP]
have "u \<oplus> 0.5 \<in> V"
[PROOF STATE]
proof (prove)
using this:
l \<in> L
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
abss s = (l, [u]\<^sub>\<R>)
\<Union> \<R> = V
u \<oplus> 5 / 10 \<in> [u]\<^sub>\<R>

goal (1 subgoal):
 1. u \<oplus> 5 / 10 \<in> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<oplus> 5 / 10 \<in> V

goal (2 subgoals):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<not> (\<forall>c\<in>\<X>. real (k c) < u c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u \<oplus> 5 / 10 \<in> V

goal (2 subgoals):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<not> (\<forall>c\<in>\<X>. real (k c) < u c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with calculation * alpha_interp.region_unique_spec
[PROOF STATE]
proof (chain)
picking this:
u \<oplus> 5 / 10 \<in> [u]\<^sub>\<R>
u \<oplus> 5 / 10 \<in> V
l \<in> L
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
abss s = (l, [u]\<^sub>\<R>)
\<lbrakk>?u \<in> ?R; ?R \<in> \<R>\<rbrakk> \<Longrightarrow> [?u]\<^sub>\<R> = ?R
u \<oplus> 5 / 10 \<in> V
[PROOF STEP]
have "[u \<oplus> 0.5]\<^sub>\<R> = [u]\<^sub>\<R>"
[PROOF STATE]
proof (prove)
using this:
u \<oplus> 5 / 10 \<in> [u]\<^sub>\<R>
u \<oplus> 5 / 10 \<in> V
l \<in> L
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
abss s = (l, [u]\<^sub>\<R>)
\<lbrakk>?u \<in> ?R; ?R \<in> \<R>\<rbrakk> \<Longrightarrow> [?u]\<^sub>\<R> = ?R
u \<oplus> 5 / 10 \<in> V

goal (1 subgoal):
 1. [u \<oplus> 5 / 10]\<^sub>\<R> = [u]\<^sub>\<R>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[u \<oplus> 5 / 10]\<^sub>\<R> = [u]\<^sub>\<R>

goal (2 subgoals):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<not> (\<forall>c\<in>\<X>. real (k c) < u c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[u \<oplus> 5 / 10]\<^sub>\<R> = [u]\<^sub>\<R>

goal (2 subgoals):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<not> (\<forall>c\<in>\<X>. real (k c) < u c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
note * \<open>rept _ _ = _\<close> \<open>s = _\<close> T \<open>\<mu> = _\<close> \<open>(l, _) \<in> \<S>\<close> \<S>_inv
[PROOF STATE]
proof (state)
this:
l \<in> L
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
abss s = (l, [u]\<^sub>\<R>)
rept s \<mu> = return_pmf (l, u \<oplus> 5 / 10)
s = (l, u)
s \<in> S
\<mu> = return_pmf (abss s)
(l, [u]\<^sub>\<R>) \<in> \<S>
(?l, ?R) \<in> \<S> \<Longrightarrow> ?R \<subseteq> {v. v \<turnstile> PTA.inv_of A ?l}

goal (2 subgoals):
 1. \<forall>c\<in>\<X>. real (k c) < u c \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
 2. \<not> (\<forall>c\<in>\<X>. real (k c) < u c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
u \<oplus> 5 / 10 \<in> [u]\<^sub>\<R>
u \<oplus> 5 / 10 \<in> V
[u \<oplus> 5 / 10]\<^sub>\<R> = [u]\<^sub>\<R>
l \<in> L
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
abss s = (l, [u]\<^sub>\<R>)
rept s \<mu> = return_pmf (l, u \<oplus> 5 / 10)
s = (l, u)
s \<in> S
\<mu> = return_pmf (abss s)
(l, [u]\<^sub>\<R>) \<in> \<S>
(?l, ?R) \<in> \<S> \<Longrightarrow> ?R \<subseteq> {v. v \<turnstile> PTA.inv_of A ?l}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u \<oplus> 5 / 10 \<in> [u]\<^sub>\<R>
u \<oplus> 5 / 10 \<in> V
[u \<oplus> 5 / 10]\<^sub>\<R> = [u]\<^sub>\<R>
l \<in> L
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
abss s = (l, [u]\<^sub>\<R>)
rept s \<mu> = return_pmf (l, u \<oplus> 5 / 10)
s = (l, u)
s \<in> S
\<mu> = return_pmf (abss s)
(l, [u]\<^sub>\<R>) \<in> \<S>
(?l, ?R) \<in> \<S> \<Longrightarrow> ?R \<subseteq> {v. v \<turnstile> PTA.inv_of A ?l}

goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
unfolding rept_def
[PROOF STATE]
proof (prove)
using this:
u \<oplus> 5 / 10 \<in> [u]\<^sub>\<R>
u \<oplus> 5 / 10 \<in> V
[u \<oplus> 5 / 10]\<^sub>\<R> = [u]\<^sub>\<R>
l \<in> L
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
abss s = (l, [u]\<^sub>\<R>)
(let (l, u) = s in if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> [u]\<^sub>\<R> = R' \<and> (\<forall>c\<in>\<X>. real (k c) < u c) then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u) else SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) = return_pmf (l, u \<oplus> 5 / 10)
s = (l, u)
s \<in> S
\<mu> = return_pmf (abss s)
(l, [u]\<^sub>\<R>) \<in> \<S>
(?l, ?R) \<in> \<S> \<Longrightarrow> ?R \<subseteq> {v. v \<turnstile> PTA.inv_of A ?l}

goal (1 subgoal):
 1. (let (l, u) = s in if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> [u]\<^sub>\<R> = R' \<and> (\<forall>c\<in>\<X>. real (k c) < u c) then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u) else SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) \<in> K s \<and> abst (let (l, u) = s in if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> [u]\<^sub>\<R> = R' \<and> (\<forall>c\<in>\<X>. real (k c) < u c) then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u) else SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) = \<mu>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u \<oplus> 1 / 2 \<in> [u]\<^sub>\<R>; u \<oplus> 1 / 2 \<in> V; [u \<oplus> 1 / 2]\<^sub>\<R> = [u]\<^sub>\<R>; l \<in> L; u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>; abss (l, u) = (l, [u]\<^sub>\<R>); (if \<forall>c\<in>\<X>. real (k c) < u c then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u) else SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) = return_pmf (l, u \<oplus> 1 / 2); s = (l, u); (l, u) \<in> S; \<mu> = return_pmf (l, [u]\<^sub>\<R>); (l, [u]\<^sub>\<R>) \<in> \<S>; \<And>l R. (l, R) \<in> \<S> \<Longrightarrow> R \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> return_pmf (l, u \<oplus> 1 / 2) \<in> K (l, u) \<and> abst (return_pmf (l, u \<oplus> 1 / 2)) = return_pmf (l, [u]\<^sub>\<R>)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>u \<oplus> 1 / 2 \<in> [u]\<^sub>\<R>; u \<oplus> 1 / 2 \<in> V; [u \<oplus> 1 / 2]\<^sub>\<R> = [u]\<^sub>\<R>; l \<in> L; u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>; abss (l, u) = (l, [u]\<^sub>\<R>); (if \<forall>c\<in>\<X>. real (k c) < u c then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> return_pmf (l, [u]\<^sub>\<R>) = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. return_pmf (l, [u]\<^sub>\<R>) = return_pmf (l, R')) u) else SOME \<mu>. \<mu> \<in> K (l, u) \<and> abst \<mu> = return_pmf (l, [u]\<^sub>\<R>)) = return_pmf (l, u \<oplus> 1 / 2); (l, u) \<in> S; \<mu> = return_pmf (l, [u]\<^sub>\<R>); (l, [u]\<^sub>\<R>) \<in> \<S>; \<And>l R. (l, R) \<in> \<S> \<Longrightarrow> R \<subseteq> {v. v \<turnstile> PTA.inv_of A l}; s = (l, u)\<rbrakk> \<Longrightarrow> return_pmf (l, u \<oplus> 1 / 2) \<in> K (l, u)
 2. \<lbrakk>u \<oplus> 1 / 2 \<in> [u]\<^sub>\<R>; u \<oplus> 1 / 2 \<in> V; [u \<oplus> 1 / 2]\<^sub>\<R> = [u]\<^sub>\<R>; l \<in> L; u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>; abss (l, u) = (l, [u]\<^sub>\<R>); (if \<forall>c\<in>\<X>. real (k c) < u c then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> return_pmf (l, [u]\<^sub>\<R>) = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. return_pmf (l, [u]\<^sub>\<R>) = return_pmf (l, R')) u) else SOME \<mu>. \<mu> \<in> K (l, u) \<and> abst \<mu> = return_pmf (l, [u]\<^sub>\<R>)) = return_pmf (l, u \<oplus> 1 / 2); (l, u) \<in> S; \<mu> = return_pmf (l, [u]\<^sub>\<R>); (l, [u]\<^sub>\<R>) \<in> \<S>; \<And>l R. (l, R) \<in> \<S> \<Longrightarrow> R \<subseteq> {v. v \<turnstile> PTA.inv_of A l}; s = (l, u)\<rbrakk> \<Longrightarrow> abst (return_pmf (l, u \<oplus> 1 / 2)) = return_pmf (l, [u]\<^sub>\<R>)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u \<oplus> 1 / 2 \<in> [u]\<^sub>\<R>; u \<oplus> 1 / 2 \<in> V; [u \<oplus> 1 / 2]\<^sub>\<R> = [u]\<^sub>\<R>; l \<in> L; u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>; abss (l, u) = (l, [u]\<^sub>\<R>); (if \<forall>c\<in>\<X>. real (k c) < u c then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> return_pmf (l, [u]\<^sub>\<R>) = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. return_pmf (l, [u]\<^sub>\<R>) = return_pmf (l, R')) u) else SOME \<mu>. \<mu> \<in> K (l, u) \<and> abst \<mu> = return_pmf (l, [u]\<^sub>\<R>)) = return_pmf (l, u \<oplus> 1 / 2); (l, u) \<in> S; \<mu> = return_pmf (l, [u]\<^sub>\<R>); (l, [u]\<^sub>\<R>) \<in> \<S>; \<And>l R. (l, R) \<in> \<S> \<Longrightarrow> R \<subseteq> {v. v \<turnstile> PTA.inv_of A l}; s = (l, u)\<rbrakk> \<Longrightarrow> abst (return_pmf (l, u \<oplus> 1 / 2)) = return_pmf (l, [u]\<^sub>\<R>)
[PROOF STEP]
apply (simp add: abst_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u \<oplus> 1 / 2 \<in> [u]\<^sub>\<R>; u \<oplus> 1 / 2 \<in> V; [u \<oplus> 1 / 2]\<^sub>\<R> = [u]\<^sub>\<R>; l \<in> L; u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>; abss (l, u) = (l, [u]\<^sub>\<R>); (if \<forall>c\<in>\<X>. real (k c) < u c then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> return_pmf (l, [u]\<^sub>\<R>) = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. return_pmf (l, [u]\<^sub>\<R>) = return_pmf (l, R')) u) else SOME \<mu>. \<mu> \<in> K (l, u) \<and> abst \<mu> = return_pmf (l, [u]\<^sub>\<R>)) = return_pmf (l, u \<oplus> 1 / 2); (l, u) \<in> S; \<mu> = return_pmf (l, [u]\<^sub>\<R>); (l, [u]\<^sub>\<R>) \<in> \<S>; \<And>l R. (l, R) \<in> \<S> \<Longrightarrow> R \<subseteq> {v. v \<turnstile> PTA.inv_of A l}; s = (l, u)\<rbrakk> \<Longrightarrow> abss (l, u \<oplus> 1 / 2) = (l, [u]\<^sub>\<R>)
[PROOF STEP]
apply (subst abst_def abss_S)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>u \<oplus> 1 / 2 \<in> [u]\<^sub>\<R>; u \<oplus> 1 / 2 \<in> V; [u \<oplus> 1 / 2]\<^sub>\<R> = [u]\<^sub>\<R>; l \<in> L; u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>; abss (l, u) = (l, [u]\<^sub>\<R>); (if \<forall>c\<in>\<X>. real (k c) < u c then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> return_pmf (l, [u]\<^sub>\<R>) = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. return_pmf (l, [u]\<^sub>\<R>) = return_pmf (l, R')) u) else SOME \<mu>. \<mu> \<in> K (l, u) \<and> abst \<mu> = return_pmf (l, [u]\<^sub>\<R>)) = return_pmf (l, u \<oplus> 1 / 2); (l, u) \<in> S; \<mu> = return_pmf (l, [u]\<^sub>\<R>); (l, [u]\<^sub>\<R>) \<in> \<S>; \<And>l R. (l, R) \<in> \<S> \<Longrightarrow> R \<subseteq> {v. v \<turnstile> PTA.inv_of A l}; s = (l, u)\<rbrakk> \<Longrightarrow> (l, u \<oplus> 1 / 2) \<in> S
 2. \<lbrakk>u \<oplus> 1 / 2 \<in> [u]\<^sub>\<R>; u \<oplus> 1 / 2 \<in> V; [u \<oplus> 1 / 2]\<^sub>\<R> = [u]\<^sub>\<R>; l \<in> L; u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>; abss (l, u) = (l, [u]\<^sub>\<R>); (if \<forall>c\<in>\<X>. real (k c) < u c then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> return_pmf (l, [u]\<^sub>\<R>) = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. return_pmf (l, [u]\<^sub>\<R>) = return_pmf (l, R')) u) else SOME \<mu>. \<mu> \<in> K (l, u) \<and> abst \<mu> = return_pmf (l, [u]\<^sub>\<R>)) = return_pmf (l, u \<oplus> 1 / 2); (l, u) \<in> S; \<mu> = return_pmf (l, [u]\<^sub>\<R>); (l, [u]\<^sub>\<R>) \<in> \<S>; \<And>l R. (l, R) \<in> \<S> \<Longrightarrow> R \<subseteq> {v. v \<turnstile> PTA.inv_of A l}; s = (l, u)\<rbrakk> \<Longrightarrow> (l, [u \<oplus> 1 / 2]\<^sub>\<R>) = (l, [u]\<^sub>\<R>)
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>

goal (1 subgoal):
 1. \<not> (\<forall>c\<in>\<X>. real (k c) < u c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>c\<in>\<X>. real (k c) < u c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>c\<in>\<X>. real (k c) < u c)

goal (1 subgoal):
 1. \<not> (\<forall>c\<in>\<X>. real (k c) < u c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with * \<open>s = _\<close> \<open>\<mu> = _\<close>
[PROOF STATE]
proof (chain)
picking this:
l \<in> L
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
abss s = (l, [u]\<^sub>\<R>)
s = (l, u)
\<mu> = return_pmf (abss s)
\<not> (\<forall>c\<in>\<X>. real (k c) < u c)
[PROOF STEP]
have
        "rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)"
[PROOF STATE]
proof (prove)
using this:
l \<in> L
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
abss s = (l, [u]\<^sub>\<R>)
s = (l, u)
\<mu> = return_pmf (abss s)
\<not> (\<forall>c\<in>\<X>. real (k c) < u c)

goal (1 subgoal):
 1. rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
unfolding rept_def
[PROOF STATE]
proof (prove)
using this:
l \<in> L
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
abss s = (l, [u]\<^sub>\<R>)
s = (l, u)
\<mu> = return_pmf (abss s)
\<not> (\<forall>c\<in>\<X>. real (k c) < u c)

goal (1 subgoal):
 1. (let (l, u) = s in if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> [u]\<^sub>\<R> = R' \<and> (\<forall>c\<in>\<X>. real (k c) < u c) then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u) else SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)

goal (1 subgoal):
 1. \<not> (\<forall>c\<in>\<X>. real (k c) < u c) \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with \<open>\<mu> = _\<close>
[PROOF STATE]
proof (chain)
picking this:
\<mu> = return_pmf (abss s)
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<mu> = return_pmf (abss s)
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)

goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
by simp (rule someI[where x = "return_pmf s"], auto simp: abst_def)
[PROOF STATE]
proof (state)
this:
rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>

goal (1 subgoal):
 1. s \<notin> S \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<notin> S \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
s \<notin> S

goal (1 subgoal):
 1. s \<notin> S \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with \<open>s = _\<close> \<open>\<mu> = _\<close>
[PROOF STATE]
proof (chain)
picking this:
s = (l, u)
\<mu> = return_pmf (abss s)
s \<notin> S
[PROOF STEP]
have
        "rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)"
[PROOF STATE]
proof (prove)
using this:
s = (l, u)
\<mu> = return_pmf (abss s)
s \<notin> S

goal (1 subgoal):
 1. rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
unfolding rept_def
[PROOF STATE]
proof (prove)
using this:
s = (l, u)
\<mu> = return_pmf (abss s)
s \<notin> S

goal (1 subgoal):
 1. (let (l, u) = s in if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> [u]\<^sub>\<R> = R' \<and> (\<forall>c\<in>\<X>. real (k c) < u c) then return_pmf (l, u \<oplus> 5 / 10) else if \<exists>R'. (l, u) \<in> S \<and> \<mu> = return_pmf (l, R') \<and> R' \<in> Succ \<R> ([u]\<^sub>\<R>) \<and> [u]\<^sub>\<R> \<noteq> R' \<and> (\<forall>u\<in>R'. \<forall>c\<in>\<X>. \<not> (\<exists>d\<le>k c. u c = real d)) then return_pmf (l, delayedR (SOME R'. \<mu> = return_pmf (l, R')) u) else SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>) = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)

goal (1 subgoal):
 1. s \<notin> S \<Longrightarrow> rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
with \<open>\<mu> = _\<close>
[PROOF STATE]
proof (chain)
picking this:
\<mu> = return_pmf (abss s)
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<mu> = return_pmf (abss s)
rept s \<mu> = (SOME \<mu>'. \<mu>' \<in> K s \<and> abst \<mu>' = \<mu>)

goal (1 subgoal):
 1. rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>
[PROOF STEP]
by simp (rule someI[where x = "return_pmf s"], auto simp: abst_def)
[PROOF STATE]
proof (state)
this:
rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rept s \<mu> \<in> K s \<and> abst (rept s \<mu>) = \<mu>

goal:
No subgoals!
[PROOF STEP]
qed