Theory Crowds_Protocol

(* Author: Johannes Hölzl <hoelzl@in.tum.de> *)

section ‹Formalization of the Crowds-Protocol›

theory Crowds_Protocol
  imports "../Discrete_Time_Markov_Chain"
begin

lemma cond_prob_nonneg[simp]: "0  cond_prob M A B"
  by (auto simp: cond_prob_def)

lemma (in MC_syntax) emeasure_suntil_geometric:
  assumes [measurable]: "Measurable.pred S P"
  assumes "s  X" and *[simp]: "0  p" "0  r"
  assumes r: "s. s  X  emeasure (T s) {ωspace (T s). P ω} = ennreal r"
  assumes p: "s. s  X  emeasure (K s) X = ennreal p" "p < 1"
  assumes "t. AE ω in T t. ¬ (P  (HLD X  nxt (HLD X suntil P))) ω"
  shows "emeasure (T s) {ωspace (T s). (HLD X suntil P) ω} = r / (1 - p)"
proof (subst emeasure_suntil_disj)
  let ?F = "λF s. emeasure (T s) {ω  space (T s). P ω} + + t. F t * indicator X t K s"
  let ?f = "λx. ennreal r + ennreal p * x"

  have "mono ?F" "mono ?f"
    by (auto intro!: monoI max.mono add_mono nn_integral_mono mult_left_mono mult_right_mono simp: le_fun_def)

  have 1: "lfp ?f  lfp ?F s"
    using s  X
  proof (induction arbitrary: s rule: lfp_ordinal_induct[OF mono ?f])
    case step: (1 x)
    then have "?f x  ?F (λ_. x) s"
      by (auto simp: p r[simplified] nn_integral_cmult mult.commute[of _ x]
               intro!: add_mono mult_right_mono)
    also have "?F (λ_. x)  ?F (lfp ?F)"
      using step
      by (intro le_funI add_mono order_refl nn_integral_mono) (auto simp: split: split_indicator)
    finally show ?case
      by (subst lfp_unfold[OF mono ?F]) (auto simp: le_fun_def)
  qed (auto intro!: Sup_least)
  also have 2: "lfp ?F s  r / (1 - p)"
    using s  X
  proof (induction arbitrary: s rule: lfp_ordinal_induct[OF mono ?F])
    case (1 S)
    with r have "?F S s  ennreal r + (+x. ennreal (r / (1 - p)) * indicator X x K s)"
      by (intro add_mono nn_integral_mono) (auto split: split_indicator)
    also have "  ennreal r + ennreal (r * p / (1 - p))"
      using s  X by (simp add: nn_integral_cmult_indicator p ennreal_mult''[symmetric])
    also have " = ennreal (r / (1 - p))"
      using p < 1 by (simp add: field_simps ennreal_plus[symmetric] del: ennreal_plus)
    finally show ?case .
  qed (auto intro!: SUP_least)
  finally obtain x where x: "lfp ?f = ennreal x" and [simp]: "0  x"
    by (cases "lfp ?f") (auto simp: top_unique)
  from p < 1 have "x. x = r + p * x  x = r / (1 - p)"
    by (auto simp: field_simps)
  with lfp_unfold[OF mono ?f] p < 1 have "lfp ?f = r / (1 - p)"
    unfolding x by (auto simp add: ennreal_plus[symmetric] ennreal_mult[symmetric] simp del: ennreal_plus)
  with 1 2 show "lfp ?F s = ennreal (r / (1 - p))"
    by auto
qed fact+

subsection ‹Definition of the Crowds-Protocol›

datatype 'a state = Start | Init 'a | Mix 'a | End

lemma inj_Mix[simp]: "inj_on Mix A"
  by (auto intro: inj_onI)

lemma inj_Init[simp]: "inj_on Init A"
  by (auto intro: inj_onI)

lemma distinct_state_image[simp]:
  "Start  Mix ` A" "Init j  Mix ` A" "End  Mix ` A" "Mix j  Mix ` A  j  A"
  "Start  Init ` A" "Mix j  Init ` A" "End  Init ` A" "Init j  Init ` A  j  A"
  by auto

lemma Init_cut_Mix[simp]:
  "Init ` H  Mix ` J = {}"
  by auto

abbreviation "Jondo B  Init`B  Mix`B"

locale Crowds_Protocol =
  fixes J :: "'a set" and C :: "'a set" and p_f :: real and p_i :: "'a  real"
  assumes J_not_empty: "J  {}" and finite_J[simp]: "finite J"
  assumes C_smaller: "C  J" and C_non_empty: "C  {}"
  assumes p_f: "0 < p_f" "p_f < 1"
  assumes p_i_nonneg[simp]: "j. j  J  0  p_i j"
  assumes p_i_distr: "(jJ. p_i j) = 1"
  assumes p_i_C: "j. j  C  p_i j = 0"
begin

abbreviation H :: "'a set" where
  "H  J - C"

definition "p_j = 1 / card J"

lemma p_f_nonneg[simp]: "0  p_f" "p_f  1"
  using p_f by simp_all

lemma p_j_nonneg[simp]: "0  p_j"
  by (simp add: p_j_def)

definition "p_H = card H / card J"

lemma p_H_nonneg[simp]: "0  p_H" "p_H  1"
  by (auto simp: p_H_def divide_le_eq_1 card_gt_0_iff intro!: card_mono )

