Theory MDP_Reachability_Problem

theory MDP_Reachability_Problem
  imports Markov_Decision_Process
begin

inductive_set directed_towards :: "'a set  ('a × 'a) set  'a set" for A r where
  start: "x. x  A  x  directed_towards A r"
| step: "x y. y  directed_towards A r  (x, y)  r  x  directed_towards A r"

hide_fact (open) start step

lemma directed_towards_mono:
  assumes "s  directed_towards A F" "F  G" shows "s  directed_towards A G"
  using assms by induct (auto intro: directed_towards.intros)

lemma directed_eq_rtrancl: "x  directed_towards A r  (aA. (x, a)  r*)"
proof
  assume "x  directed_towards A r" then show "aA. (x, a)  r*"
    by induction (auto intro: converse_rtrancl_into_rtrancl)
next
  assume "aA. (x, a)  r*"
  then obtain a where "(x, a)  r*" "a  A" by auto
  then show "x  directed_towards A r"
    by (induction rule: converse_rtrancl_induct)
       (auto intro: directed_towards.start directed_towards.step)
qed

lemma directed_eq_rtrancl_Image: "directed_towards A r = (r*)¯ `` A"
  unfolding set_eq_iff directed_eq_rtrancl Image_iff by simp

locale Reachability_Problem = Finite_Markov_Decision_Process K S for K :: "'s  's pmf set" and S +
  fixes S1 S2 :: "'s set"
  assumes S1: "S1  S" and S2: "S2  S" and S1_S2: "S1  S2 = {}"
begin

lemma [measurable]:
  "S  sets (count_space UNIV)" "S1  sets (count_space UNIV)" "S2  sets (count_space UNIV)"
  by auto

definition
  "v = (λcfgvalid_cfg. emeasure (T cfg) {xspace St. (HLD S1 suntil HLD S2) (state cfg ## x)})"

