Theory PTA_Reachability

theory PTA_Reachability
  imports PTA
begin

section ‹Classifying Regions for Divergence›

subsection ‹Pairwise›

coinductive pairwise :: "('a ⇒ 'a ⇒ bool) ⇒ 'a stream ⇒ bool" for P where
  "P a b ⟹ pairwise P (b ## xs) ⟹ pairwise P (a ## b ## xs)"

lemma pairwise_Suc:
  "pairwise P xs ⟹ P (xs !! i) (xs !! (Suc i))"
  by (induction i arbitrary: xs) (force elim: pairwise.cases)+

lemma Suc_pairwise:
  "∀ i. P (xs !! i) (xs !! (Suc i)) ⟹ pairwise P xs"
  apply (coinduction arbitrary: xs)
  apply (subst stream.collapse[symmetric])
  apply (rewrite in "stl _" stream.collapse[symmetric])
  apply (intro exI conjI, rule HOL.refl)
   apply (erule allE[where x = 0]; simp; fail)
  by simp (metis snth.simps(2))

lemma pairwise_iff:
  "pairwise P xs ⟷ (∀ i. P (xs !! i) (xs !! (Suc i)))"
using pairwise_Suc Suc_pairwise by blast

lemma pairwise_stlD:
  "pairwise P xs ⟹ pairwise P (stl xs)"
by (auto elim: pairwise.cases)

lemma pairwise_pairD:
  "pairwise P xs ⟹ P (shd xs) (shd (stl xs))"
by (auto elim: pairwise.cases)

lemma pairwise_mp:
  assumes "pairwise P xs" and lift: "⋀ x y. x ∈ sset xs ⟹ y ∈ sset xs ⟹ P x y ⟹ Q x y"
  shows "pairwise Q xs" using assms
 apply (coinduction arbitrary: xs)
 subgoal for xs
 apply (subst stream.collapse[symmetric])
 apply (rewrite in "stl _" stream.collapse[symmetric])
 apply (intro exI conjI)
  apply (rule HOL.refl)
 by (auto intro: stl_sset dest: pairwise_pairD pairwise_stlD)
done

lemma pairwise_sdropD:
  "pairwise P (sdrop i xs)" if "pairwise P xs"
  using that
proof (coinduction arbitrary: i xs)
  case (pairwise i xs)
  then show ?case
    apply (inst_existentials "shd (sdrop i xs)" "shd (stl (sdrop i xs))" "stl (stl (sdrop i xs))")
    subgoal
      by (auto dest: pairwise_Suc) (metis sdrop_simps(1) sdrop_stl stream.collapse)
    subgoal
      by (inst_existentials "i - 1" "stl xs") (auto dest: pairwise_Suc pairwise_stlD)
    by (metis sdrop_simps(2) stream.collapse)
qed


subsection ‹Regions›

(* XXX Move. Rename? *)
lemma gt_GreaterD:
  assumes "u ∈ region X I r" "valid_region X k I r" "c ∈ X" "u c > k c"
  shows "I c = Greater (k c)"
proof -
  from assms have "intv_elem c u (I c)" "valid_intv (k c) (I c)" by auto
  with assms(4) show ?thesis by (cases "I c") auto
qed

lemma const_ConstD:
  assumes "u ∈ region X I r" "valid_region X k I r" "c ∈ X" "u c = d" "d ≤ k c"
  shows "I c = Const d"
proof -
  from assms have "intv_elem c u (I c)" "valid_intv (k c) (I c)" by auto
  with assms(4,5) show ?thesis by (cases "I c") auto
qed

lemma not_Greater_bounded:
  assumes "I x ≠ Greater (k x)" "x ∈ X" "valid_region X k I r" "u ∈ region X I r"
  shows "u x ≤ k x"
proof -
  from assms have "intv_elem x u (I x)" "valid_intv (k x) (I x)" by auto
  with assms(1) show "u x ≤ k x" by (cases "I x") auto
qed

lemma Greater_closed:
  fixes t :: "real"
  assumes "u ∈ region X I r" "valid_region X k I r" "c ∈ X" "I c = Greater (k c)" "t > k c"
  shows "u(c := t) ∈ region X I r"
  using assms
  apply (intro region.intros)
     apply (auto; fail)
    apply standard
  subgoal for x
    by (cases "x = c"; cases "I x"; force intro!: intv_elem.intros)
  by auto

lemma Greater_unbounded_aux:
  assumes "finite X" "valid_region X k I r" "c ∈ X" "I c = Greater (k c)"
  shows "∃ u ∈ region X I r. u c > t"
using assms Greater_closed[OF _ assms(2-4)] 
proof -
  let ?R = "region X I r"
  let ?t = "if t > k c then t + 1 else k c + 1"
  have t: "?t > k c" by auto
  from region_not_empty[OF assms(1,2)] obtain u where u: "u ∈ ?R" by auto
  from Greater_closed[OF this assms(2-4) t] have "u(c:=?t) ∈ ?R" by auto
  with t show ?thesis by (inst_existentials "u(c:=?t)") auto
qed


subsection ‹Unbounded and Zero Regions›

definition "unbounded x R ≡ ∀ t. ∃ u ∈ R. u x > t"

definition "zero x R ≡ ∀ u ∈ R. u x = 0"

lemma Greater_unbounded:
  assumes "finite X" "valid_region X k I r" "c ∈ X" "I c = Greater (k c)"
  shows "unbounded c (region X I r)"
using Greater_unbounded_aux[OF assms] unfolding unbounded_def by blast

lemma unbounded_Greater:
  assumes "valid_region X k I r" "c ∈ X" "unbounded c (region X I r)"
  shows "I c = Greater (k c)"
using assms unfolding unbounded_def by (auto intro: gt_GreaterD)

lemma Const_zero:
  assumes "c ∈ X" "I c = Const 0"
  shows "zero c (region X I r)"
using assms unfolding zero_def by force

lemma zero_Const:
  assumes "finite X" "valid_region X k I r" "c ∈ X" "zero c (region X I r)"
  shows "I c = Const 0"
proof -
  from assms obtain u where "u ∈ region X I r" by atomize_elim (auto intro: region_not_empty)
  with assms show ?thesis unfolding zero_def by (auto intro: const_ConstD)
qed

lemma zero_all:
  assumes "finite X" "valid_region X k I r" "c ∈ X" "u ∈ region X I r" "u c = 0"
  shows "zero c (region X I r)"
proof -
  from assms have "intv_elem c u (I c)" "valid_intv (k c) (I c)" by auto
  then have "I c = Const 0" using assms(5) by cases auto
  with assms have "u' c = 0" if "u' ∈ region X I r" for u' using that by force
  then show ?thesis unfolding zero_def by blast
qed


section ‹Reachability›

subsection ‹Definitions›

locale Probabilistic_Timed_Automaton_Regions_Reachability =
  Probabilistic_Timed_Automaton_Regions k v n not_in_X A
    for k v n not_in_X and A :: "('c, t, 's) pta" +
  fixes φ ψ :: "('s * ('c, t) cval) ⇒ bool" fixes s
  assumes φ: "⋀ x y. x ∈ S ⟹ x ~ y ⟹ φ x ⟷ φ y"
  assumes ψ: "⋀ x y. x ∈ S ⟹ x ~ y ⟹ ψ x ⟷ ψ y"
  assumes s[intro, simp]: "s ∈ S"
begin

definition "φ' ≡ absp φ"
definition "ψ' ≡ absp ψ"
definition "s' ≡ abss s"

lemma s_s'_cfg_on[intro]:
  assumes "cfg ∈ MDP.cfg_on s"
  shows "absc cfg ∈ R_G.cfg_on s'"
proof -
  from assms s have "cfg ∈ valid_cfg" unfolding MDP.valid_cfg_def by auto
  then have "absc cfg ∈ R_G.cfg_on (state (absc cfg))" by (auto intro: R_G.valid_cfgD)
  with assms show ?thesis unfolding s'_def by (auto simp: state_absc)
qed

lemma s'_𝒮[simp, intro]:
  "s' ∈ 𝒮"
  unfolding s'_def using s by auto

lemma s'_s_cfg_on[intro]:
  assumes "cfg ∈ R_G.cfg_on s'"
  shows "repcs s cfg ∈ MDP.cfg_on s"