definition next_prob :: "'a state  'a state  real" where
  "next_prob s t = (case (s, t) of (Start, Init j)  if j  H then p_i j else 0
                                 | (Init j, Mix j')  if j'  J then p_j else 0
                                 | (Mix j, Mix j')  if j'  J then p_f * p_j else 0
                                 | (Mix j, End)  1 - p_f
                                 | (End, End)  1
                                 | _  0)"

definition "N s = embed_pmf (next_prob s)"

interpretation MC_syntax N .

abbreviation "𝔓  T Start"

abbreviation "E s  set_pmf (N s)"

lemma finite_C[simp]: "finite C"
  using C_smaller finite_J by (blast intro: finite_subset)

lemma sum_p_i_C[simp]: "sum p_i C = 0"
  by (auto intro: sum.neutral p_i_C)

lemma sum_p_i_H[simp]: "sum p_i H = 1"
  using C_smaller by (simp add: sum_diff p_i_distr)

lemma possible_jondo:
  obtains j where "j  J" "j  C" "p_i j  0"
proof (atomize_elim, rule ccontr)
  assume "¬ (j. j  J  j  C  p_i j  0)"
  with p_i_C have "jJ. p_i j = 0"
    by auto
  with p_i_distr show False
    by simp
qed

lemma C_le_J[simp]: "card C < card J"
  using C_smaller
  by (intro psubset_card_mono) auto

lemma p_H: "0 < p_H" "p_H < 1"
  using J_not_empty C_smaller C_non_empty
  by (simp_all add: p_H_def card_Diff_subset card_mono field_simps zero_less_divide_iff card_gt_0_iff)

lemma p_H_p_f_pos: "0 < p_H * p_f"
  using p_f p_H by (simp add: zero_less_mult_iff)

lemma p_H_p_f_less_1: "p_H * p_f < 1"
proof -
  have "p_H * p_f < 1 * 1"
    using p_H p_f by (intro mult_strict_mono) auto
  then show "p_H * p_f < 1" by simp
qed

lemma p_j_pos: "0 < p_j"
  unfolding p_j_def using J_not_empty by auto

lemma H_compl: "1 - p_H = real (card C) / real (card J)"
  using C_non_empty J_not_empty C_smaller
  by (simp add: p_H_def card_Diff_subset card_mono of_nat_diff divide_eq_eq field_simps)

lemma H_compl2: "1 - p_H = card C * p_j"
  unfolding H_compl p_j_def by simp

lemma H_eq2: "card H * p_j = p_H"
  unfolding p_j_def p_H_def by simp

lemma pmf_next_pmf[simp]: "pmf (N s) t = next_prob s t"
  unfolding N_def
proof (rule pmf_embed_pmf)
  show "x. 0  next_prob s x"
    using p_j_pos p_f by (auto simp: next_prob_def intro: p_i_nonneg split: state.split)
  show "(+ x. ennreal (next_prob s x) count_space UNIV) = 1"
    using p_f J_not_empty
    by (subst nn_integral_count_space'[where A="Init`H  Mix`J  {End}"])
       (auto simp: next_prob_def sum.reindex sum.union_disjoint p_i_distr p_j_def
             split: state.split)
qed

lemma next_prob_Start[simp]: "next_prob Start (Init j) = (if j  H then p_i j else 0)"
  by (auto simp: next_prob_def)

lemma next_prob_to_Init[simp]: "j  H  next_prob s (Init j) =
    (case s of Start  p_i j | _  0)"
  by (cases s) (auto simp: next_prob_def)

lemma next_prob_to_Mix[simp]: "j  J  next_prob s (Mix j) =
    (case s of Init j  p_j | Mix j  p_f * p_j | _  0)"
  by (cases s) (auto simp: next_prob_def)

lemma next_prob_to_End[simp]: "next_prob s End =
    (case s of Mix j  1 - p_f | End  1 | _  0)"
  by (cases s) (auto simp: next_prob_def)

lemma next_prob_from_End[simp]: "next_prob End s = 0  s  End"
  by (cases s) (auto simp: next_prob_def)

lemma next_prob_Mix_MixI: "j. s = Mix j  jJ. s' = Mix j  next_prob s s' = p_f * p_j"
  by (cases s) auto


lemma E_Start: "E Start = {Init j | j. j  H  p_i j  0 }"
  using p_i_C by (auto simp: set_pmf_iff next_prob_def split: state.splits if_split_asm)

lemma E_Init: "E (Init j) = {Mix j | j. j  J }"
  using p_j_pos C_smaller by (auto simp: set_pmf_iff next_prob_def split: state.splits if_split_asm)

lemma E_Mix: "E (Mix j) = {Mix j | j. j  J }  {End}"
  using p_j_pos p_f by (auto simp: set_pmf_iff next_prob_def split: state.splits if_split_asm)

lemma E_End: "E End = {End}"
  by (auto simp: set_pmf_iff next_prob_def split: state.splits if_split_asm)

lemma enabled_End:
  "enabled End ω  ω = sconst End"
proof safe
  assume "enabled End ω" then show "ω = sconst End"
  proof (coinduction arbitrary: ω)
    case Eq_stream then show ?case
      by (auto simp: enabled.simps[of _ ω] E_End)
  qed
next
  show "enabled End (sconst End)"
    by coinduction (simp add: E_End)
qed

lemma AE_End: "(AE ω in T End. P ω)  P (sconst End)"
proof -
  have "(AE ω in T End. P ω)  (AE ω in T End. P ω  ω = sconst End)"
    using AE_T_enabled[of End] by (simp add: enabled_End)
  also have " = (AE ω in T End. P (sconst End)  ω = sconst End)"
    by (simp add: enabled_End del: AE_conj_iff cong: rev_conj_cong)
  also have " = (AE ω in T End. P (sconst End))"
    using AE_T_enabled[of End] by (simp add: enabled_End)
  finally show ?thesis
    by simp
qed

lemma emeasure_Init_eq_Mix:
  assumes [measurable]: "Measurable.pred S P"
  assumes AE_End: "AE x in T End. ¬ P (End ## x)"
  shows "emeasure (T (Init j)) {xspace (T (Init j)). P x} =
    emeasure (T (Mix j)) {xspace (T (Mix j)). P x} / p_f"
proof -
  have *: "{Mix j | j. j  J } = Mix ` J"
    by auto
  show ?thesis
    using emeasure_eq_0_AE[OF AE_End] p_f
    apply (subst (1 2) emeasure_Collect_T)
    apply simp
    apply (subst (1 2) nn_integral_measure_pmf_finite)
    apply (auto simp: E_Mix E_Init * sum.reindex sum_distrib_right[symmetric] divide_ennreal
      ennreal_times_divide[symmetric])
    done
qed

text ‹

What is the probability that the server sees a specific jondo (including the initiator) as sender.

›

definition visit :: "'a set  'a set  'a state stream  bool" where
  "visit I L = Init`(I  H)  (HLD (Mix`J) suntil (Mix`(L  J)  HLD {End}))"

lemma visit_unique1:
  "visit I1 L1 ω  visit I2 L2 ω  I1  I2  {}"
  by (auto simp: visit_def HLD_iff)

lemma visit_unique2:
  assumes "visit I1 L1 ω" "visit I2 L2 ω"
  shows "L1  L2  {}"
proof -
  let ?U = "λL ω. (HLD (Mix`J) suntil ((Mix`(LJ))  HLD {End})) ω"
  have "?U L1 (stl ω)" "?U L2 (stl ω)"
    using assms by (auto simp: visit_def)
  then show "L1  L2  {}"
  proof (induction "stl ω" arbitrary: ω rule: suntil_induct_strong)
    case base then show ?case
      by (auto simp add: suntil.simps[of _ _ "stl (stl ω)"] suntil.simps[of _ _ "stl ω"] HLD_iff)
  next
    case step
    show ?case
    proof cases
      assume "((Mix`(L2J))  HLD {End}) (stl ω)"
      with step.hyps show ?thesis
        by (auto simp: inj_Mix HLD_iff elim: suntil.cases)
    next
      assume "¬ ((Mix`(L2J))  HLD {End}) (stl ω)"
      with step.prems have "?U L2 (stl (stl ω))"
        by (auto elim: suntil.cases)
      then show ?thesis
        by (rule step.hyps(4)[OF refl])
    qed
  qed
qed

lemma visit_imp_in_H: "visit {i} J ω  i  H"
  by (auto simp: visit_def HLD_iff)

lemma emeasure_visit:
  assumes I: "I  H" and L: "L  J"
  shows "emeasure 𝔓 {ωspace 𝔓. visit I L ω} = (iI. p_i i) * (card L * p_j)"
proof -
  let ?J = "HLD (Mix`J)" and ?E = "(Mix`L)  HLD {End}"
  let  = "?J aand not ?E"
  let ?P = "λx P. emeasure (T x) {ωspace (T x). P ω}"

  have [intro]: "finite L"
    using finite_J L  J by (blast intro: finite_subset)
  have [simp, intro]: "finite I"
    using finite_J I  H by (blast intro: finite_subset)

  { fix j assume j: "j  H"
    have "?P (Mix j) (?J suntil ?E) = (p_f * p_j * (1 - p_f) * card L) / (1 - p_f)"
    proof (rule emeasure_suntil_geometric)
      fix s assume s: "s  Mix ` J"
      then have "?P s ?E = (+x. ennreal (1 - p_f) * indicator (Mix`L) x N s)"
        by (auto simp add: emeasure_HLD_nxt emeasure_HLD AE_measure_pmf_iff emeasure_pmf_single
                 split: state.split split_indicator simp del: space_T nxt.simps
                 intro!: nn_integral_cong_AE)
      also have " = ennreal (1 - p_f) * emeasure (N s) (Mix`L)"
        using p_f by (intro nn_integral_cmult_indicator) auto
      also have " = ennreal ((1 - p_f) * card L * p_j * p_f)"
        using s assms
        by (subst emeasure_measure_pmf_finite)
           (auto simp: sum.reindex subset_eq ennreal_mult mult_ac)
      finally show "?P s ?E = p_f * p_j * (1 - p_f) * card L"
        by simp
    next
      show "t. AE ω in T  t. ¬ (?E  (?J  nxt (?J suntil ?E))) ω"
        by (intro AE_I2) (auto simp: HLD_iff elim: suntil.cases)
    qed (insert p_f j, auto simp: emeasure_measure_pmf_finite sum.reindex p_j_def)
    then have "?P (Init j) (?J suntil ?E) = (p_f * p_j * (1 - p_f) * card L) / (1 - p_f) / p_f"
      by (subst emeasure_Init_eq_Mix) (simp_all add:  suntil.simps[of _ _ "x ## s" for x s] divide_ennreal p_f)
    then have "?P (Init j) (?J suntil ?E) = p_j * card L"
      using p_f by simp }
  note J_suntil_E = this

  have "?P Start (visit I L) = (+x. ?P x (?J suntil ?E) * indicator (Init`I) x N Start)"
    unfolding visit_def using I L by (subst emeasure_HLD_nxt) (auto simp: Int_absorb2)
  also have " = (+x. ennreal (p_j * card L) * indicator (Init`I) x N Start)"
    using I J_suntil_E
    by (intro nn_integral_cong ennreal_mult_right_cong)
       (auto split: split_indicator_asm)
  also have " = ennreal ((iI. p_i i) * card L * p_j)"
    using p_j_pos assms
    by (subst nn_integral_cmult_indicator)
       (auto simp: emeasure_measure_pmf_finite sum.reindex subset_eq ennreal_mult[symmetric] sum_nonneg)
  finally show ?thesis by (simp add: ac_simps)
qed

lemma measurable_visit[measurable]: "Measurable.pred S (visit I L)"
  by (simp add: visit_def)

lemma AE_visit: "AE ω in 𝔓. visit H J ω"
proof (rule T.AE_I_eq_1)
  show "emeasure 𝔓 {ωspace 𝔓. visit H J ω} = 1"
    using J_not_empty by (subst emeasure_visit ) (simp_all add: p_j_def)
qed simp

subsection ‹Server gets no information›

lemma server_view1: "j  J  𝒫(ω in 𝔓. visit H {j} ω) = p_j"
  unfolding measure_def by (subst emeasure_visit) simp_all

lemma server_view_indep:
  "L  J  I  H  𝒫(ω in 𝔓. visit I L ω) = 𝒫(ω in 𝔓. visit H L ω) * 𝒫(ω in 𝔓. visit I J ω)"
  unfolding measure_def
  by (subst (1 2 3) emeasure_visit) (auto simp: p_j_def sum_nonneg subset_eq)

lemma server_view: "𝒫(ω in 𝔓. jH. visit {j} {j} ω) = p_j"
  using finite_J
proof (subst T.prob_sum[where I="H" and P="λj. visit {j} {j}"])
  show "(jH. 𝒫(ω in 𝔓. visit {j} {j} ω)) = p_j"
    by (auto simp: measure_def emeasure_visit sum_distrib_right[symmetric] simp del: space_T sets_T)
  show "AE x in 𝔓. (nH. visit {n} {n} x  (jH. visit {j} {j} x)) 
                ((jH. visit {j} {j} x)  (∃!n. n  H  visit {n} {n} x))"
    by (auto dest: visit_unique1)
qed simp_all

subsection ‹Probability that collaborators gain information›

definition "hit_C = Init`H  ev (HLD (Mix`C))"
definition "before_C B = (HLD (Jondo H)) suntil ((Jondo (B  H))  HLD (Mix ` C))"

lemma measurable_hit_C[measurable]: "Measurable.pred S hit_C"
  by (simp add: hit_C_def)

lemma measurable_before_C[measurable]: "Measurable.pred S (before_C B)"
  by (simp add: before_C_def)

lemma before_C:
  assumes ω: "enabled Start ω"
  shows "before_C B ω 
    ((Init`H  (HLD (Mix`H) suntil (Mix`(B  H)  HLD (Mix`C)))) or (Init`(B  H)  HLD (Mix`C))) ω"