lemma v_eq: "cfg  valid_cfg 
    v cfg = emeasure (T cfg) {xspace St. (HLD S1 suntil HLD S2) (state cfg ## x)}"
  by (auto simp add: v_def)

lemma real_v: "cfg  valid_cfg  enn2real (v cfg) = 𝒫(ω in T cfg. (HLD S1 suntil HLD S2) (state cfg ## ω))"
  by (auto simp add: v_def T.emeasure_eq_measure)

lemma v_le_1: "cfg  valid_cfg  v cfg  1"
  by (auto simp add: v_def T.emeasure_eq_measure)

lemma v_neq_Pinf[simp]: "cfg  valid_cfg  v cfg  top"
  by (auto simp add: v_def)

lemma v_1_AE: "cfg  valid_cfg  v cfg = 1  (AE ω in T cfg. (HLD S1 suntil HLD S2) (state cfg ## ω))"
  unfolding v_eq T.emeasure_eq_measure ennreal_eq_1 space_T[symmetric, of cfg]
  by (rule T.prob_Collect_eq_1) simp

lemma v_0_AE: "cfg  valid_cfg  v cfg = 0  (AE x in T cfg. not (HLD S1 suntil HLD S2) (state cfg ## x))"
  unfolding v_eq T.emeasure_eq_measure space_T[symmetric, of cfg] ennreal_eq_zero_iff[OF measure_nonneg]
  by (rule T.prob_Collect_eq_0) simp

lemma v_S2[simp]: "cfg  valid_cfg  state cfg  S2  v cfg = 1"
  using S2 by (subst v_1_AE) (auto simp: suntil_Stream)

lemma v_nS12[simp]: "cfg  valid_cfg  state cfg  S1  state cfg  S2  v cfg = 0"
  by (subst v_0_AE) (auto simp: suntil_Stream)

lemma v_nS[simp]: "cfg  valid_cfg  v cfg = undefined"
  by (auto simp add: v_def)

lemma v_S1:
  assumes cfg[simp, intro]: "cfg  valid_cfg" and cfg_S1[simp]: "state cfg  S1"
  shows "v cfg = (+s. v (cont cfg s) action cfg)"
proof -
  have [simp]: "state cfg  S2"
    using cfg_S1 S1_S2 S1 by blast
  show ?thesis
    by (auto simp: v_eq emeasure_Collect_T[of _ cfg] K_cfg_def map_pmf_rep_eq nn_integral_distr
                   AE_measure_pmf_iff suntil_Stream[of _ _ "state cfg"]
                   valid_cfg_cont
             intro!: nn_integral_cong_AE)
qed

lemma real_v_integrable:
  "integrable (action cfg) (λs. enn2real (v (cont cfg s)))"
  by (rule measure_pmf.integrable_const_bound[where B="max 1 (enn2real undefined)"])
     (auto simp add: v_def measure_def[symmetric] le_max_iff_disj)

lemma real_v_integral_eq:
  assumes cfg[simp]: "cfg  valid_cfg"
  shows "enn2real (+ s. v (cont cfg s) action cfg) =  s. enn2real (v (cont cfg s)) action cfg"
 by (subst integral_eq_nn_integral)
    (auto simp: AE_measure_pmf_iff v_eq T.emeasure_eq_measure valid_cfg_cont
          intro!: arg_cong[where f=enn2real] nn_integral_cong_AE)

lemma v_eq_0_coinduct[consumes 3, case_names valid nS2 cont]:
  assumes *: "P cfg"
  assumes valid: "cfg. P cfg  cfg  valid_cfg"
  assumes nS2: "cfg. P cfg  state cfg  S2"
  assumes cont: "cfg cfg'. P cfg  state cfg  S1  cfg'  K_cfg cfg  P cfg'  v cfg' = 0"
  shows "v cfg = 0"
proof -
  from * valid[OF *]
  have "AE x in MC_syntax.T K_cfg cfg. ¬ (HLD S1 suntil HLD S2) (state cfg ## smap state x)"
    unfolding stream.map[symmetric] suntil_smap hld_smap'
  proof (coinduction arbitrary: cfg rule: MC.AE_not_suntil_coinduct_strong)
    case (ψ cfg) then show ?case
      by (auto simp del: cfg_onD_state dest: nS2)
  next
    case (φ cfg' cfg)
    then have *: "P cfg" "state cfg  S1" "cfg'  K_cfg cfg" and [simp, intro]: "cfg  valid_cfg"
      by auto
    with cont[OF *] show ?case
      by (subst (asm) v_0_AE)
         (auto simp: suntil_Stream T_def AE_distr_iff suntil_smap hld_smap' cong del: AE_cong)
  qed
  then have "AE ω in T cfg. ¬ (HLD S1 suntil HLD S2) (state cfg ## ω)"
    unfolding T_def by (subst AE_distr_iff) simp_all
  with valid[OF *] show ?thesis
    by (simp add: v_0_AE)
qed


definition "p = (λsS. P_sup s (λω. (HLD S1 suntil HLD S2) (s ## ω)))"

lemma p_eq_SUP_v: "s  S  p s =  (v ` cfg_on s)"
  by (auto simp add: p_def v_def P_sup_def T.emeasure_eq_measure intro: valid_cfgI intro!: SUP_cong cong: SUP_cong_simp)

lemma v_le_p: "cfg  valid_cfg  v cfg  p (state cfg)"
  by (subst p_eq_SUP_v) (auto intro!: SUP_upper dest: valid_cfgD valid_cfg_state_in_S)

lemma p_eq_0_imp: "cfg  valid_cfg  p (state cfg) = 0  v cfg = 0"
  using v_le_p[of cfg] by (auto intro: antisym)

lemma p_eq_0_iff: "s  S  p s = 0  (cfgcfg_on s. v cfg = 0)"
  unfolding p_eq_SUP_v by (subst SUP_eq_iff) auto

lemma p_le_1: "s  S  p s  1"
  by (auto simp: p_eq_SUP_v intro!: SUP_least v_le_1 intro: valid_cfgI)

lemma p_undefined[simp]: "s  S  p s = undefined"
  by (simp add: p_def)

lemma p_not_inf[simp]: "s  S  p s  top"
  using p_le_1[of s] by (auto simp: top_unique)

lemma p_S1: "s  S1  p s = (DK s. + t. p t measure_pmf D)"
  using S1 S1_S2 K_closed[of s] unfolding p_def
  by (simp add: P_sup_iterate[of _ s] subset_eq set_eq_iff suntil_Stream[of _ _ s])
     (auto intro!: SUP_cong nn_integral_cong_AE simp add: AE_measure_pmf_iff)

lemma p_S2[simp]: "s  S2  p s = 1"
  using S2 by (auto simp: v_S2[OF valid_cfgI] p_eq_SUP_v)

lemma p_nS12: "s  S  s  S1  s  S2  p s = 0"
  by (auto simp: p_eq_SUP_v v_nS12[OF valid_cfgI])

lemma p_pos:
  assumes "(s, t)  (SIGMA s:S1. DK s. set_pmf D)*" "t  S2" shows "0 < p s"
using assms proof (induction rule: converse_rtrancl_induct)
  case (step s t')
  then obtain D where "s  S1" "D  K s" "t'  D" "0 < p t'"
    by auto
  with S1 set_pmf_closed[of s D] have in_S: "t. t  D  t  S"
    by auto
  from t'  D 0 < p t' have "0 < pmf D t' * p t'"
    by (auto simp add: ennreal_zero_less_mult_iff pmf_positive)
  also have "  (+t. p t' * indicator {t'} tD)"
    using in_S[OF t'  D]
    by (subst nn_integral_cmult_indicator) (auto simp: ac_simps emeasure_pmf_single)
  also have "  (+t. p t D)"
    by (auto intro!: nn_integral_mono_AE split: split_indicator simp: in_S AE_measure_pmf_iff
      simp del: nn_integral_indicator_singleton)
  also have "  p s"
    using s  S1 D  K s by (auto intro: SUP_upper simp add: p_S1)
  finally show ?case .
qed simp

definition F_sup :: "('s  ennreal)  's  ennreal" where
  "F_sup f = (λsS. if s  S2 then 1 else if s  S1 then SUP DK s. +t. f t measure_pmf D else 0)"

lemma F_sup_cong: "(s. s  S  f s = g s)  F_sup f s = F_sup g s"
  using K_closed[of s]
  by (auto simp: F_sup_def AE_measure_pmf_iff subset_eq
              intro!: SUP_cong nn_integral_cong_AE)

lemma continuous_F_sup: "sup_continuous F_sup"
  unfolding sup_continuous_def fun_eq_iff F_sup_def[abs_def]
  by (auto simp:  SUP_apply[abs_def] nn_integral_monotone_convergence_SUP intro: SUP_commute)

lemma mono_F_sup: "mono F_sup"
  by (intro sup_continuous_mono continuous_F_sup)

lemma lfp_F_sup_iterate: "lfp F_sup = (SUP i. (F_sup ^^ i) (λxS. 0))"
proof -
  { have "(SUP i. (F_sup ^^ i) ) = (SUP i. (F_sup ^^ i) (λxS. 0))"
    proof (rule SUP_eq)
      fix i show "jUNIV. (F_sup ^^ i)   (F_sup ^^ j) (λxS. 0)"
        by (intro bexI[of _ i] funpow_mono mono_F_sup) auto
      have *: "(λxS. 0)  F_sup "
        using K_wf by (auto simp: F_sup_def le_fun_def)
      show "jUNIV. (F_sup ^^ i) (λxS. 0)  (F_sup ^^ j) "
        by (auto intro!: exI[of _ "Suc i"] funpow_mono mono_F_sup  *
                 simp del: funpow.simps simp add: funpow_Suc_right le_funI)
    qed }
  then show ?thesis
    by (auto simp: sup_continuous_lfp continuous_F_sup)
qed

lemma p_eq_lfp_F_sup: "p = lfp F_sup"
proof -
  { fix s assume "s  S" let ?F = "λP. HLD S2 or (HLD S1 aand nxt P)"
    have "P_sup s (λω. (HLD S1 suntil HLD S2) (s ## ω)) = (i. P_sup s (λω. (?F ^^ i)  (s ## ω)))"
    proof (simp add: suntil_def, rule P_sup_lfp)
      show "(##) s  measurable St St"
        by simp
      (* This proof should work automatically *)
      fix P assume P: "Measurable.pred St P"
      show "Measurable.pred St (HLD S2 or (HLD S1 aand (λω. P (stl ω))))"
        by (intro pred_intros_logic measurable_compose[OF _ P] measurable_compose[OF measurable_shd]) auto
    qed (auto simp: sup_continuous_def)
    also have " = (SUP i. (F_sup ^^ i) (λxS. 0) s)"
    proof (rule SUP_cong)
      fix i from s  S show "P_sup s (λω. (?F ^^ i)  (s##ω)) = (F_sup ^^ i) (λxS. 0) s"
      proof (induct i arbitrary: s)
        case (Suc n) show ?case
        proof (subst P_sup_iterate)
          (* This proof should work automatically *)
          show "Measurable.pred St (λω. (?F ^^ Suc n)  (s ## ω))"
            apply (intro measurable_compose[OF measurable_Stream[OF measurable_const measurable_ident_sets[OF refl]] measurable_predpow])
            apply simp
            apply (simp add: bot_fun_def[abs_def])
            apply (intro pred_intros_logic measurable_compose[OF measurable_stl]  measurable_compose[OF measurable_shd])
            apply auto
            done
        next
          show "(DK s. + t. P_sup t (λω. (?F ^^ Suc n)  (s ## t ## ω)) measure_pmf D) =
            (F_sup ^^ Suc n) (λxS. 0) s"
            unfolding funpow.simps comp_def
            using S1 S2 s  S
            by (subst F_sup_cong[OF Suc(1)[symmetric]])
               (auto simp add: F_sup_def measure_pmf.emeasure_space_1[simplified] K_wf subset_eq)
        qed
      qed simp
    qed simp
    finally have "lfp F_sup s = P_sup s (λω. (HLD S1 suntil HLD S2) (s ## ω))"
      by (simp add: lfp_F_sup_iterate image_comp) }
  moreover have "s. s  S  lfp F_sup s = undefined"
    by (subst lfp_unfold[OF mono_F_sup]) (auto simp add: F_sup_def)
  ultimately show ?thesis
    by (auto simp: p_def)
qed

definition "Se = {sS. p s = 0}"

lemma Se: "Se  S"
  by (auto simp add: Se_def)

lemma v_Se: "cfg  valid_cfg  state cfg  Se  v cfg = 0"
  using p_eq_0_imp[of cfg] by (auto simp: Se_def)

lemma Se_nS2: "Se  S2 = {}"
  by (auto simp: Se_def)

lemma Se_E1: "s  Se  S1  (s, t)  E  t  Se"
  unfolding Se_def using S1
  by (auto simp: p_S1 SUP_eq_iff K_wf nn_integral_0_iff_AE AE_measure_pmf_iff E_def
           intro: set_pmf_closed antisym
           cong: rev_conj_cong)

lemma Se_E2: "s  S1  (t. (s, t)  E  t  Se)  s  Se"
  unfolding Se_def using S1 S1_S2
  by (force simp: p_S1 SUP_eq_iff K_wf nn_integral_0_iff_AE AE_measure_pmf_iff E_def
            cong: rev_conj_cong)

lemma Se_E_iff: "s  S1  s  Se  (t. (s, t)  E  t  Se)"
  using Se_E1[of s] Se_E2[of s] by blast

definition "Sr = S - (Se  S2)"

lemma Sr: "Sr  S"
  by (auto simp: Sr_def)

lemma Sr_S1: "Sr  S1"
  by (auto simp: p_nS12 Sr_def Se_def)

lemma Sr_eq: "Sr = S1 - Se"
  using S1_S2 S1 S2 by (auto simp add: Sr_def Se_def p_nS12)

lemma v_neq_0_imp: "cfg  valid_cfg  v cfg  0  state cfg  Sr  S2"
  using p_eq_0_imp[of cfg] by (auto simp add: Sr_def Se_def valid_cfg_state_in_S)

lemma valid_cfg_action_in_K: "cfg  valid_cfg  action cfg  K (state cfg)"
  by (auto dest!: valid_cfgD)

lemma K_cfg_E: "cfg  valid_cfg  cfg'  K_cfg cfg  (state cfg, state cfg')  E"
  by (auto simp: E_def K_cfg_def valid_cfg_action_in_K)

lemma Sr_directed_towards_S2:
  assumes s: "s  Sr"
  shows "s  directed_towards S2 {(s, t) | s t. s  Sr  (s, t)  E}" (is "s  ?D")
proof -
  { fix cfg assume "s  ?D" "cfg  cfg_on s"
    with s Sr have "state cfg  Sr" "state cfg  ?D" "cfg  valid_cfg"
      by (auto intro: valid_cfgI)
    then have "v cfg = 0"
    proof (coinduction arbitrary: cfg rule: v_eq_0_coinduct)
      case (cont cfg' cfg)
      with v_neq_0_imp[of cfg'] show ?case
        by (auto intro: directed_towards.intros K_cfg_E)
    qed (auto intro: directed_towards.intros) }
  with p_eq_0_iff[of s] s show ?thesis
    unfolding Sr_def Se_def by blast
qed

definition "proper ct  ct  PiE S K  (sSr. v (simple ct s) > 0)"

lemma Sr_nS2: "s  Sr  s  S2"
  by (auto simp: Sr_def)

lemma properD1: "proper ct  ct  PiE S K"
  by (auto simp: proper_def)

lemma proper_eq:
  assumes ct[simp, intro]: "ct  PiE S K"
  shows "proper ct  Sr  directed_towards S2 (SIGMA s:Sr. ct s)"
    (is "_  _  ?D")
proof -
  have *[simp]: "s. s  Sr  s  S" and ct': "ct  Pi S K"
    using ct by (auto simp: Sr_def simp del: ct)
  { fix s t have "s  S  t  ct s  t  S"
      using K_closed[of s] ct' by (auto simp add: subset_eq) }
  note ct_closed = this

  let ?C = "simple ct"
  from ct have valid_C[simp]: "s. s  S  ?C s  valid_cfg"
    by (auto simp add: PiE_def)
  { fix s assume "s  ?D"
    then have "0 < v (?C s)"
    proof induct
      case (step s t)
      then have s: "s  Sr" and t: "t  ct s" and [simp]: "s  S"
        by auto
      with Sr_S1 ct have "v (?C s) = (+t. v (?C t) ct s)"
        by (subst v_S1) (auto intro!: nn_integral_cong_AE AE_pmfI)
      also have "  0"
        using ct t step
        by (subst nn_integral_0_iff_AE) (auto simp add: AE_measure_pmf_iff zero_less_iff_neq_zero)
      finally show ?case
        using ct by (auto simp add: less_le)
    qed (subst v_S2, insert S2, auto) }
  moreover
  { fix s assume s: "s  ?D" "s  Sr"
    with ct' have C: "?C s  cfg_on s" and [simp]: "s  S"
      by auto
    from s have "v (?C s) = 0"
    proof (coinduction arbitrary: s rule: v_eq_0_coinduct)
      case (cont cfg s)
      with S1 obtain t where "cfg = ?C t" "t  ct s" "s  S"
        by (auto simp: set_K_cfg subset_eq)
      with cont(1,2) v_neq_0_imp[of "?C t"] ct_closed[of s t] show ?case
        by (intro exI[of _ t] disjCI) (auto intro: directed_towards.intros)
    qed (auto simp: Sr_nS2) }
  ultimately show ?thesis
    unfolding proper_def using ct by (force simp del: v_nS v_S2 v_nS12 ct)
qed

lemma exists_proper:
  obtains ct where "proper ct"
proof atomize_elim
  define r where "r = rec_nat S2 (λ_ S'. {sSr. tS'. (s, t)  E})"
  then have [simp]: "r 0 = S2" "n. r (Suc n) = {sSr. tr n. (s, t)  E}"
    by simp_all

  { fix s assume "s  Sr"
    then have "s  directed_towards S2 {(s, t) | s t. s  Sr  (s, t)  E}"
      by (rule Sr_directed_towards_S2)
    from this sSr have "n. s  r n"
    proof induction
      case (step s t)
      show ?case
      proof cases
        assume "t  S2" with step.prems step.hyps show ?thesis
          by (intro exI[of _ "Suc 0"]) force
      next
        assume "t  S2"
        with step obtain n where "t  r n" "t  Sr"
          by (auto elim: directed_towards.cases)
        with tSr step.hyps show ?thesis
          by (intro exI[of _ "Suc n"]) force
      qed
    qed (simp add: Sr_def) }
  note r = this

  { fix s assume "s  S"
    have "DK s. s  Sr  (tD. n. t  r n  (m. s  r m  n < m))"
    proof cases
      assume s: "s  Sr"
      define n where "n = (LEAST n. s  r n)"
      then have "s  r n" and n: "i. i < n  s  r i"
        using r s by (auto intro: LeastI_ex dest: not_less_Least)
      with s have "n  0"
        by (intro notI) (auto simp: Sr_def)
      then obtain n' where "n = Suc n'"
        by (cases n) auto
      with s  r n obtain t D where "D  K s" "t  D" "t  r n'"
        by (auto simp: E_def)
      with n n = Suc n' s show ?thesis
        by (auto intro!: bexI[of _ D] bexI[of _ t] exI[of _ n'] simp: not_less_eq[symmetric])
    qed (insert K_wf sS, auto) }
  then obtain ct where ct: "s. s  S  ct s  K s"
    "s. s  S  s  Sr  tct s. n. t  r n  (m. s  r m  n < m)"
    by metis
  then have *: "restrict ct S  PiE S K"
    by auto

  moreover
  { fix s assume "s  Sr"
    then obtain n where "s  r n"
      by (metis r)
    with s  Sr have "s  directed_towards S2 (SIGMA s : Sr. ct s)"
    proof (induction n arbitrary: s rule: less_induct)
      case (less n s)
      moreover with Sr have "s  S" by auto
      ultimately obtain t m where "t  ct s" "t  r m" "m < n"
        using ct[of s] by (auto simp: E_def)
      with less.IH[of m t] s  Sr show ?case
        by (cases m) (auto intro: directed_towards.intros)
    qed }

  ultimately show "ct. proper ct"
    using Sr S2
    by (auto simp: proper_eq[OF *] subset_eq
             intro!: exI[of _ "restrict ct S"]
             cong: Sigma_cong)
qed

definition "l_desc X ct l s 
    s  directed_towards S2 (SIGMA s : X. {l s}) 
    v (simple ct s)  v (simple ct (l s)) 
    l s  maximal (λs. v (simple ct s)) (ct s)"

lemma exists_l_desc:
  assumes ct: "proper ct"
  shows "lSr  Sr  S2. sSr. l_desc Sr ct l s"
proof -
  have ct_closed: "s t. s  S  t  ct s  t  S"
    using ct K_closed by (auto simp: proper_def PiE_iff)
  have ct_Pi: "ct  Pi S K"
    using ct by (auto simp: proper_def)

  have "finite Sr"
    using S_finite by (auto simp: Sr_def)
  then show ?thesis
  proof (induct rule: finite_induct_select)
    case (select X)
    then obtain l where l: "l  X  X  S2" and desc: "s. s  X  l_desc X ct l s"
      by auto
    obtain x where x: "x  Sr - X"
      using X  Sr by auto
    then have "x  S"
      by (auto simp: Sr_def)

    let ?C = "simple ct"
    let ?v = "λs. v (?C s)" and ?E = "λs. set_pmf (ct s)"
    let ?M = "λs. maximal ?v (?E s)"

    have finite_E[simp]: "s. s  S  finite (?E s)"
      using K_closed ct by (intro finite_subset[OF _ S_finite]) (auto simp: proper_def subset_eq)

    have valid_C[simp]: "s. s  S  ?C s  valid_cfg"
      using ct by (auto simp: proper_def intro!: simple_valid_cfg)

    have E_ne[simp]: "s. ?E s  {}"
        by (rule set_pmf_not_empty)

    have "sSr - X. t?M s. t  S2  X"
    proof (rule ccontr)
      assume "¬ ?thesis"
      then have not_M: "s. s  Sr - X  ?M s  (S2  X) = {}"
        by auto

      let ?Sm = "maximal ?v (Sr - X)"

      have "finite (Sr - X)" "Sr - X  {}"
        using X  Sr by (auto intro!: finite_subset[OF _ S_finite] simp: Sr_def)
      from maximal_ne[OF this] obtain sm where sm: "sm  ?Sm"
        by force

      have "s0?Sm. t?E s0. t  ?Sm"
      proof (rule ccontr)
        assume "¬ ?thesis"
        then have Sm: "s0 t. s0  ?Sm  t  ?E s0  t  ?Sm" by blast
        from sm  ?Sm have [simp]: "sm  S" and "sm  Sr"
          by (auto simp: Sr_def dest: maximalD1)

        from sm  ?Sm have "v (?C sm) = 0"
        proof (coinduction arbitrary: sm rule: v_eq_0_coinduct)
          case (cont t sm) with S1 show ?case
            by (intro exI[of _ "state t"] disjCI conjI Sm[of sm "state t"])
               (auto simp: set_K_cfg)
        qed (auto simp: Sr_def ct_Pi dest!: maximalD1)
        with sm  Sr proper ct show False
          by (auto simp: proper_def)
      qed
      then obtain s0 t where "s0  ?Sm" and t: "t  ?E s0" "t  ?Sm"
        by metis
      with Sr_S1 have s0: "s0  Sr - X" and [simp]: "s0  S" and "s0  S1"
        by (auto simp: Sr_def dest: maximalD1)

      from proper ct s0  S s0 have "?v s0  0"
        by (auto simp add: proper_def)
      then have "0 < ?v s0" by (simp add: zero_less_iff_neq_zero)

      { fix t assume "t  Se  S2  X" "t  ?E s0" and "?v s0  ?v t"
        moreover have "t  Se  ?v t = 0"
          by (simp add: p_eq_0_imp Se_def ct_Pi)
        ultimately have t: "t  S2  X" "t  ?E s0"
          using 0 < ?v s0 by (auto simp: Se_def)

        have "maximal ?v (?E s0  (S2  X))  {}"
          using finite_E t by (intro maximal_ne) auto
        moreover
        { fix x y assume x: "x  S2  X" "x  ?E s0"
            and *: "y?E s0  (S2  X). ?v y  ?v x" and y: "y  ?E s0"
          with S2 s0  S[THEN ct_closed] have [simp]: "x  S" "y  S"
            by auto

          have "?v y  ?v x"
          proof cases
            assume "y  Sr - X"
            then have "?v y  ?v s0"
              using s0  ?Sm by (auto intro: maximalD2)
            also note ?v s0  ?v t
            also have "?v t  ?v x"
              using * t by auto
            finally show ?thesis .
          next
            assume "y  Sr - X" with y * show ?thesis
              by (auto simp: Sr_def v_Se[of "?C y"] ct_Pi)
          qed }
        then have "maximal ?v (?E s0  (S2  X))  maximal ?v (?E s0)"
          by (auto simp: maximal_def)
        moreover note not_M[OF s0]
        ultimately have False
          by (blast dest: maximalD1) }
      then have less_s0: "t. t  Se  S2  X  t  ?E s0  ?v t < ?v s0"
        by (auto simp add: not_le[symmetric])

      let ?K = "ct s0"

      have "?v s0 = (+ x. ?v x ?K)"
        using v_S1[of "?C s0"] s0  S1 s0  S
        by (auto simp add: ct_Pi intro!: nn_integral_cong_AE AE_pmfI)
      also have " < (+x. ?v s0 ?K)"
      proof (intro nn_integral_less)
        have "(+x. ?v x ?K)  (+x. 1 ?K)"
          using ct ct_closed[of s0]
          by (intro nn_integral_mono_AE)
             (auto intro!: v_le_1 simp: AE_measure_pmf_iff proper_def ct_Pi)
        then show "(+x. ?v x ?K)  "
          by (auto simp: top_unique)
        have "?v t < ?v s0"
        proof cases
          assume "t  Se  S2  X" then show ?thesis
            using less_s0[of t] t by simp
        next
          assume "t  Se  S2  X"
          with t(1) ct_closed[of s0 t] have "t  Sr - X"
            unfolding Sr_def by (auto simp: E_def)
          with t(2) show ?thesis
            using s0  ?Sm by (auto simp: maximal_def not_le intro: less_le_trans)
        qed
        then show "¬ (AE x in ?K. ?v s0  ?v x)"
          using t by (auto simp: not_le AE_measure_pmf_iff E_def cong del: AE_cong intro!: exI[of _ "t"])

        show "AE x in ?K. ?v x  ?v s0"
        proof (subst AE_measure_pmf_iff, safe)
          fix t assume t: "t  ?E s0"
          show "?v t  ?v s0"
          proof cases
            assume "t  Se  S2  X" then show ?thesis
              using less_s0[of t] t by simp
          next
            assume "t  Se  S2  X" with t s0  ?Sm s0  S show ?thesis
              by (elim maximalD2) (auto simp: Sr_def intro!: ct_closed[of _ t])
          qed
        qed
      qed (insert ct_closed[of s0], auto simp: AE_measure_pmf_iff)
      also have " = ?v s0"
        using s0  S measure_pmf.emeasure_space_1[of "ct s0"] by simp
      finally show False
        by simp
    qed
    then obtain s t where s: "s  Sr - X" and t: "t  S2  X" "t  ?M s"
      by auto
    with S2 X  Sr have "s  S2" and "s  S  s  S2" and "s  X"and [simp]: "t  S"
      by (auto simp add: Sr_def)
    define l' where "l' = l(s := t)"
    then have l'_s[simp, intro]: "l' s = t"
      by simp

    let ?D = "λX l. directed_towards S2 (SIGMA s : X. {l s})"
    { fix s' assume "s'  ?D X l" "s'  X"
      from this(1) have "s'  ?D (insert s X) l'"
        by (rule directed_towards_mono) (auto simp: l'_def s  X) }
    note directed_towards_l' = this

    show ?case
    proof (intro bexI ballI, elim insertE)
      show "s  Sr - X" by fact
      show "l'  insert s X  insert s X  S2"
        using s t l by (auto simp: l'_def)
    next
      fix s' assume s': "s'  X"
      moreover
      from desc[OF s'] have "s'  ?D X l" and *: "?v s'  ?v (l s')" "l s'  ?M s'"
        by (auto simp: l_desc_def)
      moreover have "l' s' = l s'"
        using s'  X s by (auto simp add: l'_def)
      ultimately show "l_desc (insert s X) ct l' s'"
        by (auto simp: l_desc_def intro!: directed_towards_l')
    next
      fix s' assume "s' = s"
      show "l_desc (insert s X) ct l' s'"
        unfolding s' = s l_desc_def l'_s
      proof (intro conjI)
        show "s  ?D (insert s X) l'"
        proof cases
          assume "t  S2"
          with t have "t  X" by auto
          with desc have "t  ?D X l"
            by (simp add: l_desc_def)
          then show ?thesis
            by (force intro: directed_towards.step[OF directed_towards_l'] t  X)
        qed (force intro: directed_towards.step directed_towards.start)

        from s  Sr - X Sr_S1 have [simp]: "s  S1" "s  S"
          by (auto simp: Sr_def)
        show "?v s  ?v t"
          using t(2)[THEN maximalD2] ct
          by (auto simp add: v_S1 AE_measure_pmf_iff proper_def Pi_iff PiE_def
                   intro!: measure_pmf.nn_integral_le_const)
      qed fact
    qed
  qed simp
qed

lemma F_v_memoryless:
  obtains ct where "ct  PiE S K" "vsimple ct = F_sup (vsimple ct)"
proof atomize_elim
  define R where "R = {(ct(s := D), ct) | ct s D.
    ct  PiE S K  proper ct  s  Sr  D  K s  v (simple ct s) < (+t. v (simple ct t) D) }"

  { fix ct ct' assume ct_ct': "(ct', ct)  R"
    let ?v = "λs. v (simple ct s)" and ?v' = "λs. v (simple ct' s)"

    from ct_ct' obtain s D where "ct  PiE S K" "proper ct" and s: "s  Sr" and D: "D  K s"
      and not_maximal: "?v s < (+t. ?v t D)" and ct'_eq: "ct' = ct(s := D)"
      by (auto simp: R_def)
    with Sr_S1 have ct: "ct  Pi S K" and "s  S" and "s  S1"
      by (auto simp: Sr_def)
    then have valid_ct[simp]: "s. s  S  simple ct s  cfg_on s"
      by simp

    from ct'_eq have [simp]: "ct' s = D" "t. t  s  ct' t = ct t"
      by simp_all

    from ct_ct' Sr have ct'_E: "ct'  PiE S K"
      by (auto simp: ct'_eq R_def)
    from ct s D have ct': "ct'  Pi S K"
      by (auto simp: ct'_eq)
    then have valid_ct'[simp]: "s. s  S  simple ct' s  cfg_on s"
      by simp

    from exists_l_desc[OF proper ct]
    obtain l where l: "l  Sr  Sr  S2" and "s. s  Sr  l_desc Sr ct l s"
      by auto
    then have directed_l: "s. s  Sr  s  directed_towards S2 (SIGMA s:Sr. {l s})"
      and v_l_mono: "s. s  Sr  ?v s  ?v (l s)"
      and l_in_Ea: "s. s  Sr  l s  ct s"
      by (auto simp: l_desc_def dest!: maximalD1)

    let ?E = "λct. SIGMA s:Sr. ct s"
    let ?D = "λct. directed_towards S2 (?E ct)"

    have finite_E[simp]: "s. s  S  finite (ct' s)"
      using ct' K_closed by (intro rev_finite_subset[OF S_finite]) auto

    have "maximal ?v (ct' s)  {}"
      using ct' D sS finite_E[of s] by (intro maximal_ne set_pmf_not_empty) (auto simp del: finite_E)
    then obtain s' where s': "s'  maximal ?v (ct' s)"
      by blast
    with K_closed[OF s  S] D have "s'  S"
      by (auto dest!: maximalD1)

    have "s'  s"
    proof
      assume [simp]: "s' = s"
      have "?v s < (+t. ?v t D)"
        by fact
      also have "  (+t. ?v s D)"
        using s  S s' D by (intro nn_integral_mono_AE) (auto simp: AE_measure_pmf_iff intro: maximalD2)
      finally show False
        using measure_pmf.emeasure_space_1[of D] by (simp add: s  S ct)
    qed

    have "p s'  0"
    proof
      assume "p s' = 0"
      then have "?v s' = 0"
        using v_le_p[of "simple ct s'"] ct s'  S by (auto intro!: antisym ct)
      then have "(+t. ?v t D) = 0"
        using maximalD2[OF s'] by (subst nn_integral_0_iff_AE) (auto simp: sS D AE_measure_pmf_iff)
      then have "?v s < 0"
        using not_maximal by auto
      then show False
        using sS by (simp add: ct)
    qed
    with s'  S have "s'  S2  Sr"
      by (auto simp: Sr_def Se_def)

    have l_acyclic: "(s', s)  (SIGMA s:Sr. {l s})^+"
    proof
      assume "(s', s)  (SIGMA s:Sr. {l s})^+"
      then have "?v s'  ?v s"
        by induct (blast intro: order_trans v_l_mono)+
      also have " < (+t. ?v t D)"
        using not_maximal .
      also have "  (+t. ?v s' D)"
        using s' by (intro nn_integral_mono_AE) (auto simp: s  S D AE_measure_pmf_iff intro: maximalD2)
      finally show False
        using measure_pmf.emeasure_space_1[of D] by (simp add:s'  S ct)
    qed

    from s'  S2  Sr have "s'  ?D ct'"
    proof
      assume "s'  Sr"
      then have "l s'  directed_towards S2 (SIGMA s:Sr. {l s})"
        using l directed_l[of "l s'"] by (auto intro: directed_towards.start)
      moreover from s'  Sr have "(s', l s')  (SIGMA s:Sr. {l s})^+"
        by auto
      ultimately have "l s'  ?D ct'"
      proof induct
        case (step t t')
        then have t: "t  s" "t  Sr" "t' = l t"
          using l_acyclic by auto

        from step have "(s', t')  (SIGMA s:Sr. {l s})+"
          by (blast intro: trancl_into_trancl)
        from step(2)[OF this] show ?case
          by (rule directed_towards.step) (simp add: l_in_Ea t)
      qed (rule directed_towards.start)
      then show "s'  ?D ct'"
        by (rule directed_towards.step)
           (simp add: l_in_Ea s'  Sr s  Sr s'  s)
    qed (rule directed_towards.start)

    have proper: "proper ct'"
      unfolding proper_eq[OF ct'_E]
    proof
      fix t assume "t  Sr"
      from directed_l[OF this] show "t  ?D ct'"
      proof induct
        case (step t t')
        show ?case
        proof cases
          assume "t = s"
          with s  Sr s'[THEN maximalD1] have "(t, s')  ?E ct'"
            by auto
          with s'  ?D ct' show ?thesis
            by (rule directed_towards.step)
        next
          assume "t  s"
          with step have "(t, t')  ?E ct'"
            by (auto simp: l_in_Ea)
          with step.hyps(2) show ?thesis
            by (rule directed_towards.step)
        qed
      qed (rule directed_towards.start)
    qed

    have "?v  ?v'"
    proof (intro le_funI leI notI)
      fix t' assume *: "?v' t' < ?v t'"
      then have "t'  S"
        by (metis v_nS simple_valid_cfg_iff ct' ct order.irrefl)

      define Δ where "Δ t = enn2real (?v t) - enn2real (?v' t)" for t
      with * t'  S have "0 < Δ t'"
        by (cases "?v t'" "?v' t'" rule: ennreal2_cases) (auto simp add: ct' ct ennreal_less_iff)

      { fix t assume t: "t  maximal Δ S"
        with t'  S have "Δ t'  Δ t"
          by (auto intro: maximalD2)
        with 0 < Δ t' have "0 < Δ t" by simp
        with t have "t  Sr"
          by (auto simp add: Sr_def v_Se ct ct' Δ_def dest!: maximalD1) }
      note max_is_Sr = this

      { fix s assume "s  S"
        with v_le_1[of "simple ct' s"] v_le_1[of "simple ct s"]
        have "¦Δ s¦  1"
          by (cases "?v s" "?v' s" rule: ennreal2_cases) (auto simp: Δ_def ct ct') }
      note Δ_le_1[simp] = this
      then have ennreal_Δ: "s. s  S  Δ s = ?v s - ?v' s"
        by (auto simp add: Δ_def v_def T.emeasure_eq_measure ct ct' ennreal_minus)

      from s  S S_finite have "maximal Δ S  {}"
        by (intro maximal_ne) auto
      then obtain t where "t  maximal Δ S" by auto
      from max_is_Sr[OF this] proper have "t  ?D ct'"
        unfolding proper_eq[OF ct'_E] by auto
      from this t  maximal Δ S show False
      proof induct
        case (start t)
        then have "t  Sr"
          by (intro max_is_Sr)
        with t  S2 show False
          by (auto simp: Sr_def)
      next
        case (step t t')
        then have t': "t'  ct' t" and "t  Sr" and t: "t  maximal Δ S"
          by (auto intro: max_is_Sr simp: comp_def)
        then have "t'  S" "t  S1" "t  S"
          using Sr_S1 S1
          by (auto simp: Pi_closed[OF ct'])

        have "Δ t  Δ t'"
        proof (intro leI notI)
          assume less: "Δ t' < Δ t"
          have "(s. Δ s ct' t) < (s. Δ t ct' t)"
          proof (intro measure_pmf.integral_less_AE)
            show "emeasure (ct' t) {t'}  0" "{t'}  sets (ct' t)"
              "AE s in ct' t. s{t'}  Δ s  Δ t"
              using t' less by (auto simp add: emeasure_pmf_single_eq_zero_iff)
            show "AE s in ct' t. Δ s  Δ t"
              using ct' ct t D
              by (auto simp add: AE_measure_pmf_iff ct tS Pi_iff E_def Pi_closed[OF ct']
                       intro!: maximalD2[of t Δ] intro: Pi_closed[OF ct'] maximalD1)
            show "integrable (ct' t) (λ_. Δ t)" "integrable (ct' t) Δ"
              using ct ct' t  S D
              by (auto intro!: measure_pmf.integrable_const_bound[where B=1] Δ_le_1
                       simp: AE_measure_pmf_iff dest: Pi_closed)
          qed
          also have " = Δ t"
            using measure_pmf.prob_space[of "ct' t"] by simp
          also have "Δ t  (s. enn2real (?v s) ct' t) - (s. enn2real (?v' s) ct' t)"
          proof -
            have "?v t  (+s. ?v s ct' t)"
            proof cases
              assume "t = s" with not_maximal show ?thesis by simp
            next
              assume "t  s" with S1 tS1 t  S ct ct' show ?thesis
                by (subst v_S1) (auto intro!: nn_integral_mono_AE AE_pmfI)
            qed
            also have " = ennreal (s. enn2real (?v s) ct' t)"
              using ct ct' tS
              by (intro measure_pmf.ennreal_integral_real[symmetric, where B=1])
                 (auto simp: AE_measure_pmf_iff one_ennreal_def[symmetric]
                       intro!: v_le_1 simple_valid_cfg intro: Pi_closed)
            finally have "enn2real (?v t)  (s. enn2real (?v s) ct' t)"
              using ct tS by (simp add: v_def T.emeasure_eq_measure)
            moreover
            { have "?v' t = (+s. ?v' s ct' t)"
                using ct ct' t  S t  S1 S1 by (subst v_S1) (auto intro!: nn_integral_cong_AE AE_pmfI)
              also have " = ennreal (s. enn2real (?v' s) ct' t)"
                using ct' tS
                by (intro measure_pmf.ennreal_integral_real[symmetric, where B=1])
                   (auto simp: AE_measure_pmf_iff one_ennreal_def[symmetric]
                         intro!:  v_le_1 simple_valid_cfg intro: Pi_closed)
              finally have "enn2real (?v' t) = (s. enn2real (?v' s) ct' t)"
                using ct' tS by (simp add: v_def T.emeasure_eq_measure) }
            ultimately show ?thesis
              using t  S by (simp add: Δ_def ennreal_minus_mono)
          qed
          also have " = (s. Δ s ct' t)"
            unfolding Δ_def using Pi_closed[OF ct tS] Pi_closed[OF ct' tS] ct ct'
            by (intro Bochner_Integration.integral_diff[symmetric] measure_pmf.integrable_const_bound[where B=1])
               (auto simp: AE_measure_pmf_iff real_v)
          finally show False
            by simp
        qed
        with t[THEN  maximalD2] t  S t'  S have "Δ t = Δ t'"
          by (auto intro: antisym)
        with t t'  S have "t'  maximal Δ S"
          by (auto simp: maximal_def)
        then show ?case
          by fact
      qed
    qed
    moreover have "?v s < ?v' s"
    proof -
      have "?v s < (+t. ?v t D)"
        by fact
      also have "  (+t. ?v' t D)"
        using ?v  ?v' sS D ct ct'
        by (intro nn_integral_mono) (auto simp: le_fun_def)
      also have " = ?v' s"
        using sS1 S1 ct' s  S by (subst (2) v_S1) (auto intro!: nn_integral_cong_AE AE_pmfI)
      finally show ?thesis .
    qed
    ultimately have "?v < ?v'"
      by (auto simp: less_le le_fun_def fun_eq_iff)
    note this proper ct' }
  note v_strict = this(1) and proper = this(2) and sc'_R = this(3)

  have "finite (PiE S K × PiE S K)"
    by (intro finite_PiE S_finite K_finite finite_SigmaI)
  then have "finite R"
    by (rule rev_finite_subset) (auto simp add: PiE_iff Sr_def R_def intro: extensional_arb)
  moreover
  from v_strict have "acyclic R"
    by (rule acyclicI_order)
  ultimately have "wf R"
    by (rule finite_acyclic_wf)

  from exists_proper obtain ct' where ct': "proper ct'" .
  define ct where "ct = restrict ct' S"
  with ct' have sc_Pi: "ct  Pi S K" and "ct'  Pi S K"
    by (auto simp: proper_def)
  then have ct: "ct  {ct  PiE S K. proper ct}"
    using ct' directed_towards_mono[where F="SIGMA s:Sr. ct' s" and G="SIGMA s:Sr. ct s"]
    apply simp
    apply (subst proper_eq)
    by (auto simp: ct_def proper_eq[OF properD1[OF ct']] subset_eq Sr_def)

  show "ct. ct  PiE S K  vsimple ct = F_sup (vsimple ct)"
  proof (rule wfE_min[OF wf R ct])
    fix ct assume ct: "ct  {ct  PiE S K. proper ct}"
    then have "ct  Pi S K" "proper ct"
      by (auto simp: proper_def)
    assume min: "ct'. (ct', ct)  R  ct'  {ct  PiE S K. proper ct}"
    let ?v = "λs. v (simple ct s)"
    { fix s assume "s  S" "s  S1" "s  S2"
      with ct have "ct s  K s" "?v s  integralN (ct s) ?v"
        by (auto simp: v_S1 PiE_def intro!: nn_integral_mono_AE AE_pmfI)
      moreover
      { have "0  ?v s"
          using sS ct by (simp add: PiE_def)
        also assume v_less: "?v s < (DK s. + s. v (simple ct s) measure_pmf D)"
        also have "  p s"
          unfolding p_S1[OF sS1] using sS ct v_le_p[OF simple_valid_cfg, OF ct  Pi S K]
          by (auto intro!: SUP_mono nn_integral_mono_AE bexI
                   simp: PiE_def AE_measure_pmf_iff set_pmf_closed)
        finally have "s  Sr"
          using sS sS2 by (simp add: Sr_def Se_def)

        from v_less obtain D where "D  K s" "?v s < integralN D ?v"
          by (auto simp: less_SUP_iff)
        with ct sS sSr have "(ct(s:=D), ct)  R" "ct(s:=D)  PiE S K"
          unfolding R_def by (auto simp: PiE_def extensional_def)
        from proper[OF this(1)] min[OF this(1)] ct D  K s sS this(2)
        have False
          by simp }
      ultimately have "?v s = (DK s. + s. ?v s measure_pmf D)"
        by (auto intro: antisym SUP_upper2[where i="ct s"] leI)
      also have " = (DK s. integralN (measure_pmf D) (λsS. ?v s))"
        using sS by (auto intro!: SUP_cong nn_integral_cong v_nS simp: ct simple_valid_cfg_iff ct  Pi S K)
      finally have "?v s = (DK s. integralN (measure_pmf D) (λsS. ?v s))" . }
    then have "?v = F_sup ?v"
      unfolding F_sup_def using ct
      by (auto intro!: ext v_S2 simple_cfg_on v_nS v_nS12 SUP_cong nn_integral_cong
               simp: PiE_def simple_valid_cfg_iff)
    with ct show ?thesis
      by (auto simp: comp_def)
  qed
qed

lemma p_v_memoryless:
  obtains ct where "ct  PiE S K" "p = vsimple ct"
proof -
  obtain ct where ct_PiE: "ct  PiE S K" and eq: "vsimple ct = F_sup (vsimple ct)"
    by (rule F_v_memoryless)
  then have ct: "ct  Pi S K"
    by (simp add: PiE_def)
  have "p = vsimple ct"
  proof (rule antisym)
    show "p  vsimple ct"
      unfolding p_eq_lfp_F_sup by (rule lfp_lowerbound) (metis order_refl eq)
    show "vsimple ct  p"
    proof (rule le_funI)
      fix s show "(vsimple ct) s  p s"
        using v_le_p[of "simple ct s"]
        by (cases "s  S") (auto simp del: simp add: v_def ct)
    qed
  qed
  with ct_PiE that show thesis by auto
qed

definition "n = (λsS. P_inf s (λω. (HLD S1 suntil HLD S2) (s ## ω)))"

lemma n_eq_INF_v: "s  S  n s = (cfgcfg_on s. v cfg)"
  by (auto simp add: n_def v_def P_inf_def T.emeasure_eq_measure valid_cfgI intro!: INF_cong)

lemma n_le_v: "s  S  cfg  cfg_on s  n s  v cfg"
  by (subst n_eq_INF_v) (blast intro!: INF_lower)+

lemma n_eq_1_imp: "s  S  cfg  cfg_on s  n s = 1  v cfg = 1"
  using n_le_v[of s cfg] v_le_1[of cfg] by (auto intro: antisym valid_cfgI)

lemma n_eq_1_iff: "s  S  n s = 1  (cfgcfg_on s. v cfg = 1)"
  apply rule
  apply (metis n_eq_1_imp)
  apply (auto simp: n_eq_INF_v intro!: INF_eqI)
  done

lemma n_le_1: "s  S  n s  1"
  by (auto simp: n_eq_INF_v intro!: INF_lower2[OF simple_cfg_on[of arb_act]] v_le_1)

lemma n_undefined[simp]: "s  S  n s = undefined"
  by (simp add: n_def)

lemma n_eq_0: "s  S  cfg  cfg_on s  v cfg = 0  n s = 0"
  using n_le_v[of s cfg] by auto

lemma n_not_inf[simp]: "s  S  n s  top"
  using n_le_1[of s] by (auto simp: top_unique)

lemma n_S1: "s  S1  n s = (DK s. + t. n t measure_pmf D)"
  using S1 S1_S2 unfolding n_def
  apply auto
  apply (subst P_inf_iterate)
  apply (auto intro!: nn_integral_cong_AE INF_cong intro: set_pmf_closed
              simp: AE_measure_pmf_iff suntil_Stream set_eq_iff)
  done

lemma n_S2[simp]: "s  S2  n s = 1"
  using S2 by (auto simp add: n_eq_INF_v valid_cfgI)

lemma n_nS12: "s  S  s  S1  s  S2  n s = 0"
  by (auto simp add: n_eq_INF_v valid_cfgI)

lemma n_pos:
  assumes "P s" "s  S1" "wf R"
  assumes cont: "s D. P s  s  S1  D  K s  wD. ((w, s)  R  w  S1  P w)  0 < n w"
  shows "0 < n s"
  using wf R P s sS1
proof (induction s)
  case (less s)
  with S1 have [simp]: "s  S" by auto
  let ?I = "λD::'s pmf. +t. n t D"
  have "0 < Min (?I`K s)"
  proof (safe intro!: Min_gr_iff [THEN iffD2])
    fix D assume [simp]: "D  K s"
    from cont[OF P s s  S1 D  K s]
    obtain w where w: "w  D" "0 < n w"
      by (force intro: less.IH)
    have in_S: "t. t  D  t  S"
      using set_pmf_closed[OF s  S D  K s] by auto
    from w have "0 < pmf D w * n w"
      by (simp add: pmf_positive ennreal_zero_less_mult_iff)
    also have " = (+t. n w * indicator {w} t D)"
      by (subst nn_integral_cmult_indicator)
         (auto simp: ac_simps emeasure_pmf_single in_S w  D)
    also have "  (+t. n t D)"
      by (intro nn_integral_mono_AE) (auto split: split_indicator simp: AE_measure_pmf_iff in_S)
    finally show "0 < (+t. n t D)" .
  qed (insert K_wf K_finite sS, auto)
  also have " = n s"
    unfolding n_S1[OF s  S1]
    using K_wf K_finite sS by (intro Min_Inf) auto
  finally show "0 < n s" .
qed

definition F_inf :: "('s  ennreal)  ('s  ennreal)" where
  "F_inf f = (λsS. if s  S2 then 1 else if s  S1 then (DK s. + t. f t measure_pmf D) else 0)"

lemma F_inf_n: "F_inf n = n"
  by (simp add: F_inf_def n_nS12 n_S1 fun_eq_iff)

lemma F_inf_nS[simp]: "s  S  F_inf f s = undefined"
  by (simp add: F_inf_def)

lemma mono_F_inf: "mono F_inf"
  by (auto intro!: INF_superset_mono nn_integral_mono simp: mono_def F_inf_def le_fun_def)

lemma S1_nS2: "s  S1  s  S2"
  using S1_S2 by auto

lemma n_eq_lfp_F_inf: "n = lfp F_inf"
proof (intro antisym lfp_lowerbound le_funI)
  fix s let ?I = "λD. (+t. lfp F_inf t measure_pmf D)"
  define ct where "ct s = (SOME D. D  K s  (s  S1  lfp F_inf s = ?I D))" for s
  { fix s assume s: "s  S"
    then have "finite (?I ` K s)"
      by (auto intro: K_finite)
    with s obtain D where "D  K s" "(+t. lfp F_inf t D) = Min (?I ` K s)"
      by (auto simp: K_wf dest!: Min_in)
    note this(2)
    also have " = (INF D  K s. ?I D)"
      using s K_wf by (subst Min_Inf) (auto intro: K_finite)
    also have "s  S1   = lfp F_inf s"
      using s S1_S2 by (subst (3) lfp_unfold[OF mono_F_inf]) (auto simp add: F_inf_def)
    finally have "D. D  K s  (s  S1  lfp F_inf s = ?I D)"
      using D  K s by auto
    then have "ct s  K s  (s  S1  lfp F_inf s = ?I (ct s))"
      unfolding ct_def by (rule someI_ex)
    then have "ct s  K s" "s  S1  lfp F_inf s = ?I (ct s)"
      by auto }
  note ct = this
  then have Pi_ct: "ct  Pi S K"
    by auto
  then have valid_ct[simp]: "s. s  S  simple ct s  valid_cfg"
    by simp
  let ?F = "λP. HLD S2 or (HLD S1 aand nxt P)"
  define P where "P s n =
      emeasure (T (simple ct s)) {xspace (T (simple ct s)). (?F ^^ n) (λx. False) (s ## x)}"
    for s n
  { assume "s  S"
    with S1 have [simp, measurable]: "s  S" by auto
    then have "n s  v (simple ct s)"
      by (intro n_le_v) (auto intro: simple_cfg_on[OF Pi_ct])
    also have " = emeasure (T (simple ct s)) {xspace (T (simple ct s)). lfp ?F (s ## x)}"
      using S1_S2
      by (simp add: v_eq[OF simple_valid_cfg[OF Pi_ct sS]])
         (simp add: suntil_lfp space_T[symmetric, of "simple ct s"] del: space_T)
    also have " = (n. P s n)" unfolding P_def
      apply (rule emeasure_lfp2[where P="λM. s. M = T (simple ct s)" and M="T (simple ct s)"])
      apply (intro exI[of _ s] refl)
      apply (auto simp: sup_continuous_def) []
      apply auto []
    proof safe
      fix A s assume "N. s. N = T (simple ct s)  Measurable.pred N A"
      then have "s. Measurable.pred (T (simple ct s)) A"
        by metis
      then have "s. Measurable.pred St A"
        by simp
      then show "Measurable.pred (T (simple ct s)) (λxs. HLD S2 xs  HLD S1 xs  nxt A xs)"
        by simp
    qed
    also have "  lfp F_inf s"
    proof (intro SUP_least)
      fix n from sS show "P s n  lfp F_inf s"
      proof (induct n arbitrary: s)
        case 0 with S1 show ?case
          by (subst lfp_unfold[OF mono_F_inf]) (auto simp: P_def)
      next
        case (Suc n)

        show ?case
        proof cases
          assume "s  S1" with S1_S2 S1 have s[simp]: "s  S2" "s  S" "s  S1" by auto
          have "P s (Suc n) = (+t. P t n ct s)"
            unfolding P_def space_T
            apply (subst emeasure_Collect_T)
            apply (rule measurable_compose[OF measurable_Stream[OF measurable_const measurable_ident_sets[OF refl]]])
            apply (measurable, assumption)
            apply (auto simp: K_cfg_def map_pmf_rep_eq nn_integral_distr
                        intro!: nn_integral_cong_AE AE_pmfI)
            done
          also have "  (+t. lfp F_inf t ct s)"
            using Pi_closed[OF Pi_ct s  S]
            by (auto intro!: nn_integral_mono_AE Suc simp: AE_measure_pmf_iff)
          also have " = lfp F_inf s"
            by (intro ct(2)[symmetric]) auto
          finally show ?thesis .
        next
          assume "s  S1" with S2 s  S show ?case
            using T.emeasure_space_1[of "simple ct s"]
            by (subst lfp_unfold[OF mono_F_inf]) (auto simp: F_inf_def P_def)
        qed
      qed
    qed
    finally have "n s  lfp F_inf s" . }
  moreover have "s  S  n s  lfp F_inf s"
    by (subst lfp_unfold[OF mono_F_inf]) (simp add: n_def F_inf_def)
  ultimately show "n s  lfp F_inf s"
    by blast
qed (simp add: F_inf_n)


lemma real_n: "s  S  ennreal (enn2real (n s)) = n s"
  by (cases "n s") simp_all

lemma real_p: "s  S  ennreal (enn2real (p s)) = p s"
  by (cases "p s") simp_all

lemma p_ub:
  fixes x
  assumes "s  S"
  assumes solution: "s D. s  S1  D  K s  (tS. pmf D t * x t)  x s"
  assumes solution_0: "s. s  S  p s = 0  x s = 0"
  assumes solution_S2: "s. s  S2  x s = 1"
  shows "enn2real (p s)  x s" (is "?y s  _")
proof -
  let ?p = "λs. enn2real (p s)"
  from p_v_memoryless obtain sc where "sc  PiE S K" and p_eq: "p = v  simple sc"
    by auto
  then have sch: "s. s  S  sc s  K s" and sc_Pi: "sc  Pi S K"
    by (auto simp: PiE_iff)

  interpret sc: MC_syntax sc .

  define N where "N = {sS. p s = 0}  S2"
  { fix s assume "s  S" "s  N"
    with p_nS12 have "s  S1"
      by (auto simp add: N_def) }
  note N = this

  have N_S: "N  S"
    using S2 by (auto simp: N_def)

  have finite_sc[intro]: "s  S  finite (sc s)" for s
    using sc  PiE S K by (auto simp: PiE_iff intro: set_pmf_finite)


  show ?thesis
  proof cases
    assume "s  S - N"
    then show ?thesis
    proof (rule mono_les)
      show "(xS - N. set_pmf (sc x))  S - N  N"
        using Pi_closed[OF sc_Pi] by auto
      show "finite ((λs. ?p s - x s) ` (S - N  N))"
        using N_S by (intro finite_imageI finite_subset[OF _ S_finite]) auto
    next
      fix s assume "s  N" then show "?p s  x s"
        by (auto simp: N_def solution_S2 solution_0)
    next
      fix s assume s: "s  S - N"
      then show "integrable (sc s) x" "integrable (sc s) ?p"
        by (auto intro!: integrable_measure_pmf_finite set_pmf_finite sch)

      from s have "s  S1" "s  S"
        using p_nS12[of s] by (auto simp: N_def)
      then show "?p s  ( t. ?p t sc s) + 0"
        unfolding p_eq using real_v_integral_eq[of "simple sc s"]
        by (auto simp add: v_S1 sc_Pi intro!: integral_mono_AE integrable_measure_pmf_finite AE_pmfI)
      show "( t. x t sc s) + 0  x s"
        using solution[OF s  S1 sch[OF s  S]]
        by (subst integral_measure_pmf[where A=S])
           (auto intro: S_finite Pi_closed[OF sc_Pi] s  S simp: ac_simps)

      define X where "X = (SIGMA x:UNIV. sc x)"
      show "tN. (s, t)  X*"
      proof (rule ccontr)
        assume "¬ ?thesis"
        then have *: "tN. (s, t)  X*"
          by auto
        with sS have "v (simple sc s) = 0"
        proof (coinduction arbitrary: s rule: v_eq_0_coinduct)
          case (valid t) with sch show ?case
            by auto
        next
          case (nS2 s) then show ?case
            by (auto simp: N_def)
        next
          case (cont cfg s)
          then have "(s, state cfg)  X*"
            by (auto simp: X_def set_K_cfg)
          with cont show ?case
            by (auto simp: set_K_cfg intro!: exI intro: Pi_closed[OF sc_Pi])
               (blast intro: rtrancl_trans)
        qed
        then have "p s = 0"
          unfolding p_eq by simp
        with sS have "sN"
          by (auto simp: N_def)
        with * show False
          by auto
      qed
    qed
  next
    assume "s  S - N" with s  S show "?p s  x s"
      by (auto simp: N_def solution_0 solution_S2)
  qed
qed

lemma n_lb:
  fixes x
  assumes "s  S"
  assumes solution: "s D. s  S1  D  K s  x s  (tS. pmf D t * x t)"
  assumes solution_n0: "s. s  S  n s = 0  x s = 0"
  assumes solution_S2: "s. s  S2  x s = 1"
  shows "x s  enn2real (n s)" (is "_  ?y s")
proof -
  let ?I = "λD::'s pmf. +x. n x <