# 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]
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: "(∑j∈J. 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"

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 "∀j∈J. 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 ⟹ ∃j∈J. 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)"
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)) {x∈space (T (Init j)). P x} =
emeasure (T (Mix j)) {x∈space (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`(L∩J)) ⋅ 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`(L2∩J)) ⋅ HLD {End}) (stl ω)"
with step.hyps show ?thesis
by (auto simp: inj_Mix HLD_iff elim: suntil.cases)
next
assume "¬ ((Mix`(L2∩J)) ⋅ 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 ω} = (∑i∈I. 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 ((∑i∈I. 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)"

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 𝔓. ∃j∈H. visit {j} {j} ω) = p_j"
using finite_J
proof (subst T.prob_sum[where I="H" and P="λj. visit {j} {j}"])
show "(∑j∈H. 𝒫(ω 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 𝔓. (∀n∈H. visit {n} {n} x ⟶ (∃j∈H. visit {j} {j} x)) ∧
((∃j∈H. 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"

lemma measurable_before_C[measurable]: "Measurable.pred S (before_C B)"

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 "∃i∈I ∩ 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
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 ω ) =
(∑i∈I. p_i i) * card L * p_j * p_f + (∑i∈I ∩ 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) = (∑i∈I∩L. 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) = (∑i∈I. ?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 "… = (∑i∈I. 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)) * (∑i∈I. p_i i) +
(∑i∈I ∩ 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 𝔓. ∃j∈H. 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 ω))"
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
qed

lemma probably_innocent:
assumes approx: "1 / (2 * (p_H - p_j)) ≤ p_f" and "p_H ≠ p_j"
shows "𝒫(ω in 𝔓. ∃j∈H. 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 + (∑l∈L. 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 + (∑i∈L. 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 ω ) = (∑i∈I. 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

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 (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 (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. ∑l∈H. ?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 =
(∑l∈H - {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))"
also have "… =
(∑l∈H - {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 (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 "(∑i∈H. ?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 "(∑i∈H. ?inner i) ≤ (1 - ?f) * log 2 h" .
also have "(∑i∈H. ?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"
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])
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"