[STATEMENT]
lemma mem_range_tms_Cons_iff[simp]: "x#xs all_in\<^sub>i range_tms e (X#XS) \<longleftrightarrow> x \<in>\<^sub>i range_tm e X \<and> xs all_in\<^sub>i range_tms e XS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x # xs all_in\<^sub>i range_tms e (X # XS)) = (x \<in>\<^sub>i range_tm e X \<and> xs all_in\<^sub>i range_tms e XS)
[PROOF STEP]
by (auto simp: range_tms_def all_in_i_def nth_Cons split: nat.splits)


[STATEMENT]
lemma approx_slp'_range:
  assumes i: "i all_subset I"
  assumes dev: "develops_at_within e i I"
  assumes vs: "vs all_in\<^sub>i range_tms e VS" "(\<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I)"
  assumes appr: "approx_slp' p ord I i ra VS = Some X"
  shows "interpret_slp ra vs all_in\<^sub>i range_tms e X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_slp ra vs all_in\<^sub>i range_tms e X
[PROOF STEP]
using appr vs
[PROOF STATE]
proof (prove)
using this:
approx_slp' p ord I i ra VS = Some X
vs all_in\<^sub>i range_tms e VS
?tm \<in> set VS \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. interpret_slp ra vs all_in\<^sub>i range_tms e X
[PROOF STEP]
proof (induction ra arbitrary: X vs VS)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>X vs VS. \<lbrakk>approx_slp' p ord I i [] VS = Some X; vs all_in\<^sub>i range_tms e VS; \<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> interpret_slp [] vs all_in\<^sub>i range_tms e X
 2. \<And>a ra X vs VS. \<lbrakk>\<And>X vs VS. \<lbrakk>approx_slp' p ord I i ra VS = Some X; vs all_in\<^sub>i range_tms e VS; \<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> interpret_slp ra vs all_in\<^sub>i range_tms e X; approx_slp' p ord I i (a # ra) VS = Some X; vs all_in\<^sub>i range_tms e VS; \<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> interpret_slp (a # ra) vs all_in\<^sub>i range_tms e X
[PROOF STEP]
case (Cons ra ras)
[PROOF STATE]
proof (state)
this:
\<lbrakk>approx_slp' p ord I i ras ?VS = Some ?X; ?vs all_in\<^sub>i range_tms e ?VS; \<And>tm. tm \<in> set ?VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> interpret_slp ras ?vs all_in\<^sub>i range_tms e ?X
approx_slp' p ord I i (ra # ras) VS = Some X
vs all_in\<^sub>i range_tms e VS
?tm \<in> set VS \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (2 subgoals):
 1. \<And>X vs VS. \<lbrakk>approx_slp' p ord I i [] VS = Some X; vs all_in\<^sub>i range_tms e VS; \<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> interpret_slp [] vs all_in\<^sub>i range_tms e X
 2. \<And>a ra X vs VS. \<lbrakk>\<And>X vs VS. \<lbrakk>approx_slp' p ord I i ra VS = Some X; vs all_in\<^sub>i range_tms e VS; \<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> interpret_slp ra vs all_in\<^sub>i range_tms e X; approx_slp' p ord I i (a # ra) VS = Some X; vs all_in\<^sub>i range_tms e VS; \<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> interpret_slp (a # ra) vs all_in\<^sub>i range_tms e X
[PROOF STEP]
from Cons.prems
[PROOF STATE]
proof (chain)
picking this:
approx_slp' p ord I i (ra # ras) VS = Some X
vs all_in\<^sub>i range_tms e VS
?tm \<in> set VS \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I
[PROOF STEP]
obtain a where a: "approx_tm p ord I i ra VS = Some a"
    and r: "approx_slp' p ord I i ras (a # VS) = Some X"
[PROOF STATE]
proof (prove)
using this:
approx_slp' p ord I i (ra # ras) VS = Some X
vs all_in\<^sub>i range_tms e VS
?tm \<in> set VS \<Longrightarrow> num_params (tm_poly ?tm) \<le> length I

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>approx_tm p ord I i ra VS = Some a; approx_slp' p ord I i ras (a # VS) = Some X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: bind_eq_Some_conv)
[PROOF STATE]
proof (state)
this:
approx_tm p ord I i ra VS = Some a
approx_slp' p ord I i ras (a # VS) = Some X

goal (2 subgoals):
 1. \<And>X vs VS. \<lbrakk>approx_slp' p ord I i [] VS = Some X; vs all_in\<^sub>i range_tms e VS; \<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> interpret_slp [] vs all_in\<^sub>i range_tms e X
 2. \<And>a ra X vs VS. \<lbrakk>\<And>X vs VS. \<lbrakk>approx_slp' p ord I i ra VS = Some X; vs all_in\<^sub>i range_tms e VS; \<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> interpret_slp ra vs all_in\<^sub>i range_tms e X; approx_slp' p ord I i (a # ra) VS = Some X; vs all_in\<^sub>i range_tms e VS; \<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> interpret_slp (a # ra) vs all_in\<^sub>i range_tms e X
[PROOF STEP]
from approx_tm_range[OF i a Cons.prems(2) dev Cons.prems(3)]
[PROOF STATE]
proof (chain)
picking this:
(\<And>tm. tm \<in> set VS \<Longrightarrow> tm \<in> set VS) \<Longrightarrow> interpret_floatarith ra vs \<in>\<^sub>i range_tm e a
[PROOF STEP]
have "interpret_floatarith ra vs \<in>\<^sub>i range_tm e a"
[PROOF STATE]
proof (prove)
using this:
(\<And>tm. tm \<in> set VS \<Longrightarrow> tm \<in> set VS) \<Longrightarrow> interpret_floatarith ra vs \<in>\<^sub>i range_tm e a

goal (1 subgoal):
 1. interpret_floatarith ra vs \<in>\<^sub>i range_tm e a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
interpret_floatarith ra vs \<in>\<^sub>i range_tm e a

goal (2 subgoals):
 1. \<And>X vs VS. \<lbrakk>approx_slp' p ord I i [] VS = Some X; vs all_in\<^sub>i range_tms e VS; \<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> interpret_slp [] vs all_in\<^sub>i range_tms e X
 2. \<And>a ra X vs VS. \<lbrakk>\<And>X vs VS. \<lbrakk>approx_slp' p ord I i ra VS = Some X; vs all_in\<^sub>i range_tms e VS; \<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> interpret_slp ra vs all_in\<^sub>i range_tms e X; approx_slp' p ord I i (a # ra) VS = Some X; vs all_in\<^sub>i range_tms e VS; \<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> interpret_slp (a # ra) vs all_in\<^sub>i range_tms e X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
interpret_floatarith ra vs \<in>\<^sub>i range_tm e a
[PROOF STEP]
have 1: "interpret_floatarith ra vs#vs all_in\<^sub>i range_tms e (a#VS)"
[PROOF STATE]
proof (prove)
using this:
interpret_floatarith ra vs \<in>\<^sub>i range_tm e a

goal (1 subgoal):
 1. interpret_floatarith ra vs # vs all_in\<^sub>i range_tms e (a # VS)
[PROOF STEP]
using Cons.prems(2)
[PROOF STATE]
proof (prove)
using this:
interpret_floatarith ra vs \<in>\<^sub>i range_tm e a
vs all_in\<^sub>i range_tms e VS

goal (1 subgoal):
 1. interpret_floatarith ra vs # vs all_in\<^sub>i range_tms e (a # VS)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
interpret_floatarith ra vs # vs all_in\<^sub>i range_tms e (a # VS)

goal (2 subgoals):
 1. \<And>X vs VS. \<lbrakk>approx_slp' p ord I i [] VS = Some X; vs all_in\<^sub>i range_tms e VS; \<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> interpret_slp [] vs all_in\<^sub>i range_tms e X
 2. \<And>a ra X vs VS. \<lbrakk>\<And>X vs VS. \<lbrakk>approx_slp' p ord I i ra VS = Some X; vs all_in\<^sub>i range_tms e VS; \<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> interpret_slp ra vs all_in\<^sub>i range_tms e X; approx_slp' p ord I i (a # ra) VS = Some X; vs all_in\<^sub>i range_tms e VS; \<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> interpret_slp (a # ra) vs all_in\<^sub>i range_tms e X
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_slp (ra # ras) vs all_in\<^sub>i range_tms e X
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_slp ras (interpret_floatarith ra vs # vs) all_in\<^sub>i range_tms e X
[PROOF STEP]
apply (rule Cons.IH)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. approx_slp' p ord I i ras ?VS = Some X
 2. interpret_floatarith ra vs # vs all_in\<^sub>i range_tms e ?VS
 3. \<And>tm. tm \<in> set ?VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I
[PROOF STEP]
apply (rule r)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. interpret_floatarith ra vs # vs all_in\<^sub>i range_tms e (a # VS)
 2. \<And>tm. tm \<in> set (a # VS) \<Longrightarrow> num_params (tm_poly tm) \<le> length I
[PROOF STEP]
apply (rule 1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>tm. tm \<in> set (a # VS) \<Longrightarrow> num_params (tm_poly tm) \<le> length I
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. num_params (tm_poly a) \<le> length I
 2. \<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I
[PROOF STEP]
apply (rule num_params_approx_tm)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. approx_tm ?prec6 ?ord6 I ?a6 ?f6 ?env6 = Some a
 2. \<And>tm. tm \<in> set ?env6 \<Longrightarrow> num_params (tm_poly tm) \<le> length I
 3. \<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I
[PROOF STEP]
apply (rule a)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I
 2. \<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I
[PROOF STEP]
by (auto intro!: Cons.prems)
[PROOF STATE]
proof (state)
this:
interpret_slp (ra # ras) vs all_in\<^sub>i range_tms e X

goal (1 subgoal):
 1. \<And>X vs VS. \<lbrakk>approx_slp' p ord I i [] VS = Some X; vs all_in\<^sub>i range_tms e VS; \<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I\<rbrakk> \<Longrightarrow> interpret_slp [] vs all_in\<^sub>i range_tms e X
[PROOF STEP]
qed auto


[STATEMENT]
lemma length_range_tms[simp]: "length (range_tms e VS) = length VS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (range_tms e VS) = length VS
[PROOF STEP]
by (auto simp: range_tms_def)


[STATEMENT]
lemma set_of_Ivl: "set_of (Ivl a b) = {a .. b}" if "a \<le> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of (Ivl a b) = {a..b}
[PROOF STEP]
by (auto simp: set_of_eq that min_def)


[STATEMENT]
lemma set_of_zero[simp]: "set_of 0 = {0::'a::ordered_comm_monoid_add}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_of 0 = {0::'a}
[PROOF STEP]
by (auto simp: set_of_eq)


[STATEMENT]
theorem approx_slp_range_tms:
  assumes "approx_slp p ord d slp VS = Some X"
  assumes slp_def: "slp = slp_of_fas fas"
  assumes d_def: "d = length fas"
  assumes e: "e \<in> UNIV \<rightarrow> {-1 .. 1}"
  assumes vs: "vs all_in\<^sub>i range_tms e VS"
  assumes lens: "\<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length vs"
  shows "interpret_floatariths fas vs all_in\<^sub>i range_tms e X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatariths fas vs all_in\<^sub>i range_tms e X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. interpret_floatariths fas vs all_in\<^sub>i range_tms e X
[PROOF STEP]
have "interpret_floatariths fas vs = take d (interpret_slp slp vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatariths fas vs = take d (interpret_slp slp vs)
[PROOF STEP]
by (simp add: slp_of_fas slp_def d_def)
[PROOF STATE]
proof (state)
this:
interpret_floatariths fas vs = take d (interpret_slp slp vs)

goal (1 subgoal):
 1. interpret_floatariths fas vs all_in\<^sub>i range_tms e X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
interpret_floatariths fas vs = take d (interpret_slp slp vs)

goal (1 subgoal):
 1. interpret_floatariths fas vs all_in\<^sub>i range_tms e X
[PROOF STEP]
have lvs: "length vs = length VS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length vs = length VS
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
local.approx_slp p ord d slp VS = Some X
slp = slp_of_fas fas
d = length fas
e \<in> UNIV \<rightarrow> {- 1..1}
vs all_in\<^sub>i range_tms e VS
?tm \<in> set VS \<Longrightarrow> num_params (tm_poly ?tm) \<le> length vs

goal (1 subgoal):
 1. length vs = length VS
[PROOF STEP]
by (auto simp: all_in_i_def)
[PROOF STATE]
proof (state)
this:
length vs = length VS

goal (1 subgoal):
 1. interpret_floatariths fas vs all_in\<^sub>i range_tms e X
[PROOF STEP]
define i where "i = replicate (length vs) (0::float interval)"
[PROOF STATE]
proof (state)
this:
i = replicate (length vs) 0

goal (1 subgoal):
 1. interpret_floatariths fas vs all_in\<^sub>i range_tms e X
[PROOF STEP]
define I where "I = replicate (length vs) (Ivl (-1) 1::float interval)"
[PROOF STATE]
proof (state)
this:
I = replicate (length vs) (Ivl (- 1) 1)

goal (1 subgoal):
 1. interpret_floatariths fas vs all_in\<^sub>i range_tms e X
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
local.approx_slp p ord d slp VS = Some X
slp = slp_of_fas fas
d = length fas
e \<in> UNIV \<rightarrow> {- 1..1}
vs all_in\<^sub>i range_tms e VS
?tm \<in> set VS \<Longrightarrow> num_params (tm_poly ?tm) \<le> length vs
[PROOF STEP]
obtain XS where
    XS: "approx_slp' p ord I i slp VS = Some XS"
    and X: "take d XS = X"
[PROOF STATE]
proof (prove)
using this:
local.approx_slp p ord d slp VS = Some X
slp = slp_of_fas fas
d = length fas
e \<in> UNIV \<rightarrow> {- 1..1}
vs all_in\<^sub>i range_tms e VS
?tm \<in> set VS \<Longrightarrow> num_params (tm_poly ?tm) \<le> length vs

goal (1 subgoal):
 1. (\<And>XS. \<lbrakk>approx_slp' p ord I i slp VS = Some XS; take d XS = X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: approx_slp_def lvs i_def I_def)
[PROOF STATE]
proof (state)
this:
approx_slp' p ord I i slp VS = Some XS
take d XS = X

goal (1 subgoal):
 1. interpret_floatariths fas vs all_in\<^sub>i range_tms e X
[PROOF STEP]
have iI: "i all_subset I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i all_subset I
[PROOF STEP]
by (auto simp: i_def I_def set_of_Ivl)
[PROOF STATE]
proof (state)
this:
i all_subset I

goal (1 subgoal):
 1. interpret_floatariths fas vs all_in\<^sub>i range_tms e X
[PROOF STEP]
have dev: "develops_at_within e i I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. develops_at_within e i I
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
e \<in> UNIV \<rightarrow> {- 1..1}

goal (1 subgoal):
 1. develops_at_within e i I
[PROOF STEP]
by (auto simp: develops_at_within_def i_def I_def set_of_Ivl real_interval_Ivl
        real_interval_minus real_interval_zero set_of_eq Pi_iff min_def)
[PROOF STATE]
proof (state)
this:
develops_at_within e i I

goal (1 subgoal):
 1. interpret_floatariths fas vs all_in\<^sub>i range_tms e X
[PROOF STEP]
from approx_slp'_range[OF iI dev vs _ XS] lens
[PROOF STATE]
proof (chain)
picking this:
(\<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I) \<Longrightarrow> interpret_slp slp vs all_in\<^sub>i range_tms e XS
?tm \<in> set VS \<Longrightarrow> num_params (tm_poly ?tm) \<le> length vs
[PROOF STEP]
have "interpret_slp slp vs all_in\<^sub>i range_tms e XS"
[PROOF STATE]
proof (prove)
using this:
(\<And>tm. tm \<in> set VS \<Longrightarrow> num_params (tm_poly tm) \<le> length I) \<Longrightarrow> interpret_slp slp vs all_in\<^sub>i range_tms e XS
?tm \<in> set VS \<Longrightarrow> num_params (tm_poly ?tm) \<le> length vs

goal (1 subgoal):
 1. interpret_slp slp vs all_in\<^sub>i range_tms e XS
[PROOF STEP]
by (auto simp: I_def)
[PROOF STATE]
proof (state)
this:
interpret_slp slp vs all_in\<^sub>i range_tms e XS

goal (1 subgoal):
 1. interpret_floatariths fas vs all_in\<^sub>i range_tms e X
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
interpret_slp slp vs all_in\<^sub>i range_tms e XS
[PROOF STEP]
have "take d (interpret_slp slp vs) all_in\<^sub>i range_tms e (take d XS)"
[PROOF STATE]
proof (prove)
using this:
interpret_slp slp vs all_in\<^sub>i range_tms e XS

goal (1 subgoal):
 1. take d (interpret_slp slp vs) all_in\<^sub>i range_tms e (take d XS)
[PROOF STEP]
by (auto simp: all_in_i_def range_tms_def)
[PROOF STATE]
proof (state)
this:
take d (interpret_slp slp vs) all_in\<^sub>i range_tms e (take d XS)

goal (1 subgoal):
 1. interpret_floatariths fas vs all_in\<^sub>i range_tms e X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
take d (interpret_slp slp vs) all_in\<^sub>i range_tms e (take d XS)

goal (1 subgoal):
 1. interpret_floatariths fas vs all_in\<^sub>i range_tms e X
[PROOF STEP]
note \<open>take d XS = X\<close>
[PROOF STATE]
proof (state)
this:
take d XS = X

goal (1 subgoal):
 1. interpret_floatariths fas vs all_in\<^sub>i range_tms e X
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
interpret_floatariths fas vs all_in\<^sub>i range_tms e X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
interpret_floatariths fas vs all_in\<^sub>i range_tms e X

goal (1 subgoal):
 1. interpret_floatariths fas vs all_in\<^sub>i range_tms e X
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
interpret_floatariths fas vs all_in\<^sub>i range_tms e X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma T_eq_rel_half[consumes 4, case_names prob sets cont]:
  fixes R :: "'s \<Rightarrow> 't \<Rightarrow> bool" and f :: "'s \<Rightarrow> 't" and S :: "'s set"
  assumes R_def: "\<And>s t. R s t \<longleftrightarrow> (s \<in> S \<and> f s = t)"
  assumes A[measurable]: "A \<in> sets (stream_space (count_space UNIV))"
    and B[measurable]: "B \<in> sets (stream_space (count_space UNIV))"
    and AB: "rel_set_strong (stream_all2 R) A B" and KL: "rel_fun R (rel_pmf R) K L" and xy: "R x y"
  shows "MC_syntax.T K x A = MC_syntax.T L y B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (MC_syntax.T K x) A = emeasure (MC_syntax.T L y) B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. emeasure (MC_syntax.T K x) A = emeasure (MC_syntax.T L y) B
[PROOF STEP]
interpret K: MC_syntax K
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (MC_syntax.T L y) B
[PROOF STEP]
interpret L: MC_syntax L
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
have "x \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> S
[PROOF STEP]
using \<open>R x y\<close>
[PROOF STATE]
proof (prove)
using this:
R x y

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

goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
define g where "g t = (SOME s. R s t)" for t
[PROOF STATE]
proof (state)
this:
g ?t = (SOME s. R s ?t)

goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
have measurable_g: "g \<in> count_space UNIV \<rightarrow>\<^sub>M count_space UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<in> count_space UNIV \<rightarrow>\<^sub>M count_space UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<in> count_space UNIV \<rightarrow>\<^sub>M count_space UNIV

goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
have g: "R i j \<Longrightarrow> R (g j) j" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R i j \<Longrightarrow> R (g j) j
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R i j \<Longrightarrow> R (SOME s. R s j) j
[PROOF STEP]
by (rule someI)
[PROOF STATE]
proof (state)
this:
R ?i1 ?j1 \<Longrightarrow> R (g ?j1) ?j1

goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
have K_subset: "x \<in> S \<Longrightarrow> K x \<subseteq> S" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> S \<Longrightarrow> set_pmf (K x) \<subseteq> S
[PROOF STEP]
using KL[THEN rel_funD, of x "f x", THEN rel_pmf_imp_rel_set]
[PROOF STATE]
proof (prove)
using this:
R x (f x) \<Longrightarrow> rel_set R (set_pmf (K x)) (set_pmf (L (f x)))

goal (1 subgoal):
 1. x \<in> S \<Longrightarrow> set_pmf (K x) \<subseteq> S
[PROOF STEP]
by (auto simp: rel_set_def R_def)
[PROOF STATE]
proof (state)
this:
?x1 \<in> S \<Longrightarrow> set_pmf (K ?x1) \<subseteq> S

goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
have in_S: "AE \<omega> in K.T x. \<omega> \<in> streams S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE \<omega> in K.T x. \<omega> \<in> streams S
[PROOF STEP]
using K.AE_T_enabled
[PROOF STATE]
proof (prove)
using this:
almost_everywhere (K.T ?s) (K.enabled ?s)

goal (1 subgoal):
 1. AE \<omega> in K.T x. \<omega> \<in> streams S
[PROOF STEP]
proof eventually_elim
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<omega>. K.enabled x \<omega> \<Longrightarrow> \<omega> \<in> streams S
[PROOF STEP]
case (elim \<omega>)
[PROOF STATE]
proof (state)
this:
K.enabled x \<omega>

goal (1 subgoal):
 1. \<And>\<omega>. K.enabled x \<omega> \<Longrightarrow> \<omega> \<in> streams S
[PROOF STEP]
with \<open>x \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> S
K.enabled x \<omega>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> S
K.enabled x \<omega>

goal (1 subgoal):
 1. \<omega> \<in> streams S
[PROOF STEP]
apply (coinduction arbitrary: x \<omega>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa \<omega>. \<lbrakk>xa \<in> S; K.enabled xa \<omega>\<rbrakk> \<Longrightarrow> \<exists>a s. \<omega> = a ## s \<and> a \<in> S \<and> ((\<exists>x \<omega>. s = \<omega> \<and> x \<in> S \<and> K.enabled x \<omega>) \<or> s \<in> streams S)
[PROOF STEP]
subgoal for x \<omega>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> S; K.enabled x \<omega>\<rbrakk> \<Longrightarrow> \<exists>a s. \<omega> = a ## s \<and> a \<in> S \<and> ((\<exists>x \<omega>. s = \<omega> \<and> x \<in> S \<and> K.enabled x \<omega>) \<or> s \<in> streams S)
[PROOF STEP]
using K_subset
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> S \<Longrightarrow> set_pmf (K ?x1) \<subseteq> S

goal (1 subgoal):
 1. \<lbrakk>x \<in> S; K.enabled x \<omega>\<rbrakk> \<Longrightarrow> \<exists>a s. \<omega> = a ## s \<and> a \<in> S \<and> ((\<exists>x \<omega>. s = \<omega> \<and> x \<in> S \<and> K.enabled x \<omega>) \<or> s \<in> streams S)
[PROOF STEP]
by (cases \<omega>) (auto simp: K.enabled_Stream)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<omega> \<in> streams S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
AE \<omega> in K.T x. \<omega> \<in> streams S

goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
have L_eq: "L y = map_pmf f (K x)" if xy: "R x y" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L y = map_pmf f (K x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L y = map_pmf f (K x)
[PROOF STEP]
have "rel_pmf (\<lambda>x y. x = y) (map_pmf f (K x)) (L y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pmf (=) (map_pmf f (K x)) (L y)
[PROOF STEP]
using KL[THEN rel_funD, OF xy]
[PROOF STATE]
proof (prove)
using this:
rel_pmf R (K x) (L y)

goal (1 subgoal):
 1. rel_pmf (=) (map_pmf f (K x)) (L y)
[PROOF STEP]
by (auto intro: pmf.rel_mono_strong simp: R_def pmf.rel_map)
[PROOF STATE]
proof (state)
this:
rel_pmf (=) (map_pmf f (K x)) (L y)

goal (1 subgoal):
 1. L y = map_pmf f (K x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rel_pmf (=) (map_pmf f (K x)) (L y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rel_pmf (=) (map_pmf f (K x)) (L y)

goal (1 subgoal):
 1. L y = map_pmf f (K x)
[PROOF STEP]
unfolding pmf.rel_eq
[PROOF STATE]
proof (prove)
using this:
map_pmf f (K x) = L y

goal (1 subgoal):
 1. L y = map_pmf f (K x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
L y = map_pmf f (K x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
R ?x1 ?y1 \<Longrightarrow> L ?y1 = map_pmf f (K ?x1)

goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
let ?D = "\<lambda>x. distr (K.T x) K.S (smap f)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
have prob_space_D: "?D x \<in> space (prob_algebra K.S)" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distr (K.T x) (stream_space (count_space UNIV)) (smap f) \<in> space (prob_algebra (stream_space (count_space UNIV)))
[PROOF STEP]
by (auto simp: space_prob_algebra K.T.prob_space_distr)
[PROOF STATE]
proof (state)
this:
distr (K.T ?x1) (stream_space (count_space UNIV)) (smap f) \<in> space (prob_algebra (stream_space (count_space UNIV)))

goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
have D_eq_D: "?D x = ?D x'" if "R x y" "R x' y" for x x' y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distr (K.T x) (stream_space (count_space UNIV)) (smap f) = distr (K.T x') (stream_space (count_space UNIV)) (smap f)
[PROOF STEP]
proof (rule stream_space_eq_sstart)
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. countable ?S
 2. prob_space (distr (K.T x) (stream_space (count_space UNIV)) (smap f))
 3. prob_space (distr (K.T x') (stream_space (count_space UNIV)) (smap f))
 4. AE x in distr (K.T x) (stream_space (count_space UNIV)) (smap f). x \<in> streams ?S
 5. AE x in distr (K.T x') (stream_space (count_space UNIV)) (smap f). x \<in> streams ?S
 6. sets (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
 7. sets (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
 8. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists ?S\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart ?S xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart ?S xs)
[PROOF STEP]
define A where "A = K.acc `` {x, x'}"
[PROOF STATE]
proof (state)
this:
A = K.acc `` {x, x'}

goal (8 subgoals):
 1. countable ?S
 2. prob_space (distr (K.T x) (stream_space (count_space UNIV)) (smap f))
 3. prob_space (distr (K.T x') (stream_space (count_space UNIV)) (smap f))
 4. AE x in distr (K.T x) (stream_space (count_space UNIV)) (smap f). x \<in> streams ?S
 5. AE x in distr (K.T x') (stream_space (count_space UNIV)) (smap f). x \<in> streams ?S
 6. sets (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
 7. sets (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
 8. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists ?S\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart ?S xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart ?S xs)
[PROOF STEP]
have x_A: "x \<in> A" "x' \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> A &&& x' \<in> A
[PROOF STEP]
by (auto simp: A_def)
[PROOF STATE]
proof (state)
this:
x \<in> A
x' \<in> A

goal (8 subgoals):
 1. countable ?S
 2. prob_space (distr (K.T x) (stream_space (count_space UNIV)) (smap f))
 3. prob_space (distr (K.T x') (stream_space (count_space UNIV)) (smap f))
 4. AE x in distr (K.T x) (stream_space (count_space UNIV)) (smap f). x \<in> streams ?S
 5. AE x in distr (K.T x') (stream_space (count_space UNIV)) (smap f). x \<in> streams ?S
 6. sets (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
 7. sets (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
 8. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists ?S\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart ?S xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart ?S xs)
[PROOF STEP]
let ?\<Omega> = "f ` A"
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. countable ?S
 2. prob_space (distr (K.T x) (stream_space (count_space UNIV)) (smap f))
 3. prob_space (distr (K.T x') (stream_space (count_space UNIV)) (smap f))
 4. AE x in distr (K.T x) (stream_space (count_space UNIV)) (smap f). x \<in> streams ?S
 5. AE x in distr (K.T x') (stream_space (count_space UNIV)) (smap f). x \<in> streams ?S
 6. sets (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
 7. sets (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
 8. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists ?S\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart ?S xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart ?S xs)
[PROOF STEP]
show "countable ?\<Omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable (f ` A)
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable (f ` K.acc `` {x, x'})
[PROOF STEP]
by (intro countable_image K.countable_acc) auto
[PROOF STATE]
proof (state)
this:
countable (f ` A)

goal (7 subgoals):
 1. prob_space (distr (K.T x) (stream_space (count_space UNIV)) (smap f))
 2. prob_space (distr (K.T x') (stream_space (count_space UNIV)) (smap f))
 3. AE x in distr (K.T x) (stream_space (count_space UNIV)) (smap f). x \<in> streams (f ` K.acc `` {x, x'})
 4. AE x in distr (K.T x') (stream_space (count_space UNIV)) (smap f). x \<in> streams (f ` K.acc `` {x, x'})
 5. sets (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
 6. sets (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
 7. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists (f ` K.acc `` {x, x'})\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` K.acc `` {x, x'}) xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` K.acc `` {x, x'}) xs)
[PROOF STEP]
show "prob_space (?D x)" "prob_space (?D x')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob_space (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) &&& prob_space (distr (K.T x') (stream_space (count_space UNIV)) (smap f))
[PROOF STEP]
by (auto intro!: K.T.prob_space_distr)
[PROOF STATE]
proof (state)
this:
prob_space (distr (K.T x) (stream_space (count_space UNIV)) (smap f))
prob_space (distr (K.T x') (stream_space (count_space UNIV)) (smap f))

goal (5 subgoals):
 1. AE x in distr (K.T x) (stream_space (count_space UNIV)) (smap f). x \<in> streams (f ` K.acc `` {x, x'})
 2. AE x in distr (K.T x') (stream_space (count_space UNIV)) (smap f). x \<in> streams (f ` K.acc `` {x, x'})
 3. sets (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
 4. sets (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
 5. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists (f ` K.acc `` {x, x'})\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` K.acc `` {x, x'}) xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` K.acc `` {x, x'}) xs)
[PROOF STEP]
show "sets (?D x) = sets L.S" "sets (?D x') = sets L.S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sets (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV)) &&& sets (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sets (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
sets (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))

goal (3 subgoals):
 1. AE x in distr (K.T x) (stream_space (count_space UNIV)) (smap f). x \<in> streams (f ` K.acc `` {x, x'})
 2. AE x in distr (K.T x') (stream_space (count_space UNIV)) (smap f). x \<in> streams (f ` K.acc `` {x, x'})
 3. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists (f ` K.acc `` {x, x'})\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` K.acc `` {x, x'}) xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` K.acc `` {x, x'}) xs)
[PROOF STEP]
have AE_streams: "AE x in ?D x''. x \<in> streams ?\<Omega>" if "x'' \<in> A" for x''
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in distr (K.T x'') (stream_space (count_space UNIV)) (smap f). x \<in> streams (f ` A)
[PROOF STEP]
apply (simp add: space_stream_space streams_sets AE_distr_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in K.T x''. smap f x \<in> streams (f ` A)
[PROOF STEP]
using K.AE_T_reachable[of x'']
[PROOF STATE]
proof (prove)
using this:
almost_everywhere (K.T x'') (alw (HLD (K.acc `` {x''})))

goal (1 subgoal):
 1. AE x in K.T x''. smap f x \<in> streams (f ` A)
[PROOF STEP]
unfolding alw_HLD_iff_streams
[PROOF STATE]
proof (prove)
using this:
AE \<omega> in K.T x''. \<omega> \<in> streams (K.acc `` {x''})

goal (1 subgoal):
 1. AE x in K.T x''. smap f x \<in> streams (f ` A)
[PROOF STEP]
proof eventually_elim
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> streams (K.acc `` {x''}) \<Longrightarrow> smap f x \<in> streams (f ` A)
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> streams (K.acc `` {x''}) \<Longrightarrow> smap f x \<in> streams (f ` A)
[PROOF STEP]
assume "s \<in> streams (K.acc `` {x''})"
[PROOF STATE]
proof (state)
this:
s \<in> streams (K.acc `` {x''})

goal (1 subgoal):
 1. \<And>x. x \<in> streams (K.acc `` {x''}) \<Longrightarrow> smap f x \<in> streams (f ` A)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s \<in> streams (K.acc `` {x''})

goal (1 subgoal):
 1. \<And>x. x \<in> streams (K.acc `` {x''}) \<Longrightarrow> smap f x \<in> streams (f ` A)
[PROOF STEP]
have "K.acc `` {x''} \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K.acc `` {x''} \<subseteq> A
[PROOF STEP]
using \<open>x'' \<in> A\<close>
[PROOF STATE]
proof (prove)
using this:
x'' \<in> A

goal (1 subgoal):
 1. K.acc `` {x''} \<subseteq> A
[PROOF STEP]
by (auto simp: A_def Image_def intro: rtrancl_trans)
[PROOF STATE]
proof (state)
this:
K.acc `` {x''} \<subseteq> A

goal (1 subgoal):
 1. \<And>x. x \<in> streams (K.acc `` {x''}) \<Longrightarrow> smap f x \<in> streams (f ` A)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s \<in> streams (K.acc `` {x''})
K.acc `` {x''} \<subseteq> A
[PROOF STEP]
show "smap f s \<in> streams (f ` A)"
[PROOF STATE]
proof (prove)
using this:
s \<in> streams (K.acc `` {x''})
K.acc `` {x''} \<subseteq> A

goal (1 subgoal):
 1. smap f s \<in> streams (f ` A)
[PROOF STEP]
by (auto intro: smap_streams)
[PROOF STATE]
proof (state)
this:
smap f s \<in> streams (f ` A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x''1 \<in> A \<Longrightarrow> AE x in distr (K.T ?x''1) (stream_space (count_space UNIV)) (smap f). x \<in> streams (f ` A)

goal (3 subgoals):
 1. AE x in distr (K.T x) (stream_space (count_space UNIV)) (smap f). x \<in> streams (f ` K.acc `` {x, x'})
 2. AE x in distr (K.T x') (stream_space (count_space UNIV)) (smap f). x \<in> streams (f ` K.acc `` {x, x'})
 3. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists (f ` K.acc `` {x, x'})\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` K.acc `` {x, x'}) xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` K.acc `` {x, x'}) xs)
[PROOF STEP]
with x_A
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
x' \<in> A
?x''1 \<in> A \<Longrightarrow> AE x in distr (K.T ?x''1) (stream_space (count_space UNIV)) (smap f). x \<in> streams (f ` A)
[PROOF STEP]
show "AE x in ?D x'. x \<in> streams ?\<Omega>" "AE x in ?D x. x \<in> streams ?\<Omega>"
[PROOF STATE]
proof (prove)
using this:
x \<in> A
x' \<in> A
?x''1 \<in> A \<Longrightarrow> AE x in distr (K.T ?x''1) (stream_space (count_space UNIV)) (smap f). x \<in> streams (f ` A)

goal (1 subgoal):
 1. AE x in distr (K.T x') (stream_space (count_space UNIV)) (smap f). x \<in> streams (f ` A) &&& AE x in distr (K.T x) (stream_space (count_space UNIV)) (smap f). x \<in> streams (f ` A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in distr (K.T x') (stream_space (count_space UNIV)) (smap f). x \<in> streams (f ` A)
AE x in distr (K.T x) (stream_space (count_space UNIV)) (smap f). x \<in> streams (f ` A)

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>xs \<noteq> []; xs \<in> lists (f ` K.acc `` {x, x'})\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` K.acc `` {x, x'}) xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` K.acc `` {x, x'}) xs)
[PROOF STEP]
from \<open>x \<in> A\<close> \<open>x' \<in> A\<close> that
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
x' \<in> A
R x y
R x' y
[PROOF STEP]
show "?D x (sstart (f ` A) xs) = ?D x' (sstart (f ` A) xs)" for xs
[PROOF STATE]
proof (prove)
using this:
x \<in> A
x' \<in> A
R x y
R x' y

goal (1 subgoal):
 1. emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs)
[PROOF STEP]
proof (induction xs arbitrary: x x' y)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x x' y. \<lbrakk>x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) []) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) [])
 2. \<And>a xs x x' y. \<lbrakk>\<And>x x' y. \<lbrakk>x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs); x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs)) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
x \<in> A
x' \<in> A
R x y
R x' y

goal (2 subgoals):
 1. \<And>x x' y. \<lbrakk>x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) []) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) [])
 2. \<And>a xs x x' y. \<lbrakk>\<And>x x' y. \<lbrakk>x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs); x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs)) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> A
x' \<in> A
R x y
R x' y

goal (2 subgoals):
 1. \<And>x x' y. \<lbrakk>x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) []) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) [])
 2. \<And>a xs x x' y. \<lbrakk>\<And>x x' y. \<lbrakk>x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs); x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs)) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs))
[PROOF STEP]
have "?D x (streams (f ` A)) = 1" if "x \<in> A" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (streams (f ` A)) = 1
[PROOF STEP]
using AE_streams[of x] that
[PROOF STATE]
proof (prove)
using this:
x \<in> A \<Longrightarrow> AE x in distr (K.T x) (stream_space (count_space UNIV)) (smap f). x \<in> streams (f ` A)
x \<in> A

goal (1 subgoal):
 1. emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (streams (f ` A)) = 1
[PROOF STEP]
by (intro prob_space.emeasure_eq_1_AE[OF K.T.prob_space_distr]) (auto simp: streams_sets)
[PROOF STATE]
proof (state)
this:
?x1 \<in> A \<Longrightarrow> emeasure (distr (K.T ?x1) (stream_space (count_space UNIV)) (smap f)) (streams (f ` A)) = 1

goal (2 subgoals):
 1. \<And>x x' y. \<lbrakk>x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) []) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) [])
 2. \<And>a xs x x' y. \<lbrakk>\<And>x x' y. \<lbrakk>x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs); x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs)) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
x' \<in> A
R x y
R x' y
?x1 \<in> A \<Longrightarrow> emeasure (distr (K.T ?x1) (stream_space (count_space UNIV)) (smap f)) (streams (f ` A)) = 1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> A
x' \<in> A
R x y
R x' y
?x1 \<in> A \<Longrightarrow> emeasure (distr (K.T ?x1) (stream_space (count_space UNIV)) (smap f)) (streams (f ` A)) = 1

goal (1 subgoal):
 1. emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) []) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) []) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) [])

goal (1 subgoal):
 1. \<And>a xs x x' y. \<lbrakk>\<And>x x' y. \<lbrakk>x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs); x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs)) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs x x' y. \<lbrakk>\<And>x x' y. \<lbrakk>x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs); x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs)) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs))
[PROOF STEP]
case (Cons z zs x x' y)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x1 \<in> A; ?x'1 \<in> A; R ?x1 ?y1; R ?x'1 ?y1\<rbrakk> \<Longrightarrow> emeasure (distr (K.T ?x1) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) zs) = emeasure (distr (K.T ?x'1) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) zs)
x \<in> A
x' \<in> A
R x y
R x' y

goal (1 subgoal):
 1. \<And>a xs x x' y. \<lbrakk>\<And>x x' y. \<lbrakk>x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs); x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs)) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs))
[PROOF STEP]
have "rel_pmf (R OO R\<inverse>\<inverse>) (K x) (K x')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pmf (R OO R\<inverse>\<inverse>) (K x) (K x')
[PROOF STEP]
using KL[THEN rel_funD, OF Cons(4)] KL[THEN rel_funD, OF Cons(5)]
[PROOF STATE]
proof (prove)
using this:
rel_pmf R (K x) (L y)
rel_pmf R (K x') (L y)

goal (1 subgoal):
 1. rel_pmf (R OO R\<inverse>\<inverse>) (K x) (K x')
[PROOF STEP]
unfolding pmf.rel_compp pmf.rel_flip
[PROOF STATE]
proof (prove)
using this:
rel_pmf R (K x) (L y)
rel_pmf R (K x') (L y)

goal (1 subgoal):
 1. (rel_pmf R OO (\<lambda>a b. rel_pmf R b a)) (K x) (K x')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rel_pmf (R OO R\<inverse>\<inverse>) (K x) (K x')

goal (1 subgoal):
 1. \<And>a xs x x' y. \<lbrakk>\<And>x x' y. \<lbrakk>x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs); x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs)) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rel_pmf (R OO R\<inverse>\<inverse>) (K x) (K x')
[PROOF STEP]
obtain p :: "('s \<times> 's) pmf" where p: "\<And>a b. (a, b) \<in> p \<Longrightarrow> (R OO R\<inverse>\<inverse>) a b" and
        eq: "map_pmf fst p = K x" "map_pmf snd p = K x'"
[PROOF STATE]
proof (prove)
using this:
rel_pmf (R OO R\<inverse>\<inverse>) (K x) (K x')

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>\<And>a b. (a, b) \<in> set_pmf p \<Longrightarrow> (R OO R\<inverse>\<inverse>) a b; map_pmf fst p = K x; map_pmf snd p = K x'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: pmf.in_rel)
[PROOF STATE]
proof (state)
this:
(?a1, ?b1) \<in> set_pmf p \<Longrightarrow> (R OO R\<inverse>\<inverse>) ?a1 ?b1
map_pmf fst p = K x
map_pmf snd p = K x'

goal (1 subgoal):
 1. \<And>a xs x x' y. \<lbrakk>\<And>x x' y. \<lbrakk>x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs); x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs)) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs))
[PROOF STEP]
let ?S = "stream_space (count_space UNIV)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs x x' y. \<lbrakk>\<And>x x' y. \<lbrakk>x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs); x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs)) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs))
[PROOF STEP]
have *: "(##) y -` smap f -` sstart (f ` A) (z # zs) = (if f y = z then smap f -` sstart (f ` A) zs else {})" for y z zs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (##) y -` smap f -` sstart (f ` A) (z # zs) = (if f y = z then smap f -` sstart (f ` A) zs else {})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(##) ?y2 -` smap f -` sstart (f ` A) (?z2 # ?zs2) = (if f ?y2 = ?z2 then smap f -` sstart (f ` A) ?zs2 else {})

goal (1 subgoal):
 1. \<And>a xs x x' y. \<lbrakk>\<And>x x' y. \<lbrakk>x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs); x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs)) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs))