proof -
  { fix ω s assume "((HLD (Jondo H)) suntil (Jondo (B  H)  HLD (Mix ` C))) ω"
      "enabled s ω" "s  Jondo H"
    then have "(HLD (Mix ` H) suntil (Mix ` (B  H)  (HLD (Mix ` C)))) ω"
    proof (induction arbitrary: s)
      case (base ω) then show ?case
        by (auto simp: HLD_iff enabled.simps[of _ ω] E_Init E_Mix intro!: suntil.intros(1))
    next
      case (step ω) from step.prems step.hyps step.IH[of "shd ω"] show ?case
        by (auto simp: HLD_iff enabled.simps[of _ ω] E_Init E_Mix
                       suntil.simps[of _ _ ω] enabled_End suntil_sconst)
    qed }
  note this[of "stl ω" "shd ω"]
  moreover
  { fix ω s assume "(HLD (Mix ` H) suntil (Mix ` (B  H)  (HLD (Mix ` C)))) ω"
      "enabled s ω" "s  Jondo H"
    then have "((HLD (Jondo H)) suntil ((Jondo (B  H))  HLD (Mix ` C))) ω"
    proof (induction arbitrary: s)
      case (step ω) from step.prems step.hyps step.IH[of "shd ω"] show ?case
        by (auto simp: HLD_iff enabled.simps[of _ ω] E_Init E_Mix
                       suntil.simps[of _ _ ω] enabled_End suntil_sconst)
    qed (auto intro: suntil.intros simp: HLD_iff) }
  note this[of "stl ω" "shd ω"]
  ultimately show ?thesis
    using assms
    using enabled Start ω
    unfolding before_C_def suntil.simps[of _ _ ω] enabled.simps[of _ ω]
    by (auto simp: E_Start HLD_iff)
