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

goal (1 subgoal):
 1. abst (rept (reps s) \<mu>) = \<mu>
[PROOF STEP]
by auto


[STATEMENT]
lemma rept_K2:
  assumes "\<mu> \<in> \<K> s" "s \<in> \<S>"
  shows "rept (reps s) \<mu> \<in> K (reps s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rept (reps s) \<mu> \<in> K (reps s)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<mu> \<in> \<K> s
s \<in> \<S>

goal (1 subgoal):
 1. rept (reps s) \<mu> \<in> K (reps s)
[PROOF STEP]
by auto


[STATEMENT]
lemma theI':
  assumes "P a"
    and "\<And>x. P x \<Longrightarrow> x = a"
  shows "P (THE x. P x) \<and> (\<forall> y. P y \<longrightarrow> y = (THE x. P x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (THE x. P x) \<and> (\<forall>y. P y \<longrightarrow> y = (THE x. P x))
[PROOF STEP]
using theI assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?P ?a; \<And>x. ?P x \<Longrightarrow> x = ?a\<rbrakk> \<Longrightarrow> ?P (THE x. ?P x)
P a
P ?x5 \<Longrightarrow> ?x5 = a

goal (1 subgoal):
 1. P (THE x. P x) \<and> (\<forall>y. P y \<longrightarrow> y = (THE x. P x))
[PROOF STEP]
by metis


[STATEMENT]
lemma cont_cfg_defined:
  fixes cfg s
  assumes "cfg \<in> valid_cfg" "s \<in> abst (action cfg)"
  defines "x \<equiv> THE x. abss x = s \<and> x \<in> action cfg"
  shows "(abss x = s \<and> x \<in> action cfg) \<and> (\<forall> y. abss y = s \<and> y \<in> action cfg \<longrightarrow> y = x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (abss x = s \<and> x \<in> set_pmf (action cfg)) \<and> (\<forall>y. abss y = s \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (abss x = s \<and> x \<in> set_pmf (action cfg)) \<and> (\<forall>y. abss y = s \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = x)
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
s \<in> set_pmf (abst (action cfg))
[PROOF STEP]
obtain s' where "s' \<in> action cfg" "s = abss s'"
[PROOF STATE]
proof (prove)
using this:
s \<in> set_pmf (abst (action cfg))