[PROOF STEP]
have **: "?D x (sstart (f ` A) (z # zs)) = (\<integral>\<^sup>+ y'. (if f y' = z then ?D y' (sstart (f ` A) zs) else 0) \<partial>K x)" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (z # zs)) = \<integral>\<^sup>+ y'. (if f y' = z then emeasure (distr (K.T y') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) zs) else 0) \<partial>measure_pmf (K x)
[PROOF STEP]
apply (simp add: emeasure_distr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (K.T x) (smap f -` sstart (f ` A) (z # zs) \<inter> space (stream_space (count_space UNIV))) = \<integral>\<^sup>+ y'. (if f y' = z then emeasure (distr (K.T y') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) zs) else 0) \<partial>measure_pmf (K x)
[PROOF STEP]
apply (subst K.T_eq_bind)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (measure_pmf (K x) \<bind> (\<lambda>t. distr (K.T t) (stream_space (count_space UNIV)) ((##) t))) (smap f -` sstart (f ` A) (z # zs) \<inter> space (stream_space (count_space UNIV))) = \<integral>\<^sup>+ y'. (if f y' = z then emeasure (distr (K.T y') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) zs) else 0) \<partial>measure_pmf (K x)
[PROOF STEP]
apply (subst emeasure_bind[where N="?S"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. space (measure_pmf (K x)) \<noteq> {}
 2. measure_pmf.random_variable (K x) (subprob_algebra (stream_space (count_space UNIV))) (\<lambda>t. distr (K.T t) (stream_space (count_space UNIV)) ((##) t))
 3. smap f -` sstart (f ` A) (z # zs) \<inter> space (stream_space (count_space UNIV)) \<in> sets (stream_space (count_space UNIV))
 4. \<integral>\<^sup>+ x. emeasure (distr (K.T x) (stream_space (count_space UNIV)) ((##) x)) (smap f -` sstart (f ` A) (z # zs) \<inter> space (stream_space (count_space UNIV))) \<partial>measure_pmf (K x) = \<integral>\<^sup>+ y'. (if f y' = z then emeasure (distr (K.T y') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) zs) else 0) \<partial>measure_pmf (K x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. measure_pmf.random_variable (K x) (subprob_algebra (stream_space (count_space UNIV))) (\<lambda>t. distr (K.T t) (stream_space (count_space UNIV)) ((##) t))
 2. smap f -` sstart (f ` A) (z # zs) \<inter> space (stream_space (count_space UNIV)) \<in> sets (stream_space (count_space UNIV))
 3. \<integral>\<^sup>+ x. emeasure (distr (K.T x) (stream_space (count_space UNIV)) ((##) x)) (smap f -` sstart (f ` A) (z # zs) \<inter> space (stream_space (count_space UNIV))) \<partial>measure_pmf (K x) = \<integral>\<^sup>+ y'. (if f y' = z then emeasure (distr (K.T y') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) zs) else 0) \<partial>measure_pmf (K x)
[PROOF STEP]
apply (rule measurable_distr2[where M="?S"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (\<lambda>(x, y). x ## y) \<in> measure_pmf (K x) \<Otimes>\<^sub>M stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 2. measure_pmf.random_variable (K x) (subprob_algebra (stream_space (count_space UNIV))) K.T
 3. smap f -` sstart (f ` A) (z # zs) \<inter> space (stream_space (count_space UNIV)) \<in> sets (stream_space (count_space UNIV))
 4. \<integral>\<^sup>+ x. emeasure (distr (K.T x) (stream_space (count_space UNIV)) ((##) x)) (smap f -` sstart (f ` A) (z # zs) \<inter> space (stream_space (count_space UNIV))) \<partial>measure_pmf (K x) = \<integral>\<^sup>+ y'. (if f y' = z then emeasure (distr (K.T y') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) zs) else 0) \<partial>measure_pmf (K x)
[PROOF STEP]
apply measurable
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. emeasure (distr (K.T x) (stream_space (count_space UNIV)) ((##) x)) (smap f -` sstart (f ` A) (z # zs) \<inter> space (stream_space (count_space UNIV))) \<partial>measure_pmf (K x) = \<integral>\<^sup>+ y'. (if f y' = z then emeasure (distr (K.T y') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) zs) else 0) \<partial>measure_pmf (K x)
[PROOF STEP]
apply (intro nn_integral_cong_AE AE_pmfI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y \<in> set_pmf (K x) \<Longrightarrow> emeasure (distr (K.T y) (stream_space (count_space UNIV)) ((##) y)) (smap f -` sstart (f ` A) (z # zs) \<inter> space (stream_space (count_space UNIV))) = (if f y = z then emeasure (distr (K.T y) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) zs) else 0)
[PROOF STEP]
apply (auto simp add: emeasure_distr)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>y \<in> set_pmf (K x); z = f y\<rbrakk> \<Longrightarrow> emeasure (K.T y) ((##) y -` smap f -` sstart (f ` A) (f y # zs) \<inter> (##) y -` space (stream_space (count_space UNIV)) \<inter> space (stream_space (count_space UNIV))) = emeasure (K.T y) (smap f -` sstart (f ` A) zs \<inter> space (stream_space (count_space UNIV)))
 2. \<And>y. \<lbrakk>y \<in> set_pmf (K x); f y \<noteq> z\<rbrakk> \<Longrightarrow> emeasure (K.T y) ((##) y -` smap f -` sstart (f ` A) (z # zs) \<inter> (##) y -` space (stream_space (count_space UNIV)) \<inter> space (stream_space (count_space UNIV))) = 0
[PROOF STEP]
apply (simp_all add: * space_stream_space)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
emeasure (distr (K.T ?x2) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (z # zs)) = \<integral>\<^sup>+ y'. (if f y' = z then emeasure (distr (K.T y') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) zs) else 0) \<partial>measure_pmf (K ?x2)

goal (1 subgoal):
 1. \<And>a xs x x' y. \<lbrakk>\<And>x x' y. \<lbrakk>x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs); x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs)) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs))
[PROOF STEP]
have fst_A: "fst ab \<in> A" if "ab \<in> p" for ab
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ab \<in> A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst ab \<in> A
[PROOF STEP]
have "fst ab \<in> K x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ab \<in> set_pmf (K x)
[PROOF STEP]
using \<open>ab \<in> p\<close> set_map_pmf [of fst p]
[PROOF STATE]
proof (prove)
using this:
ab \<in> set_pmf p
set_pmf (map_pmf fst p) = fst ` set_pmf p

goal (1 subgoal):
 1. fst ab \<in> set_pmf (K x)
[PROOF STEP]
by (auto simp: eq)
[PROOF STATE]
proof (state)
this:
fst ab \<in> set_pmf (K x)

goal (1 subgoal):
 1. fst ab \<in> A
[PROOF STEP]
with \<open>x \<in> A\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
fst ab \<in> set_pmf (K x)
[PROOF STEP]
show "fst ab \<in> A"
[PROOF STATE]
proof (prove)
using this:
x \<in> A
fst ab \<in> set_pmf (K x)

goal (1 subgoal):
 1. fst ab \<in> A
[PROOF STEP]
by (auto simp: A_def intro: rtrancl.rtrancl_into_rtrancl)
[PROOF STATE]
proof (state)
this:
fst ab \<in> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?ab2 \<in> set_pmf p \<Longrightarrow> fst ?ab2 \<in> A

goal (1 subgoal):
 1. \<And>a xs x x' y. \<lbrakk>\<And>x x' y. \<lbrakk>x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs); x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs)) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs))
[PROOF STEP]
have snd_A: "snd ab \<in> A" if "ab \<in> p" for ab
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd ab \<in> A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. snd ab \<in> A
[PROOF STEP]
have "snd ab \<in> K x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd ab \<in> set_pmf (K x')
[PROOF STEP]
using \<open>ab \<in> p\<close> set_map_pmf [of snd p]
[PROOF STATE]
proof (prove)
using this:
ab \<in> set_pmf p
set_pmf (map_pmf snd p) = snd ` set_pmf p

goal (1 subgoal):
 1. snd ab \<in> set_pmf (K x')
[PROOF STEP]
by (auto simp: eq)
[PROOF STATE]
proof (state)
this:
snd ab \<in> set_pmf (K x')

goal (1 subgoal):
 1. snd ab \<in> A
[PROOF STEP]
with \<open>x' \<in> A\<close>
[PROOF STATE]
proof (chain)
picking this:
x' \<in> A
snd ab \<in> set_pmf (K x')
[PROOF STEP]
show "snd ab \<in> A"
[PROOF STATE]
proof (prove)
using this:
x' \<in> A
snd ab \<in> set_pmf (K x')

goal (1 subgoal):
 1. snd ab \<in> A
[PROOF STEP]
by (auto simp: A_def intro: rtrancl.rtrancl_into_rtrancl)
[PROOF STATE]
proof (state)
this:
snd ab \<in> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?ab2 \<in> set_pmf p \<Longrightarrow> snd ?ab2 \<in> A

goal (1 subgoal):
 1. \<And>a xs x x' y. \<lbrakk>\<And>x x' y. \<lbrakk>x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) xs); x \<in> A; x' \<in> A; R x y; R x' y\<rbrakk> \<Longrightarrow> emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs)) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (a # xs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (z # zs)) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (z # zs))
[PROOF STEP]
unfolding ** eq[symmetric] nn_integral_map_pmf
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. (if f (fst x) = z then emeasure (distr (K.T (fst x)) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) zs) else 0) \<partial>measure_pmf p = \<integral>\<^sup>+ x. (if f (snd x) = z then emeasure (distr (K.T (snd x)) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) zs) else 0) \<partial>measure_pmf p
[PROOF STEP]
apply (intro nn_integral_cong_AE AE_pmfI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y \<in> set_pmf p \<Longrightarrow> (if f (fst y) = z then emeasure (distr (K.T (fst y)) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) zs) else 0) = (if f (snd y) = z then emeasure (distr (K.T (snd y)) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) zs) else 0)
[PROOF STEP]
subgoal for ab
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ab \<in> set_pmf p \<Longrightarrow> (if f (fst ab) = z then emeasure (distr (K.T (fst ab)) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) zs) else 0) = (if f (snd ab) = z then emeasure (distr (K.T (snd ab)) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) zs) else 0)
[PROOF STEP]
using p[of "fst ab" "snd ab"]
[PROOF STATE]
proof (prove)
using this:
(fst ab, snd ab) \<in> set_pmf p \<Longrightarrow> (R OO R\<inverse>\<inverse>) (fst ab) (snd ab)

goal (1 subgoal):
 1. ab \<in> set_pmf p \<Longrightarrow> (if f (fst ab) = z then emeasure (distr (K.T (fst ab)) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) zs) else 0) = (if f (snd ab) = z then emeasure (distr (K.T (snd ab)) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) zs) else 0)
[PROOF STEP]
by (auto simp: R_def intro!: Cons(1) fst_A snd_A)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (z # zs)) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) (z # zs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) ?xs1) = emeasure (distr (K.T x') (stream_space (count_space UNIV)) (smap f)) (sstart (f ` A) ?xs1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>R ?x1 ?y1; R ?x'1 ?y1\<rbrakk> \<Longrightarrow> distr (K.T ?x1) (stream_space (count_space UNIV)) (smap f) = distr (K.T ?x'1) (stream_space (count_space UNIV)) (smap f)

goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
have L_eq_D: "L.T y = ?D x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L.T y = distr (K.T x) (stream_space (count_space UNIV)) (smap f)
[PROOF STEP]
using \<open>R x y\<close>
[PROOF STATE]
proof (prove)
using this:
R x y

goal (1 subgoal):
 1. L.T y = distr (K.T x) (stream_space (count_space UNIV)) (smap f)
[PROOF STEP]
proof (coinduction arbitrary: x y rule: L.T_coinduct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xa y. R xa y \<Longrightarrow> prob_space (distr (K.T xa) (stream_space (count_space UNIV)) (smap f))
 2. \<And>xa y. R xa y \<Longrightarrow> sets (distr (K.T xa) (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
 3. \<And>xa y. R xa y \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (L y). \<exists>x ya. y = ya \<and> M' y = distr (K.T x) (stream_space (count_space UNIV)) (smap f) \<and> R x ya) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (K.T xa) (stream_space (count_space UNIV)) (smap f) = measure_pmf (L y) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
case (cont x y)
[PROOF STATE]
proof (state)
this:
R x y

goal (3 subgoals):
 1. \<And>xa y. R xa y \<Longrightarrow> prob_space (distr (K.T xa) (stream_space (count_space UNIV)) (smap f))
 2. \<And>xa y. R xa y \<Longrightarrow> sets (distr (K.T xa) (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
 3. \<And>xa y. R xa y \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (L y). \<exists>x ya. y = ya \<and> M' y = distr (K.T x) (stream_space (count_space UNIV)) (smap f) \<and> R x ya) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (K.T xa) (stream_space (count_space UNIV)) (smap f) = measure_pmf (L y) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
R x y
[PROOF STEP]
have Kx_Ly: "rel_pmf R (K x) (L y)"
[PROOF STATE]
proof (prove)
using this:
R x y

goal (1 subgoal):
 1. rel_pmf R (K x) (L y)
[PROOF STEP]
by (rule KL[THEN rel_funD])
[PROOF STATE]
proof (state)
this:
rel_pmf R (K x) (L y)

goal (3 subgoals):
 1. \<And>xa y. R xa y \<Longrightarrow> prob_space (distr (K.T xa) (stream_space (count_space UNIV)) (smap f))
 2. \<And>xa y. R xa y \<Longrightarrow> sets (distr (K.T xa) (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
 3. \<And>xa y. R xa y \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (L y). \<exists>x ya. y = ya \<and> M' y = distr (K.T x) (stream_space (count_space UNIV)) (smap f) \<and> R x ya) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (K.T xa) (stream_space (count_space UNIV)) (smap f) = measure_pmf (L y) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rel_pmf R (K x) (L y)
[PROOF STEP]
have *: "y' \<in> L y \<Longrightarrow> \<exists>x'\<in>K x. R x' y'" for y'
[PROOF STATE]
proof (prove)
using this:
rel_pmf R (K x) (L y)

goal (1 subgoal):
 1. y' \<in> set_pmf (L y) \<Longrightarrow> \<exists>x'\<in>set_pmf (K x). R x' y'
[PROOF STEP]
by (auto dest!: rel_pmf_imp_rel_set simp: rel_set_def)
[PROOF STATE]
proof (state)
this:
?y'1 \<in> set_pmf (L y) \<Longrightarrow> \<exists>x'\<in>set_pmf (K x). R x' ?y'1

goal (3 subgoals):
 1. \<And>xa y. R xa y \<Longrightarrow> prob_space (distr (K.T xa) (stream_space (count_space UNIV)) (smap f))
 2. \<And>xa y. R xa y \<Longrightarrow> sets (distr (K.T xa) (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
 3. \<And>xa y. R xa y \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (L y). \<exists>x ya. y = ya \<and> M' y = distr (K.T x) (stream_space (count_space UNIV)) (smap f) \<and> R x ya) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (K.T xa) (stream_space (count_space UNIV)) (smap f) = measure_pmf (L y) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
have **: "y' \<in> L y \<Longrightarrow> R (g y') y'" for y'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y' \<in> set_pmf (L y) \<Longrightarrow> R (g y') y'
[PROOF STEP]
using *[of y']
[PROOF STATE]
proof (prove)
using this:
y' \<in> set_pmf (L y) \<Longrightarrow> \<exists>x'\<in>set_pmf (K x). R x' y'

goal (1 subgoal):
 1. y' \<in> set_pmf (L y) \<Longrightarrow> R (g y') y'
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
using this:
y' \<in> set_pmf (L y) \<Longrightarrow> \<exists>x'\<in>set_pmf (K x). R x' y'

goal (1 subgoal):
 1. y' \<in> set_pmf (L y) \<Longrightarrow> R (SOME s. R s y') y'
[PROOF STEP]
by (auto intro: someI)
[PROOF STATE]
proof (state)
this:
?y'1 \<in> set_pmf (L y) \<Longrightarrow> R (g ?y'1) ?y'1

goal (3 subgoals):
 1. \<And>xa y. R xa y \<Longrightarrow> prob_space (distr (K.T xa) (stream_space (count_space UNIV)) (smap f))
 2. \<And>xa y. R xa y \<Longrightarrow> sets (distr (K.T xa) (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
 3. \<And>xa y. R xa y \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (L y). \<exists>x ya. y = ya \<and> M' y = distr (K.T x) (stream_space (count_space UNIV)) (smap f) \<and> R x ya) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (K.T xa) (stream_space (count_space UNIV)) (smap f) = measure_pmf (L y) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
have D_SCons_eq_D_D: "distr (K.T i) K.S (\<lambda>x. z ## smap f x) = distr (?D i) K.S (\<lambda>x. z ## x)" for i z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distr (K.T i) (stream_space (count_space UNIV)) (\<lambda>x. z ## smap f x) = distr (distr (K.T i) (stream_space (count_space UNIV)) (smap f)) (stream_space (count_space UNIV)) ((##) z)
[PROOF STEP]
by (subst distr_distr) (auto simp: comp_def)
[PROOF STATE]
proof (state)
this:
distr (K.T ?i1) (stream_space (count_space UNIV)) (\<lambda>x. ?z1 ## smap f x) = distr (distr (K.T ?i1) (stream_space (count_space UNIV)) (smap f)) (stream_space (count_space UNIV)) ((##) ?z1)

goal (3 subgoals):
 1. \<And>xa y. R xa y \<Longrightarrow> prob_space (distr (K.T xa) (stream_space (count_space UNIV)) (smap f))
 2. \<And>xa y. R xa y \<Longrightarrow> sets (distr (K.T xa) (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
 3. \<And>xa y. R xa y \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (L y). \<exists>x ya. y = ya \<and> M' y = distr (K.T x) (stream_space (count_space UNIV)) (smap f) \<and> R x ya) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (K.T xa) (stream_space (count_space UNIV)) (smap f) = measure_pmf (L y) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
have D_eq_D_gi: "?D i = ?D (g (f i))" if i: "i \<in> K x" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distr (K.T i) (stream_space (count_space UNIV)) (smap f) = distr (K.T (g (f i))) (stream_space (count_space UNIV)) (smap f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distr (K.T i) (stream_space (count_space UNIV)) (smap f) = distr (K.T (g (f i))) (stream_space (count_space UNIV)) (smap f)
[PROOF STEP]
obtain j where "j \<in> L y" "R i j" "f i = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j. \<lbrakk>j \<in> set_pmf (L y); R i j; f i = j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Kx_Ly i
[PROOF STATE]
proof (prove)
using this:
rel_pmf R (K x) (L y)
i \<in> set_pmf (K x)

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>j \<in> set_pmf (L y); R i j; f i = j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (force dest!: rel_pmf_imp_rel_set simp: rel_set_def R_def)
[PROOF STATE]
proof (state)
this:
j \<in> set_pmf (L y)
R i j
f i = j

goal (1 subgoal):
 1. distr (K.T i) (stream_space (count_space UNIV)) (smap f) = distr (K.T (g (f i))) (stream_space (count_space UNIV)) (smap f)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j \<in> set_pmf (L y)
R i j
f i = j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
j \<in> set_pmf (L y)
R i j
f i = j

goal (1 subgoal):
 1. distr (K.T i) (stream_space (count_space UNIV)) (smap f) = distr (K.T (g (f i))) (stream_space (count_space UNIV)) (smap f)
[PROOF STEP]
by (auto intro!: D_eq_D[OF \<open>R i j\<close>] g)
[PROOF STATE]
proof (state)
this:
distr (K.T i) (stream_space (count_space UNIV)) (smap f) = distr (K.T (g (f i))) (stream_space (count_space UNIV)) (smap f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i1 \<in> set_pmf (K x) \<Longrightarrow> distr (K.T ?i1) (stream_space (count_space UNIV)) (smap f) = distr (K.T (g (f ?i1))) (stream_space (count_space UNIV)) (smap f)

goal (3 subgoals):
 1. \<And>xa y. R xa y \<Longrightarrow> prob_space (distr (K.T xa) (stream_space (count_space UNIV)) (smap f))
 2. \<And>xa y. R xa y \<Longrightarrow> sets (distr (K.T xa) (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
 3. \<And>xa y. R xa y \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (L y). \<exists>x ya. y = ya \<and> M' y = distr (K.T x) (stream_space (count_space UNIV)) (smap f) \<and> R x ya) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (K.T xa) (stream_space (count_space UNIV)) (smap f) = measure_pmf (L y) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
have ***: "?D x = measure_pmf (L y) \<bind> (\<lambda>y. distr (?D (g y)) K.S ((##) y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distr (K.T x) (stream_space (count_space UNIV)) (smap f) = measure_pmf (L y) \<bind> (\<lambda>y. distr (distr (K.T (g y)) (stream_space (count_space UNIV)) (smap f)) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
apply (subst K.T_eq_bind)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distr (measure_pmf (K x) \<bind> (\<lambda>t. distr (K.T t) (stream_space (count_space UNIV)) ((##) t))) (stream_space (count_space UNIV)) (smap f) = measure_pmf (L y) \<bind> (\<lambda>y. distr (distr (K.T (g y)) (stream_space (count_space UNIV)) (smap f)) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
apply (subst distr_bind[of _ _ K.S])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. measure_pmf.random_variable (K x) (subprob_algebra (stream_space (count_space UNIV))) (\<lambda>t. distr (K.T t) (stream_space (count_space UNIV)) ((##) t))
 2. space (measure_pmf (K x)) \<noteq> {}
 3. smap f \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 4. measure_pmf (K x) \<bind> (\<lambda>x. distr (distr (K.T x) (stream_space (count_space UNIV)) ((##) x)) (stream_space (count_space UNIV)) (smap f)) = measure_pmf (L y) \<bind> (\<lambda>y. distr (distr (K.T (g y)) (stream_space (count_space UNIV)) (smap f)) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
apply (rule measurable_distr2[of _  _ "K.S"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. (\<lambda>(x, y). x ## y) \<in> measure_pmf (K x) \<Otimes>\<^sub>M stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 2. measure_pmf.random_variable (K x) (subprob_algebra (stream_space (count_space UNIV))) K.T
 3. space (measure_pmf (K x)) \<noteq> {}
 4. smap f \<in> stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 5. measure_pmf (K x) \<bind> (\<lambda>x. distr (distr (K.T x) (stream_space (count_space UNIV)) ((##) x)) (stream_space (count_space UNIV)) (smap f)) = measure_pmf (L y) \<bind> (\<lambda>y. distr (distr (K.T (g y)) (stream_space (count_space UNIV)) (smap f)) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
apply (simp_all add: Pi_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf (K x) \<bind> (\<lambda>x. distr (distr (K.T x) (stream_space (count_space UNIV)) ((##) x)) (stream_space (count_space UNIV)) (smap f)) = measure_pmf (L y) \<bind> (\<lambda>y. distr (distr (K.T (g y)) (stream_space (count_space UNIV)) (smap f)) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
apply (simp add: distr_distr comp_def L_eq[OF cont] map_pmf_rep_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf (K x) \<bind> (\<lambda>x. distr (K.T x) (stream_space (count_space UNIV)) (\<lambda>xa. f x ## smap f xa)) = distr (measure_pmf (K x)) (count_space UNIV) f \<bind> (\<lambda>y. distr (K.T (g y)) (stream_space (count_space UNIV)) (\<lambda>x. y ## smap f x))
[PROOF STEP]
apply (subst bind_distr[where K=K.S])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. measure_pmf.random_variable (K x) (count_space UNIV) f
 2. (\<lambda>y. distr (K.T (g y)) (stream_space (count_space UNIV)) (\<lambda>x. y ## smap f x)) \<in> count_space UNIV \<rightarrow>\<^sub>M subprob_algebra (stream_space (count_space UNIV))
 3. space (measure_pmf (K x)) \<noteq> {}
 4. measure_pmf (K x) \<bind> (\<lambda>x. distr (K.T x) (stream_space (count_space UNIV)) (\<lambda>xa. f x ## smap f xa)) = measure_pmf (K x) \<bind> (\<lambda>x. distr (K.T (g (f x))) (stream_space (count_space UNIV)) (\<lambda>xa. f x ## smap f xa))
[PROOF STEP]
apply measurable []
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (\<lambda>y. distr (K.T (g y)) (stream_space (count_space UNIV)) (\<lambda>x. y ## smap f x)) \<in> count_space UNIV \<rightarrow>\<^sub>M subprob_algebra (stream_space (count_space UNIV))
 2. space (measure_pmf (K x)) \<noteq> {}
 3. measure_pmf (K x) \<bind> (\<lambda>x. distr (K.T x) (stream_space (count_space UNIV)) (\<lambda>xa. f x ## smap f xa)) = measure_pmf (K x) \<bind> (\<lambda>x. distr (K.T (g (f x))) (stream_space (count_space UNIV)) (\<lambda>xa. f x ## smap f xa))
[PROOF STEP]
apply (rule measurable_distr2[of _  _ "K.S"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (\<lambda>(xa, x). xa ## smap f x) \<in> count_space UNIV \<Otimes>\<^sub>M stream_space (count_space UNIV) \<rightarrow>\<^sub>M stream_space (count_space UNIV)
 2. (\<lambda>x. K.T (g x)) \<in> count_space UNIV \<rightarrow>\<^sub>M subprob_algebra (stream_space (count_space UNIV))
 3. space (measure_pmf (K x)) \<noteq> {}
 4. measure_pmf (K x) \<bind> (\<lambda>x. distr (K.T x) (stream_space (count_space UNIV)) (\<lambda>xa. f x ## smap f xa)) = measure_pmf (K x) \<bind> (\<lambda>x. distr (K.T (g (f x))) (stream_space (count_space UNIV)) (\<lambda>xa. f x ## smap f xa))
[PROOF STEP]
apply measurable []
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (\<lambda>x. K.T (g x)) \<in> count_space UNIV \<rightarrow>\<^sub>M subprob_algebra (stream_space (count_space UNIV))
 2. space (measure_pmf (K x)) \<noteq> {}
 3. measure_pmf (K x) \<bind> (\<lambda>x. distr (K.T x) (stream_space (count_space UNIV)) (\<lambda>xa. f x ## smap f xa)) = measure_pmf (K x) \<bind> (\<lambda>x. distr (K.T (g (f x))) (stream_space (count_space UNIV)) (\<lambda>xa. f x ## smap f xa))
[PROOF STEP]
apply (rule measurable_compose[OF measurable_g])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. K.T \<in> count_space UNIV \<rightarrow>\<^sub>M subprob_algebra (stream_space (count_space UNIV))
 2. space (measure_pmf (K x)) \<noteq> {}
 3. measure_pmf (K x) \<bind> (\<lambda>x. distr (K.T x) (stream_space (count_space UNIV)) (\<lambda>xa. f x ## smap f xa)) = measure_pmf (K x) \<bind> (\<lambda>x. distr (K.T (g (f x))) (stream_space (count_space UNIV)) (\<lambda>xa. f x ## smap f xa))
[PROOF STEP]
apply measurable []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. space (measure_pmf (K x)) \<noteq> {}
 2. measure_pmf (K x) \<bind> (\<lambda>x. distr (K.T x) (stream_space (count_space UNIV)) (\<lambda>xa. f x ## smap f xa)) = measure_pmf (K x) \<bind> (\<lambda>x. distr (K.T (g (f x))) (stream_space (count_space UNIV)) (\<lambda>xa. f x ## smap f xa))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf (K x) \<bind> (\<lambda>x. distr (K.T x) (stream_space (count_space UNIV)) (\<lambda>xa. f x ## smap f xa)) = measure_pmf (K x) \<bind> (\<lambda>x. distr (K.T (g (f x))) (stream_space (count_space UNIV)) (\<lambda>xa. f x ## smap f xa))
[PROOF STEP]
apply (rule bind_measure_pmf_cong[where N="K.S"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. distr (K.T x) (stream_space (count_space UNIV)) (\<lambda>xa. f x ## smap f xa) \<in> space (subprob_algebra (stream_space (count_space UNIV)))
 2. \<And>x. distr (K.T (g (f x))) (stream_space (count_space UNIV)) (\<lambda>xa. f x ## smap f xa) \<in> space (subprob_algebra (stream_space (count_space UNIV)))
 3. \<And>i. i \<in> set_pmf (K x) \<Longrightarrow> distr (K.T i) (stream_space (count_space UNIV)) (\<lambda>x. f i ## smap f x) = distr (K.T (g (f i))) (stream_space (count_space UNIV)) (\<lambda>x. f i ## smap f x)
[PROOF STEP]
apply (auto simp: space_subprob_algebra space_stream_space intro!: K.T.subprob_space_distr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> set_pmf (K x) \<Longrightarrow> distr (K.T i) (stream_space (count_space UNIV)) (\<lambda>x. f i ## smap f x) = distr (K.T (g (f i))) (stream_space (count_space UNIV)) (\<lambda>x. f i ## smap f x)
[PROOF STEP]
unfolding D_SCons_eq_D_D D_eq_D_gi
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> set_pmf (K x) \<Longrightarrow> distr (distr (K.T (g (f i))) (stream_space (count_space UNIV)) (smap f)) (stream_space (count_space UNIV)) ((##) (f i)) = distr (distr (K.T (g (f i))) (stream_space (count_space UNIV)) (smap f)) (stream_space (count_space UNIV)) ((##) (f i))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
distr (K.T x) (stream_space (count_space UNIV)) (smap f) = measure_pmf (L y) \<bind> (\<lambda>y. distr (distr (K.T (g y)) (stream_space (count_space UNIV)) (smap f)) (stream_space (count_space UNIV)) ((##) y))

goal (3 subgoals):
 1. \<And>xa y. R xa y \<Longrightarrow> prob_space (distr (K.T xa) (stream_space (count_space UNIV)) (smap f))
 2. \<And>xa y. R xa y \<Longrightarrow> sets (distr (K.T xa) (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
 3. \<And>xa y. R xa y \<Longrightarrow> \<exists>M'. (\<forall>y\<in>set_pmf (L y). \<exists>x ya. y = ya \<and> M' y = distr (K.T x) (stream_space (count_space UNIV)) (smap f) \<and> R x ya) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (K.T xa) (stream_space (count_space UNIV)) (smap f) = measure_pmf (L y) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>M'. (\<forall>y\<in>set_pmf (L y). \<exists>x ya. y = ya \<and> M' y = distr (K.T x) (stream_space (count_space UNIV)) (smap f) \<and> R x ya) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (K.T x) (stream_space (count_space UNIV)) (smap f) = measure_pmf (L y) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))
[PROOF STEP]
by (intro exI[of _ "\<lambda>t. distr (K.T (g t)) (stream_space (count_space UNIV)) (smap f)"])
         (auto simp add: K.T.prob_space_distr *** dest: **)
[PROOF STATE]
proof (state)
this:
\<exists>M'. (\<forall>y\<in>set_pmf (L y). \<exists>x ya. y = ya \<and> M' y = distr (K.T x) (stream_space (count_space UNIV)) (smap f) \<and> R x ya) \<and> (\<forall>y. sets (M' y) = sets (stream_space (count_space UNIV)) \<and> prob_space (M' y)) \<and> distr (K.T x) (stream_space (count_space UNIV)) (smap f) = measure_pmf (L y) \<bind> (\<lambda>y. distr (M' y) (stream_space (count_space UNIV)) ((##) y))

goal (2 subgoals):
 1. \<And>xa y. R xa y \<Longrightarrow> prob_space (distr (K.T xa) (stream_space (count_space UNIV)) (smap f))
 2. \<And>xa y. R xa y \<Longrightarrow> sets (distr (K.T xa) (stream_space (count_space UNIV)) (smap f)) = sets (stream_space (count_space UNIV))
[PROOF STEP]
qed (auto intro: K.T.prob_space_distr)
[PROOF STATE]
proof (state)
this:
L.T y = distr (K.T x) (stream_space (count_space UNIV)) (smap f)

goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
have "stream_all2 R s t \<longleftrightarrow> (s \<in> streams S \<and> smap f s = t)" for s t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stream_all2 R s t = (s \<in> streams S \<and> smap f s = t)
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. stream_all2 R s t \<Longrightarrow> s \<in> streams S
 2. stream_all2 R s t \<Longrightarrow> smap f s = t
 3. \<lbrakk>s \<in> streams S; t = smap f s\<rbrakk> \<Longrightarrow> stream_all2 (\<lambda>x y. R x (f y)) s s
[PROOF STEP]
show "stream_all2 R s t \<Longrightarrow> s \<in> streams S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stream_all2 R s t \<Longrightarrow> s \<in> streams S
[PROOF STEP]
apply (coinduction arbitrary: s t)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s t. stream_all2 R s t \<Longrightarrow> \<exists>a sa. s = a ## sa \<and> a \<in> S \<and> ((\<exists>s t. sa = s \<and> stream_all2 R s t) \<or> sa \<in> streams S)
[PROOF STEP]
subgoal for s t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stream_all2 R s t \<Longrightarrow> \<exists>a s. s = a ## s \<and> a \<in> S \<and> ((\<exists>sa t. s = sa \<and> stream_all2 R sa t) \<or> s \<in> streams S)
[PROOF STEP]
by (cases s; cases t) (auto simp: R_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
stream_all2 R s t \<Longrightarrow> s \<in> streams S

goal (2 subgoals):
 1. stream_all2 R s t \<Longrightarrow> smap f s = t
 2. \<lbrakk>s \<in> streams S; t = smap f s\<rbrakk> \<Longrightarrow> stream_all2 (\<lambda>x y. R x (f y)) s s
[PROOF STEP]
show "stream_all2 R s t \<Longrightarrow> smap f s = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stream_all2 R s t \<Longrightarrow> smap f s = t
[PROOF STEP]
apply (coinduction arbitrary: s t rule: stream.coinduct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s t. stream_all2 R s t \<Longrightarrow> shd (smap f s) = shd t \<and> (\<exists>sa ta. stl (smap f s) = smap f sa \<and> stl t = ta \<and> stream_all2 R sa ta)
[PROOF STEP]
subgoal for s t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stream_all2 R s t \<Longrightarrow> shd (smap f s) = shd t \<and> (\<exists>s t. stl (smap f s) = smap f s \<and> stl t = t \<and> stream_all2 R s t)
[PROOF STEP]
by (cases s; cases t) (auto simp: R_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
stream_all2 R s t \<Longrightarrow> smap f s = t

goal (1 subgoal):
 1. \<lbrakk>s \<in> streams S; t = smap f s\<rbrakk> \<Longrightarrow> stream_all2 (\<lambda>x y. R x (f y)) s s
[PROOF STEP]
qed (auto intro!: stream.rel_refl_strong simp: stream.rel_map R_def streams_iff_sset)
[PROOF STATE]
proof (state)
this:
stream_all2 R ?s1 ?t1 = (?s1 \<in> streams S \<and> smap f ?s1 = ?t1)

goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
stream_all2 R ?s1 ?t1 = (?s1 \<in> streams S \<and> smap f ?s1 = ?t1)
[PROOF STEP]
have "\<omega> \<in> streams S \<Longrightarrow> \<omega> \<in> A \<longleftrightarrow> smap f \<omega> \<in> B" for \<omega>
[PROOF STATE]
proof (prove)
using this:
stream_all2 R ?s1 ?t1 = (?s1 \<in> streams S \<and> smap f ?s1 = ?t1)

goal (1 subgoal):
 1. \<omega> \<in> streams S \<Longrightarrow> (\<omega> \<in> A) = (smap f \<omega> \<in> B)
[PROOF STEP]
using AB
[PROOF STATE]
proof (prove)
using this:
stream_all2 R ?s1 ?t1 = (?s1 \<in> streams S \<and> smap f ?s1 = ?t1)
PTA.rel_set_strong (stream_all2 R) A B

goal (1 subgoal):
 1. \<omega> \<in> streams S \<Longrightarrow> (\<omega> \<in> A) = (smap f \<omega> \<in> B)
[PROOF STEP]
by (auto simp: rel_set_strong_def)
[PROOF STATE]
proof (state)
this:
?\<omega>1 \<in> streams S \<Longrightarrow> (?\<omega>1 \<in> A) = (smap f ?\<omega>1 \<in> B)

goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
with in_S
[PROOF STATE]
proof (chain)
picking this:
AE \<omega> in K.T x. \<omega> \<in> streams S
?\<omega>1 \<in> streams S \<Longrightarrow> (?\<omega>1 \<in> A) = (smap f ?\<omega>1 \<in> B)
[PROOF STEP]
have "K.T x A = K.T x (smap f -` B \<inter> space (K.T x))"
[PROOF STATE]
proof (prove)
using this:
AE \<omega> in K.T x. \<omega> \<in> streams S
?\<omega>1 \<in> streams S \<Longrightarrow> (?\<omega>1 \<in> A) = (smap f ?\<omega>1 \<in> B)

goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (K.T x) (smap f -` B \<inter> space (K.T x))
[PROOF STEP]
by (auto intro!: emeasure_eq_AE streams_sets)
[PROOF STATE]
proof (state)
this:
emeasure (K.T x) A = emeasure (K.T x) (smap f -` B \<inter> space (K.T x))

goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
emeasure (K.T x) A = emeasure (K.T x) (smap f -` B \<inter> space (K.T x))

goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
have "\<dots> = (distr (K.T x) K.S (smap f)) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (K.T x) (smap f -` B \<inter> space (K.T x)) = emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) B
[PROOF STEP]
by (intro emeasure_distr[symmetric]) auto
[PROOF STATE]
proof (state)
this:
emeasure (K.T x) (smap f -` B \<inter> space (K.T x)) = emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) B

goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
emeasure (K.T x) (smap f -` B \<inter> space (K.T x)) = emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) B

goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
have "\<dots> = (L.T y) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) B = emeasure (L.T y) B
[PROOF STEP]
unfolding L_eq_D
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) B = emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) B
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
emeasure (distr (K.T x) (stream_space (count_space UNIV)) (smap f)) B = emeasure (L.T y) B

goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
emeasure (K.T x) A = emeasure (L.T y) B

goal (1 subgoal):
 1. emeasure (K.T x) A = emeasure (L.T y) B
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
emeasure (K.T x) A = emeasure (L.T y) B

goal:
No subgoals!
[PROOF STEP]
qed