qed

lemma before_C_unique:
  assumes ω: "before_C I1 ω" "before_C I2 ω" shows "I1  I2  {}"
  using ω unfolding before_C_def
proof induction
  case (base ω) then show ?case
    by (auto simp add: suntil.simps[of _ _ ω] suntil.simps[of _ _ "stl ω"] HLD_iff)
next
  case (step ω) then show ?case
    by (auto simp add: suntil.simps[of _ _ ω] suntil.simps[of _ _ "stl ω"] HLD_iff)
qed

lemma hit_C_imp_before_C:
  assumes "enabled Start ω" "hit_C ω" shows "before_C H ω"
proof -
  let ?X = "Init`H  Mix`H"
  { fix ω s assume "ev (HLD (Mix`C)) ω" "s?X" "enabled s ω"
    then have "((HLD (Jondo H)) suntil (?X  HLD (Mix ` C))) (s ## ω)"
    proof (induction arbitrary: s rule: ev_induct_strong)
      case (step ω s) from step.IH[of "shd ω"] step.prems step.hyps show ?case
        by (auto simp: enabled.simps[of _ ω] suntil_Stream E_Init E_Mix HLD_iff
          enabled_End ev_sconst)
    qed (auto simp: suntil_Stream) }
  from this[of "stl ω" "shd ω"] assms show ?thesis
    by (auto simp: before_C_def hit_C_def enabled.simps[of _ ω] E_Start)
qed

lemma before_C_single:
  assumes "before_C I ω" shows "iI  H. before_C {i} ω"
  using assms unfolding before_C_def by induction (auto simp: HLD_iff intro: suntil.intros)

lemma before_C_imp_in_H: "before_C {i} ω  i  H"
  by (auto dest: before_C_single)

subsection ‹The probability that the sender hits a collaborator›

lemma Pr_hit_C: "𝒫(ω in 𝔓. hit_C ω) = (1 - p_H) / (1 - p_H * p_f)"
proof -
  let ?P = "λx P. emeasure (T x) {ωspace (T x). P ω}"
  let ?M = "HLD (Mix ` C)" and ?I = "Init`H" and ?J = "Mix`H"
  let  = "(HLD ?J) aand not ?M"

  { fix s assume s: "s  Jondo J"
    have "AE ω in T s. ev ?M ω  (HLD ?J suntil ?M) ω"
      using AE_T_enabled
    proof eventually_elim
      fix ω assume ω: "enabled s ω"
      show "ev ?M ω  (HLD ?J suntil ?M) ω"
      proof
        assume "ev ?M ω"
        from this ω s show "(HLD ?J suntil ?M) ω"
        proof (induct arbitrary: s rule: ev_induct_strong)
          case (step ω) then show ?case
            by (auto simp: HLD_iff enabled.simps[of _ ω] suntil.simps[of _ _ ω] E_End E_Init E_Mix
                           enabled_End ev_sconst)
        qed (auto simp: HLD_iff E_Init intro: suntil.intros)
      qed (rule ev_suntil)
    qed }
  note ev_eq_suntil = this

  have "?P Start hit_C = (+x. ?P x (ev ?M) * indicator ?I x N Start)"
    unfolding hit_C_def by (rule emeasure_HLD_nxt) measurable
  also have " = (+x. ennreal ((1 - p_H) / (1 - p_f * p_H)) * indicator ?I x N Start)"
  proof (intro nn_integral_cong ennreal_mult_right_cong refl)
    fix x assume "indicator (Init ` H) x  0"
    then have "x  ?I"
      by (auto split: split_indicator_asm)
    { fix j assume j: "j  H"
      with ev_eq_suntil[of "Mix j"] have "?P (Mix j) (ev ?M) = ?P (Mix j) ((HLD ?J) suntil ?M)"
        by (intro emeasure_eq_AE) auto
      also have " = (((1 - p_H) * p_f)) / (1 - p_H * p_f)"
      proof (rule emeasure_suntil_geometric)
        fix s assume s: "s  Mix ` H"
        from s C_smaller show "?P s ?M = ennreal ((1 - p_H) * p_f)"
          by (subst emeasure_HLD)
             (auto simp add: emeasure_measure_pmf_finite sum.reindex subset_eq p_j_def H_compl)
        from s show "emeasure (N s) (Mix`H) = p_H * p_f"
          by (auto simp: emeasure_measure_pmf_finite sum.reindex p_H_def p_j_def)
      qed (insert j, auto simp: HLD_iff p_H_p_f_less_1)
      finally have "?P (Init j) (ev ?M) = (1 - p_H) / (1 - p_H * p_f)"
        using p_f
        by (subst emeasure_Init_eq_Mix)
           (auto simp: ev_Stream AE_End ev_sconst HLD_iff mult_le_one divide_ennreal) }
    then show "?P x (ev ?M) = (1 - p_H) / (1 - p_f * p_H)"
      using x  ?I by (auto simp: mult_ac)
  qed
  also have " = ennreal ((1 - p_H) / (1 - p_H * p_f))"
    using p_j_pos p_H p_H_p_f_less_1
    by (subst nn_integral_cmult_indicator)
       (auto simp: emeasure_measure_pmf_finite sum.reindex subset_eq mult_ac
             intro!: divide_nonneg_nonneg)
  finally show ?thesis
    by (simp add: measure_def mult_le_one)