goal (1 subgoal):
 1. (\<And>s'. \<lbrakk>s' \<in> set_pmf (action cfg); s = abss s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding abst_def
[PROOF STATE]
proof (prove)
using this:
s \<in> set_pmf (map_pmf abss (action cfg))

goal (1 subgoal):
 1. (\<And>s'. \<lbrakk>s' \<in> set_pmf (action cfg); s = abss s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s' \<in> set_pmf (action cfg)
s = abss s'

goal (1 subgoal):
 1. (abss x = s \<and> x \<in> set_pmf (action cfg)) \<and> (\<forall>y. abss y = s \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = x)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> MDP.valid_cfg
s \<in> set_pmf (abst (action cfg))
x \<equiv> THE x. abss x = s \<and> x \<in> set_pmf (action cfg)
s' \<in> set_pmf (action cfg)
s = abss s'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cfg \<in> MDP.valid_cfg
s \<in> set_pmf (abst (action cfg))
x \<equiv> THE x. abss x = s \<and> x \<in> set_pmf (action cfg)
s' \<in> set_pmf (action cfg)
s = abss s'

goal (1 subgoal):
 1. (abss x = s \<and> x \<in> set_pmf (action cfg)) \<and> (\<forall>y. abss y = s \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = x)
[PROOF STEP]
unfolding x_def
[PROOF STATE]
proof (prove)
using this:
cfg \<in> MDP.valid_cfg
s \<in> set_pmf (abst (action cfg))
THE x. abss x = s \<and> x \<in> set_pmf (action cfg) \<equiv> THE x. abss x = s \<and> x \<in> set_pmf (action cfg)
s' \<in> set_pmf (action cfg)
s = abss s'

goal (1 subgoal):
 1. (abss (THE x. abss x = s \<and> x \<in> set_pmf (action cfg)) = s \<and> (THE x. abss x = s \<and> x \<in> set_pmf (action cfg)) \<in> set_pmf (action cfg)) \<and> (\<forall>y. abss y = s \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = (THE x. abss x = s \<and> x \<in> set_pmf (action cfg)))
[PROOF STEP]
by -(rule theI'[of _ s'],auto intro: K_bisim_unique MDP.valid_cfg_state_in_S dest: MDP.valid_cfgD)
[PROOF STATE]
proof (state)
this:
(abss x = s \<and> x \<in> set_pmf (action cfg)) \<and> (\<forall>y. abss y = s \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<S>_state_absc_repc[simp]:
  "state cfg \<in> \<S> \<Longrightarrow> state (absc (repc cfg)) = state cfg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state cfg \<in> \<S> \<Longrightarrow> state (absc (repc cfg)) = state cfg
[PROOF STEP]
by (simp add: absc_def repc_def repcs_def)


[STATEMENT]
lemma action_repc:
  "action (repc cfg) = rept (reps (state cfg)) (action cfg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. action (repc cfg) = rept (reps (state cfg)) (action cfg)
[PROOF STEP]
unfolding repc_def repcs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. action (cfg_corec (reps (state cfg)) (\<lambda>(s, cfg). rept s (action cfg)) (\<lambda>(s, cfg) s'. (s', cont cfg (abss s'))) (reps (state cfg), cfg)) = rept (reps (state cfg)) (action cfg)
[PROOF STEP]
by simp


[STATEMENT]
lemma action_absc:
  "action (absc cfg) = abst (action cfg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. action (absc cfg) = abst (action cfg)
[PROOF STEP]
unfolding absc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. action (cfg_corec (abss (state cfg)) (abst \<circ> action) (\<lambda>cfg s. cont cfg (THE x. abss x = s \<and> x \<in> set_pmf (action cfg))) cfg) = abst (action cfg)
[PROOF STEP]
by simp


[STATEMENT]
lemma action_absc':
  "action (absc cfg) = map_pmf abss (action cfg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. action (absc cfg) = map_pmf abss (action cfg)
[PROOF STEP]
unfolding absc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. action (cfg_corec (abss (state cfg)) (abst \<circ> action) (\<lambda>cfg s. cont cfg (THE x. abss x = s \<and> x \<in> set_pmf (action cfg))) cfg) = map_pmf abss (action cfg)
[PROOF STEP]
unfolding abst_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. action (cfg_corec (abss (state cfg)) (map_pmf abss \<circ> action) (\<lambda>cfg s. cont cfg (THE x. abss x = s \<and> x \<in> set_pmf (action cfg))) cfg) = map_pmf abss (action cfg)
[PROOF STEP]
by simp


[STATEMENT]
lemma cont_repcs1:
  notes R_G.cfg_onD_state[simp del]
  assumes "abss s \<in> \<S>" "s' \<in> set_pmf (action (repcs s cfg))" "cfg \<in> R_G.cfg_on (abss s)"
  shows "cont (repcs s cfg) s' = repcs s' (cont cfg (abss s'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (repcs s cfg) s' = repcs s' (cont cfg (abss s'))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
abss s \<in> \<S>
s' \<in> set_pmf (action (repcs s cfg))
cfg \<in> R_G.cfg_on (abss s)

goal (1 subgoal):
 1. cont (repcs s cfg) s' = repcs s' (cont cfg (abss s'))
[PROOF STEP]
by (auto simp: repc_def repcs_def abss_reps_id)


[STATEMENT]
lemma cont_absc_1:
  notes MDP.cfg_onD_state[simp del]
  assumes "cfg \<in> valid_cfg" "s' \<in> set_pmf (action cfg)"
  shows "cont (absc cfg) (abss s') = absc (cont cfg s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (absc cfg) (abss s') = absc (cont cfg s')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cont (absc cfg) (abss s') = absc (cont cfg s')
[PROOF STEP]
define x where "x \<equiv> THE x. x ~ s' \<and> x \<in> set_pmf (action cfg)"
[PROOF STATE]
proof (state)
this:
x \<equiv> THE x. x ~ s' \<and> x \<in> set_pmf (action cfg)

goal (1 subgoal):
 1. cont (absc cfg) (abss s') = absc (cont cfg s')
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
s' \<in> set_pmf (action cfg)
[PROOF STEP]
have "abss s' \<in> set_pmf (abst (action cfg))"
[PROOF STATE]
proof (prove)
using this:
s' \<in> set_pmf (action cfg)

goal (1 subgoal):
 1. abss s' \<in> set_pmf (abst (action cfg))
[PROOF STEP]
unfolding abst_def
[PROOF STATE]
proof (prove)
using this:
s' \<in> set_pmf (action cfg)

goal (1 subgoal):
 1. abss s' \<in> set_pmf (map_pmf abss (action cfg))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
abss s' \<in> set_pmf (abst (action cfg))

goal (1 subgoal):
 1. cont (absc cfg) (abss s') = absc (cont cfg s')
[PROOF STEP]
from cont_cfg_defined[OF assms(1) this]
[PROOF STATE]
proof (chain)
picking this:
((THE x. x ~ s' \<and> x \<in> set_pmf (action cfg)) ~ s' \<and> (THE x. x ~ s' \<and> x \<in> set_pmf (action cfg)) \<in> set_pmf (action cfg)) \<and> (\<forall>y. y ~ s' \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = (THE x. x ~ s' \<and> x \<in> set_pmf (action cfg)))
[PROOF STEP]
have
    "(x ~ s' \<and> x \<in> set_pmf (action cfg)) \<and> (\<forall>y. y ~ s' \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = x)"
[PROOF STATE]
proof (prove)
using this:
((THE x. x ~ s' \<and> x \<in> set_pmf (action cfg)) ~ s' \<and> (THE x. x ~ s' \<and> x \<in> set_pmf (action cfg)) \<in> set_pmf (action cfg)) \<and> (\<forall>y. y ~ s' \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = (THE x. x ~ s' \<and> x \<in> set_pmf (action cfg)))

goal (1 subgoal):
 1. (x ~ s' \<and> x \<in> set_pmf (action cfg)) \<and> (\<forall>y. y ~ s' \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = x)
[PROOF STEP]
unfolding x_def
[PROOF STATE]
proof (prove)
using this:
((THE x. x ~ s' \<and> x \<in> set_pmf (action cfg)) ~ s' \<and> (THE x. x ~ s' \<and> x \<in> set_pmf (action cfg)) \<in> set_pmf (action cfg)) \<and> (\<forall>y. y ~ s' \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = (THE x. x ~ s' \<and> x \<in> set_pmf (action cfg)))

goal (1 subgoal):
 1. ((THE x. x ~ s' \<and> x \<in> set_pmf (action cfg)) ~ s' \<and> (THE x. x ~ s' \<and> x \<in> set_pmf (action cfg)) \<in> set_pmf (action cfg)) \<and> (\<forall>y. y ~ s' \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = (THE x. x ~ s' \<and> x \<in> set_pmf (action cfg)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(x ~ s' \<and> x \<in> set_pmf (action cfg)) \<and> (\<forall>y. y ~ s' \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = x)

goal (1 subgoal):
 1. cont (absc cfg) (abss s') = absc (cont cfg s')
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> MDP.valid_cfg
s' \<in> set_pmf (action cfg)
(x ~ s' \<and> x \<in> set_pmf (action cfg)) \<and> (\<forall>y. y ~ s' \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = x)
[PROOF STEP]
have "s' = x"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> MDP.valid_cfg
s' \<in> set_pmf (action cfg)
(x ~ s' \<and> x \<in> set_pmf (action cfg)) \<and> (\<forall>y. y ~ s' \<and> y \<in> set_pmf (action cfg) \<longrightarrow> y = x)

goal (1 subgoal):
 1. s' = x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
s' = x

goal (1 subgoal):
 1. cont (absc cfg) (abss s') = absc (cont cfg s')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s' = x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s' = x

goal (1 subgoal):
 1. cont (absc cfg) (abss s') = absc (cont cfg s')
[PROOF STEP]
unfolding absc_def abst_def repc_def x_def
[PROOF STATE]
proof (prove)
using this:
s' = (THE x. x ~ s' \<and> x \<in> set_pmf (action cfg))

goal (1 subgoal):
 1. cont (cfg_corec (abss (state cfg)) (map_pmf abss \<circ> action) (\<lambda>cfg s. cont cfg (THE x. abss x = s \<and> x \<in> set_pmf (action cfg))) cfg) (abss s') = cfg_corec (abss (state (cont cfg s'))) (map_pmf abss \<circ> action) (\<lambda>cfg s. cont cfg (THE x. abss x = s \<and> x \<in> set_pmf (action cfg))) (cont cfg s')
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
s' = (THE x. x ~ s' \<and> x \<in> set_pmf (action cfg))
s' \<in> set_pmf (action cfg)

goal (1 subgoal):
 1. cont (cfg_corec (abss (state cfg)) (map_pmf abss \<circ> action) (\<lambda>cfg s. cont cfg (THE x. abss x = s \<and> x \<in> set_pmf (action cfg))) cfg) (abss s') = cfg_corec (abss (state (cont cfg s'))) (map_pmf abss \<circ> action) (\<lambda>cfg s. cont cfg (THE x. abss x = s \<and> x \<in> set_pmf (action cfg))) (cont cfg s')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cont (absc cfg) (abss s') = absc (cont cfg s')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma state_repc:
  "state (repc cfg) = reps (state cfg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state (repc cfg) = reps (state cfg)
[PROOF STEP]
unfolding repc_def repcs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state (cfg_corec (reps (state cfg)) (\<lambda>(s, cfg). rept s (action cfg)) (\<lambda>(s, cfg) s'. (s', cont cfg (abss s'))) (reps (state cfg), cfg)) = reps (state cfg)
[PROOF STEP]
by simp


[STATEMENT]
lemma abss_reps_id':
  notes R_G.cfg_onD_state[simp del]
  assumes "cfg \<in> R_G.valid_cfg" "s \<in> set_pmf (action cfg)"
  shows "abss (reps s) = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abss (reps s) = s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
s \<in> set_pmf (action cfg)

goal (1 subgoal):
 1. abss (reps s) = s
[PROOF STEP]
by (auto intro: abss_reps_id R_G.valid_cfg_state_in_S R_G.valid_cfgD)


[STATEMENT]
lemma valid_cfg_coinduct[coinduct set: valid_cfg]:
  assumes "P cfg"
  assumes "\<And>cfg. P cfg \<Longrightarrow> state cfg \<in> S"
  assumes "\<And>cfg. P cfg \<Longrightarrow> action cfg \<in> K (state cfg)"
  assumes "\<And>cfg t. P cfg \<Longrightarrow> t \<in> action cfg \<Longrightarrow> P (cont cfg t)"
  shows "cfg \<in> valid_cfg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfg \<in> MDP.valid_cfg
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cfg \<in> MDP.valid_cfg
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
P cfg
P ?cfg5 \<Longrightarrow> state ?cfg5 \<in> S
P ?cfg5 \<Longrightarrow> action ?cfg5 \<in> K (state ?cfg5)
\<lbrakk>P ?cfg5; ?t5 \<in> set_pmf (action ?cfg5)\<rbrakk> \<Longrightarrow> P (cont ?cfg5 ?t5)
[PROOF STEP]
have "cfg \<in> MDP.cfg_on (state cfg)"
[PROOF STATE]
proof (prove)
using this:
P cfg
P ?cfg5 \<Longrightarrow> state ?cfg5 \<in> S
P ?cfg5 \<Longrightarrow> action ?cfg5 \<in> K (state ?cfg5)
\<lbrakk>P ?cfg5; ?t5 \<in> set_pmf (action ?cfg5)\<rbrakk> \<Longrightarrow> P (cont ?cfg5 ?t5)

goal (1 subgoal):
 1. cfg \<in> MDP.cfg_on (state cfg)
[PROOF STEP]
by (coinduction arbitrary: cfg) auto
[PROOF STATE]
proof (state)
this:
cfg \<in> MDP.cfg_on (state cfg)

goal (1 subgoal):
 1. cfg \<in> MDP.valid_cfg
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cfg \<in> MDP.cfg_on (state cfg)

goal (1 subgoal):
 1. cfg \<in> MDP.valid_cfg
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
P cfg
P ?cfg5 \<Longrightarrow> state ?cfg5 \<in> S
P ?cfg5 \<Longrightarrow> action ?cfg5 \<in> K (state ?cfg5)
\<lbrakk>P ?cfg5; ?t5 \<in> set_pmf (action ?cfg5)\<rbrakk> \<Longrightarrow> P (cont ?cfg5 ?t5)
[PROOF STEP]
have "state cfg \<in> S"
[PROOF STATE]
proof (prove)
using this:
P cfg
P ?cfg5 \<Longrightarrow> state ?cfg5 \<in> S
P ?cfg5 \<Longrightarrow> action ?cfg5 \<in> K (state ?cfg5)
\<lbrakk>P ?cfg5; ?t5 \<in> set_pmf (action ?cfg5)\<rbrakk> \<Longrightarrow> P (cont ?cfg5 ?t5)

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

goal (1 subgoal):
 1. cfg \<in> MDP.valid_cfg
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> MDP.cfg_on (state cfg)
state cfg \<in> S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cfg \<in> MDP.cfg_on (state cfg)
state cfg \<in> S

goal (1 subgoal):
 1. cfg \<in> MDP.valid_cfg
[PROOF STEP]
by (intro MDP.valid_cfgI)
[PROOF STATE]
proof (state)
this:
cfg \<in> MDP.valid_cfg

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma state_repcD[simp]:
  assumes "cfg \<in> R_G.cfg_on s"
  shows "state (repc cfg) = reps s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state (repc cfg) = reps s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.cfg_on s

goal (1 subgoal):
 1. state (repc cfg) = reps s
[PROOF STEP]
unfolding repc_def repcs_def
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.cfg_on s

goal (1 subgoal):
 1. state (cfg_corec (reps (state cfg)) (\<lambda>(s, cfg). rept s (action cfg)) (\<lambda>(s, cfg) s'. (s', cont cfg (abss s'))) (reps (state cfg), cfg)) = reps s
[PROOF STEP]
by auto


[STATEMENT]
lemma ccompatible_subs[intro]:
  assumes "ccompatible \<R> g" "R \<in> \<R>" "u \<in> R" "u \<turnstile> g"
  shows "R \<subseteq> {u. u \<turnstile> g}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> {u. u \<turnstile> g}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ccompatible \<R> g
R \<in> \<R>
u \<in> R
u \<turnstile> g

goal (1 subgoal):
 1. R \<subseteq> {u. u \<turnstile> g}
[PROOF STEP]
unfolding ccompatible_def
[PROOF STATE]
proof (prove)
using this:
\<forall>R\<in>\<R>. R \<subseteq> {v. v \<turnstile> g} \<or> {v. v \<turnstile> g} \<inter> R = {}
R \<in> \<R>
u \<in> R
u \<turnstile> g

goal (1 subgoal):
 1. R \<subseteq> {u. u \<turnstile> g}
[PROOF STEP]
by auto


[STATEMENT]
lemma action_abscD[dest]:
  "cfg \<in> MDP.cfg_on s \<Longrightarrow> action (absc cfg) \<in> \<K> (abss s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfg \<in> MDP.cfg_on s \<Longrightarrow> action (absc cfg) \<in> \<K> (abss s)
[PROOF STEP]
unfolding absc_def abst_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfg \<in> MDP.cfg_on s \<Longrightarrow> action (cfg_corec (abss (state cfg)) (map_pmf abss \<circ> action) (\<lambda>cfg s. cont cfg (THE x. abss x = s \<and> x \<in> set_pmf (action cfg))) cfg) \<in> \<K> (abss s)
[PROOF STEP]
proof simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cfg \<in> MDP.cfg_on s \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
assume cfg: "cfg \<in> MDP.cfg_on s"
[PROOF STATE]
proof (state)
this:
cfg \<in> MDP.cfg_on s

goal (1 subgoal):
 1. cfg \<in> MDP.cfg_on s \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> MDP.cfg_on s
[PROOF STEP]
have "action cfg \<in> K s"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> MDP.cfg_on s

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

goal (1 subgoal):
 1. cfg \<in> MDP.cfg_on s \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
action cfg \<in> K s
[PROOF STEP]
show "map_pmf abss (action cfg) \<in> \<K> (abss s)"
[PROOF STATE]
proof (prove)
using this:
action cfg \<in> K s

goal (1 subgoal):
 1. map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>l u t. \<lbrakk>action cfg = return_pmf (l, u \<oplus> t); s \<in> S; s = (l, u); 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l\<rbrakk> \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
 2. \<And>l u g \<mu>. \<lbrakk>action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>; s \<in> S; s = (l, u); (l, g, \<mu>) \<in> PTA.trans_of A; u \<turnstile> g\<rbrakk> \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
 3. action cfg = return_pmf s \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
case prems: (delay l u t)
[PROOF STATE]
proof (state)
this:
action cfg = return_pmf (l, u \<oplus> t)
s \<in> S
s = (l, u)
0 \<le> t
u \<oplus> t \<turnstile> PTA.inv_of A l

goal (3 subgoals):
 1. \<And>l u t. \<lbrakk>action cfg = return_pmf (l, u \<oplus> t); s \<in> S; s = (l, u); 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l\<rbrakk> \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
 2. \<And>l u g \<mu>. \<lbrakk>action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>; s \<in> S; s = (l, u); (l, g, \<mu>) \<in> PTA.trans_of A; u \<turnstile> g\<rbrakk> \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
 3. action cfg = return_pmf s \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
action cfg = return_pmf (l, u \<oplus> t)
s \<in> S
s = (l, u)
0 \<le> t
u \<oplus> t \<turnstile> PTA.inv_of A l
[PROOF STEP]
have "[u \<oplus> t]\<^sub>\<R> \<in> \<R>"
[PROOF STATE]
proof (prove)
using this:
action cfg = return_pmf (l, u \<oplus> t)
s \<in> S
s = (l, u)
0 \<le> t
u \<oplus> t \<turnstile> PTA.inv_of A l

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

goal (3 subgoals):
 1. \<And>l u t. \<lbrakk>action cfg = return_pmf (l, u \<oplus> t); s \<in> S; s = (l, u); 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l\<rbrakk> \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
 2. \<And>l u g \<mu>. \<lbrakk>action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>; s \<in> S; s = (l, u); (l, g, \<mu>) \<in> PTA.trans_of A; u \<turnstile> g\<rbrakk> \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
 3. action cfg = return_pmf s \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[u \<oplus> t]\<^sub>\<R> \<in> \<R>

goal (3 subgoals):
 1. \<And>l u t. \<lbrakk>action cfg = return_pmf (l, u \<oplus> t); s \<in> S; s = (l, u); 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l\<rbrakk> \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
 2. \<And>l u g \<mu>. \<lbrakk>action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>; s \<in> S; s = (l, u); (l, g, \<mu>) \<in> PTA.trans_of A; u \<turnstile> g\<rbrakk> \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
 3. action cfg = return_pmf s \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
with prems ccompatible_inv[of l]
[PROOF STATE]
proof (chain)
picking this:
action cfg = return_pmf (l, u \<oplus> t)
s \<in> S
s = (l, u)
0 \<le> t
u \<oplus> t \<turnstile> PTA.inv_of A l
ccompatible \<R> (PTA.inv_of A l)
[u \<oplus> t]\<^sub>\<R> \<in> \<R>
[PROOF STEP]
have
      "[u \<oplus> t]\<^sub>\<R> \<subseteq> {v. v \<turnstile> PTA.inv_of A l}"
[PROOF STATE]
proof (prove)
using this:
action cfg = return_pmf (l, u \<oplus> t)
s \<in> S
s = (l, u)
0 \<le> t
u \<oplus> t \<turnstile> PTA.inv_of A l
ccompatible \<R> (PTA.inv_of A l)
[u \<oplus> t]\<^sub>\<R> \<in> \<R>

goal (1 subgoal):
 1. [u \<oplus> t]\<^sub>\<R> \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
[PROOF STEP]
unfolding ccompatible_def
[PROOF STATE]
proof (prove)
using this:
action cfg = return_pmf (l, u \<oplus> t)
s \<in> S
s = (l, u)
0 \<le> t
u \<oplus> t \<turnstile> PTA.inv_of A l
\<forall>R\<in>\<R>. R \<subseteq> {v. v \<turnstile> PTA.inv_of A l} \<or> {v. v \<turnstile> PTA.inv_of A l} \<inter> R = {}
[u \<oplus> t]\<^sub>\<R> \<in> \<R>

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

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

goal (3 subgoals):
 1. \<And>l u t. \<lbrakk>action cfg = return_pmf (l, u \<oplus> t); s \<in> S; s = (l, u); 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l\<rbrakk> \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
 2. \<And>l u g \<mu>. \<lbrakk>action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>; s \<in> S; s = (l, u); (l, g, \<mu>) \<in> PTA.trans_of A; u \<turnstile> g\<rbrakk> \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
 3. action cfg = return_pmf s \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
action cfg = return_pmf (l, u \<oplus> t)
s \<in> S
s = (l, u)
0 \<le> t
u \<oplus> t \<turnstile> PTA.inv_of A l
[PROOF STEP]
have "abss (l, u \<oplus> t) = (l, [u \<oplus> t]\<^sub>\<R>)"
[PROOF STATE]
proof (prove)
using this:
action cfg = return_pmf (l, u \<oplus> t)
s \<in> S
s = (l, u)
0 \<le> t
u \<oplus> t \<turnstile> PTA.inv_of A l

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

goal (3 subgoals):
 1. \<And>l u t. \<lbrakk>action cfg = return_pmf (l, u \<oplus> t); s \<in> S; s = (l, u); 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l\<rbrakk> \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
 2. \<And>l u g \<mu>. \<lbrakk>action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>; s \<in> S; s = (l, u); (l, g, \<mu>) \<in> PTA.trans_of A; u \<turnstile> g\<rbrakk> \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
 3. action cfg = return_pmf s \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[u \<oplus> t]\<^sub>\<R> \<in> \<R>
[u \<oplus> t]\<^sub>\<R> \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
abss (l, u \<oplus> t) = (l, [u \<oplus> t]\<^sub>\<R>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[u \<oplus> t]\<^sub>\<R> \<in> \<R>
[u \<oplus> t]\<^sub>\<R> \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
abss (l, u \<oplus> t) = (l, [u \<oplus> t]\<^sub>\<R>)

goal (1 subgoal):
 1. map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
using prems
[PROOF STATE]
proof (prove)
using this:
[u \<oplus> t]\<^sub>\<R> \<in> \<R>
[u \<oplus> t]\<^sub>\<R> \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
abss (l, u \<oplus> t) = (l, [u \<oplus> t]\<^sub>\<R>)
action cfg = return_pmf (l, u \<oplus> t)
s \<in> S
s = (l, u)
0 \<le> t
u \<oplus> t \<turnstile> PTA.inv_of A l

goal (1 subgoal):
 1. map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map_pmf abss (action cfg) \<in> \<K> (abss s)

goal (2 subgoals):
 1. \<And>l u g \<mu>. \<lbrakk>action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>; s \<in> S; s = (l, u); (l, g, \<mu>) \<in> PTA.trans_of A; u \<turnstile> g\<rbrakk> \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
 2. action cfg = return_pmf s \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l u g \<mu>. \<lbrakk>action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>; s \<in> S; s = (l, u); (l, g, \<mu>) \<in> PTA.trans_of A; u \<turnstile> g\<rbrakk> \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
 2. action cfg = return_pmf s \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
case prems: (action l u g \<mu>)
[PROOF STATE]
proof (state)
this:
action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>
s \<in> S
s = (l, u)
(l, g, \<mu>) \<in> PTA.trans_of A
u \<turnstile> g

goal (2 subgoals):
 1. \<And>l u g \<mu>. \<lbrakk>action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>; s \<in> S; s = (l, u); (l, g, \<mu>) \<in> PTA.trans_of A; u \<turnstile> g\<rbrakk> \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
 2. action cfg = return_pmf s \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>
s \<in> S
s = (l, u)
(l, g, \<mu>) \<in> PTA.trans_of A
u \<turnstile> g
[PROOF STEP]
have "[u]\<^sub>\<R> \<in> \<R>"
[PROOF STATE]
proof (prove)
using this:
action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>
s \<in> S
s = (l, u)
(l, g, \<mu>) \<in> PTA.trans_of A
u \<turnstile> g

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

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

goal (2 subgoals):
 1. \<And>l u g \<mu>. \<lbrakk>action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>; s \<in> S; s = (l, u); (l, g, \<mu>) \<in> PTA.trans_of A; u \<turnstile> g\<rbrakk> \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
 2. action cfg = return_pmf s \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
with prems ccompatible_guard
[PROOF STATE]
proof (chain)
picking this:
action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>
s \<in> S
s = (l, u)
(l, g, \<mu>) \<in> PTA.trans_of A
u \<turnstile> g
(?l, ?g, ?\<mu>) \<in> PTA.trans_of A \<Longrightarrow> ccompatible \<R> ?g
[u]\<^sub>\<R> \<in> \<R>
[PROOF STEP]
have "[u]\<^sub>\<R> \<subseteq> {u. u \<turnstile> g}"
[PROOF STATE]
proof (prove)
using this:
action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>
s \<in> S
s = (l, u)
(l, g, \<mu>) \<in> PTA.trans_of A
u \<turnstile> g
(?l, ?g, ?\<mu>) \<in> PTA.trans_of A \<Longrightarrow> ccompatible \<R> ?g
[u]\<^sub>\<R> \<in> \<R>

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

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

goal (2 subgoals):
 1. \<And>l u g \<mu>. \<lbrakk>action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>; s \<in> S; s = (l, u); (l, g, \<mu>) \<in> PTA.trans_of A; u \<turnstile> g\<rbrakk> \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
 2. action cfg = return_pmf s \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
have
      "map_pmf abss (action cfg)
      = map_pmf (\<lambda>(X, l). (l, region_set' ([u]\<^sub>\<R>) (SOME r. set r = X) 0)) \<mu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf abss (action cfg) = map_pmf (\<lambda>(X, l). (l, [X::=0]([u]\<^sub>\<R>))) \<mu>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_pmf abss (action cfg) = map_pmf (\<lambda>(X, l). (l, [X::=0]([u]\<^sub>\<R>))) \<mu>
[PROOF STEP]
have "abss (l', [X:=0]u) = (l', region_set' ([u]\<^sub>\<R>) (SOME r. set r = X) 0)"
        if "(X, l') \<in> \<mu>" for X l'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abss (l', [(SOME r. set r = X)\<rightarrow>0]u) = (l', [X::=0]([u]\<^sub>\<R>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. abss (l', [(SOME r. set r = X)\<rightarrow>0]u) = (l', [X::=0]([u]\<^sub>\<R>))
[PROOF STEP]
from that prems
[PROOF STATE]
proof (chain)
picking this:
(X, l') \<in> set_pmf \<mu>
action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>
s \<in> S
s = (l, u)
(l, g, \<mu>) \<in> PTA.trans_of A
u \<turnstile> g
[PROOF STEP]
have "A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l'"
[PROOF STATE]
proof (prove)
using this:
(X, l') \<in> set_pmf \<mu>
action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>
s \<in> S
s = (l, u)
(l, g, \<mu>) \<in> PTA.trans_of A
u \<turnstile> g

goal (1 subgoal):
 1. A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l'

goal (1 subgoal):
 1. abss (l', [(SOME r. set r = X)\<rightarrow>0]u) = (l', [X::=0]([u]\<^sub>\<R>))
[PROOF STEP]
from that prems MDP.action_closed[OF _ cfg]
[PROOF STATE]
proof (chain)
picking this:
(X, l') \<in> set_pmf \<mu>
action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>
s \<in> S
s = (l, u)
(l, g, \<mu>) \<in> PTA.trans_of A
u \<turnstile> g
\<lbrakk>s \<in> S; ?t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> ?t \<in> S
[PROOF STEP]
have "(l', [X:=0]u) \<in> S"
[PROOF STATE]
proof (prove)
using this:
(X, l') \<in> set_pmf \<mu>
action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>
s \<in> S
s = (l, u)
(l, g, \<mu>) \<in> PTA.trans_of A
u \<turnstile> g
\<lbrakk>s \<in> S; ?t \<in> set_pmf (action cfg)\<rbrakk> \<Longrightarrow> ?t \<in> S

goal (1 subgoal):
 1. (l', [(SOME r. set r = X)\<rightarrow>0]u) \<in> S
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
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', [X::=0]([u]\<^sub>\<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. abss (l', [(SOME r. set r = X)\<rightarrow>0]u) = (l', [X::=0]([u]\<^sub>\<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. abss (l', [(SOME r. set r = X)\<rightarrow>0]u) = (l', [X::=0]([u]\<^sub>\<R>))
[PROOF STEP]
have
          "\<dots> = (l', region_set' ([u]\<^sub>\<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]([u]\<^sub>\<R>))
[PROOF STEP]
using region_set'_eq(1)[OF _ _ \<open>A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l'\<close>] prems
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?R \<in> \<R>; ?u \<in> ?R\<rbrakk> \<Longrightarrow> [[(SOME r. set r = X)\<rightarrow>0]?u]\<^sub>\<R> = [X::=0]?R
action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>
s \<in> S
s = (l, u)
(l, g, \<mu>) \<in> PTA.trans_of A
u \<turnstile> g

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

goal (1 subgoal):
 1. abss (l', [(SOME r. set r = X)\<rightarrow>0]u) = (l', [X::=0]([u]\<^sub>\<R>))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
abss (l', [(SOME r. set r = X)\<rightarrow>0]u) = (l', [X::=0]([u]\<^sub>\<R>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
abss (l', [(SOME r. set r = X)\<rightarrow>0]u) = (l', [X::=0]([u]\<^sub>\<R>))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(?X5, ?l'5) \<in> set_pmf \<mu> \<Longrightarrow> abss (?l'5, [(SOME r. set r = ?X5)\<rightarrow>0]u) = (?l'5, [?X5::=0]([u]\<^sub>\<R>))

goal (1 subgoal):
 1. map_pmf abss (action cfg) = map_pmf (\<lambda>(X, l). (l, [X::=0]([u]\<^sub>\<R>))) \<mu>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?X5, ?l'5) \<in> set_pmf \<mu> \<Longrightarrow> abss (?l'5, [(SOME r. set r = ?X5)\<rightarrow>0]u) = (?l'5, [?X5::=0]([u]\<^sub>\<R>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(?X5, ?l'5) \<in> set_pmf \<mu> \<Longrightarrow> abss (?l'5, [(SOME r. set r = ?X5)\<rightarrow>0]u) = (?l'5, [?X5::=0]([u]\<^sub>\<R>))

goal (1 subgoal):
 1. map_pmf abss (action cfg) = map_pmf (\<lambda>(X, l). (l, [X::=0]([u]\<^sub>\<R>))) \<mu>
[PROOF STEP]
unfolding prems(1)
[PROOF STATE]
proof (prove)
using this:
(?X5, ?l'5) \<in> set_pmf \<mu> \<Longrightarrow> abss (?l'5, [(SOME r. set r = ?X5)\<rightarrow>0]u) = (?l'5, [?X5::=0]([u]\<^sub>\<R>))

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]([u]\<^sub>\<R>))) \<mu>
[PROOF STEP]
by (auto intro: pmf.map_cong simp: map_pmf_comp)
[PROOF STATE]
proof (state)
this:
map_pmf abss (action cfg) = map_pmf (\<lambda>(X, l). (l, [X::=0]([u]\<^sub>\<R>))) \<mu>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
map_pmf abss (action cfg) = map_pmf (\<lambda>(X, l). (l, [X::=0]([u]\<^sub>\<R>))) \<mu>

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

goal (1 subgoal):
 1. map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
using prems
[PROOF STATE]
proof (prove)
using this:
[u]\<^sub>\<R> \<in> \<R>
[u]\<^sub>\<R> \<subseteq> {u. u \<turnstile> g}
map_pmf abss (action cfg) = map_pmf (\<lambda>(X, l). (l, [X::=0]([u]\<^sub>\<R>))) \<mu>
action cfg = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>
s \<in> S
s = (l, u)
(l, g, \<mu>) \<in> PTA.trans_of A
u \<turnstile> g

goal (1 subgoal):
 1. map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map_pmf abss (action cfg) \<in> \<K> (abss s)

goal (1 subgoal):
 1. action cfg = return_pmf s \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. action cfg = return_pmf s \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
case prems: loop
[PROOF STATE]
proof (state)
this:
action cfg = return_pmf s

goal (1 subgoal):
 1. action cfg = return_pmf s \<Longrightarrow> map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
action cfg = return_pmf s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
action cfg = return_pmf s

goal (1 subgoal):
 1. map_pmf abss (action cfg) \<in> \<K> (abss s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map_pmf abss (action cfg) \<in> \<K> (abss s)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
map_pmf abss (action cfg) \<in> \<K> (abss s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma repcs_valid[intro]:
  assumes "cfg \<in> R_G.valid_cfg" "abss s = state cfg"
  shows "repcs s cfg \<in> valid_cfg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. repcs s cfg \<in> MDP.valid_cfg
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg

goal (1 subgoal):
 1. repcs s cfg \<in> MDP.valid_cfg
[PROOF STEP]
proof (coinduction arbitrary: cfg s)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>cfga s. \<lbrakk>cfga \<in> R_G.valid_cfg; abss s = state cfga\<rbrakk> \<Longrightarrow> state (repcs s cfga) \<in> S
 2. \<And>cfga s. \<lbrakk>cfga \<in> R_G.valid_cfg; abss s = state cfga\<rbrakk> \<Longrightarrow> action (repcs s cfga) \<in> K (state (repcs s cfga))
 3. \<And>t cfga s. \<lbrakk>cfga \<in> R_G.valid_cfg; abss s = state cfga; t \<in> set_pmf (action (repcs s cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg sa. cont (repcs s cfga) t = repcs sa cfg \<and> cfg \<in> R_G.valid_cfg \<and> abss sa = state cfg
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
cfga \<in> R_G.valid_cfg
abss s = state cfga

goal (3 subgoals):
 1. \<And>cfga s. \<lbrakk>cfga \<in> R_G.valid_cfg; abss s = state cfga\<rbrakk> \<Longrightarrow> state (repcs s cfga) \<in> S
 2. \<And>cfga s. \<lbrakk>cfga \<in> R_G.valid_cfg; abss s = state cfga\<rbrakk> \<Longrightarrow> action (repcs s cfga) \<in> K (state (repcs s cfga))
 3. \<And>t cfga s. \<lbrakk>cfga \<in> R_G.valid_cfg; abss s = state cfga; t \<in> set_pmf (action (repcs s cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg sa. cont (repcs s cfga) t = repcs sa cfg \<and> cfg \<in> R_G.valid_cfg \<and> abss sa = state cfg
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cfga \<in> R_G.valid_cfg
abss s = state cfga
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
cfga \<in> R_G.valid_cfg
abss s = state cfga

goal (1 subgoal):
 1. state (repcs s cfga) \<in> S
[PROOF STEP]
by (auto simp: repcs_def \<S>_abss_S dest: R_G.valid_cfg_state_in_S)
[PROOF STATE]
proof (state)
this:
state (repcs s cfga) \<in> S

goal (2 subgoals):
 1. \<And>cfga s. \<lbrakk>cfga \<in> R_G.valid_cfg; abss s = state cfga\<rbrakk> \<Longrightarrow> action (repcs s cfga) \<in> K (state (repcs s cfga))
 2. \<And>t cfga s. \<lbrakk>cfga \<in> R_G.valid_cfg; abss s = state cfga; t \<in> set_pmf (action (repcs s cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg sa. cont (repcs s cfga) t = repcs sa cfg \<and> cfg \<in> R_G.valid_cfg \<and> abss sa = state cfg
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>cfga s. \<lbrakk>cfga \<in> R_G.valid_cfg; abss s = state cfga\<rbrakk> \<Longrightarrow> action (repcs s cfga) \<in> K (state (repcs s cfga))
 2. \<And>t cfga s. \<lbrakk>cfga \<in> R_G.valid_cfg; abss s = state cfga; t \<in> set_pmf (action (repcs s cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg sa. cont (repcs s cfga) t = repcs sa cfg \<and> cfg \<in> R_G.valid_cfg \<and> abss sa = state cfg
[PROOF STEP]
case (2 cfg' s)
[PROOF STATE]
proof (state)
this:
cfg' \<in> R_G.valid_cfg
abss s = state cfg'

goal (2 subgoals):
 1. \<And>cfga s. \<lbrakk>cfga \<in> R_G.valid_cfg; abss s = state cfga\<rbrakk> \<Longrightarrow> action (repcs s cfga) \<in> K (state (repcs s cfga))
 2. \<And>t cfga s. \<lbrakk>cfga \<in> R_G.valid_cfg; abss s = state cfga; t \<in> set_pmf (action (repcs s cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg sa. cont (repcs s cfga) t = repcs sa cfg \<and> cfg \<in> R_G.valid_cfg \<and> abss sa = state cfg
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cfg' \<in> R_G.valid_cfg
abss s = state cfg'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
cfg' \<in> R_G.valid_cfg
abss s = state cfg'

goal (1 subgoal):
 1. action (repcs s cfg') \<in> K (state (repcs s cfg'))
[PROOF STEP]
by (simp add: repcs_def) (rule rept_K, auto dest: R_G.valid_cfgD)
[PROOF STATE]
proof (state)
this:
action (repcs s cfg') \<in> K (state (repcs s cfg'))

goal (1 subgoal):
 1. \<And>t cfga s. \<lbrakk>cfga \<in> R_G.valid_cfg; abss s = state cfga; t \<in> set_pmf (action (repcs s cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg sa. cont (repcs s cfga) t = repcs sa cfg \<and> cfg \<in> R_G.valid_cfg \<and> abss sa = state cfg
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t cfga s. \<lbrakk>cfga \<in> R_G.valid_cfg; abss s = state cfga; t \<in> set_pmf (action (repcs s cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg sa. cont (repcs s cfga) t = repcs sa cfg \<and> cfg \<in> R_G.valid_cfg \<and> abss sa = state cfg
[PROOF STEP]
case prems: (3 s' cfg)
[PROOF STATE]
proof (state)
this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action (repcs s cfg))

goal (1 subgoal):
 1. \<And>t cfga s. \<lbrakk>cfga \<in> R_G.valid_cfg; abss s = state cfga; t \<in> set_pmf (action (repcs s cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg sa. cont (repcs s cfga) t = repcs sa cfg \<and> cfg \<in> R_G.valid_cfg \<and> abss sa = state cfg
[PROOF STEP]
let ?cfg = "cont cfg (abss s')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t cfga s. \<lbrakk>cfga \<in> R_G.valid_cfg; abss s = state cfga; t \<in> set_pmf (action (repcs s cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg sa. cont (repcs s cfga) t = repcs sa cfg \<and> cfg \<in> R_G.valid_cfg \<and> abss sa = state cfg
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action (repcs s cfg))
[PROOF STEP]
have "abss s' \<in> abst (rept s (action cfg))"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action (repcs s cfg))

goal (1 subgoal):
 1. abss s' \<in> set_pmf (abst (rept s (action cfg)))
[PROOF STEP]
unfolding repcs_def abst_def
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action (cfg_corec s (\<lambda>(s, cfg). rept s (action cfg)) (\<lambda>(s, cfg) s'. (s', cont cfg (abss s'))) (s, cfg)))

goal (1 subgoal):
 1. abss s' \<in> set_pmf (map_pmf abss (rept s (action cfg)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
abss s' \<in> set_pmf (abst (rept s (action cfg)))

goal (1 subgoal):
 1. \<And>t cfga s. \<lbrakk>cfga \<in> R_G.valid_cfg; abss s = state cfga; t \<in> set_pmf (action (repcs s cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg sa. cont (repcs s cfga) t = repcs sa cfg \<and> cfg \<in> R_G.valid_cfg \<and> abss sa = state cfg
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action (repcs s cfg))
abss s' \<in> set_pmf (abst (rept s (action cfg)))
[PROOF STEP]
have
    "abss s' \<in> action cfg"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action (repcs s cfg))
abss s' \<in> set_pmf (abst (rept s (action cfg)))

goal (1 subgoal):
 1. abss s' \<in> set_pmf (action cfg)
[PROOF STEP]
by (subst (asm) abst_rept_id) (auto dest: R_G.valid_cfgD)
[PROOF STATE]
proof (state)
this:
abss s' \<in> set_pmf (action cfg)

goal (1 subgoal):
 1. \<And>t cfga s. \<lbrakk>cfga \<in> R_G.valid_cfg; abss s = state cfga; t \<in> set_pmf (action (repcs s cfga))\<rbrakk> \<Longrightarrow> \<exists>cfg sa. cont (repcs s cfga) t = repcs sa cfg \<and> cfg \<in> R_G.valid_cfg \<and> abss sa = state cfg
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action (repcs s cfg))
abss s' \<in> set_pmf (action cfg)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
s' \<in> set_pmf (action (repcs s cfg))
abss s' \<in> set_pmf (action cfg)

goal (1 subgoal):
 1. \<exists>cfg s. cont (repcs s cfg) s' = repcs s cfg \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg
[PROOF STEP]
by (inst_existentials ?cfg s', subst cont_repcs1)
       (auto dest: R_G.valid_cfg_state_in_S intro: R_G.valid_cfgD R_G.valid_cfg_cont)
[PROOF STATE]
proof (state)
this:
\<exists>cfg s. cont (repcs s cfg) s' = repcs s cfg \<and> cfg \<in> R_G.valid_cfg \<and> abss s = state cfg

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma repc_valid[intro]:
  assumes "cfg \<in> R_G.valid_cfg"
  shows "repc cfg \<in> valid_cfg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. repc cfg \<in> MDP.valid_cfg
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg

goal (1 subgoal):
 1. repc cfg \<in> MDP.valid_cfg
[PROOF STEP]
unfolding repc_def
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg

goal (1 subgoal):
 1. repcs (reps (state cfg)) cfg \<in> MDP.valid_cfg
[PROOF STEP]
by (force dest: R_G.valid_cfg_state_in_S)


[STATEMENT]
lemma action_abst_repcs:
  assumes "cfg \<in> R_G.valid_cfg" "abss s = state cfg"
  shows "abst (action (repcs s cfg)) = action cfg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abst (action (repcs s cfg)) = action cfg
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. abst (action (repcs s cfg)) = action cfg
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
abss s = state cfg
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg

goal (1 subgoal):
 1. abst (action (repcs s cfg)) = action cfg
[PROOF STEP]
unfolding repc_def repcs_def
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
abss s = state cfg

goal (1 subgoal):
 1. abst (action (cfg_corec s (\<lambda>(s, cfg). rept s (action cfg)) (\<lambda>(s, cfg) s'. (s', cont cfg (abss s'))) (s, cfg))) = action cfg
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> abst (rept s (action cfg)) = action cfg
[PROOF STEP]
apply (subst abst_rept_id)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> action cfg \<in> \<K> (abss s)
 2. \<lbrakk>cfg \<in> R_G.valid_cfg; abss s = state cfg\<rbrakk> \<Longrightarrow> action cfg = action cfg
[PROOF STEP]
by (auto dest: R_G.cfg_onD_action R_G.valid_cfgD)
[PROOF STATE]
proof (state)
this:
abst (action (repcs s cfg)) = action cfg

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma action_abst_repc:
  assumes "cfg \<in> R_G.valid_cfg"
  shows "abst (action (repc cfg)) = action cfg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abst (action (repc cfg)) = action cfg
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. abst (action (repc cfg)) = action cfg
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
[PROOF STEP]
have "abss (reps (state cfg)) = state cfg"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg

goal (1 subgoal):
 1. abss (reps (state cfg)) = state cfg
[PROOF STEP]
by (auto dest: R_G.valid_cfg_state_in_S)
[PROOF STATE]
proof (state)
this:
abss (reps (state cfg)) = state cfg

goal (1 subgoal):
 1. abst (action (repc cfg)) = action cfg
[PROOF STEP]
with action_abst_repcs[OF assms]
[PROOF STATE]
proof (chain)
picking this:
abss ?s = state cfg \<Longrightarrow> abst (action (repcs ?s cfg)) = action cfg
abss (reps (state cfg)) = state cfg
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
abss ?s = state cfg \<Longrightarrow> abst (action (repcs ?s cfg)) = action cfg
abss (reps (state cfg)) = state cfg

goal (1 subgoal):
 1. abst (action (repc cfg)) = action cfg
[PROOF STEP]
unfolding repc_def
[PROOF STATE]
proof (prove)
using this:
abss ?s = state cfg \<Longrightarrow> abst (action (repcs ?s cfg)) = action cfg
abss (reps (state cfg)) = state cfg

goal (1 subgoal):
 1. abst (action (repcs (reps (state cfg)) cfg)) = action cfg
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
abst (action (repc cfg)) = action cfg

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma state_absc:
  "state (absc cfg) = abss (state cfg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state (absc cfg) = abss (state cfg)
[PROOF STEP]
unfolding absc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state (cfg_corec (abss (state cfg)) (abst \<circ> action) (\<lambda>cfg s. cont cfg (THE x. abss x = s \<and> x \<in> set_pmf (action cfg))) cfg) = abss (state cfg)
[PROOF STEP]
by auto


[STATEMENT]
lemma state_repcs[simp]:
  "state (repcs s cfg) = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state (repcs s cfg) = s
[PROOF STEP]
unfolding repcs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state (cfg_corec s (\<lambda>(s, cfg). rept s (action cfg)) (\<lambda>(s, cfg) s'. (s', cont cfg (abss s'))) (s, cfg)) = s
[PROOF STEP]
by auto


[STATEMENT]
lemma repcs_bisim:
  notes R_G.cfg_onD_state[simp del]
  assumes "cfg \<in> R_G.valid_cfg" "x \<in> S" "x ~ x'" "abss x = state cfg"
  shows "absc (repcs x cfg) = absc (repcs x' cfg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. absc (repcs x cfg) = absc (repcs x' cfg)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg

goal (1 subgoal):
 1. absc (repcs x cfg) = absc (repcs x' cfg)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg\<rbrakk> \<Longrightarrow> absc (repcs x cfg) = absc (repcs x' cfg)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
[PROOF STEP]
have "abss x' = state cfg"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg

goal (1 subgoal):
 1. abss x' = state cfg
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
abss x' = state cfg

goal (1 subgoal):
 1. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg\<rbrakk> \<Longrightarrow> absc (repcs x cfg) = absc (repcs x' cfg)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
[PROOF STEP]
have "abss x' \<in> \<S>"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg

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

goal (1 subgoal):
 1. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg\<rbrakk> \<Longrightarrow> absc (repcs x cfg) = absc (repcs x' cfg)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
abss x' \<in> \<S>
[PROOF STEP]
have "x' \<in> S"
[PROOF STATE]
proof (prove)
using this:
abss x' \<in> \<S>

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

goal (1 subgoal):
 1. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg\<rbrakk> \<Longrightarrow> absc (repcs x cfg) = absc (repcs x' cfg)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S

goal (1 subgoal):
 1. absc (repcs x cfg) = absc (repcs x' cfg)
[PROOF STEP]
proof (coinduction arbitrary: cfg x x')
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S\<rbrakk> \<Longrightarrow> state (absc (repcs x cfg)) = state (absc (repcs x' cfg))
 2. \<And>cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S\<rbrakk> \<Longrightarrow> action (absc (repcs x cfg)) = action (absc (repcs x' cfg))
 3. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
case state
[PROOF STATE]
proof (state)
this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S

goal (3 subgoals):
 1. \<And>cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S\<rbrakk> \<Longrightarrow> state (absc (repcs x cfg)) = state (absc (repcs x' cfg))
 2. \<And>cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S\<rbrakk> \<Longrightarrow> action (absc (repcs x cfg)) = action (absc (repcs x' cfg))
 3. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S

goal (1 subgoal):
 1. state (absc (repcs x cfg)) = state (absc (repcs x' cfg))
[PROOF STEP]
by (simp add: state_absc)
[PROOF STATE]
proof (state)
this:
state (absc (repcs x cfg)) = state (absc (repcs x' cfg))

goal (2 subgoals):
 1. \<And>cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S\<rbrakk> \<Longrightarrow> action (absc (repcs x cfg)) = action (absc (repcs x' cfg))
 2. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S\<rbrakk> \<Longrightarrow> action (absc (repcs x cfg)) = action (absc (repcs x' cfg))
 2. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
case action
[PROOF STATE]
proof (state)
this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S

goal (2 subgoals):
 1. \<And>cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S\<rbrakk> \<Longrightarrow> action (absc (repcs x cfg)) = action (absc (repcs x' cfg))
 2. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S

goal (1 subgoal):
 1. action (absc (repcs x cfg)) = action (absc (repcs x' cfg))
[PROOF STEP]
unfolding absc_def repcs_def
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S

goal (1 subgoal):
 1. action (cfg_corec (abss (state (cfg_corec x (\<lambda>(s, cfg). rept s (action cfg)) (\<lambda>(s, cfg) s'. (s', cont cfg (abss s'))) (x, cfg)))) (abst \<circ> action) (\<lambda>cfg s. cont cfg (THE x. abss x = s \<and> x \<in> set_pmf (action cfg))) (cfg_corec x (\<lambda>(s, cfg). rept s (action cfg)) (\<lambda>(s, cfg) s'. (s', cont cfg (abss s'))) (x, cfg))) = action (cfg_corec (abss (state (cfg_corec x' (\<lambda>(s, cfg). rept s (action cfg)) (\<lambda>(s, cfg) s'. (s', cont cfg (abss s'))) (x', cfg)))) (abst \<circ> action) (\<lambda>cfg s. cont cfg (THE x. abss x = s \<and> x \<in> set_pmf (action cfg))) (cfg_corec x' (\<lambda>(s, cfg). rept s (action cfg)) (\<lambda>(s, cfg) s'. (s', cont cfg (abss s'))) (x', cfg)))
[PROOF STEP]
by (auto dest: R_G.valid_cfgD)
[PROOF STATE]
proof (state)
this:
action (absc (repcs x cfg)) = action (absc (repcs x' cfg))

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
case prems: (cont s cfg x x')
[PROOF STATE]
proof (state)
this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S
s \<in> set_pmf (action (absc (repcs x cfg)))

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
define cfg' where "cfg' = cont cfg s"
[PROOF STATE]
proof (state)
this:
cfg' = cont cfg s

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
define t    where "t \<equiv> THE y. abss y = s \<and> y \<in> action (repcs x cfg)"
[PROOF STATE]
proof (state)
this:
t \<equiv> THE y. abss y = s \<and> y \<in> set_pmf (action (repcs x cfg))

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
define t'   where "t' \<equiv>THE y. abss y = s \<and> y \<in> action (repcs x' cfg)"
[PROOF STATE]
proof (state)
this:
t' \<equiv> THE y. abss y = s \<and> y \<in> set_pmf (action (repcs x' cfg))

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S
s \<in> set_pmf (action (absc (repcs x cfg)))
[PROOF STEP]
have valid: "repcs x cfg \<in> valid_cfg"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S
s \<in> set_pmf (action (absc (repcs x cfg)))

goal (1 subgoal):
 1. repcs x cfg \<in> MDP.valid_cfg
[PROOF STEP]
by (intro repcs_valid)
[PROOF STATE]
proof (state)
this:
repcs x cfg \<in> MDP.valid_cfg

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S
s \<in> set_pmf (action (absc (repcs x cfg)))
[PROOF STEP]
have *: "s \<in> abst (action (repcs x cfg))"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S
s \<in> set_pmf (action (absc (repcs x cfg)))

goal (1 subgoal):
 1. s \<in> set_pmf (abst (action (repcs x cfg)))
[PROOF STEP]
unfolding cfg'_def
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S
s \<in> set_pmf (action (absc (repcs x cfg)))

goal (1 subgoal):
 1. s \<in> set_pmf (abst (action (repcs x cfg)))
[PROOF STEP]
by (simp add: action_absc)
[PROOF STATE]
proof (state)
this:
s \<in> set_pmf (abst (action (repcs x cfg)))

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S
s \<in> set_pmf (action (absc (repcs x cfg)))
s \<in> set_pmf (abst (action (repcs x cfg)))
[PROOF STEP]
have "s \<in> action cfg"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S
s \<in> set_pmf (action (absc (repcs x cfg)))
s \<in> set_pmf (abst (action (repcs x cfg)))

goal (1 subgoal):
 1. s \<in> set_pmf (action cfg)
[PROOF STEP]
by (auto dest: R_G.valid_cfgD simp: repcs_def)
[PROOF STATE]
proof (state)
this:
s \<in> set_pmf (action cfg)

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S
s \<in> set_pmf (action (absc (repcs x cfg)))
s \<in> set_pmf (action cfg)
[PROOF STEP]
have "s \<in> \<S>"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S
s \<in> set_pmf (action (absc (repcs x cfg)))
s \<in> set_pmf (action cfg)

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

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
from cont_cfg_defined[OF valid *]
[PROOF STATE]
proof (chain)
picking this:
(abss (THE x. abss x = s \<and> x \<in> set_pmf (action (repcs x cfg))) = s \<and> (THE x. abss x = s \<and> x \<in> set_pmf (action (repcs x cfg))) \<in> set_pmf (action (repcs x cfg))) \<and> (\<forall>y. abss y = s \<and> y \<in> set_pmf (action (repcs x cfg)) \<longrightarrow> y = (THE x. abss x = s \<and> x \<in> set_pmf (action (repcs x cfg))))
[PROOF STEP]
have t:
      "abss t = s" "t \<in> action (repcs x cfg)"
[PROOF STATE]
proof (prove)
using this:
(abss (THE x. abss x = s \<and> x \<in> set_pmf (action (repcs x cfg))) = s \<and> (THE x. abss x = s \<and> x \<in> set_pmf (action (repcs x cfg))) \<in> set_pmf (action (repcs x cfg))) \<and> (\<forall>y. abss y = s \<and> y \<in> set_pmf (action (repcs x cfg)) \<longrightarrow> y = (THE x. abss x = s \<and> x \<in> set_pmf (action (repcs x cfg))))

goal (1 subgoal):
 1. abss t = s &&& t \<in> set_pmf (action (repcs x cfg))
[PROOF STEP]
unfolding t_def
[PROOF STATE]
proof (prove)
using this:
(abss (THE x. abss x = s \<and> x \<in> set_pmf (action (repcs x cfg))) = s \<and> (THE x. abss x = s \<and> x \<in> set_pmf (action (repcs x cfg))) \<in> set_pmf (action (repcs x cfg))) \<and> (\<forall>y. abss y = s \<and> y \<in> set_pmf (action (repcs x cfg)) \<longrightarrow> y = (THE x. abss x = s \<and> x \<in> set_pmf (action (repcs x cfg))))

goal (1 subgoal):
 1. abss (THE y. abss y = s \<and> y \<in> set_pmf (action (repcs x cfg))) = s &&& (THE y. abss y = s \<and> y \<in> set_pmf (action (repcs x cfg))) \<in> set_pmf (action (repcs x cfg))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
abss t = s
t \<in> set_pmf (action (repcs x cfg))

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
have "cont (absc (repcs x cfg)) s = cont (absc (repcs x cfg)) (abss t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (absc (repcs x cfg)) s = cont (absc (repcs x cfg)) (abss t)
[PROOF STEP]
using t
[PROOF STATE]
proof (prove)
using this:
abss t = s
t \<in> set_pmf (action (repcs x cfg))

goal (1 subgoal):
 1. cont (absc (repcs x cfg)) s = cont (absc (repcs x cfg)) (abss t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cont (absc (repcs x cfg)) s = cont (absc (repcs x cfg)) (abss t)

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
have "cont (absc (repcs x cfg)) s = absc (cont (repcs x cfg) t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (absc (repcs x cfg)) s = absc (cont (repcs x cfg) t)
[PROOF STEP]
using t valid
[PROOF STATE]
proof (prove)
using this:
abss t = s
t \<in> set_pmf (action (repcs x cfg))
repcs x cfg \<in> MDP.valid_cfg

goal (1 subgoal):
 1. cont (absc (repcs x cfg)) s = absc (cont (repcs x cfg) t)
[PROOF STEP]
by (auto simp: cont_absc_1)
[PROOF STATE]
proof (state)
this:
cont (absc (repcs x cfg)) s = absc (cont (repcs x cfg) t)

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cont (absc (repcs x cfg)) s = absc (cont (repcs x cfg) t)

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
have "\<dots> = absc (repcs t (cont cfg s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. absc (cont (repcs x cfg) t) = absc (repcs t (cont cfg s))
[PROOF STEP]
using prems t
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S
s \<in> set_pmf (action (absc (repcs x cfg)))
abss t = s
t \<in> set_pmf (action (repcs x cfg))

goal (1 subgoal):
 1. absc (cont (repcs x cfg) t) = absc (repcs t (cont cfg s))
[PROOF STEP]
by (subst cont_repcs1) (auto dest: R_G.valid_cfgD)
[PROOF STATE]
proof (state)
this:
absc (cont (repcs x cfg) t) = absc (repcs t (cont cfg s))

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cont (absc (repcs x cfg)) s = absc (repcs t (cont cfg s))
[PROOF STEP]
have cont_x: "cont (absc (repcs x cfg)) s = absc (repcs t (cont cfg s))"
[PROOF STATE]
proof (prove)
using this:
cont (absc (repcs x cfg)) s = absc (repcs t (cont cfg s))

goal (1 subgoal):
 1. cont (absc (repcs x cfg)) s = absc (repcs t (cont cfg s))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cont (absc (repcs x cfg)) s = absc (repcs t (cont cfg s))

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S
s \<in> set_pmf (action (absc (repcs x cfg)))
[PROOF STEP]
have valid: "repcs x' cfg \<in> valid_cfg"
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S
s \<in> set_pmf (action (absc (repcs x cfg)))

goal (1 subgoal):
 1. repcs x' cfg \<in> MDP.valid_cfg
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
repcs x' cfg \<in> MDP.valid_cfg

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
from \<open>s \<in> action cfg\<close> prems
[PROOF STATE]
proof (chain)
picking this:
s \<in> set_pmf (action cfg)
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S
s \<in> set_pmf (action (absc (repcs x cfg)))
[PROOF STEP]
have "s \<in> abst (action (repcs x' cfg))"
[PROOF STATE]
proof (prove)
using this:
s \<in> set_pmf (action cfg)
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S
s \<in> set_pmf (action (absc (repcs x cfg)))

goal (1 subgoal):
 1. s \<in> set_pmf (abst (action (repcs x' cfg)))
[PROOF STEP]
by (auto dest: R_G.valid_cfgD simp: repcs_def)
[PROOF STATE]
proof (state)
this:
s \<in> set_pmf (abst (action (repcs x' cfg)))

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
from cont_cfg_defined[OF valid this]
[PROOF STATE]
proof (chain)
picking this:
(abss (THE x. abss x = s \<and> x \<in> set_pmf (action (repcs x' cfg))) = s \<and> (THE x. abss x = s \<and> x \<in> set_pmf (action (repcs x' cfg))) \<in> set_pmf (action (repcs x' cfg))) \<and> (\<forall>y. abss y = s \<and> y \<in> set_pmf (action (repcs x' cfg)) \<longrightarrow> y = (THE x. abss x = s \<and> x \<in> set_pmf (action (repcs x' cfg))))
[PROOF STEP]
have t':
      "abss t' = s" "t' \<in> action (repcs x' cfg)"
[PROOF STATE]
proof (prove)
using this:
(abss (THE x. abss x = s \<and> x \<in> set_pmf (action (repcs x' cfg))) = s \<and> (THE x. abss x = s \<and> x \<in> set_pmf (action (repcs x' cfg))) \<in> set_pmf (action (repcs x' cfg))) \<and> (\<forall>y. abss y = s \<and> y \<in> set_pmf (action (repcs x' cfg)) \<longrightarrow> y = (THE x. abss x = s \<and> x \<in> set_pmf (action (repcs x' cfg))))

goal (1 subgoal):
 1. abss t' = s &&& t' \<in> set_pmf (action (repcs x' cfg))
[PROOF STEP]
unfolding t'_def
[PROOF STATE]
proof (prove)
using this:
(abss (THE x. abss x = s \<and> x \<in> set_pmf (action (repcs x' cfg))) = s \<and> (THE x. abss x = s \<and> x \<in> set_pmf (action (repcs x' cfg))) \<in> set_pmf (action (repcs x' cfg))) \<and> (\<forall>y. abss y = s \<and> y \<in> set_pmf (action (repcs x' cfg)) \<longrightarrow> y = (THE x. abss x = s \<and> x \<in> set_pmf (action (repcs x' cfg))))

goal (1 subgoal):
 1. abss (THE y. abss y = s \<and> y \<in> set_pmf (action (repcs x' cfg))) = s &&& (THE y. abss y = s \<and> y \<in> set_pmf (action (repcs x' cfg))) \<in> set_pmf (action (repcs x' cfg))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
abss t' = s
t' \<in> set_pmf (action (repcs x' cfg))

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
have "cont (absc (repcs x' cfg)) s = cont (absc (repcs x' cfg)) (abss t')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (absc (repcs x' cfg)) s = cont (absc (repcs x' cfg)) (abss t')
[PROOF STEP]
using t'
[PROOF STATE]
proof (prove)
using this:
abss t' = s
t' \<in> set_pmf (action (repcs x' cfg))

goal (1 subgoal):
 1. cont (absc (repcs x' cfg)) s = cont (absc (repcs x' cfg)) (abss t')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cont (absc (repcs x' cfg)) s = cont (absc (repcs x' cfg)) (abss t')

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
have "cont (absc (repcs x' cfg)) s = absc (cont (repcs x' cfg) t')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (absc (repcs x' cfg)) s = absc (cont (repcs x' cfg) t')
[PROOF STEP]
using t' valid
[PROOF STATE]
proof (prove)
using this:
abss t' = s
t' \<in> set_pmf (action (repcs x' cfg))
repcs x' cfg \<in> MDP.valid_cfg

goal (1 subgoal):
 1. cont (absc (repcs x' cfg)) s = absc (cont (repcs x' cfg) t')
[PROOF STEP]
by (auto simp: cont_absc_1)
[PROOF STATE]
proof (state)
this:
cont (absc (repcs x' cfg)) s = absc (cont (repcs x' cfg) t')

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cont (absc (repcs x' cfg)) s = absc (cont (repcs x' cfg) t')

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
have "\<dots> = absc (repcs t' (cont cfg s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. absc (cont (repcs x' cfg) t') = absc (repcs t' (cont cfg s))
[PROOF STEP]
using prems t'
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
x \<in> S
x ~ x'
abss x = state cfg
x' \<in> S
s \<in> set_pmf (action (absc (repcs x cfg)))
abss t' = s
t' \<in> set_pmf (action (repcs x' cfg))

goal (1 subgoal):
 1. absc (cont (repcs x' cfg) t') = absc (repcs t' (cont cfg s))
[PROOF STEP]
by (subst cont_repcs1) (auto dest: R_G.valid_cfgD)
[PROOF STATE]
proof (state)
this:
absc (cont (repcs x' cfg) t') = absc (repcs t' (cont cfg s))

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cont (absc (repcs x' cfg)) s = absc (repcs t' (cont cfg s))
[PROOF STEP]
have "cont (absc (repcs x' cfg)) s = absc (repcs t' (cont cfg s))"
[PROOF STATE]
proof (prove)
using this:
cont (absc (repcs x' cfg)) s = absc (repcs t' (cont cfg s))

goal (1 subgoal):
 1. cont (absc (repcs x' cfg)) s = absc (repcs t' (cont cfg s))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cont (absc (repcs x' cfg)) s = absc (repcs t' (cont cfg s))

goal (1 subgoal):
 1. \<And>t cfg x x'. \<lbrakk>cfg \<in> R_G.valid_cfg; x \<in> S; x ~ x'; abss x = state cfg; x' \<in> S; t \<in> set_pmf (action (absc (repcs x cfg)))\<rbrakk> \<Longrightarrow> \<exists>cfga xa x'a. cont (absc (repcs x cfg)) t = absc (repcs xa cfga) \<and> cont (absc (repcs x' cfg)) t = absc (repcs x'a cfga) \<and> cfga \<in> R_G.valid_cfg \<and> xa \<in> S \<and> xa ~ x'a \<and> abss xa = state cfga \<and> x'a \<in> S
[PROOF STEP]
with cont_x \<open>s \<in> action cfg\<close> prems(1) t t' \<open>s \<in> \<S>\<close>
[PROOF STATE]
proof (chain)
picking this:
cont (absc (repcs x cfg)) s = absc (repcs t (cont cfg s))
s \<in> set_pmf (action cfg)
cfg \<in> R_G.valid_cfg
abss t = s
t \<in> set_pmf (action (repcs x cfg))
abss t' = s
t' \<in> set_pmf (action (repcs x' cfg))
s \<in> \<S>
cont (absc (repcs x' cfg)) s = absc (repcs t' (cont cfg s))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
cont (absc (repcs x cfg)) s = absc (repcs t (cont cfg s))
s \<in> set_pmf (action cfg)
cfg \<in> R_G.valid_cfg
abss t = s
t \<in> set_pmf (action (repcs x cfg))
abss t' = s
t' \<in> set_pmf (action (repcs x' cfg))
s \<in> \<S>
cont (absc (repcs x' cfg)) s = absc (repcs t' (cont cfg s))

goal (1 subgoal):
 1. \<exists>cfg x x'. cont (absc (repcs x cfg)) s = absc (repcs x cfg) \<and> cont (absc (repcs x' cfg)) s = absc (repcs x' cfg) \<and> cfg \<in> R_G.valid_cfg \<and> x \<in> S \<and> x ~ x' \<and> abss x = state cfg \<and> x' \<in> S
[PROOF STEP]
by (inst_existentials "cont cfg s" t t')
         (auto intro: \<S>_abss_S R_G.valid_cfg_action R_G.valid_cfg_cont)
[PROOF STATE]
proof (state)
this:
\<exists>cfg x x'. cont (absc (repcs x cfg)) s = absc (repcs x cfg) \<and> cont (absc (repcs x' cfg)) s = absc (repcs x' cfg) \<and> cfg \<in> R_G.valid_cfg \<and> x \<in> S \<and> x ~ x' \<and> abss x = state cfg \<and> x' \<in> S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
absc (repcs x cfg) = absc (repcs x' cfg)

goal:
No subgoals!
[PROOF STEP]
qed