proof -
  from assms s have "cfg ∈ R_G.valid_cfg" unfolding R_G.valid_cfg_def by auto
  with assms have "repcs s cfg ∈ valid_cfg" by (auto simp: s'_def intro: R_G.valid_cfgD)
  then show ?thesis by (auto dest: MDP.valid_cfgD)
qed

lemma (in Probabilistic_Timed_Automaton_Regions) compatible_stream:
  assumes φ: "⋀ x y. x ∈ S ⟹ x ~ y ⟹ φ x ⟷ φ y"
  assumes "pred_stream (λs. s ∈ S) xs"
      and [intro]: "x ∈ S"
    shows "pred_stream (λs. φ (reps (abss s)) = φ s) (x ## xs)"
unfolding stream.pred_set proof clarify
  fix l u
  assume A: "(l, u) ∈ sset (x ## xs)"
  from assms have "pred_stream (λs. s ∈ S) (x ## xs)" by auto
  with A have "(l, u) ∈ S" by (fastforce simp: stream.pred_set)
  then have "abss (l, u) ∈ 𝒮" by auto
  then have "reps (abss (l, u)) ~ (l, u)" by simp
  with φ ‹(l, u) ∈ S› show "φ (reps (abss (l, u))) = φ (l, u)" by blast
qed

lemma φ_stream':
  "pred_stream (λs. φ (reps (abss s)) = φ s) (x ## xs)" if "pred_stream (λs. s ∈ S) xs" "x ∈ S"
  using compatible_stream[of φ, OF φ that] .

lemma ψ_stream':
  "pred_stream (λs. ψ (reps (abss s)) = ψ s) (x ## xs)" if "pred_stream (λs. s ∈ S) xs" "x ∈ S"
  using compatible_stream[of ψ, OF ψ that] .

lemmas φ_stream = compatible_stream[of φ, OF φ]
lemmas ψ_stream = compatible_stream[of ψ, OF ψ]

subsection ‹Easier Result on All Configurations›

(* TODO: Rename *)
lemma suntil_reps:
  assumes
    "∀s∈sset (smap abss y). s ∈ 𝒮"
    "(holds φ' suntil holds ψ') (s' ## smap abss y)"
  shows "(holds φ suntil holds ψ) (s ## y)"
  using assms
  by (subst region_compatible_suntil[symmetric]; (intro φ_stream ψ_stream)?)
     (auto simp: φ'_def ψ'_def absp_def stream.pred_set 𝒮_abss_S s'_def comp_def)

(* TODO: Rename *)
lemma suntil_abss:
  assumes
    "∀s∈sset y. s ∈ S"
    "(holds φ suntil holds ψ) (s ## y)"
  shows
    "(holds φ' suntil holds ψ') (s' ## smap abss y)"
  using assms
  by (subst (asm) region_compatible_suntil[symmetric]; (intro φ_stream ψ_stream)?)
     (auto simp: φ'_def ψ'_def absp_def stream.pred_set s'_def comp_def)

(* TODO: Generalize to CTL formulae *)
theorem P_sup_sunitl_eq:
  notes [measurable] = in_space_UNIV and [iff] = pred_stream_iff
  shows
    "(MDP.P_sup s  (λx. (holds φ suntil holds ψ)   (s  ## x)))
   = (R_G.P_sup s' (λx. (holds φ' suntil holds ψ') (s' ## x)))"
  unfolding MDP.P_sup_def R_G.P_sup_def
proof (rule SUP_eq, goal_cases)
  case prems: (1 cfg)
  let ?cfg' = "absc cfg"
  from prems have "cfg ∈ valid_cfg" by (auto intro: MDP.valid_cfgI)
  then have "?cfg' ∈ R_G.valid_cfg" by (auto intro: R_G.valid_cfgI)
  from ‹cfg ∈ valid_cfg› have alw_S: "almost_everywhere (MDP.T cfg) (pred_stream (λs. s ∈ S))"
    by (rule MDP.alw_S)
  from ‹?cfg'∈ R_G.valid_cfg› have alw_𝒮: "almost_everywhere (R_G.T ?cfg') (pred_stream (λs. s ∈ 𝒮))"
    by (rule R_G.alw_S)
  have "emeasure (MDP.T cfg) {x ∈ space MDP.St. (holds φ suntil holds ψ) (s ## x)}
       = emeasure (R_G.T ?cfg') {x ∈ space R_G.St. (holds φ' suntil holds ψ') (s' ## x)}"
    apply (rule path_measure_eq_absc1_new[symmetric, where P = "pred_stream (λ s. s ∈ 𝒮)"
          and Q = "pred_stream (λ s. s ∈ S)"]
        )
    using prems alw_S alw_𝒮 apply (auto intro: MDP.valid_cfgI simp: )[7]
    by (auto simp: S_abss_𝒮 intro: 𝒮_abss_S intro!: suntil_abss suntil_reps, measurable)
  with prems show ?case by (inst_existentials ?cfg') auto
next
  case prems: (2 cfg)
  let ?cfg' = "repcs s cfg"
  have "s = state ?cfg'" by simp
  from prems have "s' = state cfg" by auto
  have "pred_stream (λs. φ (reps (abss s)) = φ s) (state (repcs s cfg) ## x)"
    if "pred_stream (λs. s ∈ S) x" for x
    using prems that by (intro φ_stream) auto
  moreover
  have "pred_stream (λs. ψ (reps (abss s)) = ψ s) (state (repcs s cfg) ## x)"
    if "pred_stream (λs. s ∈ S) x" for x
    using prems that by (intro ψ_stream) auto
  ultimately
  have "emeasure (R_G.T cfg) {x ∈ space R_G.St. (holds φ' suntil holds ψ') (s' ## x)}
    = emeasure (MDP.T (repcs s cfg)) {x ∈ space MDP.St. (holds φ suntil holds ψ) (s ## x)}"
    apply (rewrite in "s ## _" ‹s = _›)
    apply (subst ‹s' = _›)
    unfolding φ'_def ψ'_def s'_def
    apply (rule path_measure_eq_repcs''_new)
    using prems by (auto 4 3 simp: s'_def intro: R_G.valid_cfgI MDP.valid_cfgI)
  with prems show ?case by (inst_existentials ?cfg') auto
qed

end (* PTA Reachability Problem *)


subsection ‹Divergent Adversaries›

context Probabilistic_Timed_Automaton
begin

  definition "elapsed u u' ≡ Max ({u' c - u c | c. c ∈ 𝒳} ∪ {0})"

  definition "eq_elapsed u u' ≡ elapsed u u' > 0 ⟶ (∀ c ∈ 𝒳. u' c - u c = elapsed u u')"

  fun dur :: "('c, t) cval stream ⇒ nat ⇒ t" where
    "dur _ 0 = 0" |
    "dur (x ## y ## xs) (Suc i) = elapsed x y + dur (y ## xs) i"

  definition "divergent ω ≡ ∀ t. ∃ n. dur ω n > t"

  definition "div_cfg cfg ≡ AE ω in MDP.MC.T cfg. divergent (smap (snd o state) ω)"

  definition "ℛ_div ω ≡
    ∀x ∈ 𝒳. (∀ i. (∃ j ≥ i. zero x (ω !! j)) ∧ (∃ j ≥ i. ¬ zero x (ω !! j)))
      ∨ (∃ i. ∀ j ≥ i. unbounded x (ω !! j))"

  definition "R_G_div_cfg cfg ≡ AE ω in MDP.MC.T cfg. ℛ_div (smap (snd o state) ω)"

end

context Probabilistic_Timed_Automaton_Regions
begin

definition "cfg_on_div st ≡ MDP.cfg_on st ∩ {cfg. div_cfg cfg}"

definition "R_G_cfg_on_div st ≡ R_G.cfg_on st ∩ {cfg. R_G_div_cfg cfg}"

lemma measurable_ℛ_div[measurable]: "Measurable.pred MDP.MC.S ℛ_div"
  unfolding ℛ_div_def
  by (intro
        pred_intros_finite[OF beta_interp.finite]
        pred_intros_logic pred_intros_countable
        measurable_count_space_const measurable_compose[OF measurable_snth]
     ) measurable

lemma elapsed_ge0[simp]: "elapsed x y ≥ 0"
  unfolding elapsed_def using finite(1) by auto

lemma dur_pos:
  "dur xs i ≥ 0"
 apply (induction i arbitrary: xs)
 apply (auto; fail)
 subgoal for i xs
   apply (subst stream.collapse[symmetric])
   apply (rewrite at "stl xs" stream.collapse[symmetric])
   apply (subst dur.simps)
 by simp
done

lemma dur_mono:
  "i ≤ j ⟹ dur xs i ≤ dur xs j"
proof (induction i arbitrary: xs j)
  case 0 show ?case by (auto intro: dur_pos)
next
  case (Suc i xs j)
  obtain x y ys where xs: "xs = x ## y ## ys" using stream.collapse by metis
  from Suc obtain j' where j': "j = Suc j'" by (cases j) auto
  with xs have "dur xs j = elapsed x y + dur (y ## ys) j'" by auto
  also from Suc j' have "… ≥ elapsed x y + dur (y ## ys) i" by auto
  also have "elapsed x y + dur (y ## ys) i = dur xs (Suc i)" by (simp add: xs)
  finally show ?case .
qed

lemma dur_monoD:
  assumes "dur xs i < dur xs j"
  shows "i < j" using assms
 by - (rule ccontr; auto 4 4 dest: leI dur_mono[where xs = xs])

lemma elapsed_0D:
  assumes "c ∈ 𝒳" "elapsed u u' ≤ 0"
  shows "u' c - u c ≤ 0"
proof -
  from assms have "u' c - u c ∈ {u' c - u c | c. c ∈ 𝒳} ∪ {0}" by auto
  with finite(1) have "u' c - u c ≤ Max ({u' c - u c | c. c ∈ 𝒳} ∪ {0})" by auto
  with assms(2) show ?thesis unfolding elapsed_def by auto
qed

lemma elapsed_ge:
  assumes "eq_elapsed u u'" "c ∈ 𝒳"
  shows "elapsed u u' ≥ u' c - u c"
  using assms unfolding eq_elapsed_def by (auto intro: elapsed_ge0 order.trans[OF elapsed_0D])

lemma elapsed_eq:
  assumes "eq_elapsed u u'" "c ∈ 𝒳" "u' c - u c ≥ 0"
  shows "elapsed u u' = u' c - u c"
  using elapsed_ge[OF assms(1,2)] assms unfolding eq_elapsed_def by auto

lemma dur_shift:
  "dur ω (i + j) = dur ω i + dur (sdrop i ω) j"
 apply (induction i arbitrary: ω)
  apply simp
 subgoal for i ω
  apply simp
  apply (subst stream.collapse[symmetric])
  apply (rewrite at "stl ω" stream.collapse[symmetric])
  apply (subst dur.simps)
  apply (rewrite in "dur ω" stream.collapse[symmetric])
  apply (rewrite in "dur (_ ## ⌑) (Suc _)" stream.collapse[symmetric])
  apply (subst dur.simps)
  apply simp
 done
done

lemma dur_zero:
  assumes
    "∀ i. xs !! i ∈ ω !! i" "∀ j ≤ i. zero x (ω !! j)" "x ∈ 𝒳"
    "∀ i. eq_elapsed (xs !! i) (xs !! Suc i)"
  shows "dur xs i = 0" using assms
proof (induction i arbitrary: xs ω)
  case 0
  then show ?case by simp
next
  case (Suc i xs ω)
  let ?x = "xs !! 0"
  let ?y = "xs !! 1"
  let ?ys = "stl (stl xs)"
  have xs: "xs = ?x ## ?y ## ?ys" by auto
  from Suc.prems have
    "∀ i. (?y ## ?ys) !! i ∈ stl ω !! i" "∀ j ≤ i. zero x (stl ω !! j)"
    "∀ i. eq_elapsed (stl xs !! i) (stl xs !! Suc i)"
    by (metis snth.simps(2) | auto)+
  from Suc.IH[OF this(1,2) ‹x ∈ _›] this(3) have [simp]: "dur (stl xs) i = 0" by auto
  from Suc.prems(1,2) have "?y x = 0" "?x x = 0" unfolding zero_def by force+
  then have *: "?y x - ?x x = 0" by simp
  have "dur xs (Suc i) = elapsed ?x ?y"
    apply (subst xs)
    apply (subst dur.simps)
    by simp
  also have "… = 0"
    apply (subst elapsed_eq[OF _ ‹x ∈ _›])
    unfolding One_nat_def using Suc.prems(4) apply blast
    using * by auto
  finally show ?case .
qed

lemma dur_zero_tail:
  assumes "∀ i. xs !! i ∈ ω !! i" "∀ k ≥ i. k ≤ j ⟶ zero x (ω !! k)" "x ∈ 𝒳" "j ≥ i"
          "∀ i. eq_elapsed (xs !! i) (xs !! Suc i)"
  shows "dur xs j = dur xs i"
proof -
  from ‹j ≥ i› dur_shift[of xs i "j - i"] have
    "dur xs j = dur xs i + dur (sdrop i xs) (j - i)"
  by simp
  also have "… = dur xs i"
    using assms
    by (rewrite in "dur (sdrop _ _) _" dur_zero[where ω = "sdrop i ω"])
       (auto dest: prop_nth_sdrop_pair[of eq_elapsed] prop_nth_sdrop prop_nth_sdrop_pair[of "(∈)"])
  finally show ?thesis .
qed

lemma elapsed_ge_pos:
  fixes u :: "('c, t) cval"
  assumes "eq_elapsed u u'" "c ∈ 𝒳" "u ∈ V" "u' ∈ V"
  shows "elapsed u u' ≤ u' c"
proof (cases "elapsed u u' = 0")
  case True
  with assms show ?thesis by (auto simp: V_def)
next
  case False
  from ‹u ∈ V› ‹c ∈ 𝒳 › have "u c ≥ 0" by (auto simp: V_def)
  from False assms have "elapsed u u' = u' c - u c"
    unfolding eq_elapsed_def by (auto simp add: less_le)
  also from ‹u c ≥ 0› have "… ≤ u' c" by simp
  finally show ?thesis .
qed

lemma dur_Suc:
  "dur xs (Suc i) - dur xs i = elapsed (xs !! i) (xs !! Suc i)"
 apply (induction i arbitrary: xs)
  apply simp
  apply (subst stream.collapse[symmetric])
  apply (rewrite in "stl _" stream.collapse[symmetric])
  apply (subst dur.simps)
  apply simp
 apply simp
 subgoal for i xs
  apply (subst stream.collapse[symmetric])
  apply (rewrite in "stl _" stream.collapse[symmetric])
  apply (subst dur.simps)
  apply simp
  apply (rewrite in "dur xs (Suc _)" stream.collapse[symmetric])
  apply (rewrite at "stl xs" in "_ ## stl xs" stream.collapse[symmetric])
  apply (subst dur.simps)
  apply simp
 done
done

inductive trans where
  succ: "t ≥ 0 ⟹ u' = u ⊕ t ⟹ trans u u'" |
  reset: "set l ⊆ 𝒳 ⟹ u' = clock_set l 0 u ⟹ trans u u'" |
  id: "u = u' ⟹ trans u u'"

abbreviation "stream_trans ≡ pairwise trans"

lemma K_cfg_trans:
  assumes "cfg ∈ MDP.cfg_on (l, R)" "cfg' ∈ K_cfg cfg" "state cfg' = (l', R')"
  shows "trans R R'"
using assms
 apply (simp add: set_K_cfg)
 apply (drule MDP.cfg_onD_action)
 apply (cases rule: K.cases)
    apply (auto intro: trans.intros)
using admissible_targets_clocks(2) by (blast intro: trans.intros(2))

lemma enabled_stream_trans:
  assumes "cfg ∈ valid_cfg" "MDP.MC.enabled cfg xs"
  shows "stream_trans (smap (snd o state) xs)"
  using assms
proof (coinduction arbitrary: cfg xs)
  case prems: (pairwise cfg xs)
  let ?xs = "stl (stl xs)" let ?x = "shd xs" let ?y = "shd (stl xs)"
  from MDP.pred_stream_cfg_on[OF prems] have *:
    "pred_stream (λcfg. state cfg ∈ S ∧ cfg ∈ MDP.cfg_on (state cfg)) xs" .
  obtain l R l' R' where eq: "state ?x = (l, R)" "state ?y = (l', R')" by force
  moreover from * have "?x ∈ MDP.cfg_on (state ?x)" "?x ∈ valid_cfg"
    by (auto intro: MDP.valid_cfgI simp: stream.pred_set)
  moreover from prems(2) have "?y ∈ K_cfg ?x" by (auto elim: MDP.MC.enabled.cases)
  ultimately have "trans R R'"
    by (intro K_cfg_trans[where cfg = ?x and cfg' = ?y and l = l and l' = l']) metis+
  with ‹?x ∈ valid_cfg› prems(2) show ?case
    apply (inst_existentials R R' "smap (snd o state) ?xs")
      apply (simp add: eq; fail)+
    apply (rule disjI1, inst_existentials ?x "stl xs")
    by (auto simp: eq elim: MDP.MC.enabled.cases)
qed

lemma stream_trans_trans:
  assumes "stream_trans xs"
  shows "trans (xs !! i) (stl xs !! i)"
using pairwise_Suc assms by auto

lemma trans_eq_elapsed:
  assumes "trans u u'" "u ∈ V"
  shows "eq_elapsed u u'"
using assms
proof cases
  case (succ t)
  with finite(1) show ?thesis by (auto simp: cval_add_def elapsed_def max_def eq_elapsed_def)
next
  case prems: (reset l)
  then have "u' c - u c ≤ 0" if "c ∈ 𝒳" for c
  using that ‹u ∈ V› by (cases "c ∈ set l") (auto simp: V_def)
  then have "elapsed u u' = 0" unfolding elapsed_def using finite(1)
   apply simp
   apply (subst Max_insert2)
  by auto
  then show ?thesis by (auto simp: eq_elapsed_def)
next
  case id
  then show ?thesis
    using finite(1) by (auto simp: Max_gr_iff elapsed_def eq_elapsed_def)
qed

lemma pairwise_trans_eq_elapsed:
  assumes "stream_trans xs" "pred_stream (λ u. u ∈ V) xs"
  shows "pairwise eq_elapsed xs"
using trans_eq_elapsed assms by (auto intro: pairwise_mp simp: stream.pred_set)

lemma not_reset_dur:
  assumes "∀k>i. k ≤ j ⟶ ¬ zero c ([xs !! k]⇩ℛ)" "j ≥ i" "c ∈ 𝒳" "stream_trans xs"
    "∀ i. eq_elapsed (xs !! i) (xs !! Suc i)" "∀ i. xs !! i ∈ V"
  shows "dur xs j - dur xs i = (xs !! j) c - (xs !! i) c"
  using assms
proof (induction j)
  case 0 then show ?case by simp
next
  case (Suc j)
  from stream_trans_trans[OF Suc.prems(4)] have trans: "trans (xs !! j) (xs !! Suc j)" by auto
  from Suc.prems have *:
    "¬ zero c ([xs !! Suc j]⇩ℛ)" "eq_elapsed (xs !! j) (xs !! Suc j)" if "Suc j > i"
    using that by auto
  from Suc.prems(6) have "xs !! j ∈ V" "xs !! Suc j ∈ V" by blast+
  then have regions: "[xs !! j]⇩ℛ ∈ ℛ" "[xs !! Suc j]⇩ℛ ∈ ℛ" by auto
  from trans have "(xs !! Suc j) c - (xs !! j) c ≥ 0" if "Suc j > i"
  proof (cases)
    case succ
    with regions show ?thesis by (auto simp: cval_add_def)
  next
    case prems: (reset l)
    show ?thesis
    proof (cases "c ∈ set l")
      case False
      with prems show ?thesis by auto
    next
      case True
      with prems have "(xs !! Suc j) c = 0" by auto
      moreover from assms have "xs !! Suc j ∈ [xs !! Suc j]⇩ℛ" by blast
      ultimately have
        "zero c ([xs !! Suc j]⇩ℛ)"
        using zero_all[OF finite(1) _ ‹c ∈ 𝒳›] regions(2) by (auto simp: ℛ_def)
      with * that show ?thesis by auto
    qed
  next
    case id then show ?thesis by simp
  qed
  with * ‹c ∈ 𝒳› elapsed_eq have
    *: "elapsed (xs !! j) (xs !! Suc j) = (xs !! Suc j) c - (xs !! j) c"
    if "Suc j > i"
    using that by blast
  show ?case
  proof (cases "i = Suc j")
    case False
    with Suc have
      "dur xs (Suc j) - dur xs i = dur xs (Suc j) - dur xs j + (xs !! j) c - (xs !! i) c"
      by auto
    also have "… = elapsed (xs !! j) (xs !! Suc j) + (xs !! j) c - (xs !! i) c"
      by (simp add: dur_Suc)
    also have
      "… = (xs !! Suc j) c - (xs !! j) c  + (xs !! j) c - (xs !! i) c"
      using * False Suc.prems by auto
    also have "… = (xs !! Suc j) c - (xs !! i) c" by simp
    finally show ?thesis by auto
  next
    case True
    then show ?thesis by simp
  qed
qed

lemma not_reset_dur':
  assumes "∀j≥i. ¬ zero c ([xs !! j]⇩ℛ)" "j ≥ i" "c ∈ 𝒳" "stream_trans xs"
          "∀ i. eq_elapsed (xs !! i) (xs !! Suc i)" "∀ j. xs !! j ∈ V"
  shows "dur xs j - dur xs i = (xs !! j) c - (xs !! i) c"
using assms not_reset_dur by auto

lemma not_reset_unbounded:
  assumes "∀j≥i. ¬ zero c ([xs !! j]⇩ℛ)" "j ≥ i" "c ∈ 𝒳" "stream_trans xs"
          "∀ i. eq_elapsed (xs !! i) (xs !! Suc i)" "∀ j. xs !! j ∈ V"
          "unbounded c ([xs !! i]⇩ℛ)"
  shows "unbounded c ([xs !! j]⇩ℛ)"
proof -
  let ?u = "xs !! i" let ?u' = "xs !! j" let ?R = "[xs !! i]⇩ℛ"
  from assms have "?u ∈ ?R" by auto
  from assms(6) have "?R ∈ ℛ" by auto
  then obtain I r where "?R = region 𝒳 I r" "valid_region 𝒳 k I r" unfolding ℛ_def by auto
  with assms(3,7) unbounded_Greater ‹?u ∈ ?R› have "?u c > k c" by force
  also from not_reset_dur'[OF assms(1-6)] dur_mono[OF ‹j ≥ i›, of xs] have "?u' c ≥ ?u c" by auto
  finally have "?u' c > k c" by auto
  let ?R' = "[xs !! j]⇩ℛ"
  from assms have "?u' ∈ ?R'" by auto
  from assms(6) have "?R' ∈ ℛ" by auto
  then obtain I r where "?R' = region 𝒳 I r" "valid_region 𝒳 k I r" unfolding ℛ_def by auto
  moreover with ‹?u' c > _› ‹?u' ∈ _› gt_GreaterD ‹c ∈ 𝒳› have "I c = Greater (k c)" by auto
  ultimately show ?thesis using Greater_unbounded[OF finite(1) _ ‹c ∈ 𝒳›] by auto
qed

lemma gt_unboundedD:
  assumes "u ∈ R"
    and "R ∈ ℛ"
    and "c ∈ 𝒳"
    and "real (k c) < u c"
  shows "unbounded c R"
proof -
  from assms obtain I r where "R = region 𝒳 I r" "valid_region 𝒳 k I r"
    unfolding ℛ_def by auto
  with Greater_unbounded[of 𝒳 k I r c] gt_GreaterD[of u 𝒳 I r k c] assms finite(1) show ?thesis
    by auto
qed

definition trans' :: "('c, t) cval ⇒ ('c, t) cval ⇒ bool" where
  "trans' u u' ≡
    ((∀ c ∈ 𝒳. u c > k c ∧ u' c > k c ∧ u ≠ u') ⟶ u' = u ⊕ 0.5) ∧
    ((∃ c ∈ 𝒳. u c = 0 ∧ u' c > 0 ∧ (∀c∈𝒳. ∄d. d ≤ k c ∧ u' c = real d))
    ⟶ u' = delayedR ([u']⇩ℛ) u)"

(* XXX Move *)
lemma zeroI:
  assumes "c ∈ 𝒳" "u ∈ V" "u c = 0"
  shows "zero c ([u]⇩ℛ)"
proof -
  from assms have "u ∈ [u]⇩ℛ" "[u]⇩ℛ ∈ ℛ" by auto
  then obtain I r where "[u]⇩ℛ = region 𝒳 I r" "valid_region 𝒳 k I r" unfolding ℛ_def by auto
  with zero_all[OF finite(1) this(2) ‹c ∈ 𝒳›] ‹u ∈ [u]⇩ℛ› ‹u c = 0› show ?thesis by auto
qed

(* XXX Move, rename *)
lemma zeroD:
  "u x = 0" if "zero x ([u]⇩ℛ)" "u ∈ V"
  using that by (metis regions_part_ex(1) zero_def)

lemma not_zeroD:
  assumes "¬ zero x ([u]⇩ℛ)" "u ∈ V" "x ∈ 𝒳"
  shows "u x > 0"
proof -
  from zeroI assms have "u x ≠ 0" by auto
  moreover from assms have "u x ≥ 0" unfolding V_def by auto
  ultimately show ?thesis by auto
qed

(* XXX Move *)
lemma not_const_intv:
  assumes "u ∈ V" "∀c∈𝒳. ∄d. d ≤ k c ∧ u c = real d"
  shows "∀c∈𝒳. ∀u ∈ [u]⇩ℛ. ∄d. d ≤ k c ∧ u c = real d"
proof -
  from assms have "u ∈ [u]⇩ℛ" "[u]⇩ℛ ∈ ℛ" by auto
  then obtain I r where I: "[u]⇩ℛ = region 𝒳 I r" "valid_region 𝒳 k I r" unfolding ℛ_def by auto
  have "∄d. d ≤ k c ∧ u' c = real d" if "c ∈ 𝒳" "u' ∈ [u]⇩ℛ" for c u'
  proof safe
    fix d assume A: "d ≤ k c" "u' c = real d"
    from I that have "intv_elem c u' (I c)" "valid_intv (k c) (I c)" by auto
    then show False
      using A I ‹u ∈ [u]⇩ℛ› ‹c ∈ 𝒳› assms(2) by (cases; fastforce)
  qed
  then show ?thesis by auto
qed

lemma K_cfg_trans':
  assumes "repcs (l, u) cfg ∈ MDP.cfg_on (l, u)" "cfg' ∈ K_cfg (repcs (l, u) cfg)"
          "state cfg' = (l', u')" "(l, u) ∈ S" "cfg ∈ R_G.valid_cfg" "abss (l, u) = state cfg"
  shows "trans' u u'"
using assms
 apply (simp add: set_K_cfg)
 apply (drule MDP.cfg_onD_action)
 apply (cases rule: K.cases)
 apply assumption
proof goal_cases
  case prems: (1 l u t)
  from assms ‹_ = (l, u)› have "repcs (l, u) cfg ∈ valid_cfg" by (auto intro: MDP.valid_cfgI)
  then have "absc (repcs (l, u) cfg) ∈ R_G.valid_cfg" by auto
  from prems have *: "rept (l, u) (action cfg) = return_pmf (l, u ⊕ t)" unfolding repcs_def by auto
  from ‹abss _ = _› ‹_ = (l, u)› ‹cfg ∈ R_G.valid_cfg› have
    "action cfg ∈ 𝒦 (abss (l, u))"
  by (auto dest: R_G_I)
  from abst_rept_id[OF this] * have "action cfg = abst (return_pmf (l, u ⊕ t))" by auto
  with prems have **: "action cfg = return_pmf (l, [u ⊕ t]⇩ℛ)" unfolding abst_def by auto
  show ?thesis
  proof (cases "∀ c ∈ 𝒳. u c > k c")
    case True
    from prems have "u ⊕ t ∈ [u]⇩ℛ" by (auto intro: upper_right_closed[OF True])
    with prems have "[u ⊕ t]⇩ℛ = [u]⇩ℛ" by (auto dest: alpha_interp.region_unique_spec)
    with ** have "action cfg = return_pmf (l, [u]⇩ℛ)" by simp
    with True have "rept (l, u) (action cfg) = return_pmf (l, u ⊕ 0.5)" 
    unfolding rept_def using prems by auto
    with * have "u ⊕ t = u ⊕ 0.5" by auto
    moreover from prems have "u' = u ⊕ t" by auto
    moreover from prems True have "∀ c ∈ 𝒳. u' c > k c" by (auto simp: cval_add_def)
    ultimately show ?thesis using True ‹_ = (l, u)› unfolding trans'_def by auto
  next
    case F: False
    show ?thesis
    proof (cases "∃c∈𝒳. u c = 0 ∧ 0 < u' c ∧ (∀c∈𝒳. ∄d. d ≤ k c ∧ u' c = real d)")
      case True
      from prems have "u' ∈ [u']⇩ℛ" by auto
      from prems have "[u ⊕ t]⇩ℛ ∈ Succ ℛ ([u]⇩ℛ)" by auto
      from True obtain c where "c ∈ 𝒳" "u c = 0" "u' c > 0" by auto
      with zeroI prems have "zero c ([u]⇩ℛ)" by auto
      moreover from ‹u' ∈ _› ‹u' c > 0› have "¬ zero c ([u']⇩ℛ)" unfolding zero_def by fastforce
      ultimately have "[u ⊕ t]⇩ℛ ≠ [u]⇩ℛ" using prems by auto
      moreover from True not_const_intv prems have
        "∀ u ∈ [u ⊕ t]⇩ℛ. ∀c∈𝒳. ∄d. d ≤ k c ∧ u c = real d"
      by auto
      ultimately have "∃R'. (l, u) ∈ S ∧
                     action cfg = return_pmf (l, R') ∧
                     R' ∈ Succ ℛ ([u]⇩ℛ) ∧ [u]⇩ℛ ≠ R' ∧ (∀u∈R'. ∀c∈𝒳. ∄d. d ≤ k c ∧ u c = real d)"
       apply -
       apply (rule exI[where x = "[u ⊕ t]⇩ℛ"])
       apply safe
      using prems ** by auto
      then have
        "rept (l, u) (action cfg)
       = return_pmf (l, delayedR (SOME R'. action cfg = return_pmf (l, R')) u)" 
      unfolding rept_def by auto
      with * ** prems have "u' = delayedR ([u ⊕ t]⇩ℛ) u" by auto
      with F True prems show ?thesis unfolding trans'_def by auto
    next
      case False
      with F ‹_ = (l, u)› show ?thesis unfolding trans'_def by auto
    qed
  qed
next
  case prems: (2 _ _ τ μ)
  then obtain X where X: "u' = ([X := 0]u)" "(X, l') ∈ set_pmf μ" by auto
  from ‹_ ∈ S› have "u ∈ V" by auto
  let ?r = "SOME r. set r = X"
  show ?case
  proof (cases "X = {}")
    case True
    with X have "u = u'" by auto
    with non_empty show ?thesis unfolding trans'_def by auto
  next
    case False
    then obtain x where "x ∈ X" by auto
    moreover have "X ⊆ 𝒳" using admissible_targets_clocks(1)[OF prems(10) X(2)] by auto
    ultimately have "x ∈ 𝒳" by auto
    from ‹X ⊆ 𝒳› finite(1) obtain r where "set r = X" using finite_list finite_subset by blast
    then have r: "set ?r = X" by (rule someI)
    with ‹x ∈ X› X have "u' x = 0" by auto
    from X r ‹u ∈ V› ‹X ⊆ 𝒳› have "u' x ≤ u x" for x
      by (cases "x ∈ X"; auto simp: V_def)
    have False if "u' x > 0 ∧ u x = 0" for x
      using ‹u' _ ≤ _›[of x] that by auto
    with ‹u' x = 0› show ?thesis using ‹x ∈ 𝒳› unfolding trans'_def by auto
  qed
next
  case 3
  with non_empty show ?case unfolding trans'_def by auto
qed

coinductive enabled_repcs where
  "enabled_repcs (shd xs) (stl xs) ⟹ shd xs = repcs st' cfg' ⟹ st' ∈ rept st (action cfg)
  ⟹ abss st' = state cfg'
  ⟹ cfg' ∈ R_G.valid_cfg
  ⟹ enabled_repcs (repcs st cfg) xs"

(* XXX Move *)
lemma K_cfg_rept_in:
assumes "cfg ∈ R_G.valid_cfg"
    and "abss st = state cfg"
    and "cfg' ∈ K_cfg cfg"
  shows "(THE s'. s' ∈ set_pmf (rept st (action cfg)) ∧ abss s' = state cfg')
         ∈ set_pmf (rept st (action cfg))"
proof -
  from assms(1,2) have "action cfg ∈ 𝒦 (abss st)" by (auto simp: R_G_I)
  from ‹cfg' ∈ _› have
    "cfg' = cont cfg (state cfg')" "state cfg' ∈ action cfg"
  by (auto simp: set_K_cfg)
  with abst_rept_id[OF ‹action _ ∈ _›] pmf.set_map have
    "state cfg' ∈ abss ` set_pmf (rept st (action cfg))" unfolding abst_def  by metis
  then obtain st' where
    "st' ∈ rept st (action cfg)" "abss st' = state cfg'"
  unfolding abst_def by auto
  with K_cfg_rept_aux[OF assms(1,2) this(1)] show ?thesis by auto
qed

lemma enabled_repcsI:
  assumes "cfg ∈ R_G.valid_cfg" "abss st = state cfg" "MDP.MC.enabled (repcs st cfg) xs"
  shows "enabled_repcs (repcs st cfg) xs" using assms
proof (coinduction arbitrary: cfg xs st)
  case prems: (enabled_repcs cfg xs st)
  let ?x = "shd xs" and ?y = "shd (stl xs)"
  let ?st = "THE s'. s' ∈ set_pmf (rept st (action cfg)) ∧ abss s' = state (absc ?x)"
  from prems(3) have "?x ∈ K_cfg (repcs st cfg)" by cases
  with K_cfg_map_repcs[OF prems(1,2)] obtain cfg' where
    "cfg' ∈ K_cfg cfg" "?x = repcs (THE s'. s' ∈ rept st (action cfg) ∧ abss s' = state cfg') cfg'"
    by auto
  let ?st = "THE s'. s' ∈ rept st (action cfg) ∧ abss s' = state cfg'"
  from K_cfg_rept_action[OF prems(1,2) ‹cfg' ∈ _›] have "abss ?st = state cfg'" .
  moreover from K_cfg_rept_in[OF prems(1,2) ‹cfg' ∈ _›] have "?st ∈ rept st (action cfg)" .
  moreover have "cfg' ∈ R_G.valid_cfg" using ‹cfg' ∈ K_cfg cfg› prems(1) by blast 
  moreover from absc_repcs_id[OF this ‹abss ?st = state cfg'›] ‹?x = _› have "absc ?x = cfg'"
    by auto
  moreover from prems(3) have "MDP.MC.enabled (shd xs) (stl xs)" by cases
  ultimately show ?case
    using ‹?x = _› by (inst_existentials xs ?st "absc ?x" st cfg) fastforce+
qed

lemma repcs_eq_rept:
  "rept st (action cfg) = rept st'' (action cfg'')" if "repcs st cfg = repcs st'' cfg''"
   by (metis (mono_tags, lifting) action_cfg_corec old.prod.case repcs_def that)

lemma enabled_stream_trans':
  assumes "cfg ∈ R_G.valid_cfg" "abss st = state cfg" "MDP.MC.enabled (repcs st cfg) xs"
  shows "pairwise trans' (smap (snd o state) xs)"
using assms
proof (coinduction arbitrary: cfg xs st)
  case prems: (pairwise cfg xs)
  let ?xs = "stl xs"
  from prems have A: "enabled_repcs (repcs st cfg) xs" by (auto intro: enabled_repcsI)
  then obtain st' cfg' where
    "enabled_repcs (shd xs) (stl xs)" "shd xs = repcs st' cfg'" "st' ∈ rept st (action cfg)"
    "abss st' = state cfg'" "cfg' ∈ R_G.valid_cfg"
   apply atomize_elim
   apply (cases rule: enabled_repcs.cases)
   apply assumption
   subgoal for st' cfg' st'' cfg''
     by (inst_existentials st' cfg') (auto dest: repcs_eq_rept)
  done
  then obtain st'' cfg'' where
    "enabled_repcs (shd ?xs) (stl ?xs)"
    "shd ?xs = repcs st'' cfg''" "st'' ∈ rept st' (action cfg')" "abss st'' = state cfg''"
    by atomize_elim (subst (asm)enabled_repcs.simps, fastforce dest: repcs_eq_rept)
  let ?x = "shd xs" let ?y = "shd (stl xs)"
  let ?cfg = "repcs st cfg"
  from prems have "?cfg ∈ valid_cfg" by auto
  from MDP.pred_stream_cfg_on[OF ‹?cfg ∈ valid_cfg› prems(3)] have *:
    "pred_stream (λcfg. state cfg ∈ S ∧ cfg ∈ MDP.cfg_on (state cfg)) xs" .
  obtain l u l' u' where eq: "st' = (l, u)" "st'' = (l', u')"
    by force
  moreover from * have
    "?x ∈ MDP.cfg_on (state ?x)" "?x ∈ valid_cfg"
    by (auto intro: MDP.valid_cfgI simp: stream.pred_set)
  moreover from prems(3) have "?y ∈ K_cfg ?x" by (auto elim: MDP.MC.enabled.cases)
  ultimately have "trans' u u'"
    using ‹?x = _› ‹?y = _› ‹cfg' ∈ _› ‹abss st' = _›
    by (intro K_cfg_trans') (auto dest: MDP.valid_cfg_state_in_S)
  with ‹?x ∈ valid_cfg› ‹cfg' ∈ R_G.valid_cfg› prems(3) ‹abss _ = state cfg'› show ?case
    apply (inst_existentials u u' "smap (snd o state) (stl ?xs)")
    apply (simp add: eq ‹?x = _› ‹?y = _›; fail)+
    by ((intro disjI1 exI)?; auto simp: ‹?x = _› ‹?y = _› eq elim: MDP.MC.enabled.cases)
qed

lemma divergent_ℛ_divergent:
  assumes in_S: "pred_stream (λ u. u ∈ V) xs"
     and  div:  "divergent xs"
     and trans: "stream_trans xs"
  shows "ℛ_div (smap (λ u. [u]⇩ℛ) xs)" (is "ℛ_div ?ω")
unfolding ℛ_div_def proof (safe, simp_all)
  fix x i
  assume x: "x ∈ 𝒳" and bounded: "∀i. ∃j≥i. ¬ unbounded x ([xs !! j]⇩ℛ)"
  from in_S have xs_ω: "∀i. xs !! i ∈ ?ω !! i" by (auto simp: stream.pred_set)
  from trans in_S have elapsed:
    "∀ i. eq_elapsed (xs !! i) (xs !! Suc i)"
    by (fastforce intro: pairwise_trans_eq_elapsed pairwise_Suc[where P = eq_elapsed])
  { assume A: "∀j ≥ i. ¬ zero x ([xs !! j]⇩ℛ)"
    let ?t = "dur xs i + k x"
    from div obtain j where j: "dur xs j > dur xs i + k x" unfolding divergent_def by auto
    then have "k x < dur xs j - dur xs i" by auto
    also with not_reset_dur'[OF A less_imp_le[OF dur_monoD], of xs] ‹x ∈ 𝒳› assms elapsed have
      "… = (xs !! j) x - (xs !! i) x"
      by (auto simp: stream.pred_set)
    also have "… ≤ (xs !! j) x"
      using assms(1) ‹x ∈ 𝒳› unfolding V_def by (auto simp: stream.pred_set)
    finally have "unbounded x ([xs !! j]⇩ℛ)"
      using assms ‹x ∈ 𝒳› by (intro gt_unboundedD) (auto simp: stream.pred_set)
    moreover from dur_monoD[of xs i j] j A have "∀j' ≥ j. ¬ zero x ([xs !! j']⇩ℛ)" by auto
    ultimately have "∀i≥j. unbounded x ([xs !! i]⇩ℛ)"
      using elapsed assms x by (auto intro: not_reset_unbounded simp: stream.pred_set)
    with bounded have False by auto
  }
  then show "∃j≥i. zero x ([xs !! j]⇩ℛ)" by auto
  { assume A: "∀j ≥ i. zero x ([xs !! j]⇩ℛ)"
    from div obtain j where j: "dur xs j > dur xs i" unfolding divergent_def by auto
    then have "j ≥ i" by (auto dest: dur_monoD)
    from A have "∀j ≥ i. zero x (?ω !! j)" by auto
    with dur_zero_tail[OF xs_ω _ x ‹i ≤ j› elapsed] j have False by simp
  }
  then show "∃j≥i. ¬ zero x ([xs !! j]⇩ℛ)" by auto
qed

lemma (in -)
  fixes f :: "nat ⇒ real"
  assumes "∀ i. f i ≥ 0" "∀ i. ∃ j ≥ i. f j > d" "d > 0"
  shows "∃ n. (∑ i ≤ n. f i) > t"
  oops

(* TODO: Reduce this proof to a more general theorem *)
lemma dur_ev_exceedsI:
  assumes "∀ i. ∃ j ≥ i. dur xs j - dur xs i ≥ d" and "d > 0"
  obtains i where "dur xs i > t"
proof -
  have base: "∃ i. dur xs i > t" if "t < d" for t
  proof -
    from assms obtain j where "dur xs j - dur xs 0 ≥ d" by fastforce
    with dur_pos[of xs 0] have "dur xs j ≥ d" by simp
    with ‹d > 0› ‹t < d› show ?thesis by - (rule exI[where x = j]; auto)
  qed
  have base2: "∃ i. dur xs i > t" if "t ≤ d" for t
  proof (cases "t = d")
    case False
    with ‹t ≤ d› base show ?thesis by simp
  next
    case True
    from base ‹d > 0› obtain i where "dur xs i > 0" by auto
    moreover from assms obtain j where "dur xs j - dur xs i ≥ d" by auto
    ultimately have "dur xs j > d" by auto
    with ‹t = d› show ?thesis by auto
  qed
  show ?thesis
  proof (cases "t ≥ 0")
    case False
    with dur_pos have "dur xs 0 > t" by auto
    then show ?thesis by (fastforce intro: that)
  next
    case True
    let ?m = "nat ⌈t / d⌉"
    from True have "∃ i. dur xs i > ?m * d"
    proof (induction ?m arbitrary: t)
      case 0
      with base[OF ‹0 < d›] show ?case by simp
    next
      case (Suc n t)
      let ?t = "t - d"
      show ?case
      proof (cases "t ≥ d")
        case True
        have "?t / d = t / d - 1"
        (* Generated by sledgehammer *)
        (* Alternative: by (smt assms(2) diff_divide_distrib divide_self_if) *)
        proof -
          have "t / d + - 1 * ((t + - 1 * d) / d) + - 1 * (d / d) = 0"
            by (simp add: diff_divide_distrib)
          then have "t / d + - 1 * ((t + - 1 * d) / d) = 1"
            using assms(2) by fastforce
          then show ?thesis
            by algebra
        qed
        then have "⌈?t / d⌉ = ⌈t / d⌉ - 1" by simp
        with ‹Suc n = _› have "n = nat ⌈?t / d⌉" by simp
        with Suc ‹t ≥ d› obtain i where "nat ⌈?t / d⌉ * d < dur xs i" by fastforce
        from assms obtain j where "dur xs j - dur xs i ≥ d" "j ≥ i" by auto
        with ‹dur xs i > _› have "nat ⌈?t / d⌉ * d + d < dur xs j" by simp
        with True have "dur xs j > nat ⌈t / d⌉ * d"
        by (metis Suc.hyps(2) ‹n = nat ⌈(t - d) / d⌉› add.commute distrib_left mult.commute 
                  mult.right_neutral of_nat_Suc) 
        then show ?thesis by blast
      next
        case False
        with ‹t ≥ 0› ‹d > 0› have "nat ⌈t / d⌉ ≤ 1" by simp
        then have "nat ⌈t / d⌉ * d ≤ d"
        by (metis One_nat_def ‹Suc n = _› Suc_leI add.right_neutral le_antisym mult.commute
                  mult.right_neutral of_nat_0 of_nat_Suc order_refl zero_less_Suc) 
        with base2 show ?thesis by auto
      qed
    qed
    then obtain i where "dur xs i > ?m * d" by atomize_elim
    moreover from ‹t ≥ 0› ‹d > 0› have "?m * d ≥ t"
      using pos_divide_le_eq real_nat_ceiling_ge by blast
    ultimately show ?thesis using that[of i] by simp
  qed
qed

lemma not_reset_mono:
  assumes "stream_trans xs" "shd xs c1 ≥ shd xs c2" "stream_all (λ u. u ∈ V) xs" "c2 ∈ 𝒳"
  shows "(holds (λ u. u c1 ≥ u c2) until holds (λ u. u c1 = 0)) xs" using assms
proof (coinduction arbitrary: xs)
  case prems: (UNTIL xs)
  let ?xs = "stl xs"
  let ?x = "shd xs"
  let ?y = "shd ?xs"
  show ?case
  proof (cases "?x c1 = 0")
    case False
    show ?thesis
    proof (cases "?y c1 = 0")
      case False
      from prems have "trans ?x ?y" by (intro pairwise_pairD[of trans])
      then have "?y c1 ≥ ?y c2"
      proof cases
        case A: (reset t)
        show ?thesis
        proof (cases "c1 ∈ set t")
          case True
          with A False show ?thesis by auto
        next
          case False
          from prems have "?x c2 ≥ 0" by (auto simp: V_def)
          with A have "?y c2 ≤ ?x c2" by (cases "c2 ∈ set t") auto
          with A False ‹?x c1 ≥ ?x c2› show ?thesis by auto
        qed
      qed (use prems in ‹auto simp: cval_add_def›)
      moreover from prems have "stream_trans ?xs" "stream_all (λ u. u ∈ V) ?xs"
        by (auto intro: pairwise_stlD stl_sset)
      ultimately show ?thesis
        using prems by auto
    qed (use prems in ‹auto intro: UNTIL.base›)
  qed auto
qed

lemma ℛ_divergent_divergent_aux:
  fixes xs :: "('c, t) cval stream"
  assumes "stream_trans xs" "stream_all (λ u. u ∈ V) xs"
          "(xs !! i) c1 = 0" "∃ k > i. k ≤ j ∧ (xs !! k) c2 = 0"
          "∀ k > i. k ≤ j ⟶ (xs !! k) c1 ≠ 0"
          "c1 ∈ 𝒳" "c2 ∈ 𝒳"
  shows "(xs !! j) c1 ≥ (xs !! j) c2"
proof -
  from assms obtain k where k: "k > i" "k ≤ j" "(xs !! k) c2 = 0" by auto
  with assms(5) ‹k ≤ j› have "(xs !! k) c1 ≠ 0" by auto
  moreover from assms(2) ‹c1 ∈ 𝒳› have "(xs !! k) c1 ≥ 0" by (auto simp: V_def)
  ultimately have "(xs !! k) c1 > 0" by auto
  with ‹(xs !! k) c2 = 0› have "shd (sdrop k xs) c1 ≥ shd (sdrop k xs) c2" by auto
  from not_reset_mono[OF _ this] assms have
    "(holds (λu. u c2 ≤ u c1) until holds (λu. u c1 = 0)) (sdrop k xs)"
  by (auto intro: sset_sdrop pairwise_sdropD)
  from assms(5) k(2) ‹k > i› have "∀ m ≤ j - k. (sdrop k xs !! m) c1 ≠ 0" by simp
  with holds_untilD[OF ‹(_ until _) _›, of "j - k"] have
    "(sdrop k xs !! (j - k)) c2 ≤ (sdrop k xs !! (j - k)) c1" .
  then show "(xs !! j) c2 ≤ (xs !! j) c1" using k(1,2) by simp
qed

lemma unbounded_all:
  assumes "R ∈ ℛ" "u ∈ R" "unbounded x R" "x ∈ 𝒳"
  shows "u x > k x"
proof -
  from assms obtain I r where R: "R = region 𝒳 I r" "valid_region 𝒳 k I r" unfolding ℛ_def by auto
  with unbounded_Greater ‹x ∈ 𝒳› assms(3) have "I x = Greater (k x)" by simp
  with ‹u ∈ R› R ‹x ∈ 𝒳› show ?thesis by force
qed

lemma trans_not_delay_mono:
  "u' c ≤ u c" if "trans u u'" "u ∈ V" "x ∈ 𝒳" "u' x = 0" "c ∈ 𝒳"
  using ‹trans u u'›
proof (cases)
  case (reset l)
  with that show ?thesis by (cases "c ∈ set l") (auto simp: V_def)
qed (use that in ‹auto simp: cval_add_def V_def add_nonneg_eq_0_iff›)

lemma dur_reset:
  assumes "pairwise eq_elapsed xs" "pred_stream (λ u. u ∈ V) xs" "zero x ([xs !! Suc i]⇩ℛ)" "x ∈ 𝒳"
  shows "dur xs (Suc i) - dur xs i = 0"
proof -
  from assms(2) have in_V: "xs !! Suc i ∈ V"
    unfolding stream.pred_set by auto (metis snth.simps(2) snth_sset)
  with elapsed_ge_pos[of "xs !! i" "xs !! Suc i" x] pairwise_Suc[OF assms(1)] assms(2-) have
    "elapsed (xs !! i) (xs !! Suc i) ≤ (xs !! Suc i) x"
    unfolding stream.pred_set by auto
  with in_V assms(3) have "elapsed (xs !! i) (xs !! Suc i) ≤ 0" by (auto simp: zeroD)
  with elapsed_ge0[of "xs !! i" "xs !! Suc i"] have "elapsed (xs !! i) (xs !! Suc i) = 0"
    by linarith
  then show ?thesis by (subst dur_Suc)
qed

lemma resets_mono_0':
  assumes "pairwise eq_elapsed xs" "stream_all (λ u. u ∈ V) xs" "stream_trans xs"
          "∀ j ≤ i. zero x ([xs !! j]⇩ℛ)" "x ∈ 𝒳" "c ∈ 𝒳"
  shows "(xs !! i) c = (xs !! 0) c ∨ (xs !! i) c = 0"
using assms proof (induction i)
  case 0
  then show ?case by auto
next        
  case (Suc i)
  from Suc.prems have *: "(xs !! Suc i) x = 0" "(xs !! i) x = 0"
    by (blast intro: zeroD snth_sset, force intro: zeroD snth_sset)
  from pairwise_Suc[OF Suc.prems(3)] have "trans (xs !! i) (xs !! Suc i)" .
  then show ?case
  proof cases
    case prems: (succ t)
    with * have "t = 0" unfolding cval_add_def by auto
    with prems have "(xs !! Suc i) c = (xs !! i) c" unfolding cval_add_def by auto
    with Suc show ?thesis by auto
  next
    case prems: (reset l)
    then have "(xs !! Suc i) c = 0 ∨ (xs !! Suc i) c = (xs !! i) c" by (cases "c ∈ set l") auto
    with Suc show ?thesis by auto
  next
    case id
    with Suc show ?thesis by auto
  qed
qed

lemma resets_mono':
  assumes "pairwise eq_elapsed xs" "pred_stream (λ u. u ∈ V) xs" "stream_trans xs"
          "∀ k ≥ i. k ≤ j ⟶ zero x ([xs !! k]⇩ℛ)" "x ∈ 𝒳" "c ∈ 𝒳" "i ≤ j"
  shows "(xs !! j) c = (xs !! i) c ∨ (xs !! j) c = 0" using assms
proof -
  from assms have 1: "stream_all (λ u. u ∈ V) (sdrop i xs)"
    using sset_sdrop unfolding stream.pred_set by force
  from assms have 2: "pairwise eq_elapsed (sdrop i xs)" by (intro pairwise_sdropD)
  from assms have 3: "stream_trans (sdrop i xs)" by (intro pairwise_sdropD)
  from assms have 4:
    "∀k≤j - i. zero x ([sdrop i xs !! k]⇩ℛ)"
  by (simp add: le_diff_conv2 assms(6))
  from resets_mono_0'[OF 2 1 3 4 assms(5,6)] ‹i ≤ j› show ?thesis by simp
qed

lemma resets_mono:
  assumes "pairwise eq_elapsed xs" "pred_stream (λ u. u ∈ V) xs" "stream_trans xs"
          "∀ k ≥ i. k ≤ j ⟶ zero x ([xs !! k]⇩ℛ)" "x ∈ 𝒳" "c ∈ 𝒳" "i ≤ j"
  shows "(xs !! j) c ≤ (xs !! i) c" using assms
  using assms by (auto simp: V_def dest: resets_mono'[where c = c] simp: stream.pred_set)

lemma ℛ_divergent_divergent_aux2:
  fixes M :: "(nat ⇒ bool) set"
  assumes "∀ i. ∀ P ∈ M. ∃ j ≥ i. P j" "M ≠ {}" "finite M"
  shows "∀i.∃j≥i.∃k>j.∃ P ∈ M. P j ∧ P k ∧ (∀ m < k. j < m ⟶ ¬ P m)
       ∧ (∀ Q ∈ M. ∃ m ≤ k. j < m ∧ Q m)"
proof
  fix i
  let ?j1 = "Max {LEAST m. m > i ∧ P m | P. P ∈ M}"
  from ‹M ≠ {}› obtain P where "P ∈ M" by auto
  let ?m = "LEAST m. m > i ∧ P m"
  from assms(1) ‹P ∈ M› obtain j where "j ≥ Suc i" "P j" by auto
  then have "j > i" "P j" by auto
  with ‹P ∈ M› have "?m > i ∧ P ?m" by - (rule LeastI; auto)
  moreover with ‹finite M› ‹P ∈ M› have "?j1 ≥ ?m" by - (rule Max_ge; auto)
  ultimately have "?j1 ≥ i" by simp
  moreover have "∃ m > i. m ≤ ?j1 ∧ P m" if "P ∈ M" for P
  proof -
    let ?m = "LEAST m. m > i ∧ P m"
    from assms(1) ‹P ∈ M› obtain j where "j ≥ Suc i" "P j" by auto
    then have "j > i" "P j" by auto
    with ‹P ∈ M› have "?m > i ∧ P ?m" by - (rule LeastI; auto)
    moreover with ‹finite M› ‹P ∈ M› have "?j1 ≥ ?m" by - (rule Max_ge; auto)
    ultimately show ?thesis by auto
  qed
  ultimately obtain j1 where j1: "j1 ≥ i" "∀ P ∈ M. ∃ m > i. j1 ≥ m ∧ P m" by auto
  define k where "k Q = (LEAST k. k > j1 ∧ Q k)" for Q
  let ?k = "Max {k Q | Q. Q ∈ M}"
  let ?P = "SOME P. P ∈ M ∧ k P = ?k"
  let ?j = "Max {j. i ≤ j ∧ j ≤ j1 ∧ ?P j}"
  have "?k ∈ {k Q | Q. Q ∈ M}" using assms by - (rule Max_in; auto)
  then obtain P where P: "k P = ?k" "P ∈ M" by auto
  have "?k ≥ k Q" if "Q ∈ M" for Q using assms that by - (rule Max_ge; auto)
  have *: "?P ∈ M ∧ k ?P = ?k" using P by - (rule someI[where x = P]; auto)
  with j1 have "∃ m > i. j1 ≥ m ∧ ?P m" by auto
  with ‹finite _› have "?j ∈ {j. i ≤ j ∧ j ≤ j1 ∧ ?P j}" by - (rule Max_in; auto)
  have k: "k Q > j1 ∧ Q (k Q)" if "Q ∈ M" for Q
  proof -
    from assms(1) ‹Q ∈ M› obtain m where "m ≥ Suc j1" "Q m" by auto
    then have "m > j1" "Q m" by auto
    then show "k Q > j1 ∧ Q (k Q)" unfolding k_def by - (rule LeastI; blast)
  qed
  with * ‹?j ∈ _› have "?P ?k" "?j < ?k" by fastforce+
  have "¬ ?P m" if "?j < m" "m < ?k" for m
  proof (rule ccontr, simp)
    assume "?P m"
    have "m > j1"
    proof (rule ccontr)
      assume "¬ j1 < m"
      with ‹?j < m› ‹?j ∈ _› have "i ≤ m" "m ≤ j1" by auto
      with ‹?P m› ‹finite _› have "?j ≥ m" by - (rule Max_ge; auto)
      with ‹?j < m› show False by simp
    qed
    with ‹?P m› ‹finite _› have "k ?P ≤ m" unfolding k_def by (auto intro: Least_le)
    with * ‹m < ?k› show False by auto
  qed
  moreover have "∃ m ≤ ?k. ?j < m ∧ Q m" if "Q ∈ M" for Q
  proof -
    from k[OF ‹Q ∈ M›] have "k Q > j1 ∧ Q (k Q)" .
    moreover with ‹finite _› ‹Q ∈ M› have "k Q ≤ ?k" by - (rule Max_ge; auto)
    moreover with ‹?j ∈ _› ‹k Q > _ ∧ _› have "?j < k Q" by auto
    ultimately show ?thesis by auto
  qed
  ultimately show
    "∃j≥i.∃k>j.∃ P ∈ M. P j ∧ P k ∧ (∀ m < k. j < m ⟶ ¬ P m)
       ∧ (∀ Q ∈ M. ∃ m ≤ k. j < m ∧ Q m)"
    using ‹?j < ?k› ‹?j ∈ _› ‹?P ?k› * by (inst_existentials ?j ?k ?P; blast)
qed

lemma ℛ_divergent_divergent:
  assumes in_S: "pred_stream (λ u. u ∈ V) xs"
    and div: "ℛ_div (smap (λ u. [u]⇩ℛ) xs)"
    and trans: "stream_trans xs"
    and trans': "pairwise trans' xs"
    and unbounded_not_const:
    "∀u. (∀c∈𝒳. real (k c) < u c) ⟶ ¬ ev (alw (λxs. shd xs = u)) xs"
  shows "divergent xs"
  unfolding divergent_def proof
  fix t
  from pairwise_trans_eq_elapsed[OF trans in_S] have eq_elapsed: "pairwise eq_elapsed xs" .
  define X1 where "X1 = {x. x ∈ 𝒳 ∧ (∃i. ∀ j ≥ i. unbounded x ([xs !! j]⇩ℛ))}"
  let ?i = "Max {(SOME i. ∀ j ≥ i. unbounded x ([xs !! j]⇩ℛ)) | x. x ∈ 𝒳}"
  from finite(1) non_empty have
    "?i ∈ {(SOME i. ∀ j ≥ i. unbounded x ([xs !! j]⇩ℛ)) | x. x ∈ 𝒳}"
    by (intro Max_in) auto
  have "unbounded x ([xs !! j]⇩ℛ)" if "x ∈ X1" "j ≥ ?i" for x j
  proof -
    have "X1 ⊆ 𝒳" unfolding X1_def by auto
    with finite(1) non_empty ‹x ∈ X1› have *:
      "?i ≥ (SOME i. ∀ j ≥ i. unbounded x ([xs !! j]⇩ℛ))" (is "?i ≥ ?k")
      by (intro Max_ge) auto
    from ‹x ∈ X1› have "∃ k. ∀ j ≥ k. unbounded x ([xs !! j]⇩ℛ)" by (auto simp: X1_def)
    then have "∀ j ≥ ?k. unbounded x ([xs !! j]⇩ℛ)" by (rule someI_ex)
    moreover from ‹j ≥ ?i› ‹?i ≥ _› have "j ≥ ?k" by auto
    ultimately show ?thesis by blast
  qed
  then obtain i where unbounded: "∀ x ∈ X1. ∀ j ≥ i. unbounded x ([xs !! j]⇩ℛ)"
    using finite by auto
  show "∃ n. t < dur xs n"
  proof (cases "∀ x ∈ 𝒳. (∃i. ∀ j ≥ i. unbounded x ([xs !! j]⇩ℛ))")
    case True
    then have "X1 = 𝒳" unfolding X1_def by auto
    have "∃k≥j. 0.5 ≤ dur xs k - dur xs j" for j
    proof -
      let ?u = "xs !! max i j"
      from in_S have "?u ∈ [?u]⇩ℛ" "[?u]⇩ℛ ∈ ℛ"
        by (auto simp: stream.pred_set)
      moreover from unbounded ‹X1 = 𝒳› have
        "∀ x ∈ 𝒳. unbounded x ([?u]⇩ℛ)"
        by force
      ultimately have "∀ x ∈ 𝒳. ?u x > k x"
        by (auto intro: unbounded_all)
      with unbounded_not_const have "¬ ev (alw (HLD {?u})) xs"
        unfolding HLD_iff by simp
      then obtain r where
        "r ≥ max i j" "xs !! r ≠ xs !! Suc r"
        apply atomize_elim
        apply (simp add: not_ev_iff not_alw_iff)
        apply (drule alw_sdrop[where n = "max i j"])
        apply (drule alwD)
        apply (subst (asm) (3) stream.collapse[symmetric])
        apply simp
        apply (drule ev_neq_start_implies_ev_neq[simplified comp_def])
        using stream.collapse[of "sdrop (max i j) xs"] by (auto 4 3 elim: ev_sdropD)
      let ?k = "Suc r"
      from in_S have "xs !! ?k ∈ V" using snth_sset unfolding stream.pred_set by blast
      with in_S have *:
        "xs !! r ∈ [xs !! r]⇩ℛ" "[xs !! r]⇩ℛ ∈ ℛ"
        "xs !! ?k ∈ [xs !! ?k]⇩ℛ" "[xs !! ?k]⇩ℛ ∈ ℛ"
        by (auto simp: stream.pred_set)
      from ‹r ≥ _› have "r ≥ i" "?k ≥ i" by auto
      with unbounded ‹X1 = 𝒳› have
        "∀ x ∈ 𝒳. unbounded x ([xs !! r]⇩ℛ)" "∀ x ∈ 𝒳. unbounded x ([xs !! ?k]⇩ℛ)"
        by (auto simp del: snth.simps(2))
      with in_S have "∀ x ∈ 𝒳. (xs !! r) x > k x" "∀ x ∈ 𝒳. (xs !! ?k) x > k x"
        using * by (auto intro: unbounded_all)
      moreover from trans' have "trans' (xs !! r) (xs !! ?k)"
        using pairwise_Suc by auto
      ultimately have "(xs !! ?k) = (xs !! r) ⊕ 0.5"
        unfolding trans'_def using ‹xs !! r ≠ _› by auto
      moreover from pairwise_Suc[OF eq_elapsed] have "eq_elapsed (xs !! r) (xs !! ?k)"
        by auto
      ultimately have 
        "dur xs ?k - dur xs r = 0.5"
        using non_empty by (auto simp: cval_add_def dur_Suc elapsed_eq)
      with dur_mono[of j r xs] ‹r ≥ max i j› have "dur xs ?k - dur xs j ≥ 0.5"
        by auto
      with ‹r ≥ max i j› show ?thesis by - (rule exI[where x = ?k]; auto)
    qed
    then show ?thesis by - (rule dur_ev_exceedsI[where d = "0.5"]; auto)
  next
    case False
    define X2 where "X2 = 𝒳 - X1"
    from False have "X2 ≠ {}" unfolding X1_def X2_def by fastforce
    have inf_resets:
      "∀i. (∃j≥i. zero x ([xs !! j]⇩ℛ)) ∧ (∃j≥i. ¬ zero x ([xs !! j]⇩ℛ))" if "x ∈ X2" for x
      using that div unfolding X1_def X2_def ℛ_div_def by fastforce
    have "∃ j ≥ i. ∃ k > j. ∃ x ∈ X2. zero x ([xs !! j]⇩ℛ) ∧ zero x ([xs !! k]⇩ℛ)
          ∧ (∀ m. j < m ∧ m < k ⟶ ¬ zero x ([xs !! m]⇩ℛ))
          ∧ (∀ x ∈ X2. ∃ m. j < m ∧ m ≤ k ∧ zero x ([xs !! m]⇩ℛ))
          ∧ (∀ x ∈ X1. ∀ m ≥ j. unbounded x ([xs !! m]⇩ℛ))" for i
    proof -
      from unbounded obtain i' where i': "∀ x ∈ X1. ∀ m ≥ i'. unbounded x ([xs !! m]⇩ℛ)" by auto
      then obtain i' where i':
        "i' ≥ i" "∀ x ∈ X1. ∀ m ≥ i'. unbounded x ([xs !! m]⇩ℛ)"
        by (cases "i' ≥ i"; auto)
      from finite(1) have "finite X2" unfolding X2_def by auto
      with ‹X2 ≠ {}› ℛ_divergent_divergent_aux2[where M = "{λ i. zero x ([xs !! i]⇩ℛ) | x. x ∈ X2}"]
        inf_resets
      have "∃j≥i'. ∃k>j. ∃P∈{λi. zero x ([xs !! i]⇩ℛ) |x. x ∈ X2}. P j ∧ P k
        ∧ (∀m<k. j < m ⟶ ¬ P m) ∧ (∀Q∈{λi. zero x ([xs !! i]⇩ℛ) |x. x ∈ X2}. ∃m≤k. j < m ∧ Q m)"
        by force
      then obtain j k x where
        "j ≥ i'" "k > j" "x ∈ X2" "zero x ([xs !! j]⇩ℛ)" "zero x ([xs !! k]⇩ℛ)"
        "∀m. j < m ∧ m < k ⟶ ¬ zero x ([xs !! m]⇩ℛ)"
        "∀Q∈{λi. zero x ([xs !! i]⇩ℛ) |x. x ∈ X2}. ∃m≤k. j < m ∧ Q m"
        by auto
      moreover from this(7) have "∀x∈X2. ∃m ≤ k. j < m ∧ zero x ([xs !! m]⇩ℛ)" by auto
      ultimately show ?thesis using i'
        by (inst_existentials j k x) auto
    qed
    moreover have "∃ j' ≥ j. dur xs j' - dur xs i ≥ 0.5"
      if  x: "x ∈ X2" "i < j" "zero x ([xs !! i]⇩ℛ)" "zero x ([xs !! j]⇩ℛ)"
        and not_reset: "∀ m. i < m ∧ m < j ⟶ ¬ zero x ([xs !! m]⇩ℛ)"
        and X2: "∀ x ∈ X2. ∃ m. i < m ∧ m ≤ j ∧ zero x ([xs !! m]⇩ℛ)"
        and X1: "∀ x ∈ X1. ∀ m ≥ i. unbounded x ([xs !! m]⇩ℛ)"
      for x i j
    proof -
      have "∃j'>j. ¬ zero x ([xs !! j']⇩ℛ)"
      proof -
        from inf_resets[OF x(1)] obtain j' where "j' ≥ Suc j" "¬ zero x ([xs !! j']⇩ℛ)" by auto
        then show ?thesis by - (rule exI[where x = j']; auto)
      qed
      from inf_resets[OF x(1)] obtain j' where "j' ≥ Suc j" "¬ zero x ([xs !! j']⇩ℛ)" by auto
      with nat_eventually_critical_path[OF x(4) this(2)]
      obtain j' where j':
        "j' > j" "¬ zero x ([xs !! j']⇩ℛ)" "∀ m ≥ j. m < j' ⟶ zero x ([xs !! m]⇩ℛ)"
        by auto
      from ‹x ∈ X2› have "x ∈ 𝒳" unfolding X2_def by simp
      with ‹i < j› not_reset not_reset_dur ‹stream_trans _› in_S pairwise_Suc[OF eq_elapsed] have
        "dur xs (j - 1) - dur xs i = (xs !! (j - 1)) x - (xs !! i) x" (is "?d1 = ?d2")
        by (auto simp: stream.pred_set)
      moreover from ‹zero x ([xs !! i]⇩ℛ)› in_S have "(xs !! i) x = 0"
        by (auto intro: zeroD simp: stream.pred_set)
      ultimately have
        "dur xs (j - 1) - dur xs i = (xs !! (j - 1)) x" (is "?d1 = ?d2")
        by simp
      show ?thesis
      proof (cases "?d1 ≥ 0.5")
        case True
          (* XXX Fix SMT *)
        with dur_mono[of "j - 1" j xs] have
          "5 / 10 ≤ dur xs j - dur xs i"
          by simp
        then show ?thesis by blast
      next
        case False
        have j_c_bound: "(xs !! j) c ≤ ?d2" if "c ∈ X2" for c
        proof (cases "(xs !! j) c = 0")
          case True
          from in_S ‹j > _› True ‹x ∈ 𝒳› show ?thesis by (auto simp: V_def stream.pred_set)
        next
          case False
          from X2 ‹c ∈ X2› in_S have "∃k>i. k ≤ j ∧ (xs !! k) c = 0"
            by (force simp: zeroD stream.pred_set)
          with False have
            "∃k>i. k ≤ j - Suc 0 ∧ (xs !! k) c = 0"
            by (metis Suc_le_eq Suc_pred linorder_neqE_nat not_less not_less_zero)
          moreover from that have "c ∈ 𝒳" by (auto simp: X2_def)
          moreover from not_reset in_S ‹x ∈ 𝒳› have
            "∀k>i. k ≤ j - 1 ⟶ (xs !! k) x ≠ 0"
            by (auto simp: zeroI stream.pred_set)
          ultimately have
            "(xs !! (j - 1)) c ≤ ?d2"
            using trans in_S ‹_ x = 0› ‹x ∈ 𝒳›
            by (auto intro: ℛ_divergent_divergent_aux that simp: stream.pred_set)
          moreover from
            trans_not_delay_mono[OF pairwise_Suc[OF trans], of "j - 1"]
            ‹x ∈ 𝒳› ‹c ∈ 𝒳› ‹j > _› in_S x(4)
          have "(xs !! j) c ≤ (xs !! (j - 1)) c" by (auto simp: zeroD stream.pred_set)
          ultimately show ?thesis by auto
        qed
        moreover from False ‹?d1 = ?d2› have "?d2 < 1" by auto
        moreover from in_S have "(xs !! j) c ≥ 0" if "c ∈ 𝒳" for c
          using that by (auto simp: V_def stream.pred_set)
        ultimately have frac_bound: "frac ((xs !! j) c) ≤ ?d2" if "c ∈ X2" for c
          using that frac_le_1I by (force simp: X2_def)

        let ?u = "(xs !! j)"
        from in_S have "[xs !! j]⇩ℛ ∈ ℛ" by (auto simp: stream.pred_set)
        then obtain I r where region:
          "[xs !! j]⇩ℛ = region 𝒳 I r" "valid_region 𝒳 k I r"
          unfolding ℛ_def by auto
        let ?S = "{frac (?u c) | c. c ∈ 𝒳 ∧ isIntv (I c)}"
        have 𝒳_X2: "c ∈ X2" if "c ∈ 𝒳" "isIntv (I c)" for c
        proof -
          from X1 ‹j > i› have "∀x∈X1. unbounded x ([xs !! j]⇩ℛ)" by auto
          with unbounded_Greater[OF region(2) ‹c ∈ 𝒳›] region(1) that(2) have "c ∉ X1" by auto
          with ‹c ∈ 𝒳› show "c ∈ X2" unfolding X2_def by auto
        qed
        have frac_bound: "frac ((xs !! j) c) ≤ ?d2" if "c ∈ 𝒳" "isIntv (I c)" for c
          using frac_bound[OF 𝒳_X2] that .
        have "dur xs (j' - 1) = dur xs j" using j' ‹x ∈ 𝒳› in_S eq_elapsed
          by (subst dur_zero_tail[where ω = "smap (λ u. [u]⇩ℛ) xs"])
            (auto dest: pairwise_Suc simp: stream.pred_set)
        moreover from dur_reset[OF eq_elapsed in_S, of x "j - 1"] ‹x ∈ 𝒳› x(4) ‹j > _› have
          "dur xs j = dur xs (j - 1)"
          by (auto simp: stream.pred_set)
        ultimately have "dur xs (j' - 1) = dur xs (j - 1)" by auto
        moreover have "dur xs j' - dur xs (j' - 1) ≥ (1 - ?d2) / 2"
        proof -
          from ‹j' > _› have "j' > 0" by auto
          with pairwise_Suc[OF trans', of "j' - 1"] have
            "trans' (xs !! (j' - 1)) (xs !! j')"
            by auto
          moreover from j' have
            "(xs !! (j' - 1)) x = 0" "(xs !! j') x > 0"
            using in_S ‹x ∈ 𝒳› by (force intro: zeroD dest: not_zeroD simp: stream.pred_set)+
          moreover note delayedR_aux = calculation
          obtain t where
            "(xs !! j') = (xs !! (j' - 1)) ⊕ t" "t ≥ (1 - ?d2) / 2" "t ≥ 0"
          proof -
            from in_S have "[xs !! j']⇩ℛ ∈ ℛ" by (auto simp: stream.pred_set)
            then obtain I' r' where region':
              "[xs !! j']⇩ℛ = region 𝒳 I' r'" "valid_region 𝒳 k I' r'"
              unfolding ℛ_def by auto            
            let ?S' = "{frac ((xs !! (j' - 1)) c) |c. c ∈ 𝒳 ∧ Regions.isIntv (I' c)}"

            from finite(1) have "?d2 ≥ Max (?S' ∪ {0})"
              apply -
              apply (rule Max.boundedI)
                apply fastforce
               apply fastforce
              apply safe
              subgoal premises prems for _ c d
              proof -
                from j' have "(xs !! (j' - 1)) c = ?u c ∨ (xs !! (j' - 1)) c = 0"
                  by (intro resets_mono'[OF eq_elapsed in_S trans _ ‹x ∈ 𝒳› ‹c ∈ 𝒳›]; auto)
                then show ?thesis
                proof (standard, goal_cases)
                  case A: 1
                  show ?thesis
                  proof (cases "c ∈ X1")
                    case True
                    with X1 ‹j' > j› ‹j > i› have "unbounded c ([xs !! j']⇩ℛ)" by auto
                    with region' ‹c ∈ 𝒳› have "I' c = Greater (k c)"
                      by (auto intro: unbounded_Greater)
                    with prems show ?thesis by auto
                  next
                    case False
                    with ‹c ∈ 𝒳› have "c ∈ X2" unfolding X2_def by auto
                    with j_c_bound have mono: "(xs !! j) c ≤ (xs !! (j - 1)) x" .
                    from in_S ‹c ∈ 𝒳› have "(xs !! (j' - 1)) c ≥ 0"
                      unfolding V_def stream.pred_set by auto
                    then have
                      "frac ((xs !! (j' - 1)) c) ≤ (xs !! (j' - 1)) c"
                      using frac_le_self by auto
                    with A mono show ?thesis by auto
                  qed
                next
                  case prems: 2
                    (* XXX *)
                  have "frac (0 :: real) = (0 :: real)" by auto
                  then have "frac (0 :: real) ≤ (0 :: real)" by linarith
                  moreover from in_S ‹x ∈ 𝒳› have "(xs !! (j - 1)) x ≥ 0"
                    unfolding V_def stream.pred_set by auto
                  ultimately show ?thesis using prems by auto
                qed
              qed
              using in_S ‹x ∈ 𝒳› by (auto simp: V_def stream.pred_set)
            then have le: "(1 - ?d2) / 2 ≤ (1 - Max (?S' ∪ {0})) / 2" by simp

            let ?u = "xs !! j'"
            let ?u' = "xs !! (j' - 1)"
            from in_S have *: "?u' ∈ V" "[?u']⇩ℛ ∈ ℛ" "?u ∈ V" "[?u]⇩ℛ ∈ ℛ"
              by (auto simp: stream.pred_set)
            from pairwise_Suc[OF trans, of "j' - 1"] ‹j' > j› have
              "trans (xs !! (j' - 1)) (xs !! j')"
              by auto
            then have Succ:
              "[xs !! j']⇩ℛ ∈ Succ ℛ ([xs !! (j' - 1)]⇩ℛ) ∧ (∃ t≥ 0. ?u = ?u' ⊕ t)"
            proof cases
              case prems: (succ t)
              from * have "?u' ∈ [?u']⇩ℛ" by auto
              with prems * show ?thesis by auto
            next
              case (reset l)
              with ‹?u' ∈ V› have "?u x ≤ ?u' x" by (cases "x ∈ set l") (auto simp: V_def)
              from j' have "zero x ([?u']⇩ℛ)" by auto
              with ‹?u' ∈ V› have "?u' x = 0" unfolding zero_def by auto
              with ‹?u x ≤ _› ‹?u x > 0› show ?thesis by auto
            next
              case id
              with * Succ_refl[of ℛ 𝒳 k, folded ℛ_def, OF _ finite(1)] show ?thesis
                unfolding cval_add_def by auto
            qed
            then obtain t where t: "?u = xs !! (j' - 1) ⊕ t" "t ≥ 0" by auto
            note Succ = Succ[THEN conjunct1]

            show ?thesis
            proof (cases "∃ c ∈ X2. ∃ d :: nat. ?u c = d")
              case True
              from True obtain c and d :: nat where c:
                "c ∈ 𝒳" "c ∈ X2" "?u c = d"
                by (auto simp: X2_def)
              have "?u x > 0" by fact
              from pairwise_Suc[OF eq_elapsed, of "j' - 1"] ‹j' > j› have
                "eq_elapsed (xs !! (j' - 1)) ?u"
                by auto
              moreover from
                elapsed_eq[OF this ‹x ∈ 𝒳›] ‹(xs !! (j' - 1)) x = 0› ‹(xs !! j') x > 0›
              have "elapsed (xs !! (j' - 1)) (xs !! j') > 0"
                by auto
              ultimately have
                "?u c - (xs !! (j' - 1)) c > 0"
                using ‹c ∈ 𝒳› unfolding eq_elapsed_def by auto
              moreover from in_S have "xs !! (j' - 1) ∈ V" by (auto simp: stream.pred_set)
              ultimately have "?u c > 0" using ‹c ∈ 𝒳› unfolding V_def by auto
              from region' in_S ‹c ∈ 𝒳› have "intv_elem c ?u (I' c)"
                by (force simp: stream.pred_set)
              with ‹?u c = d› ‹?u c > 0› have "?u c ≥ 1" by auto
              moreover have "(xs !! (j' - 1)) c ≤ 0.5"
              proof -
                have "(xs !! (j' - 1)) c ≤ (xs !! j) c"
                  (* XXX This proof is duplicated at least once above *)
                  using j'(1,3)
                  by (auto intro: resets_mono[OF eq_elapsed in_S trans _ ‹x ∈ 𝒳› ‹c ∈ 𝒳›])
                also have "… ≤ ?d2" using j_c_bound[OF ‹c ∈ X2›] .
                also from ‹?d1 = ?d2› ‹¬ 5 / 10 ≤ _› have "… ≤ 0.5" by simp
                finally show ?thesis .
              qed
              moreover have "?d2 ≥ 0" using in_S ‹x ∈ 𝒳› by (auto simp: V_def stream.pred_set)
              ultimately have "?u c - (xs !! (j' - 1)) c ≥ (1 - ?d2) / 2" by auto
              with t have "t ≥ (1 - ?d2) / 2" unfolding cval_add_def by auto
              with t show ?thesis by (auto intro: that)
            next
              case F: False
              have not_const: "¬ isConst (I' c)" if "c ∈ 𝒳" for c
              proof (rule ccontr, simp)
                assume A: "isConst (I' c)"
                show False
                proof (cases "c ∈ X1")
                  case True
                  with X1 ‹j' > j› ‹j > _› have "unbounded c ([xs !! j']⇩ℛ)" by auto
                  with unbounded_Greater ‹c ∈ 𝒳› region' have "isGreater (I' c)" by force
                  with A show False by auto
                next
                  case False
                  with ‹c ∈ 𝒳› have "c ∈ X2" unfolding X2_def by auto
                  from region' in_S ‹c ∈ 𝒳› have "intv_elem c ?u (I' c)"
                    unfolding stream.pred_set  by force
                  with ‹c ∈ X2› A False F show False by auto
                qed
              qed
              have "∄x. x ≤ k c ∧ (xs !! j') c = real x" if "c ∈ 𝒳" for c
              proof (cases "c ∈ X2"; safe)
                fix d
                assume "c ∈ X2" "(xs !! j') c = real d"
                with F show False by auto
              next
                fix d
                assume "c ∉ X2" 
                with that have "c ∈ X1" unfolding X2_def by auto
                with X1 ‹j' > j› ‹j > i› have "unbounded c ([?u]⇩ℛ)" by auto
                from unbounded_all[OF _ _ this] ‹c ∈ 𝒳› in_S have "?u c > k c"
                  by (force simp: stream.pred_set)
                moreover assume "?u c = real d" "d ≤ k c"
                ultimately show False by auto
              qed
              with delayedR_aux have
                "(xs !! j') = delayedR ([xs !! j']⇩ℛ) (xs !! (j' - 1))"
                using ‹x ∈ 𝒳› unfolding trans'_def by auto
              from not_const region'(1)  in_S Succ(1) have
                "∃t≥0. delayedR ([xs !! j']⇩ℛ) (xs !! (j' - 1)) = xs !! (j' - 1) ⊕ t ∧
                      (1 - Max (?S' ∪ {0})) / 2 ≤ t"
                apply simp
                apply (rule delayedR_correct(2)[OF _ _ region'(2), simplified])
                by (auto simp: stream.pred_set)
              with le ‹_ = delayedR _ _› show ?thesis by (auto intro: that)
            qed
          qed
          moreover from pairwise_Suc[OF eq_elapsed, of "j' - 1"] ‹j' > 0› have
            "eq_elapsed (xs !! (j' - 1)) (xs !! j')"
            by auto
          ultimately show "dur xs j' - dur xs (j' - 1) ≥ (1 - ?d2) / 2" 
            using ‹j' > 0› dur_Suc[of _ "j' - 1"] ‹x ∈ 𝒳› by (auto simp: cval_add_def elapsed_eq)
        qed
        moreover from dur_mono[of i "j - 1" xs] ‹i < j› have "dur xs i ≤ dur xs (j - 1)" by simp
        ultimately have "dur xs j' - dur xs i ≥ 0.5" unfolding ‹?d1 = ?d2›[symmetric] by auto
        then show ?thesis using ‹j < j'› by - (rule exI[where x = j']; auto)
      qed
    qed
    moreover
    have "∃ j' ≥ i. dur xs j' - dur xs i ≥ 0.5" for i
    proof -
      from calculation(1)[of i] obtain j k x where
        "j≥i" "k>j" "x∈X2" "zero x ([xs !! j]⇩ℛ)"
        "zero x ([xs !! k]⇩ℛ)"
        "∀m. j < m ∧ m < k ⟶ ¬ zero x ([xs !! m]⇩ℛ)"
        "∀x∈X2. ∃m>j. m ≤ k ∧ zero x ([xs !! m]⇩ℛ)"
        "∀x∈X1. ∀m≥j. unbounded x ([xs !! m]⇩ℛ)"
        by auto
      from calculation(2)[OF this(3,2,4-8)] obtain j' where
        "j'≥k" "5 / 10 ≤ dur xs j' - dur xs j"
        by auto
      with dur_mono[of i j xs] ‹j ≥ i› ‹k > j› show ?thesis by (intro exI[where x = j']; auto)
    qed
    then show ?thesis by - (rule dur_ev_exceedsI[where d = "0.5"]; auto)
  qed
qed

lemma cfg_on_div_absc:
  notes in_space_UNIV[measurable]
  assumes "cfg ∈ cfg_on_div st" "st ∈ S"
  shows "absc cfg ∈ R_G_cfg_on_div (abss st)"
proof -
  from assms have *: "cfg ∈ MDP.cfg_on st" "state cfg = st" "div_cfg cfg"
    unfolding cfg_on_div_def by auto
  with assms have "cfg ∈ valid_cfg" by (auto intro: MDP.valid_cfgI)
  have "almost_everywhere (MDP.MC.T cfg) (MDP.MC.enabled cfg)"
    by (rule MDP.MC.AE_T_enabled)
  moreover from * have "AE x in MDP.MC.T cfg. divergent (smap (snd ∘ state) x)"
    by (simp add: div_cfg_def)
  ultimately have "AE x in MDP.MC.T cfg. ℛ_div (smap (snd ∘ state) (smap absc x))"
  proof eventually_elim
    case (elim ω)
    let ?xs = "smap (snd o state) ω"
    from MDP.pred_stream_cfg_on[OF ‹_ ∈ valid_cfg› ‹MDP.MC.enabled _ _›] have *:
      "pred_stream (λ x. x ∈ S) (smap state ω)"
      by (auto simp: stream.pred_set)
    have "[snd (state x)]⇩ℛ = snd (abss (state x))" if "x ∈ sset ω" for x
    proof -
      from * that have "state x ∈ S" by (auto simp: stream.pred_set)
      then have "snd (abss (state x)) = [snd (state x)]⇩ℛ" by (metis abss_S snd_conv surj_pair)
      then show ?thesis ..
    qed
    then have "smap (λz. [snd (state z)]⇩ℛ) ω = (smap (λz. snd (abss (state z))) ω)" by auto
    from * have  "pred_stream (λ u. u ∈ V) ?xs"
      apply (simp add: map_def stream.pred_set)
      apply (subst (asm) surjective_pairing)
      using S_V by blast
    moreover have "stream_trans ?xs"
      by (rule enabled_stream_trans ‹_ ∈ valid_cfg› ‹MDP.MC.enabled _ _›)+
    ultimately show ?case using ‹divergent _› ‹smap _ ω = _›
      by - (drule divergent_ℛ_divergent, auto simp add: stream.map_comp state_absc)
  qed
  with ‹cfg ∈ valid_cfg› have "R_G_div_cfg (absc cfg)" unfolding R_G_div_cfg_def
    by (subst absc_distr_self) (auto intro: MDP.valid_cfgI simp: AE_distr_iff)
  with R_G.valid_cfgD ‹cfg ∈ valid_cfg› * show ?thesis unfolding R_G_cfg_on_div_def by auto force
qed

definition
  "alternating cfg = (AE ω in MDP.MC.T cfg.
      alw (ev (HLD {cfg. ∀cfg' ∈ K_cfg cfg. fst (state cfg') = fst (state cfg)})) ω)"

lemma K_cfg_same_loc_iff:
  "(∀cfg'∈ K_cfg cfg. fst (state cfg') = fst (state cfg))
  ⟷ (∀cfg'∈ K_cfg (absc cfg). fst (state cfg') = fst (state (absc cfg)))"
  if "cfg ∈ valid_cfg"
  using that by (auto simp: state_absc fst_abss K_cfg_map_absc)

lemma (in -) stream_all2_flip:
  "stream_all2 (λa b. R b a) xs ys = stream_all2 R ys xs"
  by (standard; coinduction arbitrary: xs ys; auto dest: sym)

(* TODO: Lots of duplication here, e.g. with path_measure_eq_repcs1_new *)
lemma AE_alw_ev_same_loc_iff:
  assumes "cfg ∈ valid_cfg"
  shows "alternating cfg ⟷ alternating (absc cfg)"
  unfolding alternating_def
  apply (simp add: MDP.MC.T.AE_iff_emeasure_eq_1)
  subgoal
  proof -
    show ?thesis (is "(?x = 1) = (?y = 1)")
    proof -
      have *: "stream_all2 (λs t. t = absc s) x y = stream_all2 (=) y (smap absc x)" for x y
        by (subst stream_all2_flip) simp
      have "?x = ?y"
        apply (rule T_eq_rel_half[where f = absc and S = valid_cfg, OF HOL.refl, rotated 2])
        subgoal
          apply (simp add: space_stream_space rel_set_strong_def)
          apply (intro allI impI)
          apply (frule stream.rel_mono_strong[where Ra = "λs t. t = absc s"])
          by (auto simp: * stream.rel_eq stream_all2_refl alw_holds_pred_stream_iff[symmetric]
              K_cfg_same_loc_iff HLD_def elim!: alw_ev_cong)
        subgoal
          by (rule rel_funI) (auto intro!: rel_pmf_reflI simp: pmf.rel_map(2) K_cfg_map_absc)
        using ‹cfg ∈ valid_cfg› by simp+
      then show ?thesis
        by simp
    qed
  qed
  done

lemma AE_alw_ev_same_loc_iff':
  assumes "cfg ∈ R_G.cfg_on (abss st)" "st ∈ S"
  shows "alternating cfg ⟷ alternating (repcs st cfg)"
proof -
  from assms have "cfg ∈ R_G.valid_cfg"
    by (auto intro: R_G.valid_cfgI)
  with assms show ?thesis
    by (subst AE_alw_ev_same_loc_iff) (auto simp: absc_repcs_id)
qed

lemma (in -) cval_add_non_id:
  False if "b ⊕ d = b" "d > 0" for d :: real
proof -
  from that(1) have "(b ⊕ d) x = b x"
    by (rule fun_cong)
  with ‹d > 0› show False
    unfolding cval_add_def by simp
qed

lemma repcs_unbounded_AE_non_loop_end_strong:
  assumes "cfg ∈ R_G.cfg_on (abss st)" "st ∈ S"
    and "alternating cfg"
  shows "AE ω in MDP.MC.T (repcs st cfg).
      (∀ u :: ('c ⇒ real). (∀ c ∈ 𝒳. u c > real (k c)) ⟶
      ¬ (ev (alw (λ xs. shd xs = u))) (smap (snd o state) ω))" (is "AE ω in ?M. ?P ω")
proof -
  from assms have "cfg ∈ R_G.valid_cfg"
    by (auto intro: R_G.valid_cfgI)
  with assms(1) have "repcs st cfg ∈ valid_cfg"
    by auto
  from R_G.valid_cfgD[OF ‹cfg ∈ R_G.valid_cfg›] have "cfg ∈ R_G.cfg_on (state cfg)" .
  let ?U = "λ u. ⋃ l ∈ L. {μ ∈ K (l, u). μ ≠ return_pmf (l, u) ∧ (∀ x ∈ μ. fst x = l)}"
  let ?r = "λ u. Sup ({0} ∪ (λ μ. measure_pmf μ {x. snd x = u}) ` ?U u)"
  have lt_1: "?r u < 1" for u
  proof -
    have *: "emeasure (measure_pmf μ) {x. snd x = u} < 1"
      if "μ ≠ return_pmf (l, u)" "∀x∈set_pmf μ. fst x = l" for μ and l :: 's
    proof (rule ccontr)
      assume "¬ emeasure (measure_pmf μ) {x. snd x = u} < 1"
      then have "1 = emeasure (measure_pmf μ) {x. snd x = u}"
        using measure_pmf.emeasure_ge_1_iff by force
      also from that(2) have "… ≤ emeasure (measure_pmf μ) {(l, u)}"
        by (subst emeasure_Int_set_pmf[symmetric]) (auto intro!: emeasure_mono)
      finally show False
        by (simp add: measure_pmf.emeasure_ge_1_iff measure_pmf_eq_1_iff that(1))
    qed
    let ?S =
      "{map_pmf (λ (X, l). (l, ([X := 0]u))) μ | μ l g. (l, g, μ) ∈ trans_of A}"
    have "(λ μ. measure_pmf μ {x. snd x = u}) ` ?U u
      ⊆ {0, 1} ∪ (λ μ. measure_pmf μ {x. snd x = u}) ` ?S"
      by (force elim!: K.cases)
    moreover have "finite ?S"
    proof -
      have "?S ⊆ (λ (l, g, μ). map_pmf (λ (X, l). (l, ([X := 0]u))) μ) ` trans_of A"
        by force
      also from finite(3) have "finite …" ..
      finally show ?thesis .
    qed
    ultimately have "finite ((λ μ. measure_pmf μ {x. snd x = u}) ` ?U u)"
      by (auto intro: finite_subset)
    then show ?thesis
      by (fastforce intro: * finite_imp_Sup_less)
  qed
  { fix l :: 's and u :: "'c ⇒ real" and cfg :: "('s × ('c ⇒ real) set) cfg"
    assume unbounded: "∀ c ∈ 𝒳. u c > k c" and "cfg ∈ R_G.cfg_on (abss (l, u))" "abss (l, u) ∈ 𝒮"
      and same_loc: "∀ cfg' ∈ K_cfg cfg. fst (state cfg') = l"
    then have "cfg ∈ R_G.valid_cfg" "repcs (l, u) cfg ∈ valid_cfg"
      by (auto intro: R_G.valid_cfgI)
    then have cfg_on: "repcs (l, u) cfg ∈ MDP.cfg_on (l, u)"
      by (auto dest: MDP.valid_cfgD)
    from ‹cfg ∈ R_G.cfg_on _› have "action cfg ∈ 𝒦 (abss (l, u))"
      by (rule R_G.cfg_onD_action)
        (* TODO: Pull out? *)
    have K_cfg_rept: "state ` K_cfg (repcs (l, u) cfg) = rept (l, u) (action cfg)"
      unfolding K_cfg_def by (force simp: action_repcs)
    have "l ∈ L"
      using MDP.valid_cfg_state_in_S ‹repcs (l, u) cfg ∈ MDP.valid_cfg› by fastforce
    moreover have "rept (l, u) (action cfg) ≠ return_pmf (l, u)"
    proof (rule ccontr, simp)
      assume "rept (l, u) (action cfg) = return_pmf (l, u)"
      then have "action cfg = return_pmf (abss (l, u))"
        using abst_rept_id[OF ‹action cfg ∈ _›]
        by (simp add: abst_def)
      moreover have "(l, u) ∈ S"
        using ‹_ ∈ 𝒮› by (auto dest: 𝒮_abss_S)
      moreover have "abss (l, u) = (l, [u]⇩ℛ)"
        by (metis abss_S calculation(2))
      ultimately show False
        using ‹rept (l, u) _ = _› unbounded unfolding rept_def by (auto dest: cval_add_non_id)
    qed
    moreover have "rept (l, u) (action cfg) ∈ K (l, u)"
    proof -
      have "action (repcs (l, u) cfg) ∈ K (l, u)"
        using cfg_on by blast
      then show ?thesis
        by (simp add: repcs_def)
    qed
    moreover have "∀x∈set_pmf (rept (l, u) (action cfg)). fst x = l"
      using same_loc K_cfg_same_loc_iff[of "repcs (l, u) cfg"]
        ‹repcs (l, u) _ ∈ valid_cfg› ‹cfg ∈ R_G.valid_cfg› ‹cfg ∈ R_G.cfg_on _›
      by (simp add: absc_repcs_id fst_abss K_cfg_rept[symmetric])
    ultimately have "rept (l, u) (action cfg) ∈ ?U u"
      by blast
    then have "measure_pmf (rept (l, u) (action cfg)) {x. snd x = u} ≤ ?r u"
      by (fastforce intro: Sup_upper)
    moreover have "rept (l, u) (action cfg) = action (repcs (l, u) cfg)"
      by (simp add: repcs_def)
    ultimately have "measure_pmf (action (repcs (l, u) cfg)) {x. snd x = u} ≤ ?r u"
      by auto
  }
  note * = this
  let ?S = "{cfg. ∃ cfg' s. cfg' ∈ R_G.valid_cfg ∧ cfg = repcs s cfg' ∧ abss s = state cfg'}"
  have start: "repcs st cfg ∈ ?S"
    using ‹cfg ∈ R_G.valid_cfg› assms unfolding R_G_cfg_on_div_def
    by clarsimp (inst_existentials cfg "fst st" "snd st", auto)
  have step: "y ∈ ?S" if "y ∈ K_cfg x" "x ∈ ?S" for x y
    using that apply safe
    subgoal for cfg' l u
      apply (inst_existentials "absc y" "state y")
      subgoal
        by blast
      subgoal
        by (metis
            K_cfg_valid_cfgD R_G.valid_cfgD R_G.valid_cfg_state_in_S absc_repcs_id cont_absc_1
            cont_repcs1 repcs_valid
            )
      subgoal
        by (simp add: state_absc)
      done
    done
  have **: "x ∈ ?S" if "(repcs st cfg, x) ∈ MDP.MC.acc" for x
  proof -
    from MDP.MC.acc_relfunD[OF that] obtain n where "((λ a b. b ∈ K_cfg a) ^^ n) (repcs st cfg) x" .
    then show ?thesis
    proof (induction n arbitrary: x) (* XXX Extract induction rule *)
      case 0
      with start show ?case
        by simp
    next
      case (Suc n)
      from this(2)[simplified] show ?case
        apply (rule relcomppE)
        apply (erule step)
        apply (erule Suc.IH)
        done
    qed
  qed
  have ***: "almost_everywhere (MDP.MC.T (repcs st cfg)) (alw (HLD ?S))"
    by (rule AE_mp[OF MDP.MC.AE_T_reachable]) (fastforce dest: ** simp: HLD_iff elim: alw_mono)

  from ‹alternating cfg› assms have "alternating (repcs st cfg)"
    by (simp add: AE_alw_ev_same_loc_iff'[of _ st])
  then have alw_ev_same2: "almost_everywhere (MDP.MC.T (repcs st cfg))
     (alw (λω. HLD (state -` snd -` {u}) ω ⟶
      ev (HLD {cfg. ∀cfg'∈set_pmf (K_cfg cfg). fst (state cfg') = fst (state cfg)}) ω))"
    for u unfolding alternating_def by (auto elim: alw_mono)

  let ?X = "{cfg :: ('s × ('c ⇒ real)) cfg. ∀ c ∈ 𝒳. snd (state cfg) c > k c}"
  let ?Y = "{cfg. ∀ cfg' ∈ K_cfg cfg. fst (state cfg') = fst (state cfg)}"

  have "(AE ω in ?M. ?P ω) ⟷
    (AE ω in ?M. ∀ u :: ('c ⇒ real).
      (∀ c ∈ 𝒳. u c > k c) ∧ u ∈ snd ` state ` (MDP.MC.acc `` {repcs st cfg}) ⟶
      ¬ (ev (alw (λ xs. shd xs = u))) (smap (snd o state) ω))" (is "?L ⟷ ?R")
  proof
    assume ?L
    then show ?R
      by eventually_elim auto
  next
    assume ?R
    with MDP.MC.AE_T_reachable[of "repcs st cfg"] show ?L
    proof (eventually_elim, intro allI impI notI, goal_cases)
      case (1 ω u)
      then show ?case
        by - (intro alw_HLD_smap alw_disjoint_ccontr[where
              S = "(snd o state) ` MDP.MC.acc `` {repcs st cfg}"
              and R = "{u}" and ω = "smap (snd o state) ω"
              ]; auto simp: HLD_iff)
    qed
  qed

  also have "… ⟷
      (∀ u :: ('c ⇒ real).
        (∀ c ∈ 𝒳. u c > k c) ∧ u ∈ snd ` state ` (MDP.MC.acc `` {repcs st cfg}) ⟶
        (AE ω in ?M. ¬ (ev (alw (λ xs. shd xs = u))) (smap (snd o state) ω)))"
    using MDP.MC.countable_reachable[of "repcs st cfg"]
    by - (rule AE_all_imp_countable,
        auto intro: countable_subset[where B = "snd ` state ` MDP.MC.acc `` {repcs st cfg}"])
  also show ?thesis
    unfolding calculation
    apply clarsimp
    subgoal for l u x
      apply (rule
          MDP.non_loop_tail_strong[simplified, of snd "snd (state x)" ?Y ?S "?r (snd (state x))"]
          )
      subgoal
        apply safe
        subgoal premises prems for cfg l1 u1 _ cfg' l2 u2
        proof -
          have [simp]: "l2 = l1" "u2 = u1"
            subgoal
              by (metis MDP.cfg_onD_state Pair_inject prems(4) state_repcs)
            subgoal
              by (metis MDP.cfg_onD_state prems(4) snd_conv state_repcs)
            done
          with prems have [simp]: "u2 = u"
            by (metis ‹(l, u) = state x› ‹snd (l1, u1) = snd (state x)› ‹u2 = u1› snd_conv)
          have [simp]: "snd -` {snd (state x)} = {y. snd y = snd (state x)}"
            by (simp add: vimage_def)
          from prems show ?thesis
            apply simp
            apply (erule *[simplified])
            subgoal
              using prems(1) prems(2)[symmetric] prems(3-) by (auto simp: R_G.valid_cfg_def)
            subgoal
              using prems(1) prems(2)[symmetric] prems(3-) by (auto simp: R_G.valid_cfg_def)
            subgoal
              using K_cfg_same_loc_iff[of "repcs (l1, snd (state x)) cfg'"]
              by (simp add: absc_repcs_id) (metis fst_abss fst_conv repcs_valid)
            done
        qed
        done
      subgoal
        by (auto intro: lt_1[simplified])
        apply (rule MDP.valid_cfgD[OF ‹repcs st cfg ∈ valid_cfg›]; fail)
      subgoal
        using *** unfolding alw_holds_pred_stream_iff[symmetric] HLD_def .
      subgoal
        by (rule alw_ev_same2)
      done
    done
qed

lemma cfg_on_div_repcs_strong:
  notes in_space_UNIV[measurable]
  assumes "cfg ∈ R_G_cfg_on_div (abss st)" "st ∈ S" and "alternating cfg"
  shows "repcs st cfg ∈ cfg_on_div st"
proof -
  let ?st = "abss st"
  let ?cfg = "repcs st cfg"
  from assms have *:
    "cfg ∈ R_G.cfg_on ?st" "state cfg = ?st" "R_G_div_cfg cfg"
    unfolding R_G_cfg_on_div_def by auto
  with assms have "cfg ∈ R_G.valid_cfg" by (auto intro: R_G.valid_cfgI)
  with ‹st ∈ S› ‹_ = ?st› have "?cfg ∈ valid_cfg" by auto
  from *(1) ‹st ∈ S› ‹alternating cfg› have
    "AE ω in MDP.MC.T ?cfg. ∀u. (∀c∈𝒳. real (k c) < u c) ⟶
                          ¬ ev (alw (λxs. shd xs = u)) (smap (snd ∘ state) ω)"
    by (rule repcs_unbounded_AE_non_loop_end_strong)
  ― ‹Move to lower level›
  moreover from *(2,3) have "AE ω in MDP.MC.T ?cfg. ℛ_div (smap (snd ∘ state) (smap absc ω))"
    unfolding R_G_div_cfg_def
    by (subst (asm) R_G_trace_space_distr_eq[OF ‹cfg ∈ R_G.valid_cfg›]; simp add: AE_distr_iff)
  ultimately have "div_cfg ?cfg"
    unfolding div_cfg_def using MDP.MC.AE_T_enabled[of ?cfg]
  proof eventually_elim
    case prems: (elim ω)
      let ?xs = "smap (snd o state) ω"
      from MDP.pred_stream_cfg_on[OF ‹_ ∈ valid_cfg› ‹MDP.MC.enabled _ _›] have *:
        "pred_stream (λ x. x ∈ S) (smap state ω)"
        by (auto simp: stream.pred_set)
      have "[snd (state x)]⇩ℛ = snd (abss (state x))" if "x ∈ sset ω" for x
      proof -
        from * that have "state x ∈ S" by (auto simp: stream.pred_set)
        then have "snd (abss (state x)) = [snd (state x)]⇩ℛ" by (metis abss_S snd_conv surj_pair)
        then show ?thesis ..
      qed
      then have "smap (λz. [snd (state z)]⇩ℛ) ω = (smap (λz. snd (abss (state z))) ω)" by auto
      from * have  "pred_stream (λ u. u ∈ V) ?xs"
        by (simp add: map_def stream.pred_set, subst (asm) surjective_pairing, blast)
      moreover have "stream_trans ?xs"
        by (rule enabled_stream_trans ‹_ ∈ valid_cfg› ‹MDP.MC.enabled _ _›)+
      moreover have "pairwise trans' ?xs"
        using ‹_ ∈ R_G.valid_cfg› ‹state cfg = _›[symmetric] ‹MDP.MC.enabled _ _›
        by (rule enabled_stream_trans')
      moreover from prems(1) have
        "∀u. (∀c∈𝒳. real (k c) < u c) ⟶ ¬ ev (alw (λxs. snd (shd xs) = u)) (smap state ω)"
        by simp
      ultimately show ?case using ‹ℛ_div _›
        by (simp add: stream.map_comp state_absc ‹smap _ ω = _› ℛ_divergent_divergent)
    qed
  with MDP.valid_cfgD ‹cfg ∈ R_G.valid_cfg› * show ?thesis unfolding cfg_on_div_def by auto force
qed

lemma repcs_unbounded_AE_non_loop_end:
  assumes "cfg ∈ R_G.cfg_on (abss st)" "st ∈ S"
  shows "AE ω in MDP.MC.T (repcs st cfg).
      (∀ s :: ('s × ('c ⇒ real)). (∀ c ∈ 𝒳. snd s c > k c) ⟶
      ¬ (ev (alw (λ xs. shd xs = s))) (smap state ω))" (is "AE ω in ?M. ?P ω")
proof -
  from assms have "cfg ∈ R_G.valid_cfg"
    by (auto intro: R_G.valid_cfgI)
  with assms(1) have "repcs st cfg ∈ valid_cfg"
    by auto
  from R_G.valid_cfgD[OF ‹cfg ∈ R_G.valid_cfg›] have "cfg ∈ R_G.cfg_on (state cfg)" .
  let ?K = "λ x. {μ ∈ K x. μ ≠ return_pmf x}"
  let ?r = "λ x. Sup ((λ μ. measure_pmf μ {x}) ` ?K x)"
  have lt_1: "?r x < 1" if "μ ∈ ?K x" for μ x
  proof -
    have *: "emeasure (measure_pmf μ) {x} < 1" if "μ ≠ return_pmf x" for μ
    proof (rule ccontr)
      assume "¬ emeasure (measure_pmf μ) {x} < 1"
      then have "emeasure (measure_pmf μ) {x} = 1"
        using measure_pmf.emeasure_ge_1_iff by force
      with that show False
        by (simp add: measure_pmf_eq_1_iff)
    qed
    let ?S =
      "{map_pmf (λ (X, l). (l, ([X := 0]u))) μ | μ l u g.
          x = (l, u) ∧ (l, g, μ) ∈ trans_of A}"
    have "(λ μ. measure_pmf μ {x}) ` ?K x
      ⊆ {0, 1} ∪ (λ μ. measure_pmf μ {x}) ` ?S"
      by (force elim!: K.cases)
    moreover have "finite ?S"
    proof -
      have "?S ⊆ (λ (l, g, μ). map_pmf (λ (X, l). (l, (clock_set_set X 0(snd x)))) μ) ` trans_of A"
        by force
      also from finite(3) have "finite …" ..
      finally show ?thesis .
    qed
    ultimately have "finite ((λ μ. measure_pmf μ {x}) ` ?K x)"
      by (auto intro: finite_subset)
    then show ?thesis
      using that by (auto intro: * finite_imp_Sup_less)
  qed
  { fix s :: "'s × ('c ⇒ real)" and cfg :: "('s × ('c ⇒ real) set) cfg"
    assume unbounded: "∀ c ∈ 𝒳. snd s c > k c" and "cfg ∈ R_G.cfg_on (abss s)" "abss s ∈ 𝒮"
    then have "repcs s cfg ∈ valid_cfg"
      by (auto intro: R_G.valid_cfgI)
    then have cfg_on: "repcs s cfg ∈ MDP.cfg_on s"
      by (auto dest: MDP.valid_cfgD)
    from ‹cfg ∈ _› have "action cfg ∈ 𝒦 (abss s)"
      by (rule R_G.cfg_onD_action)
    have "rept s (action cfg) ≠ return_pmf s"
    proof (rule ccontr, simp)
      assume "rept s (action cfg) = return_pmf s"
      then have "action cfg = return_pmf (abss s)"
        using abst_rept_id[OF ‹action cfg ∈ _›]
        by (simp add: abst_def)
      moreover have "(fst s, snd s) ∈ S"
        using ‹_ ∈ 𝒮› by (auto dest: 𝒮_abss_S)
      moreover have "abss s = (fst s, [snd s]⇩ℛ)"
        by (metis abss_S calculation(2) prod.collapse)
      ultimately show False
        using ‹rept s _ = _› unbounded unfolding rept_def by (cases s) (auto dest: cval_add_non_id)
    qed
    moreover have "rept s (action cfg) ∈ K s"
    proof -
      have "action (repcs s cfg) ∈ K s"
        using cfg_on by blast
      then show ?thesis
        by (simp add: repcs_def)
    qed
    ultimately have "rept s (action cfg) ∈ ?K s"
      by blast
    then have "measure_pmf (rept s (action cfg)) {s} ≤ ?r s"
      by (auto intro: Sup_upper)
    moreover have "rept s (action cfg) = action (repcs s cfg)"
      by (simp add: repcs_def)
    ultimately have "measure_pmf (action (repcs s cfg)) {s} ≤ ?r s"
      by auto
    note this ‹rept s (action cfg) ∈ ?K s›
  }
  note * = this
  let ?S = "{cfg. ∃ cfg' s. cfg' ∈ R_G.valid_cfg ∧ cfg = repcs s cfg' ∧ abss s = state cfg'}"
  have start: "repcs st cfg ∈ ?S"
    using ‹cfg ∈ R_G.valid_cfg› assms unfolding R_G_cfg_on_div_def
    by clarsimp (inst_existentials cfg "fst st" "snd st", auto)
  have step: "y ∈ ?S" if "y ∈ K_cfg x" "x ∈ ?S" for x y
    using that apply safe
    subgoal for cfg' l u
      apply (inst_existentials "absc y" "state y")
      subgoal
        by blast
      subgoal
        by (metis
            K_cfg_valid_cfgD R_G.valid_cfgD R_G.valid_cfg_state_in_S absc_repcs_id cont_absc_1
            cont_repcs1 repcs_valid
            )
      subgoal
        by (simp add: state_absc)
      done
    done
  have **: "x ∈ ?S" if "(repcs st cfg, x) ∈ MDP.MC.acc" for x
  proof -
    from MDP.MC.acc_relfunD[OF that] obtain n where "((λ a b. b ∈ K_cfg a) ^^ n) (repcs st cfg) x" .
    then show ?thesis
    proof (induction n arbitrary: x) (* XXX Extract induction rule *)
      case 0
      with start show ?case
        by simp
    next
      case (Suc n)
      from this(2)[simplified] show ?case
        by (elim relcomppE step Suc.IH)
    qed
  qed
  have ***: "almost_everywhere (MDP.MC.T (repcs st cfg)) (alw (HLD ?S))"
    by (rule AE_mp[OF MDP.MC.AE_T_reachable]) (fastforce dest: ** simp: HLD_iff elim: alw_mono)

  have "(AE ω in ?M. ?P ω) ⟷
    (AE ω in ?M. ∀ s :: ('s × ('c ⇒ real)).
      (∀ c ∈ 𝒳. snd s c > k c) ∧ s ∈ state ` (MDP.MC.acc `` {repcs st cfg}) ⟶
      ¬ (ev (alw (λ xs. shd xs = s))) (smap state ω))" (is "?L ⟷ ?R")
  proof
    assume ?L
    then show ?R
      by eventually_elim auto
  next
    assume ?R
    with MDP.MC.AE_T_reachable[of "repcs st cfg"] show ?L
    proof (eventually_elim, intro allI impI notI, goal_cases)
      case (1 ω s)
      from this(1,2,5,6) show ?case
        by (intro alw_HLD_smap alw_disjoint_ccontr[where
              S = "state ` MDP.MC.acc `` {repcs st cfg}" and R = "{s}" and ω = "smap state ω"
              ]; simp add: HLD_iff; blast)
    qed
  qed

  also have "… ⟷
      (∀ s :: ('s × ('c ⇒ real)).
        (∀ c ∈ 𝒳. snd s c > k c) ∧ s ∈ state ` (MDP.MC.acc `` {repcs st cfg}) ⟶
        (AE ω in ?M. ¬ (ev (alw (λ xs. shd xs = s))) (smap state ω)))"
    using MDP.MC.countable_reachable[of "repcs st cfg"]
    by - (rule AE_all_imp_countable,
        auto intro: countable_subset[where B = "state ` MDP.MC.acc `` {repcs st cfg}"])
  also show ?thesis
    unfolding calculation
    apply clarsimp
    subgoal for l u x
      apply (rule MDP.non_loop_tail'[simplified, of "state x" ?S "?r (state x)"])
      subgoal
        apply safe
        subgoal premises prems for cfg cfg' l' u'
        proof -
          from prems have "state x = (l', u')"
            by (metis MDP.cfg_onD_state state_repcs)
          with ‹_ = state x› have [simp]: "l = l'" "u = u'"
            by auto
          show ?thesis
            unfolding ‹state x = _› using prems(1,3-) by (auto simp: R_G.valid_cfg_def intro: *)
        qed
        done
      subgoal
        apply (drule **)
        apply clarsimp
        apply (rule lt_1)
        apply (rule *)
        apply (auto dest: R_G.valid_cfg_state_in_S R_G.valid_cfgD)
        done
       apply (rule MDP.valid_cfgD[OF ‹repcs st cfg ∈ valid_cfg›]; fail)
      using *** unfolding alw_holds_pred_stream_iff[symmetric] HLD_def .
    done
qed

end (* PTA Regions *)


subsection ‹Main Result› text_raw ‹ \label{thm:minmax} ›

context Probabilistic_Timed_Automaton_Regions_Reachability
begin

lemma R_G_cfg_on_valid:
  "cfg ∈ R_G.valid_cfg" if "cfg ∈ R_G_cfg_on_div s'"
  using that unfolding R_G_cfg_on_div_def R_G.valid_cfg_def by auto

lemma cfg_on_valid:
  "cfg ∈ valid_cfg" if "cfg ∈ cfg_on_div s"
  using that unfolding cfg_on_div_def MDP.valid_cfg_def by auto

abbreviation "path_measure P cfg ≡ emeasure (MDP.T cfg) {x∈space MDP.St. P x}"
abbreviation "R_G_path_measure P cfg ≡ emeasure (R_G.T cfg) {x∈space R_G.St. P x}"
abbreviation "progressive st ≡ cfg_on_div st ∩ {cfg. alternating cfg}"
abbreviation "R_G_progressive st ≡ R_G_cfg_on_div st ∩ {cfg. alternating cfg}"

text ‹Summary of our results on divergent configurations:›
lemma absc_valid_cfg_eq:
  "absc ` progressive s = R_G_progressive s'"
  apply safe
  subgoal
    unfolding s'_def by (rule cfg_on_div_absc) auto
  subgoal
    by (simp add: AE_alw_ev_same_loc_iff cfg_on_valid)
  subgoal for cfg
    unfolding s'_def
    by (frule cfg_on_div_repcs_strong)
       (auto 4 4
          simp: s'_def R_G_cfg_on_div_def AE_alw_ev_same_loc_iff'[symmetric]
          intro: R_G_cfg_on_valid absc_repcs_id[symmetric]
       )
  done

text ‹Main theorem:›
theorem Min_Max_reachability:
  notes in_space_UNIV[measurable] and [iff] = pred_stream_iff
  shows
  "(⨆cfg∈ progressive s.      path_measure     (λ x. (holds φ  suntil holds ψ)  (s  ## x)) cfg)
 = (⨆cfg∈ R_G_progressive s'. R_G_path_measure (λ x. (holds φ' suntil holds ψ') (s' ## x)) cfg)
 ∧ (⨅cfg∈ progressive s.      path_measure     (λ x. (holds φ  suntil holds ψ)  (s  ## x)) cfg)
 = (⨅cfg∈ R_G_progressive s'. R_G_path_measure (λ x. (holds φ' suntil holds ψ') (s' ## x)) cfg)"
proof (rule SUP_eq_and_INF_eq; rule bexI[rotated]; erule IntE)
  fix cfg assume cfg_div: "cfg ∈ R_G_cfg_on_div s'" and "cfg ∈ Collect alternating"
  then have "alternating cfg"
    by auto
  let ?cfg' = "repcs s cfg"
  from ‹alternating cfg› cfg_div have "alternating ?cfg'"
    by (simp add: R_G_cfg_on_div_def s'_def AE_alw_ev_same_loc_iff'[of _ s])
  with cfg_div ‹alternating cfg› show "?cfg' ∈ cfg_on_div s ∩ Collect alternating"
    by (auto intro: cfg_on_div_repcs_strong simp: s'_def)
  show "emeasure (R_G.T cfg)   {x ∈ space R_G.St. (holds φ' suntil holds ψ') (s' ## x)}
      = emeasure (MDP.T ?cfg') {x ∈ space MDP.St. (holds φ suntil holds ψ)   (s ## x)}"
     (is "?a = ?b")
  proof -
    from cfg_div have "cfg ∈ R_G.valid_cfg"
      by (rule R_G_cfg_on_valid)
    from cfg_div have "cfg ∈ R_G.cfg_on s'"
      unfolding R_G_cfg_on_div_def by auto
    then have "state cfg = s'"
      by auto
    have "?a = ?b"
      apply (rule
          path_measure_eq_repcs''_new[
            of s cfg φ ψ, folded φ'_def ψ'_def, unfolded ‹_ = s'› state_repcs
            ]
          )
      subgoal
        unfolding s'_def ..
      subgoal
        by fact
      subgoal
        using ‹?cfg' ∈ cfg_on_div s ∩ _› by (blast intro: cfg_on_valid)
      subgoal premises prems for xs
        using prems s by (intro φ_stream)
      subgoal premises prems
        using prems s by (intro ψ_stream)
      done
    then show ?thesis
      by simp
  qed
next
  fix cfg assume cfg_div: "cfg ∈ cfg_on_div s" and "cfg ∈ Collect alternating"
  with absc_valid_cfg_eq show "absc cfg ∈ R_G_cfg_on_div s' ∩ Collect alternating"
    by auto
  show "emeasure (MDP.T cfg)        {x ∈ space MDP.St. (holds φ suntil holds ψ)   (s ## x)}
      = emeasure (R_G.T (absc cfg)) {x ∈ space R_G.St. (holds φ' suntil holds ψ') (s' ## x)}"
    (is "?a = ?b")
  proof -
    have "absc cfg ∈ R_G.valid_cfg"
      using R_G_cfg_on_valid ‹absc cfg ∈ R_G_cfg_on_div s' ∩ _› by blast
    from cfg_div have "cfg ∈ valid_cfg"
      by (simp add: cfg_on_valid)
    with ‹absc cfg ∈ R_G.valid_cfg› have "?b = ?a"
      by (intro MDP.alw_S R_G.alw_S path_measure_eq_absc1_new
            [where P = "pred_stream (λs. s ∈ 𝒮)" and Q = "pred_stream (λs. s ∈ S)"]
         )
         (auto simp: S_abss_𝒮 intro: 𝒮_abss_S intro!: suntil_abss suntil_reps, measurable)
    then show "?a = ?b"
      by simp
  qed
qed

end (* PTA Reachability Problem *)

end (* Theory *)