qed

lemma before_C_imp_hit_C:
  assumes "enabled Start ω" "before_C B ω"
  shows "hit_C ω"
proof -
  { fix ω j assume "((HLD (Jondo H)) suntil (Jondo (B  H)  HLD (Mix ` C))) ω"
      "j  H" "enabled (Mix j) ω"
    then have "ev (HLD (Mix`C)) ω"
    proof (induction arbitrary: j rule: suntil_induct_strong)
      case (step ω) then show ?case
        by (auto simp: enabled.simps[of _ ω] E_Mix enabled_End ev_sconst suntil_sconst HLD_iff)
    qed auto }
  from this[of "stl (stl ω)"] assms show "hit_C ω"
    by (force simp: before_C_def hit_C_def E_Start HLD_iff E_Init
      enabled.simps[of _ ω] ev.simps[of _ ω] suntil.simps[of _ _ ω]
      enabled.simps[of _ "stl ω"] ev.simps[of _ "stl ω"] suntil.simps[of _ _ "stl ω"])
qed

lemma negE: "¬ P  P  False"
  by blast

lemma Pr_visit_before_C:
  assumes L: "L  H" and I: "I  H"
  shows "𝒫(ω in 𝔓. visit I J ω  before_C L ω ¦ hit_C ω ) =
    (iI. p_i i) * card L * p_j * p_f + (iI  L. p_i i) * (1 - p_H * p_f)"
proof -
  let ?M = "Mix`H"
  let ?P = "λx P. emeasure (T x) {ωspace (T x). P ω}"
  let ?V = "(visit I J aand before_C L) aand hit_C"
  let ?U = "HLD ?M suntil (Mix`L  HLD (Mix`C))"
  let ?L = "HLD (Mix`C)"

  have IJ: "x  I  x  J" for x
    using I by auto

  have [simp, intro]: "finite I" "finite L"
    using L I by (auto dest: finite_subset)

  have "?P Start ?V = ?P Start ((Init`I  ?U) or (Init`(I  L)  ?L))"
  proof (rule emeasure_Collect_eq_AE)
    show "AE ω in 𝔓. ?V ω  ((Init`I  ?U) or (Init`(I  L)  ?L)) ω"
      using AE_T_enabled AE_visit
    proof eventually_elim
      case (elim ω)
      then show ?case
        using before_C_imp_hit_C[of ω "L"]  before_C[of ω "L"] I L
        by (auto simp: visit_def HLD_iff Int_absorb2)
    qed
    show "Measurable.pred 𝔓 ((Init`I  ?U) or (Init`(I  L)  ?L))"
      by measurable
  qed measurable
  also have " = ?P Start (Init`I  ?U) + ?P Start (Init`(I  L)  ?L)"
    using L I
    apply (subst plus_emeasure)
    apply (auto intro!: arg_cong2[where f=emeasure])
    apply (subst (asm) suntil.simps)
    apply (auto simp add: HLD_iff[abs_def] elim: suntil.cases)
    done
  also have "?P Start (Init`(I  L)  ?L) = (iIL. p_i i * (1 - p_H))"
    using L I C_smaller p_j_pos
    apply (subst emeasure_HLD_nxt emeasure_HLD, simp)+
    apply (subst nn_integral_indicator_finite)
    apply (auto simp: emeasure_measure_pmf_finite sum.reindex next_prob_def sum.If_cases
                      Int_absorb2 H_compl2 ennreal_mult[symmetric] sum_nonneg
                      sum_distrib_left[symmetric] sum_distrib_right[symmetric]
                intro!: sum.cong sum_nonneg)
    apply (subst (asm) ennreal_inj)
    apply (auto intro!: mult_nonneg_nonneg sum_nonneg sum.mono_neutral_left elim!: negE)
    done
  also have "?P Start (Init`I  ?U) = (iI. ?P (Init i) ?U * p_i i)"
    using I
    by (subst emeasure_HLD_nxt, simp)
       (auto simp: nn_integral_indicator_finite sum.reindex emeasure_measure_pmf_finite
             intro!: sum.cong[OF refl])
  also have " = (iI. ennreal (p_f * (1 - p_H) * p_j * card L / (1 - p_H * p_f)) * p_i i)"
  proof (intro sum.cong refl arg_cong2[where f="(*)"])
    fix i assume "i  I"
    with I have i: "i  H"
      by auto
    have "?P (Mix i) ?U = (p_f * p_f * (1 - p_H) * p_j * card L / (1 - p_H * p_f))"
      unfolding before_C_def
    proof (rule emeasure_suntil_geometric[where X="?M"])
      show "Mix i  ?M"
        using i by auto
    next
      fix s assume "s  ?M"
      with p_f p_j_pos L C_smaller[THEN less_imp_le]
      show "?P s (Mix`L  (HLD (Mix ` C))) = ennreal (p_f * p_f * (1 - p_H) * p_j * card L)"
        apply (simp add: emeasure_HLD emeasure_HLD_nxt del: nxt.simps space_T)
        apply (subst nn_integral_measure_pmf_support[of "Mix`L"])
        apply (auto simp add: subset_eq emeasure_measure_pmf_finite sum.reindex H_compl p_j_def
          ennreal_mult[symmetric] ennreal_of_nat_eq_real_of_nat)
        done
    next
      fix s assume "s  ?M" then show "emeasure (N s) ?M = ennreal (p_H * p_f)"
        by (auto simp add: emeasure_measure_pmf_finite sum.reindex H_eq2)
    next
      show "AE ω in T t. ¬ ((Mix ` L  ?L)  (HLD (Mix ` H)  nxt ?U)) ω" for t
        using L
        apply (simp add: AE_T_iff[of _ t])
        apply (subst AE_T_iff; simp)
        apply (auto simp: HLD_iff suntil_Stream)
        done
    qed (insert L, auto simp: p_H_p_f_less_1 E_Mix)
    then show "?P (Init i) ?U = p_f * (1 - p_H) * p_j * card L / (1 - p_H * p_f)"
      by (subst emeasure_Init_eq_Mix)
         (auto simp: AE_End suntil_Stream divide_ennreal mult_le_one p_f)
  qed
  finally have *: "𝒫(ω in T Start. ?V ω) =
      (p_f * (1 - p_H) * p_j * (card L) / (1 - p_H * p_f)) * (iI. p_i i) +
      (iI  L. p_i i) * (1 - p_H)"
    using sum_nonneg [of "I  L" p_i]  sum_nonneg [of "I" p_i]
    by (simp add: mult_ac measure_def sum_distrib_right[symmetric] sum_distrib_left[symmetric]
                  sum_divide_distrib[symmetric] IJ ennreal_mult[symmetric] 
                  mult_le_one ennreal_plus[symmetric]
             del: ennreal_plus)
  show ?thesis
    unfolding cond_prob_def Pr_hit_C *
    using *
    using p_f p_H p_j_pos p_H_p_f_less_1 by (simp add: divide_simps) (simp add: field_simps)
qed

lemma Pr_visit_eq_before_C:
  "𝒫(ω in 𝔓. jH. visit {j} J ω  before_C {j} ω ¦ hit_C ω ) = 1 - (p_H - p_j) * p_f"
proof -
  let ?V = "λj. visit {j} J aand before_C {j}" and ?H = "hit_C"
  let ?J = "H"
  have "𝒫(ω in 𝔓. (j?J. ?V j ω)  ?H ω) = (j?J. 𝒫(ω in 𝔓. (?V j aand ?H) ω))"
  proof (rule T.prob_sum)
    show "AE ω in 𝔓. (j?J. (?V j aand ?H) ω  ((j?J. ?V j ω)  ?H ω)) 
      (((j?J. ?V j ω)  ?H ω)  (∃!j. j?J  (?V j aand ?H) ω))"
      by (auto intro!: AE_I2 dest: visit_unique1)
  qed auto
  then have "𝒫(ω in 𝔓. (j?J. ?V j ω) ¦ ?H ω) = (j?J. 𝒫(ω in 𝔓. ?V j ω ¦ ?H ω))"
    by (simp add: cond_prob_def sum_divide_distrib)
  also have " = p_j * p_f + (1 - p_H * p_f)"
    by (simp add: Pr_visit_before_C sum_distrib_right[symmetric] sum.distrib)
  finally show ?thesis
    by (simp add: field_simps)
qed

lemma probably_innocent:
  assumes approx: "1 / (2 * (p_H - p_j))  p_f" and "p_H  p_j"
  shows "𝒫(ω in 𝔓. jH. visit {j} J ω  before_C {j} ω ¦ hit_C ω )  1 / 2"
  unfolding Pr_visit_eq_before_C
proof -
  have [simp]: "n :: nat. 1  real n  1  n" by auto
  have "0  p_j" unfolding p_j_def by auto
  then have "1 * p_j  p_H"
    unfolding H_eq2[symmetric] using C_smaller
    by (intro mult_mono) (auto simp: Suc_le_eq card_Diff_subset not_le)
  with p_H  p_j have "p_j < p_H" by auto
  with approx show "1 - (p_H - p_j) * p_f  1 / 2"
    by (auto simp add: field_simps divide_le_eq split: if_split_asm)
qed

lemma Pr_before_C:
  assumes L: "L  H"
  shows "𝒫(ω in 𝔓. before_C L ω ¦ hit_C ω ) =
    card L * p_j * p_f + (lL. p_i l) * (1 - p_H * p_f)"
proof -
  have "𝒫(ω in 𝔓. before_C L ω ¦ hit_C ω ) =
    𝒫(ω in 𝔓. visit H J ω  before_C L ω ¦ hit_C ω )"
    using AE_visit by (auto intro!: T.cond_prob_eq_AE)
  also have " = card L * p_j * p_f + (iL. p_i i) * (1 - p_H * p_f)"
    using L by (subst Pr_visit_before_C[OF L order_refl]) (auto simp: Int_absorb1)
  finally show ?thesis .
qed

lemma P_visit:
  assumes I: "I  H"
  shows "𝒫(ω in 𝔓. visit I J ω ¦ hit_C ω ) = (iI. p_i i)"
proof -
  have "𝒫(ω in 𝔓. visit I J ω ¦ hit_C ω ) =
    𝒫(ω in 𝔓. visit I J ω  before_C H ω ¦ hit_C ω )"
  proof (rule T.cond_prob_eq_AE)
    show "AE x in 𝔓. hit_C x 
                visit I J x = (visit I J x  before_C H x)"
      using AE_T_enabled by eventually_elim (auto intro: hit_C_imp_before_C)
  qed auto
  also have " = sum p_i I"
    using I by (subst Pr_visit_before_C[OF order_refl]) (auto simp: Int_absorb2 field_simps p_H_def p_j_def)
  finally show ?thesis .
qed

subsection ‹Probability space of hitting a collaborator›

definition "hC = uniform_measure 𝔓 {ωspace 𝔓. hit_C ω}"

lemma emeasure_hit_C_not_0: "emeasure 𝔓 {ω  space 𝔓. hit_C ω}  0"
  using p_H p_H_p_f_less_1 unfolding Pr_hit_C T.emeasure_eq_measure by auto

lemma measurable_hC[measurable (raw)]:
  "A  sets S  A  sets hC"
  "f  measurable M S  f  measurable M hC"
  "g  measurable S M  g  measurable hC M"
  "A  space S  sets S  A  space hC  sets S"
  unfolding hC_def uniform_measure_def
  by simp_all

lemma vimage_Int_space_C[simp]:
  "f -` {x}  space hC = {ωspace S. f ω = x}"
  by (auto simp: hC_def)

sublocale hC: information_space hC 2
proof -
  interpret hC: prob_space hC
    unfolding hC_def
    using emeasure_hit_C_not_0
    by (intro prob_space_uniform_measure) auto
  show "information_space hC 2"
    by standard simp
qed

abbreviation
  mutual_information_Pow_CP ("ℐ'(_ ; _')") where
  "ℐ(X ; Y)  hC.mutual_information 2 (count_space (X`space hC)) (count_space (Y`space hC)) X Y"

lemma simple_functionI:
  assumes "finite (range f)"
  assumes [measurable]: "x. {ωspace S. f ω = x}  sets S"
  shows "simple_function hC f"
  using assms unfolding simple_function_def hC_def
  by (simp add: vimage_def space_stream_space)

subsection ‹Estimate the information to the collaborators›

lemma measure_hC[simp]:
  assumes A[measurable]: "A  sets S"
  shows "measure hC A = 𝒫(ω in 𝔓. ω  A ¦ hit_C ω )"
  unfolding hC_def cond_prob_def
  using emeasure_hit_C_not_0 A
  by (subst measure_uniform_measure) (simp_all add: T.emeasure_eq_measure Int_def conj_ac)

subsubsection ‹Setup random variables for mutual information›

definition "first_J ω = (THE i. visit {i} J ω)"

lemma first_J_eq:
  "visit {i} J ω  first_J ω = i"
  unfolding first_J_def by (intro the_equality) (auto dest: visit_unique1)

lemma AE_first_J:
  "AE ω in 𝔓. visit {i} J ω  first_J ω = i"
  using AE_visit
proof eventually_elim
  fix ω assume "visit H J ω"
  then obtain j where "visit {j} J ω" "j  H"
    by (auto simp: visit_def HLD_iff)
  then show "visit {i} J ω  first_J ω = i"
    by (auto dest: visit_unique1 first_J_eq)
qed

lemma measurbale_first_J[measurable]: "first_J  measurable S (count_space UNIV)"
  unfolding first_J_def[abs_def]
  by (intro measurable_THE[where I=H])
     (auto dest: visit_imp_in_H visit_unique1 intro: countable_finite)

definition "last_H ω = (THE i. before_C {i} ω)"

lemma measurbale_last_H[measurable]: "last_H  measurable S (count_space UNIV)"
  unfolding last_H_def[abs_def]
  by (intro measurable_THE[where I=H])
     (auto dest: before_C_single before_C_unique intro: countable_finite)

lemma last_H_eq:
  "before_C {i} ω  last_H ω = i"
  unfolding last_H_def by (intro the_equality) (auto dest: before_C_unique)

lemma last_H:
  assumes "enabled Start ω" "hit_C ω"
  shows "before_C {last_H ω} ω" "last_H ω  H"
  by (metis before_C_single hit_C_imp_before_C last_H_eq Int_iff assms)+

lemma AE_last_H:
  "AE ω in 𝔓. hit_C ω  before_C {i} ω  last_H ω = i"
  using AE_T_enabled
proof eventually_elim
  fix ω assume "enabled Start ω" then show "hit_C ω  before_C {i} ω = (last_H ω = i)"
    by (auto dest: last_H last_H_eq)
qed

lemma information_flow:
  defines "h  real (card H)"
  assumes init_uniform: "i. i  H  p_i i = 1 / h"
  shows "ℐ(first_J ; last_H)  (1 - (h - 1) * p_j * p_f) * log 2 h"
proof -
  let ?il = "λi l. 𝒫(ω in 𝔓. visit {i} J ω  before_C {l} ω ¦ hit_C ω )"
  let ?i = "λi. 𝒫(ω in 𝔓. visit {i} J ω ¦ hit_C ω )"
  let ?l = "λl. 𝒫(ω in 𝔓. before_C {l} ω ¦ hit_C ω )"

  from init_uniform have init_H: "i. i  H  p_i i = p_j / p_H"
    by (simp add: p_j_def p_H_def h_def)

  from h_def have "1/h = p_j/p_H" "h = p_H / p_j" "p_H = h * p_j"
    by (auto simp: p_H_def p_j_def field_simps)
  from C_smaller have h_pos: "0 < h"
    by (auto simp add: card_gt_0_iff h_def)

  let ?s = "(h - 1) * p_j"
  let ?f = "?s * p_f"

  from psubset_card_mono[OF _ C_smaller]
  have "1  card J - card C"
    by (simp del: C_le_J)
  then have "1  h"
    using C_smaller
    by (simp add: h_def card_Diff_subset card_mono field_simps del: C_le_J)

  have log_le_0: "?f * log 2 (p_H * p_f)  ?f * log 2 1"
    using p_H_p_f_less_1 p_H_p_f_pos p_j_pos p_f 1  h
    by (intro mult_left_mono log_mono mult_nonneg_nonneg) auto

  have "(h - 1) * p_j < 1"
    using 1  h C_smaller
    by (auto simp: h_def p_j_def divide_less_eq card_Diff_subset card_mono)
  then have 1: "(h - 1) * p_j * p_f < 1 * 1"
    using p_f by (intro mult_strict_mono) auto

  { fix ω have "first_J ω  H  first_J ω = (THE x. False)"
      apply (cases "i. ¬ visit {i} J ω")
      apply (simp add: first_J_def)
      apply (auto dest: visit_imp_in_H first_J_eq)
      done }
  then have range_fj: "range first_J  H  {THE x. False}"
    by auto

  have sf_fj: "simple_function hC first_J"
    by (rule simple_functionI) (auto intro: finite_subset[OF range_fj])

  have sd_fj: "simple_distributed hC first_J ?i"
    apply (rule hC.simple_distributedI[OF sf_fj])
    apply (auto intro!: T.cond_prob_eq_AE)
    apply (auto simp: space_stream_space)
    using AE_first_J
    apply eventually_elim
    apply auto
    done

  { fix ω have "last_H ω  H  last_H ω = (THE x. False)"
      apply (cases "i. ¬ before_C {i} ω")
      apply (simp add: last_H_def)
      apply (auto dest: before_C_imp_in_H last_H_eq)
      done }
  then have range_lnc: "range last_H  H  {THE x. False}"
    by auto

  have sf_lnc: "simple_function hC last_H"
    by (rule simple_functionI) (auto intro: finite_subset[OF range_lnc])

  have sd_lnc: "simple_distributed hC last_H ?l"
    apply (rule hC.simple_distributedI[OF sf_lnc])
    apply (auto intro!: T.cond_prob_eq_AE)
    apply (auto simp: space_stream_space)
    using AE_last_H
    apply eventually_elim
    apply auto
    done

  have sd_fj_lnc: "simple_distributed hC (λω. (first_J ω, last_H ω)) (λ(i, l). ?il i l)"
    apply (rule hC.simple_distributedI)
    apply (rule simple_function_Pair[OF sf_fj sf_lnc])
    apply (auto intro!: T.cond_prob_eq_AE)
    apply (auto simp: space_stream_space)
    using AE_last_H AE_first_J
    apply eventually_elim
    apply auto
    done

  define c where "c = (SOME j. j  C)"
  have c: "c  C"
    using C_non_empty unfolding ex_in_conv[symmetric] c_def by (rule someI_ex)

  let ?inner = "λi. lH. ?il i l * log 2 (?il i l / (?i i * ?l l))"
  { fix i assume i: "i  H"
    with h_pos have card_idx: "real_of_nat (card (H - {i})) = p_H / p_j - 1"
      by (auto simp add: p_j_def p_H_def h_def)

    have neq0: "p_j  0" "p_H  0"
      unfolding p_j_def p_H_def
      using C_smaller i by auto

    from i have "?inner i =
      (lH - {i}. ?il i l * log 2 (?il i l / (?i i * ?l l))) +
      ?il i i * log 2 (?il i i / (?i i * ?l i))"
      by (simp add: sum_diff)
    also have " =
      (lH - {i}. p_j/p_H * p_j * p_f * log 2 (p_j * p_f / (p_j * p_f + p_j/p_H * (1 - p_H * p_f)))) +
      p_j/p_H * (p_j * p_f + (1 - p_H * p_f)) * log 2 ((p_j * p_f + (1 - p_H * p_f)) / (p_j * p_f + p_j/p_H * (1 - p_H * p_f)))"
      using i p_f p_j_pos p_H
      apply (simp add: Pr_visit_before_C P_visit init_H Pr_before_C
                  del: sum_constant)
      apply (simp add: divide_simps distrib_left)
      apply (intro arg_cong2[where f="(*)"] refl arg_cong2[where f=log])
      apply (auto simp: field_simps)
      done
    also have " = (?f * log 2 (h * p_j * p_f) + (1 - ?f) * log 2 ((1 - ?f) * h)) / h"
      using neq0 p_f by (simp add: card_idx field_simps p_H = h * p_j)
    finally have "?inner i = (?f * log 2 (h * p_j * p_f) + (1 - ?f) * log 2 ((1 - ?f) * h)) / h" . }
  then have "(iH. ?inner i) = ?f * log 2 (h * p_j * p_f) + (1 - ?f) * log 2 ((1 - ?f) * h)"
    using h_pos by (simp add: h_def[symmetric])
  also have " = ?f * log 2 (p_H * p_f) + (1 - ?f) * log 2 ((1 - ?f) * h)"
    by (simp add: h = p_H / p_j)
  also have "  (1 - ?f) * log 2 ((1 - ?f) * h)"
    using log_le_0 by simp
  also have "  (1 - ?f) * log 2 h"
    using h_pos 1  h 1 p_j_pos p_f
    by (intro mult_left_mono log_mono mult_pos_pos mult_nonneg_nonneg) auto
  finally have "(iH. ?inner i)  (1 - ?f) * log 2 h" .
  also have "(iH. ?inner i) =
      ((i, l)(first_J`space S) × (last_H`space S). ?il i l * log 2 (?il i l / (?i i * ?l l)))"
    unfolding sum.cartesian_product
  proof (safe intro!: sum.mono_neutral_cong_left del: DiffE DiffI)
    show "finite ((first_J ` space S) × (last_H ` space S))"
      using sf_fj sf_lnc by (auto simp add: hC_def dest!: simple_functionD(1))
  next
    fix i assume "i  H"
    then have "visit {i} J (Init i ## Mix i ## sconst End)"
      "before_C {i} (Init i ## Mix c ## sconst End)"
      by (auto simp: before_C_def visit_def suntil_Stream HLD_iff c)
    then show "i  first_J ` space S" "i  last_H ` space S"
      by (auto simp: space_stream_space image_iff eq_commute dest!: first_J_eq last_H_eq)
  next
    fix i l assume "(i, l)  first_J ` space S × last_H ` space S - H × H"
    then have H: "i  H  l  H"
      by auto
    have "𝒫(ω in 𝔓. (visit {i} J ω  before_C {l} ω)  hit_C ω) = 0"
      using H by (intro T.prob_eq_0_AE) (auto dest: visit_imp_in_H before_C_imp_in_H)
    then show "?il i l * log 2 (?il i l / (?i i * ?l l)) = 0"
      by (simp add: cond_prob_def)
  qed
  also have " = ℐ(first_J ; last_H)"
    unfolding sum.cartesian_product
    apply (subst hC.mutual_information_simple_distributed[OF sd_fj sd_lnc sd_fj_lnc])
    apply (simp add: hC_def)
  proof (safe intro!: sum.mono_neutral_right imageI)
    show "finite ((first_J ` space S) × (last_H ` space S))"
      using sf_fj sf_lnc by (auto simp add: hC_def dest!: simple_functionD(1))
  next
    fix i l assume "(first_J i, last_H l)  (λx. (first_J x, last_H x)) ` space S"
    moreover
    { fix i l assume "i  H" "l  H"
      then have "visit {i} J (Init i ## Mix l ## Mix c ## sconst End)"
        "before_C {l} (Init i ## Mix l ## Mix c ## sconst End)"
        using c C_smaller by (auto simp: before_C_def visit_def HLD_iff suntil_Stream)
      then have "first_J (Init i ## Mix l ## Mix c ## sconst End) = i"
        "last_H (Init i ## Mix l ## Mix c ## sconst End) = l"
        by (auto intro!: first_J_eq last_H_eq) }
    note this[of "first_J i" "last_H l"]
    ultimately have "(first_J i, last_H l)  H×H"
      by (auto simp: space_stream_space image_iff eq_commute) metis
    then have "𝒫(ω in 𝔓. (visit {first_J i} J ω  before_C {last_H l} ω)  hit_C ω) = 0"
      by (intro T.prob_eq_0_AE) (auto dest: visit_imp_in_H before_C_imp_in_H)
    then show "?il (first_J i) (last_H l) *
      log 2 (?il (first_J i) (last_H l) / (?i (first_J i) * ?l (last_H l))) = 0"
      by (simp add: cond_prob_def)
  qed
  finally show ?thesis by simp
qed

end

end