[STATEMENT]
lemma index_update_vec1[simp]:
  assumes "i < dim_vec v" shows "(v |\<^sub>v i \<mapsto> a) $ i = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v |\<^sub>v i \<mapsto> a) $ i = a
[PROOF STEP]
unfolding update_vec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec (dim_vec v) (\<lambda>i'. if i' = i then a else v $ i') $ i = a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < dim_vec v

goal (1 subgoal):
 1. vec (dim_vec v) (\<lambda>i'. if i' = i then a else v $ i') $ i = a
[PROOF STEP]
by simp


[STATEMENT]
lemma AAss_\<tau>red0t_xt2:
  "\<tau>red0t extTA P t h (i, xs) (i', xs') \<Longrightarrow> \<tau>red0t extTA P t h (Val a\<lfloor>i\<rceil> := e, xs) (Val a\<lfloor>i'\<rceil> := e, xs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>red0t extTA P t h (i, xs) (i', xs') \<Longrightarrow> \<tau>red0t extTA P t h (Val a\<lfloor>i\<rceil> := e, xs) (Val a\<lfloor>i'\<rceil> := e, xs')
[PROOF STEP]
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAssRed2)


[STATEMENT]
lemma omega_denest [simp]: "(x + y)\<^sup>\<omega> = (x\<^sup>\<star> \<cdot> y)\<^sup>\<omega> + (x\<^sup>\<star> \<cdot> y)\<^sup>\<star> \<cdot> x\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x + y)\<^sup>\<omega> = (x\<^sup>\<star> \<cdot> y)\<^sup>\<omega> + (x\<^sup>\<star> \<cdot> y)\<^sup>\<star> \<cdot> x\<^sup>\<omega>
[PROOF STEP]
proof (rule order.antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (x + y)\<^sup>\<omega> \<le> (x\<^sup>\<star> \<cdot> y)\<^sup>\<omega> + (x\<^sup>\<star> \<cdot> y)\<^sup>\<star> \<cdot> x\<^sup>\<omega>
 2. (x\<^sup>\<star> \<cdot> y)\<^sup>\<omega> + (x\<^sup>\<star> \<cdot> y)\<^sup>\<star> \<cdot> x\<^sup>\<omega> \<le> (x + y)\<^sup>\<omega>
[PROOF STEP]
show "(x + y)\<^sup>\<omega> \<le> (x\<^sup>\<star> \<cdot> y)\<^sup>\<omega> + (x\<^sup>\<star> \<cdot> y)\<^sup>\<star> \<cdot> x\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x + y)\<^sup>\<omega> \<le> (x\<^sup>\<star> \<cdot> y)\<^sup>\<omega> + (x\<^sup>\<star> \<cdot> y)\<^sup>\<star> \<cdot> x\<^sup>\<omega>
[PROOF STEP]
by (rule omega_sum_unfold_coind)
[PROOF STATE]
proof (state)
this:
(x + y)\<^sup>\<omega> \<le> (x\<^sup>\<star> \<cdot> y)\<^sup>\<omega> + (x\<^sup>\<star> \<cdot> y)\<^sup>\<star> \<cdot> x\<^sup>\<omega>

goal (1 subgoal):
 1. (x\<^sup>\<star> \<cdot> y)\<^sup>\<omega> + (x\<^sup>\<star> \<cdot> y)\<^sup>\<star> \<cdot> x\<^sup>\<omega> \<le> (x + y)\<^sup>\<omega>
[PROOF STEP]
have "(x\<^sup>\<star> \<cdot> y)\<^sup>\<omega> \<le>  (x + y)\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>\<star> \<cdot> y)\<^sup>\<omega> \<le> (x + y)\<^sup>\<omega>
[PROOF STEP]
by (rule wagner_1_var_gen)
[PROOF STATE]
proof (state)
this:
(x\<^sup>\<star> \<cdot> y)\<^sup>\<omega> \<le> (x + y)\<^sup>\<omega>

goal (1 subgoal):
 1. (x\<^sup>\<star> \<cdot> y)\<^sup>\<omega> + (x\<^sup>\<star> \<cdot> y)\<^sup>\<star> \<cdot> x\<^sup>\<omega> \<le> (x + y)\<^sup>\<omega>
[PROOF STEP]
hence "(x\<^sup>\<star> \<cdot> y)\<^sup>\<star> \<cdot> x\<^sup>\<omega> \<le> (x + y)\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
using this:
(x\<^sup>\<star> \<cdot> y)\<^sup>\<omega> \<le> (x + y)\<^sup>\<omega>

goal (1 subgoal):
 1. (x\<^sup>\<star> \<cdot> y)\<^sup>\<star> \<cdot> x\<^sup>\<omega> \<le> (x + y)\<^sup>\<omega>
[PROOF STEP]
by (simp add: omega_sum_unfold_ind)
[PROOF STATE]
proof (state)
this:
(x\<^sup>\<star> \<cdot> y)\<^sup>\<star> \<cdot> x\<^sup>\<omega> \<le> (x + y)\<^sup>\<omega>

goal (1 subgoal):
 1. (x\<^sup>\<star> \<cdot> y)\<^sup>\<omega> + (x\<^sup>\<star> \<cdot> y)\<^sup>\<star> \<cdot> x\<^sup>\<omega> \<le> (x + y)\<^sup>\<omega>
[PROOF STEP]
thus "(x\<^sup>\<star> \<cdot> y)\<^sup>\<omega> + (x\<^sup>\<star> \<cdot> y)\<^sup>\<star> \<cdot> x\<^sup>\<omega> \<le> (x + y)\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
using this:
(x\<^sup>\<star> \<cdot> y)\<^sup>\<star> \<cdot> x\<^sup>\<omega> \<le> (x + y)\<^sup>\<omega>

goal (1 subgoal):
 1. (x\<^sup>\<star> \<cdot> y)\<^sup>\<omega> + (x\<^sup>\<star> \<cdot> y)\<^sup>\<star> \<cdot> x\<^sup>\<omega> \<le> (x + y)\<^sup>\<omega>
[PROOF STEP]
by (simp add: wagner_1_var_gen)
[PROOF STATE]
proof (state)
this:
(x\<^sup>\<star> \<cdot> y)\<^sup>\<omega> + (x\<^sup>\<star> \<cdot> y)\<^sup>\<star> \<cdot> x\<^sup>\<omega> \<le> (x + y)\<^sup>\<omega>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma PO_m3_refines_init_m2 [iff]:
  "init m3 \<subseteq> R23``(init m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init m3 \<subseteq> R23 `` init m2
[PROOF STEP]
by (auto simp add: R23_def m3_defs intro!: R23_intros)


[STATEMENT]
lemma parts_Un [simp]: "parts (G \<union> H) = parts G \<union> parts H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (G \<union> H) = parts G \<union> parts H
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. parts (G \<union> H) \<subseteq> parts G \<union> parts H
 2. parts G \<union> parts H \<subseteq> parts (G \<union> H)
[PROOF STEP]
show "parts (G \<union> H) \<subseteq> parts G \<union> parts H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (G \<union> H) \<subseteq> parts G \<union> parts H
[PROOF STEP]
by (rule, erule parts.induct) (auto)
[PROOF STATE]
proof (state)
this:
parts (G \<union> H) \<subseteq> parts G \<union> parts H

goal (1 subgoal):
 1. parts G \<union> parts H \<subseteq> parts (G \<union> H)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. parts G \<union> parts H \<subseteq> parts (G \<union> H)
[PROOF STEP]
show "parts G \<union> parts H \<subseteq> parts (G \<union> H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts G \<union> parts H \<subseteq> parts (G \<union> H)
[PROOF STEP]
by (intro Un_least parts_mono Un_upper1 Un_upper2)
[PROOF STATE]
proof (state)
this:
parts G \<union> parts H \<subseteq> parts (G \<union> H)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_ugraph_finite: "finite_graph G \<Longrightarrow> finite_graph (map_ugraph f G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_graph G \<Longrightarrow> finite_graph (map_ugraph f G)
[PROOF STEP]
unfolding finite_graph_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (uverts G) \<and> finite (uedges G) \<Longrightarrow> finite (uverts (map_ugraph f G)) \<and> finite (uedges (map_ugraph f G))
[PROOF STEP]
by (metis finite_imageI fst_conv map_ugraph.simps snd_conv surjective_pairing)


[STATEMENT]
lemma add_shift_minus:
  assumes ab: "nonsingular a b"
  and p\<^sub>1: "on_curve a b p\<^sub>1"
  and p\<^sub>2: "on_curve a b p\<^sub>2"
  and p\<^sub>3: "on_curve a b p\<^sub>3"
  and eq: "add a p\<^sub>1 p\<^sub>2 = p\<^sub>3"
  shows "p\<^sub>1 = add a p\<^sub>3 (opp p\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p\<^sub>1 = ell_field_class.add a p\<^sub>3 (opp p\<^sub>2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p\<^sub>1 = ell_field_class.add a p\<^sub>3 (opp p\<^sub>2)
[PROOF STEP]
note eq
[PROOF STATE]
proof (state)
this:
ell_field_class.add a p\<^sub>1 p\<^sub>2 = p\<^sub>3

goal (1 subgoal):
 1. p\<^sub>1 = ell_field_class.add a p\<^sub>3 (opp p\<^sub>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ell_field_class.add a p\<^sub>1 p\<^sub>2 = p\<^sub>3

goal (1 subgoal):
 1. p\<^sub>1 = ell_field_class.add a p\<^sub>3 (opp p\<^sub>2)
[PROOF STEP]
from add_minus_id [OF ab p\<^sub>3 opp_closed [OF p\<^sub>2]] p\<^sub>2
[PROOF STATE]
proof (chain)
picking this:
ell_field_class.add a (ell_field_class.add a p\<^sub>3 (opp p\<^sub>2)) (opp (opp p\<^sub>2)) = p\<^sub>3
on_curve a b p\<^sub>2
[PROOF STEP]
have "p\<^sub>3 = add a (add a p\<^sub>3 (opp p\<^sub>2)) p\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
ell_field_class.add a (ell_field_class.add a p\<^sub>3 (opp p\<^sub>2)) (opp (opp p\<^sub>2)) = p\<^sub>3
on_curve a b p\<^sub>2

goal (1 subgoal):
 1. p\<^sub>3 = ell_field_class.add a (ell_field_class.add a p\<^sub>3 (opp p\<^sub>2)) p\<^sub>2
[PROOF STEP]
by (simp add: opp_opp)
[PROOF STATE]
proof (state)
this:
p\<^sub>3 = ell_field_class.add a (ell_field_class.add a p\<^sub>3 (opp p\<^sub>2)) p\<^sub>2

goal (1 subgoal):
 1. p\<^sub>1 = ell_field_class.add a p\<^sub>3 (opp p\<^sub>2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ell_field_class.add a p\<^sub>1 p\<^sub>2 = ell_field_class.add a (ell_field_class.add a p\<^sub>3 (opp p\<^sub>2)) p\<^sub>2
[PROOF STEP]
have "add a p\<^sub>2 p\<^sub>1 = add a p\<^sub>2 (add a p\<^sub>3 (opp p\<^sub>2))"
[PROOF STATE]
proof (prove)
using this:
ell_field_class.add a p\<^sub>1 p\<^sub>2 = ell_field_class.add a (ell_field_class.add a p\<^sub>3 (opp p\<^sub>2)) p\<^sub>2

goal (1 subgoal):
 1. ell_field_class.add a p\<^sub>2 p\<^sub>1 = ell_field_class.add a p\<^sub>2 (ell_field_class.add a p\<^sub>3 (opp p\<^sub>2))
[PROOF STEP]
using p\<^sub>1 p\<^sub>2 p\<^sub>3
[PROOF STATE]
proof (prove)
using this:
ell_field_class.add a p\<^sub>1 p\<^sub>2 = ell_field_class.add a (ell_field_class.add a p\<^sub>3 (opp p\<^sub>2)) p\<^sub>2
on_curve a b p\<^sub>1
on_curve a b p\<^sub>2
on_curve a b p\<^sub>3

goal (1 subgoal):
 1. ell_field_class.add a p\<^sub>2 p\<^sub>1 = ell_field_class.add a p\<^sub>2 (ell_field_class.add a p\<^sub>3 (opp p\<^sub>2))
[PROOF STEP]
by (simp add: add_comm [of a b] add_closed opp_closed)
[PROOF STATE]
proof (state)
this:
ell_field_class.add a p\<^sub>2 p\<^sub>1 = ell_field_class.add a p\<^sub>2 (ell_field_class.add a p\<^sub>3 (opp p\<^sub>2))

goal (1 subgoal):
 1. p\<^sub>1 = ell_field_class.add a p\<^sub>3 (opp p\<^sub>2)
[PROOF STEP]
with ab p\<^sub>2 p\<^sub>1 add_closed [OF p\<^sub>3 opp_closed [OF p\<^sub>2]]
[PROOF STATE]
proof (chain)
picking this:
nonsingular a b
on_curve a b p\<^sub>2
on_curve a b p\<^sub>1
on_curve a b (ell_field_class.add a p\<^sub>3 (opp p\<^sub>2))
ell_field_class.add a p\<^sub>2 p\<^sub>1 = ell_field_class.add a p\<^sub>2 (ell_field_class.add a p\<^sub>3 (opp p\<^sub>2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nonsingular a b
on_curve a b p\<^sub>2
on_curve a b p\<^sub>1
on_curve a b (ell_field_class.add a p\<^sub>3 (opp p\<^sub>2))
ell_field_class.add a p\<^sub>2 p\<^sub>1 = ell_field_class.add a p\<^sub>2 (ell_field_class.add a p\<^sub>3 (opp p\<^sub>2))

goal (1 subgoal):
 1. p\<^sub>1 = ell_field_class.add a p\<^sub>3 (opp p\<^sub>2)
[PROOF STEP]
by (rule cancel)
[PROOF STATE]
proof (state)
this:
p\<^sub>1 = ell_field_class.add a p\<^sub>3 (opp p\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma neutralI[intro]:
  "(\<And>P P' x y z w.
    \<lbrakk> profile A Is P; profile A Is P'; {x,y,z,w} \<subseteq> A;
      \<And>i. i \<in> Is \<Longrightarrow> x \<^bsub>(P i)\<^esub>\<preceq> y \<longleftrightarrow> z \<^bsub>(P' i)\<^esub>\<preceq> w;
      \<And>i. i \<in> Is \<Longrightarrow> y \<^bsub>(P i)\<^esub>\<preceq> x \<longleftrightarrow> w \<^bsub>(P' i)\<^esub>\<preceq> z \<rbrakk>
     \<Longrightarrow> ((x \<^bsub>(scf P)\<^esub>\<preceq> y \<longleftrightarrow> z \<^bsub>(scf P')\<^esub>\<preceq> w) \<and> (y \<^bsub>(scf P)\<^esub>\<preceq> x \<longleftrightarrow> w \<^bsub>(scf P')\<^esub>\<preceq> z)))
  \<Longrightarrow> neutral scf A Is"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P P' x y z w. \<lbrakk>profile A Is P; profile A Is P'; {x, y, z, w} \<subseteq> A; \<And>i. i \<in> Is \<Longrightarrow> (x \<^bsub>(P i)\<^esub>\<preceq> y) = (z \<^bsub>(P' i)\<^esub>\<preceq> w); \<And>i. i \<in> Is \<Longrightarrow> (y \<^bsub>(P i)\<^esub>\<preceq> x) = (w \<^bsub>(P' i)\<^esub>\<preceq> z)\<rbrakk> \<Longrightarrow> (x \<^bsub>(scf P)\<^esub>\<preceq> y) = (z \<^bsub>(scf P')\<^esub>\<preceq> w) \<and> (y \<^bsub>(scf P)\<^esub>\<preceq> x) = (w \<^bsub>(scf P')\<^esub>\<preceq> z)) \<Longrightarrow> neutral scf A Is
[PROOF STEP]
unfolding neutral_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P P' x y z w. \<lbrakk>profile A Is P; profile A Is P'; {x, y, z, w} \<subseteq> A; \<And>i. i \<in> Is \<Longrightarrow> (x \<^bsub>(P i)\<^esub>\<preceq> y) = (z \<^bsub>(P' i)\<^esub>\<preceq> w); \<And>i. i \<in> Is \<Longrightarrow> (y \<^bsub>(P i)\<^esub>\<preceq> x) = (w \<^bsub>(P' i)\<^esub>\<preceq> z)\<rbrakk> \<Longrightarrow> (x \<^bsub>(scf P)\<^esub>\<preceq> y) = (z \<^bsub>(scf P')\<^esub>\<preceq> w) \<and> (y \<^bsub>(scf P)\<^esub>\<preceq> x) = (w \<^bsub>(scf P')\<^esub>\<preceq> z)) \<Longrightarrow> \<forall>P P' x y z w. profile A Is P \<and> profile A Is P' \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A \<and> w \<in> A \<and> (\<forall>i\<in>Is. (x \<^bsub>(P i)\<^esub>\<preceq> y) = (z \<^bsub>(P' i)\<^esub>\<preceq> w)) \<and> (\<forall>i\<in>Is. (y \<^bsub>(P i)\<^esub>\<preceq> x) = (w \<^bsub>(P' i)\<^esub>\<preceq> z)) \<longrightarrow> (x \<^bsub>(scf P)\<^esub>\<preceq> y) = (z \<^bsub>(scf P')\<^esub>\<preceq> w) \<and> (y \<^bsub>(scf P)\<^esub>\<preceq> x) = (w \<^bsub>(scf P')\<^esub>\<preceq> z)
[PROOF STEP]
by simp


[STATEMENT]
lemma positively_responsiveD:
  "\<lbrakk> positively_responsive scf A Is;
     profile A Is P; profile A Is P'; x \<in> A; y \<in> A;
     \<And>i. \<lbrakk> i \<in> Is; x \<^bsub>(P i)\<^esub>\<prec> y \<rbrakk> \<Longrightarrow> x \<^bsub>(P' i)\<^esub>\<prec> y;
     \<And>i. \<lbrakk> i \<in> Is; x \<^bsub>(P i)\<^esub>\<approx> y \<rbrakk> \<Longrightarrow> x \<^bsub>(P' i)\<^esub>\<preceq> y;
     \<exists>k \<in> Is. (x \<^bsub>(P k)\<^esub>\<approx> y \<and> x \<^bsub>(P' k)\<^esub>\<prec> y) \<or> (y \<^bsub>(P k)\<^esub>\<prec> x \<and> x \<^bsub>(P' k)\<^esub>\<preceq> y);
     x \<^bsub>(scf P)\<^esub>\<preceq> y \<rbrakk>
       \<Longrightarrow> x \<^bsub>(scf P')\<^esub>\<prec> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>positively_responsive scf A Is; profile A Is P; profile A Is P'; x \<in> A; y \<in> A; \<And>i. \<lbrakk>i \<in> Is; x \<^bsub>(P i)\<^esub>\<prec> y\<rbrakk> \<Longrightarrow> x \<^bsub>(P' i)\<^esub>\<prec> y; \<And>i. \<lbrakk>i \<in> Is; x \<^bsub>(P i)\<^esub>\<approx> y\<rbrakk> \<Longrightarrow> x \<^bsub>(P' i)\<^esub>\<preceq> y; \<exists>k\<in>Is. x \<^bsub>(P k)\<^esub>\<approx> y \<and> x \<^bsub>(P' k)\<^esub>\<prec> y \<or> y \<^bsub>(P k)\<^esub>\<prec> x \<and> x \<^bsub>(P' k)\<^esub>\<preceq> y; x \<^bsub>(scf P)\<^esub>\<preceq> y\<rbrakk> \<Longrightarrow> x \<^bsub>(scf P')\<^esub>\<prec> y
[PROOF STEP]
unfolding positively_responsive_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>P P' x y. profile A Is P \<and> profile A Is P' \<and> x \<in> A \<and> y \<in> A \<and> (\<forall>i\<in>Is. (x \<^bsub>(P i)\<^esub>\<prec> y \<longrightarrow> x \<^bsub>(P' i)\<^esub>\<prec> y) \<and> (x \<^bsub>(P i)\<^esub>\<approx> y \<longrightarrow> x \<^bsub>(P' i)\<^esub>\<preceq> y)) \<and> (\<exists>k\<in>Is. x \<^bsub>(P k)\<^esub>\<approx> y \<and> x \<^bsub>(P' k)\<^esub>\<prec> y \<or> y \<^bsub>(P k)\<^esub>\<prec> x \<and> x \<^bsub>(P' k)\<^esub>\<preceq> y) \<longrightarrow> x \<^bsub>(scf P)\<^esub>\<preceq> y \<longrightarrow> x \<^bsub>(scf P')\<^esub>\<prec> y; profile A Is P; profile A Is P'; x \<in> A; y \<in> A; \<And>i. \<lbrakk>i \<in> Is; x \<^bsub>(P i)\<^esub>\<prec> y\<rbrakk> \<Longrightarrow> x \<^bsub>(P' i)\<^esub>\<prec> y; \<And>i. \<lbrakk>i \<in> Is; x \<^bsub>(P i)\<^esub>\<approx> y\<rbrakk> \<Longrightarrow> x \<^bsub>(P' i)\<^esub>\<preceq> y; \<exists>k\<in>Is. x \<^bsub>(P k)\<^esub>\<approx> y \<and> x \<^bsub>(P' k)\<^esub>\<prec> y \<or> y \<^bsub>(P k)\<^esub>\<prec> x \<and> x \<^bsub>(P' k)\<^esub>\<preceq> y; x \<^bsub>(scf P)\<^esub>\<preceq> y\<rbrakk> \<Longrightarrow> x \<^bsub>(scf P')\<^esub>\<prec> y
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>P P' x y. profile A Is P \<and> profile A Is P' \<and> x \<in> A \<and> y \<in> A \<and> (\<forall>i\<in>Is. (x \<^bsub>(P i)\<^esub>\<prec> y \<longrightarrow> x \<^bsub>(P' i)\<^esub>\<prec> y) \<and> (x \<^bsub>(P i)\<^esub>\<approx> y \<longrightarrow> x \<^bsub>(P' i)\<^esub>\<preceq> y)) \<and> (\<exists>k\<in>Is. x \<^bsub>(P k)\<^esub>\<approx> y \<and> x \<^bsub>(P' k)\<^esub>\<prec> y \<or> y \<^bsub>(P k)\<^esub>\<prec> x \<and> x \<^bsub>(P' k)\<^esub>\<preceq> y) \<longrightarrow> x \<^bsub>(scf P)\<^esub>\<preceq> y \<longrightarrow> x \<^bsub>(scf P')\<^esub>\<prec> y; profile A Is P; profile A Is P'; x \<in> A; y \<in> A; \<And>i. \<lbrakk>i \<in> Is; x \<^bsub>(P i)\<^esub>\<prec> y\<rbrakk> \<Longrightarrow> x \<^bsub>(P' i)\<^esub>\<prec> y; \<And>i. \<lbrakk>i \<in> Is; x \<^bsub>(P i)\<^esub>\<approx> y\<rbrakk> \<Longrightarrow> x \<^bsub>(P' i)\<^esub>\<preceq> y; x \<^bsub>(scf P)\<^esub>\<preceq> y; k \<in> Is; x \<^bsub>(P k)\<^esub>\<approx> y \<and> x \<^bsub>(P' k)\<^esub>\<prec> y \<or> y \<^bsub>(P k)\<^esub>\<prec> x \<and> x \<^bsub>(P' k)\<^esub>\<preceq> y\<rbrakk> \<Longrightarrow> x \<^bsub>(scf P')\<^esub>\<prec> y
[PROOF STEP]
apply (erule allE[where x=P])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>profile A Is P; profile A Is P'; x \<in> A; y \<in> A; \<And>i. \<lbrakk>i \<in> Is; x \<^bsub>(P i)\<^esub>\<prec> y\<rbrakk> \<Longrightarrow> x \<^bsub>(P' i)\<^esub>\<prec> y; \<And>i. \<lbrakk>i \<in> Is; x \<^bsub>(P i)\<^esub>\<approx> y\<rbrakk> \<Longrightarrow> x \<^bsub>(P' i)\<^esub>\<preceq> y; x \<^bsub>(scf P)\<^esub>\<preceq> y; k \<in> Is; x \<^bsub>(P k)\<^esub>\<approx> y \<and> x \<^bsub>(P' k)\<^esub>\<prec> y \<or> y \<^bsub>(P k)\<^esub>\<prec> x \<and> x \<^bsub>(P' k)\<^esub>\<preceq> y; \<forall>P' x y. profile A Is P \<and> profile A Is P' \<and> x \<in> A \<and> y \<in> A \<and> (\<forall>i\<in>Is. (x \<^bsub>(P i)\<^esub>\<prec> y \<longrightarrow> x \<^bsub>(P' i)\<^esub>\<prec> y) \<and> (x \<^bsub>(P i)\<^esub>\<approx> y \<longrightarrow> x \<^bsub>(P' i)\<^esub>\<preceq> y)) \<and> (\<exists>k\<in>Is. x \<^bsub>(P k)\<^esub>\<approx> y \<and> x \<^bsub>(P' k)\<^esub>\<prec> y \<or> y \<^bsub>(P k)\<^esub>\<prec> x \<and> x \<^bsub>(P' k)\<^esub>\<preceq> y) \<longrightarrow> x \<^bsub>(scf P)\<^esub>\<preceq> y \<longrightarrow> x \<^bsub>(scf P')\<^esub>\<prec> y\<rbrakk> \<Longrightarrow> x \<^bsub>(scf P')\<^esub>\<prec> y
[PROOF STEP]
apply (erule allE[where x=P'])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>profile A Is P; profile A Is P'; x \<in> A; y \<in> A; \<And>i. \<lbrakk>i \<in> Is; x \<^bsub>(P i)\<^esub>\<prec> y\<rbrakk> \<Longrightarrow> x \<^bsub>(P' i)\<^esub>\<prec> y; \<And>i. \<lbrakk>i \<in> Is; x \<^bsub>(P i)\<^esub>\<approx> y\<rbrakk> \<Longrightarrow> x \<^bsub>(P' i)\<^esub>\<preceq> y; x \<^bsub>(scf P)\<^esub>\<preceq> y; k \<in> Is; x \<^bsub>(P k)\<^esub>\<approx> y \<and> x \<^bsub>(P' k)\<^esub>\<prec> y \<or> y \<^bsub>(P k)\<^esub>\<prec> x \<and> x \<^bsub>(P' k)\<^esub>\<preceq> y; \<forall>x y. profile A Is P \<and> profile A Is P' \<and> x \<in> A \<and> y \<in> A \<and> (\<forall>i\<in>Is. (x \<^bsub>(P i)\<^esub>\<prec> y \<longrightarrow> x \<^bsub>(P' i)\<^esub>\<prec> y) \<and> (x \<^bsub>(P i)\<^esub>\<approx> y \<longrightarrow> x \<^bsub>(P' i)\<^esub>\<preceq> y)) \<and> (\<exists>k\<in>Is. x \<^bsub>(P k)\<^esub>\<approx> y \<and> x \<^bsub>(P' k)\<^esub>\<prec> y \<or> y \<^bsub>(P k)\<^esub>\<prec> x \<and> x \<^bsub>(P' k)\<^esub>\<preceq> y) \<longrightarrow> x \<^bsub>(scf P)\<^esub>\<preceq> y \<longrightarrow> x \<^bsub>(scf P')\<^esub>\<prec> y\<rbrakk> \<Longrightarrow> x \<^bsub>(scf P')\<^esub>\<prec> y
[PROOF STEP]
apply (erule allE[where x=x])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>profile A Is P; profile A Is P'; x \<in> A; y \<in> A; \<And>i. \<lbrakk>i \<in> Is; x \<^bsub>(P i)\<^esub>\<prec> y\<rbrakk> \<Longrightarrow> x \<^bsub>(P' i)\<^esub>\<prec> y; \<And>i. \<lbrakk>i \<in> Is; x \<^bsub>(P i)\<^esub>\<approx> y\<rbrakk> \<Longrightarrow> x \<^bsub>(P' i)\<^esub>\<preceq> y; x \<^bsub>(scf P)\<^esub>\<preceq> y; k \<in> Is; x \<^bsub>(P k)\<^esub>\<approx> y \<and> x \<^bsub>(P' k)\<^esub>\<prec> y \<or> y \<^bsub>(P k)\<^esub>\<prec> x \<and> x \<^bsub>(P' k)\<^esub>\<preceq> y; \<forall>y. profile A Is P \<and> profile A Is P' \<and> x \<in> A \<and> y \<in> A \<and> (\<forall>i\<in>Is. (x \<^bsub>(P i)\<^esub>\<prec> y \<longrightarrow> x \<^bsub>(P' i)\<^esub>\<prec> y) \<and> (x \<^bsub>(P i)\<^esub>\<approx> y \<longrightarrow> x \<^bsub>(P' i)\<^esub>\<preceq> y)) \<and> (\<exists>k\<in>Is. x \<^bsub>(P k)\<^esub>\<approx> y \<and> x \<^bsub>(P' k)\<^esub>\<prec> y \<or> y \<^bsub>(P k)\<^esub>\<prec> x \<and> x \<^bsub>(P' k)\<^esub>\<preceq> y) \<longrightarrow> x \<^bsub>(scf P)\<^esub>\<preceq> y \<longrightarrow> x \<^bsub>(scf P')\<^esub>\<prec> y\<rbrakk> \<Longrightarrow> x \<^bsub>(scf P')\<^esub>\<prec> y
[PROOF STEP]
apply (erule allE[where x=y])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>profile A Is P; profile A Is P'; x \<in> A; y \<in> A; \<And>i. \<lbrakk>i \<in> Is; x \<^bsub>(P i)\<^esub>\<prec> y\<rbrakk> \<Longrightarrow> x \<^bsub>(P' i)\<^esub>\<prec> y; \<And>i. \<lbrakk>i \<in> Is; x \<^bsub>(P i)\<^esub>\<approx> y\<rbrakk> \<Longrightarrow> x \<^bsub>(P' i)\<^esub>\<preceq> y; x \<^bsub>(scf P)\<^esub>\<preceq> y; k \<in> Is; x \<^bsub>(P k)\<^esub>\<approx> y \<and> x \<^bsub>(P' k)\<^esub>\<prec> y \<or> y \<^bsub>(P k)\<^esub>\<prec> x \<and> x \<^bsub>(P' k)\<^esub>\<preceq> y; profile A Is P \<and> profile A Is P' \<and> x \<in> A \<and> y \<in> A \<and> (\<forall>i\<in>Is. (x \<^bsub>(P i)\<^esub>\<prec> y \<longrightarrow> x \<^bsub>(P' i)\<^esub>\<prec> y) \<and> (x \<^bsub>(P i)\<^esub>\<approx> y \<longrightarrow> x \<^bsub>(P' i)\<^esub>\<preceq> y)) \<and> (\<exists>k\<in>Is. x \<^bsub>(P k)\<^esub>\<approx> y \<and> x \<^bsub>(P' k)\<^esub>\<prec> y \<or> y \<^bsub>(P k)\<^esub>\<prec> x \<and> x \<^bsub>(P' k)\<^esub>\<preceq> y) \<longrightarrow> x \<^bsub>(scf P)\<^esub>\<preceq> y \<longrightarrow> x \<^bsub>(scf P')\<^esub>\<prec> y\<rbrakk> \<Longrightarrow> x \<^bsub>(scf P')\<^esub>\<prec> y
[PROOF STEP]
by auto


[STATEMENT]
lemma AE_T_fair:
  assumes "t' \<in> K t"
  shows "AE \<omega> in T s. fair t t' \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
let ?M = "\<lambda>P s. emeasure (T s) {\<omega>\<in>space (T s). P \<omega>}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
let ?t = "HLD {t}" and ?t' = "HLD {t'}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
define N where "N = alw (ev ?t) aand alw (not (?t aand nxt ?t'))"
[PROOF STATE]
proof (state)
this:
N = (\<lambda>xs. alw (ev (HLD {t})) xs \<and> alw (\<lambda>xs. \<not> (HLD {t} xs \<and> nxt (HLD {t'}) xs)) xs)

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
let ?until = "not ?t suntil (?t aand nxt (not ?t' aand nxt N))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
have N_stl: "\<And>\<omega>. N \<omega> \<Longrightarrow> N (stl \<omega>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<omega>. N \<omega> \<Longrightarrow> N (stl \<omega>)
[PROOF STEP]
by (auto simp: N_def)
[PROOF STATE]
proof (state)
this:
N ?\<omega>1 \<Longrightarrow> N (stl ?\<omega>1)

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
have [measurable]: "Measurable.pred S N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Measurable.pred (stream_space (count_space UNIV)) N
[PROOF STEP]
unfolding N_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Measurable.pred (stream_space (count_space UNIV)) (\<lambda>xs. alw (ev (HLD {t})) xs \<and> alw (\<lambda>xs. \<not> (HLD {t} xs \<and> nxt (HLD {t'}) xs)) xs)
[PROOF STEP]
by measurable
[PROOF STATE]
proof (state)
this:
Measurable.pred (stream_space (count_space UNIV)) N

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
let ?c = "pmf (K t) t'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
let ?R = "\<lambda>x. 1 \<sqinter> x * (1 - ennreal ?c)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
have "mono ?R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t')))
[PROOF STEP]
by (intro monoI mult_right_mono inf_mono) (auto simp: mono_def field_simps )
[PROOF STATE]
proof (state)
this:
mono (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t')))

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
have "\<And>s. ?M N s \<le> gfp ?R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t')))
[PROOF STEP]
proof (induction rule: gfp_ordinal_induct[OF \<open>mono ?R\<close>])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>S s. \<lbrakk>\<And>s. emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> S; gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> S\<rbrakk> \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> 1 \<sqinter> S * (1 - ennreal (pmf (K t) t'))
 2. \<And>M s. \<forall>S\<in>M. \<forall>x. emeasure (T x) {\<omega> \<in> space (T x). N \<omega>} \<le> S \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> \<Sqinter> M
[PROOF STEP]
fix x s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>S s. \<lbrakk>\<And>s. emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> S; gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> S\<rbrakk> \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> 1 \<sqinter> S * (1 - ennreal (pmf (K t) t'))
 2. \<And>M s. \<forall>S\<in>M. \<forall>x. emeasure (T x) {\<omega> \<in> space (T x). N \<omega>} \<le> S \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> \<Sqinter> M
[PROOF STEP]
assume x: "\<And>s. ?M N s \<le> x"
[PROOF STATE]
proof (state)
this:
emeasure (T ?s1) {\<omega> \<in> space (T ?s1). N \<omega>} \<le> x

goal (2 subgoals):
 1. \<And>S s. \<lbrakk>\<And>s. emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> S; gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> S\<rbrakk> \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> 1 \<sqinter> S * (1 - ennreal (pmf (K t) t'))
 2. \<And>M s. \<forall>S\<in>M. \<forall>x. emeasure (T x) {\<omega> \<in> space (T x). N \<omega>} \<le> S \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> \<Sqinter> M
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
emeasure (T ?s1) {\<omega> \<in> space (T ?s1). N \<omega>} \<le> x

goal (2 subgoals):
 1. \<And>S s. \<lbrakk>\<And>s. emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> S; gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> S\<rbrakk> \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> 1 \<sqinter> S * (1 - ennreal (pmf (K t) t'))
 2. \<And>M s. \<forall>S\<in>M. \<forall>x. emeasure (T x) {\<omega> \<in> space (T x). N \<omega>} \<le> S \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> \<Sqinter> M
[PROOF STEP]
fix \<omega>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>S s. \<lbrakk>\<And>s. emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> S; gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> S\<rbrakk> \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> 1 \<sqinter> S * (1 - ennreal (pmf (K t) t'))
 2. \<And>M s. \<forall>S\<in>M. \<forall>x. emeasure (T x) {\<omega> \<in> space (T x). N \<omega>} \<le> S \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> \<Sqinter> M
[PROOF STEP]
assume "N \<omega>"
[PROOF STATE]
proof (state)
this:
N \<omega>

goal (2 subgoals):
 1. \<And>S s. \<lbrakk>\<And>s. emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> S; gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> S\<rbrakk> \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> 1 \<sqinter> S * (1 - ennreal (pmf (K t) t'))
 2. \<And>M s. \<forall>S\<in>M. \<forall>x. emeasure (T x) {\<omega> \<in> space (T x). N \<omega>} \<le> S \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> \<Sqinter> M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N \<omega>
[PROOF STEP]
have "ev (HLD {t}) \<omega>" "N \<omega>"
[PROOF STATE]
proof (prove)
using this:
N \<omega>

goal (1 subgoal):
 1. ev (HLD {t}) \<omega> &&& N \<omega>
[PROOF STEP]
by (auto simp: N_def)
[PROOF STATE]
proof (state)
this:
ev (HLD {t}) \<omega>
N \<omega>

goal (2 subgoals):
 1. \<And>S s. \<lbrakk>\<And>s. emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> S; gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> S\<rbrakk> \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> 1 \<sqinter> S * (1 - ennreal (pmf (K t) t'))
 2. \<And>M s. \<forall>S\<in>M. \<forall>x. emeasure (T x) {\<omega> \<in> space (T x). N \<omega>} \<le> S \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> \<Sqinter> M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ev (HLD {t}) \<omega>
N \<omega>
[PROOF STEP]
have "?until \<omega>"
[PROOF STATE]
proof (prove)
using this:
ev (HLD {t}) \<omega>
N \<omega>

goal (1 subgoal):
 1. ((\<lambda>xs. \<not> HLD {t} xs) suntil (\<lambda>xs. HLD {t} xs \<and> nxt (\<lambda>xs. \<not> HLD {t'} xs \<and> nxt N xs) xs)) \<omega>
[PROOF STEP]
by (induct rule: ev_induct_strong) (auto simp: N_def intro: suntil.intros dest: N_stl)
[PROOF STATE]
proof (state)
this:
((\<lambda>xs. \<not> HLD {t} xs) suntil (\<lambda>xs. HLD {t} xs \<and> nxt (\<lambda>xs. \<not> HLD {t'} xs \<and> nxt N xs) xs)) \<omega>

goal (2 subgoals):
 1. \<And>S s. \<lbrakk>\<And>s. emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> S; gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> S\<rbrakk> \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> 1 \<sqinter> S * (1 - ennreal (pmf (K t) t'))
 2. \<And>M s. \<forall>S\<in>M. \<forall>x. emeasure (T x) {\<omega> \<in> space (T x). N \<omega>} \<le> S \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> \<Sqinter> M
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
N ?\<omega>3 \<Longrightarrow> ((\<lambda>xs. \<not> HLD {t} xs) suntil (\<lambda>xs. HLD {t} xs \<and> nxt (\<lambda>xs. \<not> HLD {t'} xs \<and> nxt N xs) xs)) ?\<omega>3

goal (2 subgoals):
 1. \<And>S s. \<lbrakk>\<And>s. emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> S; gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> S\<rbrakk> \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> 1 \<sqinter> S * (1 - ennreal (pmf (K t) t'))
 2. \<And>M s. \<forall>S\<in>M. \<forall>x. emeasure (T x) {\<omega> \<in> space (T x). N \<omega>} \<le> S \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> \<Sqinter> M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N ?\<omega>3 \<Longrightarrow> ((\<lambda>xs. \<not> HLD {t} xs) suntil (\<lambda>xs. HLD {t} xs \<and> nxt (\<lambda>xs. \<not> HLD {t'} xs \<and> nxt N xs) xs)) ?\<omega>3
[PROOF STEP]
have "?M N s \<le> ?M ?until s"
[PROOF STATE]
proof (prove)
using this:
N ?\<omega>3 \<Longrightarrow> ((\<lambda>xs. \<not> HLD {t} xs) suntil (\<lambda>xs. HLD {t} xs \<and> nxt (\<lambda>xs. \<not> HLD {t'} xs \<and> nxt N xs) xs)) ?\<omega>3

goal (1 subgoal):
 1. emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> emeasure (T s) {\<omega> \<in> space (T s). ((\<lambda>xs. \<not> HLD {t} xs) suntil (\<lambda>xs. HLD {t} xs \<and> nxt (\<lambda>xs. \<not> HLD {t'} xs \<and> nxt N xs) xs)) \<omega>}
[PROOF STEP]
by (intro emeasure_mono_AE) auto
[PROOF STATE]
proof (state)
this:
emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> emeasure (T s) {\<omega> \<in> space (T s). ((\<lambda>xs. \<not> HLD {t} xs) suntil (\<lambda>xs. HLD {t} xs \<and> nxt (\<lambda>xs. \<not> HLD {t'} xs \<and> nxt N xs) xs)) \<omega>}

goal (2 subgoals):
 1. \<And>S s. \<lbrakk>\<And>s. emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> S; gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> S\<rbrakk> \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> 1 \<sqinter> S * (1 - ennreal (pmf (K t) t'))
 2. \<And>M s. \<forall>S\<in>M. \<forall>x. emeasure (T x) {\<omega> \<in> space (T x). N \<omega>} \<le> S \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> \<Sqinter> M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> emeasure (T s) {\<omega> \<in> space (T s). ((\<lambda>xs. \<not> HLD {t} xs) suntil (\<lambda>xs. HLD {t} xs \<and> nxt (\<lambda>xs. \<not> HLD {t'} xs \<and> nxt N xs) xs)) \<omega>}

goal (2 subgoals):
 1. \<And>S s. \<lbrakk>\<And>s. emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> S; gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> S\<rbrakk> \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> 1 \<sqinter> S * (1 - ennreal (pmf (K t) t'))
 2. \<And>M s. \<forall>S\<in>M. \<forall>x. emeasure (T x) {\<omega> \<in> space (T x). N \<omega>} \<le> S \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> \<Sqinter> M
[PROOF STEP]
have "\<dots> = ?M (ev ?t) s * ?M (not ?t' aand nxt N) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (T s) {\<omega> \<in> space (T s). ((\<lambda>xs. \<not> HLD {t} xs) suntil (\<lambda>xs. HLD {t} xs \<and> nxt (\<lambda>xs. \<not> HLD {t'} xs \<and> nxt N xs) xs)) \<omega>} = emeasure (T s) {\<omega> \<in> space (T s). ev (HLD {t}) \<omega>} * emeasure (T t) {\<omega> \<in> space (T t). \<not> HLD {t'} \<omega> \<and> nxt N \<omega>}
[PROOF STEP]
by (simp_all add: emeasure_suntil_HLD del: nxt.simps space_T)
[PROOF STATE]
proof (state)
this:
emeasure (T s) {\<omega> \<in> space (T s). ((\<lambda>xs. \<not> HLD {t} xs) suntil (\<lambda>xs. HLD {t} xs \<and> nxt (\<lambda>xs. \<not> HLD {t'} xs \<and> nxt N xs) xs)) \<omega>} = emeasure (T s) {\<omega> \<in> space (T s). ev (HLD {t}) \<omega>} * emeasure (T t) {\<omega> \<in> space (T t). \<not> HLD {t'} \<omega> \<and> nxt N \<omega>}

goal (2 subgoals):
 1. \<And>S s. \<lbrakk>\<And>s. emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> S; gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> S\<rbrakk> \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> 1 \<sqinter> S * (1 - ennreal (pmf (K t) t'))
 2. \<And>M s. \<forall>S\<in>M. \<forall>x. emeasure (T x) {\<omega> \<in> space (T x). N \<omega>} \<le> S \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> \<Sqinter> M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
emeasure (T s) {\<omega> \<in> space (T s). ((\<lambda>xs. \<not> HLD {t} xs) suntil (\<lambda>xs. HLD {t} xs \<and> nxt (\<lambda>xs. \<not> HLD {t'} xs \<and> nxt N xs) xs)) \<omega>} = emeasure (T s) {\<omega> \<in> space (T s). ev (HLD {t}) \<omega>} * emeasure (T t) {\<omega> \<in> space (T t). \<not> HLD {t'} \<omega> \<and> nxt N \<omega>}

goal (2 subgoals):
 1. \<And>S s. \<lbrakk>\<And>s. emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> S; gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> S\<rbrakk> \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> 1 \<sqinter> S * (1 - ennreal (pmf (K t) t'))
 2. \<And>M s. \<forall>S\<in>M. \<forall>x. emeasure (T x) {\<omega> \<in> space (T x). N \<omega>} \<le> S \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> \<Sqinter> M
[PROOF STEP]
have "\<dots> \<le> ?M (ev ?t) s * (\<integral>\<^sup>+s'. 1 \<sqinter> x * indicator (UNIV - {t'}) s' \<partial>K t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (T s) {\<omega> \<in> space (T s). ev (HLD {t}) \<omega>} * emeasure (T t) {\<omega> \<in> space (T t). \<not> HLD {t'} \<omega> \<and> nxt N \<omega>} \<le> emeasure (T s) {\<omega> \<in> space (T s). ev (HLD {t}) \<omega>} * (\<integral>\<^sup>+s'\<in>UNIV - {t'}. (1 \<sqinter> x)\<partial>measure_pmf (K t))
[PROOF STEP]
by (auto intro!: mult_left_mono nn_integral_mono T.measure_le_1 emeasure_mono
               split: split_indicator simp add: x emeasure_Collect_T[of _ t] simp del: space_T)
[PROOF STATE]
proof (state)
this:
emeasure (T s) {\<omega> \<in> space (T s). ev (HLD {t}) \<omega>} * emeasure (T t) {\<omega> \<in> space (T t). \<not> HLD {t'} \<omega> \<and> nxt N \<omega>} \<le> emeasure (T s) {\<omega> \<in> space (T s). ev (HLD {t}) \<omega>} * (\<integral>\<^sup>+s'\<in>UNIV - {t'}. (1 \<sqinter> x)\<partial>measure_pmf (K t))

goal (2 subgoals):
 1. \<And>S s. \<lbrakk>\<And>s. emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> S; gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> S\<rbrakk> \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> 1 \<sqinter> S * (1 - ennreal (pmf (K t) t'))
 2. \<And>M s. \<forall>S\<in>M. \<forall>x. emeasure (T x) {\<omega> \<in> space (T x). N \<omega>} \<le> S \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> \<Sqinter> M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
emeasure (T s) {\<omega> \<in> space (T s). ev (HLD {t}) \<omega>} * emeasure (T t) {\<omega> \<in> space (T t). \<not> HLD {t'} \<omega> \<and> nxt N \<omega>} \<le> emeasure (T s) {\<omega> \<in> space (T s). ev (HLD {t}) \<omega>} * (\<integral>\<^sup>+s'\<in>UNIV - {t'}. (1 \<sqinter> x)\<partial>measure_pmf (K t))

goal (2 subgoals):
 1. \<And>S s. \<lbrakk>\<And>s. emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> S; gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> S\<rbrakk> \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> 1 \<sqinter> S * (1 - ennreal (pmf (K t) t'))
 2. \<And>M s. \<forall>S\<in>M. \<forall>x. emeasure (T x) {\<omega> \<in> space (T x). N \<omega>} \<le> S \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> \<Sqinter> M
[PROOF STEP]
have "\<dots> \<le> 1 * (\<integral>\<^sup>+s'. 1 \<sqinter> x * indicator (UNIV - {t'}) s' \<partial>K t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (T s) {\<omega> \<in> space (T s). ev (HLD {t}) \<omega>} * (\<integral>\<^sup>+s'\<in>UNIV - {t'}. (1 \<sqinter> x)\<partial>measure_pmf (K t)) \<le> 1 * (\<integral>\<^sup>+s'\<in>UNIV - {t'}. (1 \<sqinter> x)\<partial>measure_pmf (K t))
[PROOF STEP]
by (intro mult_right_mono T.measure_le_1) simp
[PROOF STATE]
proof (state)
this:
emeasure (T s) {\<omega> \<in> space (T s). ev (HLD {t}) \<omega>} * (\<integral>\<^sup>+s'\<in>UNIV - {t'}. (1 \<sqinter> x)\<partial>measure_pmf (K t)) \<le> 1 * (\<integral>\<^sup>+s'\<in>UNIV - {t'}. (1 \<sqinter> x)\<partial>measure_pmf (K t))

goal (2 subgoals):
 1. \<And>S s. \<lbrakk>\<And>s. emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> S; gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> S\<rbrakk> \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> 1 \<sqinter> S * (1 - ennreal (pmf (K t) t'))
 2. \<And>M s. \<forall>S\<in>M. \<forall>x. emeasure (T x) {\<omega> \<in> space (T x). N \<omega>} \<le> S \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> \<Sqinter> M
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> 1 * (\<integral>\<^sup>+s'\<in>UNIV - {t'}. (1 \<sqinter> x)\<partial>measure_pmf (K t))
[PROOF STEP]
show "?M N s \<le> 1 \<sqinter> x * (1 - ennreal ?c)"
[PROOF STATE]
proof (prove)
using this:
emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> 1 * (\<integral>\<^sup>+s'\<in>UNIV - {t'}. (1 \<sqinter> x)\<partial>measure_pmf (K t))

goal (1 subgoal):
 1. emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))
[PROOF STEP]
by (subst (asm) nn_integral_cmult_indicator) (auto simp: emeasure_Diff emeasure_pmf_single)
[PROOF STATE]
proof (state)
this:
emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))

goal (1 subgoal):
 1. \<And>M s. \<forall>S\<in>M. \<forall>x. emeasure (T x) {\<omega> \<in> space (T x). N \<omega>} \<le> S \<Longrightarrow> emeasure (T s) {\<omega> \<in> space (T s). N \<omega>} \<le> \<Sqinter> M
[PROOF STEP]
qed (auto intro: Inf_greatest)
[PROOF STATE]
proof (state)
this:
emeasure (T ?s1) {\<omega> \<in> space (T ?s1). N \<omega>} \<le> gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t')))

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
emeasure (T ?s1) {\<omega> \<in> space (T ?s1). N \<omega>} \<le> gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t')))

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
from \<open>mono ?R\<close>
[PROOF STATE]
proof (chain)
picking this:
mono (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t')))
[PROOF STEP]
have "gfp ?R = ?R (gfp ?R)"
[PROOF STATE]
proof (prove)
using this:
mono (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t')))

goal (1 subgoal):
 1. gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) = 1 \<sqinter> gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) * (1 - ennreal (pmf (K t) t'))
[PROOF STEP]
by (rule gfp_unfold)
[PROOF STATE]
proof (state)
this:
gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) = 1 \<sqinter> gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) * (1 - ennreal (pmf (K t) t'))

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) = 1 \<sqinter> gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) * (1 - ennreal (pmf (K t) t'))
[PROOF STEP]
have "gfp ?R \<le> ?R (gfp ?R)"
[PROOF STATE]
proof (prove)
using this:
gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) = 1 \<sqinter> gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) * (1 - ennreal (pmf (K t) t'))

goal (1 subgoal):
 1. gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> 1 \<sqinter> gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) * (1 - ennreal (pmf (K t) t'))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> 1 \<sqinter> gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) * (1 - ennreal (pmf (K t) t'))

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
with assms[THEN pmf_positive]
[PROOF STATE]
proof (chain)
picking this:
0 < pmf (K t) t'
gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> 1 \<sqinter> gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) * (1 - ennreal (pmf (K t) t'))
[PROOF STEP]
have "gfp ?R \<le> 0"
[PROOF STATE]
proof (prove)
using this:
0 < pmf (K t) t'
gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> 1 \<sqinter> gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) * (1 - ennreal (pmf (K t) t'))

goal (1 subgoal):
 1. gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> 0
[PROOF STEP]
by (cases "gfp ?R")
       (auto simp: top_unique inf_ennreal.rep_eq field_simps mult_le_0_iff ennreal_1[symmetric]
                   pmf_le_1 ennreal_minus ennreal_mult[symmetric] ennreal_le_iff2 inf_min min_def
             simp del: ennreal_1
             split: if_split_asm)
[PROOF STATE]
proof (state)
this:
gfp (\<lambda>x. 1 \<sqinter> x * (1 - ennreal (pmf (K t) t'))) \<le> 0

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
emeasure (T ?s2) {\<omega> \<in> space (T ?s2). N \<omega>} \<le> 0
[PROOF STEP]
have "\<And>s. AE \<omega> in T s. \<not> N \<omega>"
[PROOF STATE]
proof (prove)
using this:
emeasure (T ?s2) {\<omega> \<in> space (T ?s2). N \<omega>} \<le> 0

goal (1 subgoal):
 1. \<And>s. AE \<omega> in T s. \<not> N \<omega>
[PROOF STEP]
by (subst AE_iff_measurable[OF _ refl]) (auto intro: antisym simp: le_fun_def)
[PROOF STATE]
proof (state)
this:
AE \<omega> in T ?s1. \<not> N \<omega>

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE \<omega> in T ?s1. \<not> N \<omega>
[PROOF STEP]
have "AE \<omega> in T s. alw (not N) \<omega>"
[PROOF STATE]
proof (prove)
using this:
AE \<omega> in T ?s1. \<not> N \<omega>

goal (1 subgoal):
 1. almost_everywhere (T s) (alw (\<lambda>xs. \<not> N xs))
[PROOF STEP]
by (intro AE_T_alw) auto
[PROOF STATE]
proof (state)
this:
almost_everywhere (T s) (alw (\<lambda>xs. \<not> N xs))

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
almost_everywhere (T s) (alw (\<lambda>xs. \<not> N xs))

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
almost_everywhere (T s) (alw (\<lambda>xs. \<not> N xs))

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
fix \<omega>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
assume "alw (ev (HLD {t})) \<omega>"
[PROOF STATE]
proof (state)
this:
alw (ev (HLD {t})) \<omega>

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
alw (ev (HLD {t})) \<omega>
[PROOF STEP]
have "alw (alw (ev (HLD {t}))) \<omega>"
[PROOF STATE]
proof (prove)
using this:
alw (ev (HLD {t})) \<omega>

goal (1 subgoal):
 1. alw (alw (ev (HLD {t}))) \<omega>
[PROOF STEP]
unfolding alw_alw
[PROOF STATE]
proof (prove)
using this:
alw (ev (HLD {t})) \<omega>

goal (1 subgoal):
 1. alw (ev (HLD {t})) \<omega>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
alw (alw (ev (HLD {t}))) \<omega>

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
alw (alw (ev (HLD {t}))) \<omega>

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
assume "alw (not N) \<omega>"
[PROOF STATE]
proof (state)
this:
alw (\<lambda>xs. \<not> N xs) \<omega>

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
alw (\<lambda>xs. \<not> N xs) \<omega>
[PROOF STEP]
have "alw (alw (ev (HLD {t})) impl ev (HLD {t} aand nxt (HLD {t'}))) \<omega>"
[PROOF STATE]
proof (prove)
using this:
alw (\<lambda>xs. \<not> N xs) \<omega>

goal (1 subgoal):
 1. alw (\<lambda>xs. alw (ev (HLD {t})) xs \<longrightarrow> ev (\<lambda>xs. HLD {t} xs \<and> nxt (HLD {t'}) xs) xs) \<omega>
[PROOF STEP]
unfolding N_def not_alw_iff not_ev_iff de_Morgan_disj de_Morgan_conj not_not imp_conv_disj
[PROOF STATE]
proof (prove)
using this:
alw (\<lambda>xs. ev (alw (\<lambda>xs. \<not> HLD {t} xs)) xs \<or> ev (\<lambda>xs. HLD {t} xs \<and> nxt (HLD {t'}) xs) xs) \<omega>

goal (1 subgoal):
 1. alw (\<lambda>xs. ev (alw (\<lambda>xs. \<not> HLD {t} xs)) xs \<or> ev (\<lambda>xs. HLD {t} xs \<and> nxt (HLD {t'}) xs) xs) \<omega>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
alw (\<lambda>xs. alw (ev (HLD {t})) xs \<longrightarrow> ev (\<lambda>xs. HLD {t} xs \<and> nxt (HLD {t'}) xs) xs) \<omega>

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
alw (alw (ev (HLD {t}))) \<omega>
alw (\<lambda>xs. alw (ev (HLD {t})) xs \<longrightarrow> ev (\<lambda>xs. HLD {t} xs \<and> nxt (HLD {t'}) xs) xs) \<omega>
[PROOF STEP]
have "alw (ev (HLD {t} aand nxt (HLD {t'}))) \<omega>"
[PROOF STATE]
proof (prove)
using this:
alw (alw (ev (HLD {t}))) \<omega>
alw (\<lambda>xs. alw (ev (HLD {t})) xs \<longrightarrow> ev (\<lambda>xs. HLD {t} xs \<and> nxt (HLD {t'}) xs) xs) \<omega>

goal (1 subgoal):
 1. alw (ev (\<lambda>xs. HLD {t} xs \<and> nxt (HLD {t'}) xs)) \<omega>
[PROOF STEP]
by (rule alw_mp)
[PROOF STATE]
proof (state)
this:
alw (ev (\<lambda>xs. HLD {t} xs \<and> nxt (HLD {t'}) xs)) \<omega>

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>alw (ev (HLD {t})) ?\<omega>3; alw (\<lambda>xs. \<not> N xs) ?\<omega>3\<rbrakk> \<Longrightarrow> alw (ev (\<lambda>xs. HLD {t} xs \<and> nxt (HLD {t'}) xs)) ?\<omega>3

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>alw (ev (HLD {t})) ?\<omega>3; alw (\<lambda>xs. \<not> N xs) ?\<omega>3\<rbrakk> \<Longrightarrow> alw (ev (\<lambda>xs. HLD {t} xs \<and> nxt (HLD {t'}) xs)) ?\<omega>3
[PROOF STEP]
have "\<forall>\<omega>. alw (not N) \<omega> \<longrightarrow> fair t t' \<omega>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>alw (ev (HLD {t})) ?\<omega>3; alw (\<lambda>xs. \<not> N xs) ?\<omega>3\<rbrakk> \<Longrightarrow> alw (ev (\<lambda>xs. HLD {t} xs \<and> nxt (HLD {t'}) xs)) ?\<omega>3

goal (1 subgoal):
 1. \<forall>\<omega>. alw (\<lambda>xs. \<not> N xs) \<omega> \<longrightarrow> fair t t' \<omega>
[PROOF STEP]
by (auto simp: fair_def)
[PROOF STATE]
proof (state)
this:
\<forall>\<omega>. alw (\<lambda>xs. \<not> N xs) \<omega> \<longrightarrow> fair t t' \<omega>

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
almost_everywhere (T s) (alw (\<lambda>xs. \<not> N xs))
\<forall>\<omega>. alw (\<lambda>xs. \<not> N xs) \<omega> \<longrightarrow> fair t t' \<omega>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
almost_everywhere (T s) (alw (\<lambda>xs. \<not> N xs))
\<forall>\<omega>. alw (\<lambda>xs. \<not> N xs) \<omega> \<longrightarrow> fair t t' \<omega>

goal (1 subgoal):
 1. almost_everywhere (T s) (fair t t')
[PROOF STEP]
by (simp add: eventually_mono)
[PROOF STATE]
proof (state)
this:
almost_everywhere (T s) (fair t t')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma real_mult_commute: "(z::real) * w = w * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z * w = w * z
[PROOF STEP]
by (cases z, cases w, simp add: real_mult ac_simps)


[STATEMENT]
lemma stepsST_add:
  fixes P Q R :: "('procS, 'procT) Proc"
  assumes A1: "P \<longmapsto>ST* Q"
      and A2: "Q \<longmapsto>ST* R"
  shows "P \<longmapsto>ST* R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<longmapsto>ST* R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<longmapsto>ST* R
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto>ST* Q
[PROOF STEP]
have "P \<longmapsto>(STCal Source Target)* Q"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto>ST* Q

goal (1 subgoal):
 1. P \<longmapsto>STCal Source Target* Q
[PROOF STEP]
by (simp add: stepsST_STCal_steps)
[PROOF STATE]
proof (state)
this:
P \<longmapsto>STCal Source Target* Q

goal (1 subgoal):
 1. P \<longmapsto>ST* R
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<longmapsto>STCal Source Target* Q

goal (1 subgoal):
 1. P \<longmapsto>ST* R
[PROOF STEP]
from A2
[PROOF STATE]
proof (chain)
picking this:
Q \<longmapsto>ST* R
[PROOF STEP]
have "Q \<longmapsto>(STCal Source Target)* R"
[PROOF STATE]
proof (prove)
using this:
Q \<longmapsto>ST* R

goal (1 subgoal):
 1. Q \<longmapsto>STCal Source Target* R
[PROOF STEP]
by (simp add: stepsST_STCal_steps)
[PROOF STATE]
proof (state)
this:
Q \<longmapsto>STCal Source Target* R

goal (1 subgoal):
 1. P \<longmapsto>ST* R
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto>STCal Source Target* Q
Q \<longmapsto>STCal Source Target* R
[PROOF STEP]
have "P \<longmapsto>(STCal Source Target)* R"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto>STCal Source Target* Q
Q \<longmapsto>STCal Source Target* R

goal (1 subgoal):
 1. P \<longmapsto>STCal Source Target* R
[PROOF STEP]
by (rule steps_add)
[PROOF STATE]
proof (state)
this:
P \<longmapsto>STCal Source Target* R

goal (1 subgoal):
 1. P \<longmapsto>ST* R
[PROOF STEP]
thus "P \<longmapsto>ST* R"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto>STCal Source Target* R

goal (1 subgoal):
 1. P \<longmapsto>ST* R
[PROOF STEP]
by (simp add: stepsST_STCal_steps)
[PROOF STATE]
proof (state)
this:
P \<longmapsto>ST* R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distinct_snd: "distinct (map snd a) \<Longrightarrow> distinct a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map snd a) \<Longrightarrow> distinct a
[PROOF STEP]
by (metis distinct_zipI2 zip_map_fst_snd)


[STATEMENT]
lemma bisim_must_sync_inv:
  "t \<turnstile> (x1, m1) \<approx> (x2, m2) \<Longrightarrow> t \<turnstile> \<langle>x1, m1\<rangle> \<wrong>1 \<longleftrightarrow> t \<turnstile> \<langle>x2, m2\<rangle> \<wrong>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<turnstile> (x1, m1) \<approx> (x2, m2) \<Longrightarrow> t \<turnstile> \<langle>x1, m1\<rangle> \<wrong>1 = t \<turnstile> \<langle>x2, m2\<rangle> \<wrong>2
[PROOF STEP]
by(blast intro: bisim_must_sync_preserve1 bisim_must_sync_preserve2)


[STATEMENT]
lemma istate_\<Delta>1:
assumes B: "B vl vl1"
shows "\<Delta>1 istate vl istate vl1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta>1 istate vl istate vl1
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
B vl vl1

goal (1 subgoal):
 1. \<Delta>1 istate vl istate vl1
[PROOF STEP]
unfolding \<Delta>1_def B_def istate_def
[PROOF STATE]
proof (prove)
using this:
vl \<noteq> [] \<and> vl1 \<noteq> [] \<and> last vl = last vl1

goal (1 subgoal):
 1. (\<forall>cid. PID \<in>\<in> paperIDs \<lparr>confIDs = [], conf = \<lambda>confID. emptyConf, userIDs = [voronkovUserID], pass = \<lambda>uID. emptyPass, user = \<lambda>uID. emptyUser, roles = \<lambda>confID uID. [], paperIDs = \<lambda>confID. [], paper = \<lambda>papID. emptyPaper, pref = \<lambda>uID papID. NoPref, voronkov = voronkovUserID, news = \<lambda>confID. [], phase = \<lambda>confID. noPH\<rparr> cid \<longrightarrow> phase \<lparr>confIDs = [], conf = \<lambda>confID. emptyConf, userIDs = [voronkovUserID], pass = \<lambda>uID. emptyPass, user = \<lambda>uID. emptyUser, roles = \<lambda>confID uID. [], paperIDs = \<lambda>confID. [], paper = \<lambda>papID. emptyPaper, pref = \<lambda>uID papID. NoPref, voronkov = voronkovUserID, news = \<lambda>confID. [], phase = \<lambda>confID. noPH\<rparr> cid < disPH) \<and> \<lparr>confIDs = [], conf = \<lambda>confID. emptyConf, userIDs = [voronkovUserID], pass = \<lambda>uID. emptyPass, user = \<lambda>uID. emptyUser, roles = \<lambda>confID uID. [], paperIDs = \<lambda>confID. [], paper = \<lambda>papID. emptyPaper, pref = \<lambda>uID papID. NoPref, voronkov = voronkovUserID, news = \<lambda>confID. [], phase = \<lambda>confID. noPH\<rparr> = \<lparr>confIDs = [], conf = \<lambda>confID. emptyConf, userIDs = [voronkovUserID], pass = \<lambda>uID. emptyPass, user = \<lambda>uID. emptyUser, roles = \<lambda>confID uID. [], paperIDs = \<lambda>confID. [], paper = \<lambda>papID. emptyPaper, pref = \<lambda>uID papID. NoPref, voronkov = voronkovUserID, news = \<lambda>confID. [], phase = \<lambda>confID. noPH\<rparr> \<and> vl \<noteq> [] \<and> vl1 \<noteq> [] \<and> last vl = last vl1
[PROOF STEP]
by auto


[STATEMENT]
lemma Ri_loop: "Ri x (q \<sqinter> x) y \<le> ((fiter_id (\<lfloor>p\<rfloor> \<circ> (Ri (x \<sqinter> p) x))) \<circ> \<lfloor>q\<rfloor>) (q \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ri x (q \<sqinter> x) y \<le> (fiter_id (\<lfloor>p\<rfloor> \<circ> Ri (x \<sqinter> p) x) \<circ> \<lfloor>q\<rfloor>) (q \<sqinter> y)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Ri x (q \<sqinter> x) y \<le> (fiter_id (\<lfloor>p\<rfloor> \<circ> Ri (x \<sqinter> p) x) \<circ> \<lfloor>q\<rfloor>) (q \<sqinter> y)
[PROOF STEP]
have "(p \<sqinter> x) \<le> Ri (p \<sqinter> x) x x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<sqinter> x \<le> Ri (p \<sqinter> x) x x
[PROOF STEP]
by (simp add: Ri_spec)
[PROOF STATE]
proof (state)
this:
p \<sqinter> x \<le> Ri (p \<sqinter> x) x x

goal (1 subgoal):
 1. Ri x (q \<sqinter> x) y \<le> (fiter_id (\<lfloor>p\<rfloor> \<circ> Ri (x \<sqinter> p) x) \<circ> \<lfloor>q\<rfloor>) (q \<sqinter> y)
[PROOF STEP]
hence "x \<le> ((fiter_id (\<lfloor>p\<rfloor> \<circ> (Ri (x \<sqinter> p) x))) \<circ> \<lfloor>q\<rfloor>) (q \<sqinter> x)"
[PROOF STATE]
proof (prove)
using this:
p \<sqinter> x \<le> Ri (p \<sqinter> x) x x

goal (1 subgoal):
 1. x \<le> (fiter_id (\<lfloor>p\<rfloor> \<circ> Ri (x \<sqinter> p) x) \<circ> \<lfloor>q\<rfloor>) (q \<sqinter> x)
[PROOF STEP]
by (metis H_iso_loop inf_commute iso_Ri)
[PROOF STATE]
proof (state)
this:
x \<le> (fiter_id (\<lfloor>p\<rfloor> \<circ> Ri (x \<sqinter> p) x) \<circ> \<lfloor>q\<rfloor>) (q \<sqinter> x)

goal (1 subgoal):
 1. Ri x (q \<sqinter> x) y \<le> (fiter_id (\<lfloor>p\<rfloor> \<circ> Ri (x \<sqinter> p) x) \<circ> \<lfloor>q\<rfloor>) (q \<sqinter> y)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<le> (fiter_id (\<lfloor>p\<rfloor> \<circ> Ri (x \<sqinter> p) x) \<circ> \<lfloor>q\<rfloor>) (q \<sqinter> x)

goal (1 subgoal):
 1. Ri x (q \<sqinter> x) y \<le> (fiter_id (\<lfloor>p\<rfloor> \<circ> Ri (x \<sqinter> p) x) \<circ> \<lfloor>q\<rfloor>) (q \<sqinter> y)
[PROOF STEP]
apply (subst Ri_least, safe, simp_all add: mono_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> fiter_id (\<lfloor>p\<rfloor> \<circ> Ri (x \<sqinter> p) x) (\<lfloor>q\<rfloor> (q \<sqinter> x)) \<Longrightarrow> \<forall>xa y. xa \<le> y \<longrightarrow> fiter_id (\<lfloor>p\<rfloor> \<circ> Ri (x \<sqinter> p) x) (\<lfloor>q\<rfloor> (q \<sqinter> xa)) \<le> fiter_id (\<lfloor>p\<rfloor> \<circ> Ri (x \<sqinter> p) x) (\<lfloor>q\<rfloor> (q \<sqinter> y))
[PROOF STEP]
by (metis bqtran_iso inf_mono iso_Ri iso_fcomp iso_fiter mono_def order_refl)
[PROOF STATE]
proof (state)
this:
Ri x (q \<sqinter> x) y \<le> (fiter_id (\<lfloor>p\<rfloor> \<circ> Ri (x \<sqinter> p) x) \<circ> \<lfloor>q\<rfloor>) (q \<sqinter> y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma l2_inv3_step4:
  "{l2_inv3} l2_step4 Rb A B Ni gnx {> l2_inv3}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {l2_inv3} l2_step4 Rb A B Ni gnx {> l2_inv3}
[PROOF STEP]
apply (auto simp add: PO_hoare_defs l2_nostep_defs intro!: l2_inv3I, auto simp add: l2_defs)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>xa xb. \<lbrakk>xa \<in> l2_inv3; xb \<in> extr (bad xa) (ik xa) (chan xa); guessed_runs Rb = \<lparr>role = Resp, owner = B, partner = A\<rparr>; progress xa Rb = Some {xny, xni, xnr, xgnx, xgny, xsk}; sklvl1.guessed_frame Rb xgnx = Some gnx; sklvl1.guessed_frame Rb xni = Some Ni; Insec A B (hmac \<langle>Number (Suc 0), Exp Gen (NonceF (Rb $ ny)), gnx, Messages.Agent A, Messages.Agent B\<rangle> (hmac Ni (NonceF (Rb $ nr)))) \<in> chan xa; can_signal xa A B\<rbrakk> \<Longrightarrow> xb \<in> synth (analz (generators (xa\<lparr>progress := progress xa(Rb \<mapsto> {xny, xni, xnr, xgnx, xgny, xsk, xEnd}), secret := {x. x = Exp gnx (NonceF (Rb $ ny)) \<and> Rb = test} \<union> secret xa, signalsResp := (signalsResp xa)(Commit A B \<langle>Ni, NonceF (Rb $ nr), Exp gnx (NonceF (Rb $ ny))\<rangle> := Suc (signalsResp xa (Commit A B \<langle>Ni, NonceF (Rb $ nr), Exp gnx (NonceF (Rb $ ny))\<rangle>))), signalsResp2 := (signalsResp2 xa)(Commit A B (Exp gnx (NonceF (Rb $ ny))) := Suc (signalsResp2 xa (Commit A B (Exp gnx (NonceF (Rb $ ny))))))\<rparr>)))
 2. \<And>xa xb. \<lbrakk>xa \<in> l2_inv3; xb \<in> extr (bad xa) (ik xa) (chan xa); guessed_runs Rb = \<lparr>role = Resp, owner = B, partner = A\<rparr>; progress xa Rb = Some {xny, xni, xnr, xgnx, xgny, xsk}; sklvl1.guessed_frame Rb xgnx = Some gnx; sklvl1.guessed_frame Rb xni = Some Ni; Insec A B (hmac \<langle>Number (Suc 0), Exp Gen (NonceF (Rb $ ny)), gnx, Messages.Agent A, Messages.Agent B\<rangle> (hmac Ni (NonceF (Rb $ nr)))) \<in> chan xa; \<not> can_signal xa A B\<rbrakk> \<Longrightarrow> xb \<in> synth (analz (generators (xa\<lparr>progress := progress xa(Rb \<mapsto> {xny, xni, xnr, xgnx, xgny, xsk, xEnd}), secret := {x. x = Exp gnx (NonceF (Rb $ ny)) \<and> Rb = test} \<union> secret xa\<rparr>)))
 3. \<And>xa xb. \<lbrakk>xa \<in> l2_inv3; xb \<in> chan xa; xb \<notin> chan_generators; guessed_runs Rb = \<lparr>role = Resp, owner = B, partner = A\<rparr>; progress xa Rb = Some {xny, xni, xnr, xgnx, xgny, xsk}; sklvl1.guessed_frame Rb xgnx = Some gnx; sklvl1.guessed_frame Rb xni = Some Ni; Insec A B (hmac \<langle>Number (Suc 0), Exp Gen (NonceF (Rb $ ny)), gnx, Messages.Agent A, Messages.Agent B\<rangle> (hmac Ni (NonceF (Rb $ nr)))) \<in> chan xa; can_signal xa A B\<rbrakk> \<Longrightarrow> xb \<in> faked_chan_msgs (xa\<lparr>progress := progress xa(Rb \<mapsto> {xny, xni, xnr, xgnx, xgny, xsk, xEnd}), secret := {x. x = Exp gnx (NonceF (Rb $ ny)) \<and> Rb = test} \<union> secret xa, signalsResp := (signalsResp xa)(Commit A B \<langle>Ni, NonceF (Rb $ nr), Exp gnx (NonceF (Rb $ ny))\<rangle> := Suc (signalsResp xa (Commit A B \<langle>Ni, NonceF (Rb $ nr), Exp gnx (NonceF (Rb $ ny))\<rangle>))), signalsResp2 := (signalsResp2 xa)(Commit A B (Exp gnx (NonceF (Rb $ ny))) := Suc (signalsResp2 xa (Commit A B (Exp gnx (NonceF (Rb $ ny))))))\<rparr>)
 4. \<And>xa xb. \<lbrakk>xa \<in> l2_inv3; xb \<in> chan xa; xb \<notin> chan_generators; guessed_runs Rb = \<lparr>role = Resp, owner = B, partner = A\<rparr>; progress xa Rb = Some {xny, xni, xnr, xgnx, xgny, xsk}; sklvl1.guessed_frame Rb xgnx = Some gnx; sklvl1.guessed_frame Rb xni = Some Ni; Insec A B (hmac \<langle>Number (Suc 0), Exp Gen (NonceF (Rb $ ny)), gnx, Messages.Agent A, Messages.Agent B\<rangle> (hmac Ni (NonceF (Rb $ nr)))) \<in> chan xa; \<not> can_signal xa A B\<rbrakk> \<Longrightarrow> xb \<in> faked_chan_msgs (xa\<lparr>progress := progress xa(Rb \<mapsto> {xny, xni, xnr, xgnx, xgny, xsk, xEnd}), secret := {x. x = Exp gnx (NonceF (Rb $ ny)) \<and> Rb = test} \<union> secret xa\<rparr>)
[PROOF STEP]
apply (auto simp add: bad_runs_def intro:synth_analz_increasing dest!: l2_inv3D)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa xb. \<lbrakk>xb \<in> chan xa; xb \<notin> chan_generators; guessed_runs Rb = \<lparr>role = Resp, owner = B, partner = A\<rparr>; progress xa Rb = Some {xny, xni, xnr, xgnx, xgny, xsk}; sklvl1.guessed_frame Rb xgnx = Some gnx; sklvl1.guessed_frame Rb xni = Some Ni; Insec A B (hmac \<langle>Number (Suc 0), Exp Gen (NonceF (Rb $ ny)), gnx, Messages.Agent A, Messages.Agent B\<rangle> (hmac Ni (NonceF (Rb $ nr)))) \<in> chan xa; can_signal xa A B; extr (bad xa) (ik xa) (chan xa) \<subseteq> synth (analz ({x. \<exists>N. x = Exp Gen (Nonce N)} \<union> {x. \<exists>R. (owner (guessed_runs R) \<in> bad xa \<or> partner (guessed_runs R) \<in> bad xa) \<and> (x = NonceF (R $ ni) \<or> x = NonceF (R $ nr))} \<union> {x. \<exists>y y' z. x = hmac \<langle>y, y'\<rangle> (Hash z)} \<union> {Exp y (NonceF (R $ N)) |y N R. R \<noteq> test \<and> R \<notin> partners})); chan xa \<subseteq> faked_chan_msgs xa \<union> chan_generators\<rbrakk> \<Longrightarrow> xb \<in> faked_chan_msgs (xa\<lparr>progress := progress xa(Rb \<mapsto> {xny, xni, xnr, xgnx, xgny, xsk, xEnd}), secret := {x. x = Exp gnx (NonceF (Rb $ ny)) \<and> Rb = test} \<union> secret xa, signalsResp := (signalsResp xa)(Commit A B \<langle>Ni, NonceF (Rb $ nr), Exp gnx (NonceF (Rb $ ny))\<rangle> := Suc (signalsResp xa (Commit A B \<langle>Ni, NonceF (Rb $ nr), Exp gnx (NonceF (Rb $ ny))\<rangle>))), signalsResp2 := (signalsResp2 xa)(Commit A B (Exp gnx (NonceF (Rb $ ny))) := Suc (signalsResp2 xa (Commit A B (Exp gnx (NonceF (Rb $ ny))))))\<rparr>)
 2. \<And>xa xb. \<lbrakk>xb \<in> chan xa; xb \<notin> chan_generators; guessed_runs Rb = \<lparr>role = Resp, owner = B, partner = A\<rparr>; progress xa Rb = Some {xny, xni, xnr, xgnx, xgny, xsk}; sklvl1.guessed_frame Rb xgnx = Some gnx; sklvl1.guessed_frame Rb xni = Some Ni; Insec A B (hmac \<langle>Number (Suc 0), Exp Gen (NonceF (Rb $ ny)), gnx, Messages.Agent A, Messages.Agent B\<rangle> (hmac Ni (NonceF (Rb $ nr)))) \<in> chan xa; \<not> can_signal xa A B; extr (bad xa) (ik xa) (chan xa) \<subseteq> synth (analz ({x. \<exists>N. x = Exp Gen (Nonce N)} \<union> {x. \<exists>R. (owner (guessed_runs R) \<in> bad xa \<or> partner (guessed_runs R) \<in> bad xa) \<and> (x = NonceF (R $ ni) \<or> x = NonceF (R $ nr))} \<union> {x. \<exists>y y' z. x = hmac \<langle>y, y'\<rangle> (Hash z)} \<union> {Exp y (NonceF (R $ N)) |y N R. R \<noteq> test \<and> R \<notin> partners})); chan xa \<subseteq> faked_chan_msgs xa \<union> chan_generators\<rbrakk> \<Longrightarrow> xb \<in> faked_chan_msgs (xa\<lparr>progress := progress xa(Rb \<mapsto> {xny, xni, xnr, xgnx, xgny, xsk, xEnd}), secret := {x. x = Exp gnx (NonceF (Rb $ ny)) \<and> Rb = test} \<union> secret xa\<rparr>)
[PROOF STEP]
apply (auto simp add: l2_inv3_aux_defs dest!: subsetD [where A="chan _"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma finite_fst_ts_tuple_rel: "finite (fst ` {tas \<in> ts_tuple_rel (set xs). P tas})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (fst ` {tas \<in> ts_tuple_rel (set xs). P tas})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (fst ` {tas \<in> ts_tuple_rel (set xs). P tas})
[PROOF STEP]
have "fst ` {tas \<in> ts_tuple_rel (set xs). P tas} \<subseteq> fst ` ts_tuple_rel (set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` {tas \<in> ts_tuple_rel (set xs). P tas} \<subseteq> fst ` ts_tuple_rel (set xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst ` {tas \<in> ts_tuple_rel (set xs). P tas} \<subseteq> fst ` ts_tuple_rel (set xs)

goal (1 subgoal):
 1. finite (fst ` {tas \<in> ts_tuple_rel (set xs). P tas})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst ` {tas \<in> ts_tuple_rel (set xs). P tas} \<subseteq> fst ` ts_tuple_rel (set xs)

goal (1 subgoal):
 1. finite (fst ` {tas \<in> ts_tuple_rel (set xs). P tas})
[PROOF STEP]
have "\<dots> \<subseteq> set (map fst xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` ts_tuple_rel (set xs) \<subseteq> set (map fst xs)
[PROOF STEP]
by (force simp add: ts_tuple_rel_def)
[PROOF STATE]
proof (state)
this:
fst ` ts_tuple_rel (set xs) \<subseteq> set (map fst xs)

goal (1 subgoal):
 1. finite (fst ` {tas \<in> ts_tuple_rel (set xs). P tas})
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
fst ` {tas \<in> ts_tuple_rel (set xs). P tas} \<subseteq> set (map fst xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fst ` {tas \<in> ts_tuple_rel (set xs). P tas} \<subseteq> set (map fst xs)

goal (1 subgoal):
 1. finite (fst ` {tas \<in> ts_tuple_rel (set xs). P tas})
[PROOF STEP]
using finite_subset
[PROOF STATE]
proof (prove)
using this:
fst ` {tas \<in> ts_tuple_rel (set xs). P tas} \<subseteq> set (map fst xs)
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite (fst ` {tas \<in> ts_tuple_rel (set xs). P tas})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (fst ` {tas \<in> ts_tuple_rel (set xs). P tas})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_all2_weaken: "list_all2 f xs ys \<Longrightarrow>
  (\<And>x y. (x, y) \<in> set (zip xs ys) \<Longrightarrow> f x y \<Longrightarrow> f' x y) \<Longrightarrow> list_all2 f' xs ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 f xs ys; \<And>x y. \<lbrakk>(x, y) \<in> set (zip xs ys); f x y\<rbrakk> \<Longrightarrow> f' x y\<rbrakk> \<Longrightarrow> list_all2 f' xs ys
[PROOF STEP]
by (induction xs ys rule: list_all2_induct) auto


[STATEMENT]
lemma PO_m3_refines_init_m2 [iff]:
  "init m3 \<subseteq> R23``(init m2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init m3 \<subseteq> R23 `` init m2
[PROOF STEP]
by (auto simp add: R23_defs m2_defs m3_defs)


[STATEMENT]
lemma Labels_On_CTRL:
  "Labels On_CTRL = On_CTRL_Labels"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Labels On_CTRL = On_CTRL_Labels
[PROOF STEP]
apply (simp add: On_CTRL_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Labels (Abs_seqauto (On_CTRL_States, On_CTRL_Init, On_CTRL_Labels, On_CTRL_Delta)) = On_CTRL_Labels
[PROOF STEP]
apply (unfold Labels_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst \<circ> snd \<circ> snd \<circ> Rep_seqauto) (Abs_seqauto (On_CTRL_States, On_CTRL_Init, On_CTRL_Labels, On_CTRL_Delta)) = On_CTRL_Labels
[PROOF STEP]
apply (simp add: Abs_seqauto_inverse check_On_CTRL)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma lists_succ_permutes:
  assumes "distincts xss"
  shows "lists_succ xss permutes (\<Union>xs \<in> set xss. set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lists_succ xss permutes \<Union> (set ` set xss)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distincts xss

goal (1 subgoal):
 1. lists_succ xss permutes \<Union> (set ` set xss)
[PROOF STEP]
proof (induction xss)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. distincts [] \<Longrightarrow> lists_succ [] permutes \<Union> (set ` set [])
 2. \<And>a xss. \<lbrakk>distincts xss \<Longrightarrow> lists_succ xss permutes \<Union> (set ` set xss); distincts (a # xss)\<rbrakk> \<Longrightarrow> lists_succ (a # xss) permutes \<Union> (set ` set (a # xss))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
distincts []

goal (2 subgoals):
 1. distincts [] \<Longrightarrow> lists_succ [] permutes \<Union> (set ` set [])
 2. \<And>a xss. \<lbrakk>distincts xss \<Longrightarrow> lists_succ xss permutes \<Union> (set ` set xss); distincts (a # xss)\<rbrakk> \<Longrightarrow> lists_succ (a # xss) permutes \<Union> (set ` set (a # xss))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distincts []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
distincts []

goal (1 subgoal):
 1. lists_succ [] permutes \<Union> (set ` set [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lists_succ [] permutes \<Union> (set ` set [])

goal (1 subgoal):
 1. \<And>a xss. \<lbrakk>distincts xss \<Longrightarrow> lists_succ xss permutes \<Union> (set ` set xss); distincts (a # xss)\<rbrakk> \<Longrightarrow> lists_succ (a # xss) permutes \<Union> (set ` set (a # xss))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xss. \<lbrakk>distincts xss \<Longrightarrow> lists_succ xss permutes \<Union> (set ` set xss); distincts (a # xss)\<rbrakk> \<Longrightarrow> lists_succ (a # xss) permutes \<Union> (set ` set (a # xss))
[PROOF STEP]
case (Cons xs xss)
[PROOF STATE]
proof (state)
this:
distincts xss \<Longrightarrow> lists_succ xss permutes \<Union> (set ` set xss)
distincts (xs # xss)

goal (1 subgoal):
 1. \<And>a xss. \<lbrakk>distincts xss \<Longrightarrow> lists_succ xss permutes \<Union> (set ` set xss); distincts (a # xss)\<rbrakk> \<Longrightarrow> lists_succ (a # xss) permutes \<Union> (set ` set (a # xss))
[PROOF STEP]
have "list_succ xs permutes (set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_succ xs permutes set xs
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
distincts xss \<Longrightarrow> lists_succ xss permutes \<Union> (set ` set xss)
distincts (xs # xss)

goal (1 subgoal):
 1. list_succ xs permutes set xs
[PROOF STEP]
by (intro list_succ_permutes) (simp add: distincts_def in_set_member)
[PROOF STATE]
proof (state)
this:
list_succ xs permutes set xs

goal (1 subgoal):
 1. \<And>a xss. \<lbrakk>distincts xss \<Longrightarrow> lists_succ xss permutes \<Union> (set ` set xss); distincts (a # xss)\<rbrakk> \<Longrightarrow> lists_succ (a # xss) permutes \<Union> (set ` set (a # xss))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list_succ xs permutes set xs

goal (1 subgoal):
 1. \<And>a xss. \<lbrakk>distincts xss \<Longrightarrow> lists_succ xss permutes \<Union> (set ` set xss); distincts (a # xss)\<rbrakk> \<Longrightarrow> lists_succ (a # xss) permutes \<Union> (set ` set (a # xss))
[PROOF STEP]
have "lists_succ xss permutes (\<Union>ys \<in> set xss. set ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lists_succ xss permutes \<Union> (set ` set xss)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
distincts xss \<Longrightarrow> lists_succ xss permutes \<Union> (set ` set xss)
distincts (xs # xss)

goal (1 subgoal):
 1. lists_succ xss permutes \<Union> (set ` set xss)
[PROOF STEP]
by (auto simp: Cons distincts_def)
[PROOF STATE]
proof (state)
this:
lists_succ xss permutes \<Union> (set ` set xss)

goal (1 subgoal):
 1. \<And>a xss. \<lbrakk>distincts xss \<Longrightarrow> lists_succ xss permutes \<Union> (set ` set xss); distincts (a # xss)\<rbrakk> \<Longrightarrow> lists_succ (a # xss) permutes \<Union> (set ` set (a # xss))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
list_succ xs permutes set xs
lists_succ xss permutes \<Union> (set ` set xss)
[PROOF STEP]
show "lists_succ (xs # xss) permutes (\<Union>ys \<in> set (xs # xss). set ys)"
[PROOF STATE]
proof (prove)
using this:
list_succ xs permutes set xs
lists_succ xss permutes \<Union> (set ` set xss)

goal (1 subgoal):
 1. lists_succ (xs # xss) permutes \<Union> (set ` set (xs # xss))
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
list_succ xs permutes set xs
lists_succ xss permutes \<Union> (set ` set xss)
distincts xss \<Longrightarrow> lists_succ xss permutes \<Union> (set ` set xss)
distincts (xs # xss)

goal (1 subgoal):
 1. lists_succ (xs # xss) permutes \<Union> (set ` set (xs # xss))
[PROOF STEP]
by (auto simp: lists_succ_Cons_pf intro: permutes_compose permutes_subset)
[PROOF STATE]
proof (state)
this:
lists_succ (xs # xss) permutes \<Union> (set ` set (xs # xss))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma scaleRat_zero
  [simp]: "a *R (0::'a) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a *R (0::'a) = (0::'a)
[PROOF STEP]
using scaleRat_right_distrib[of a 0 0]
[PROOF STATE]
proof (prove)
using this:
a *R ((0::'a) + (0::'a)) = a *R (0::'a) + a *R (0::'a)

goal (1 subgoal):
 1. a *R (0::'a) = (0::'a)
[PROOF STEP]
by auto


[STATEMENT]
lemma eventually_nonneg_const [eventually_nonzero_simps]:
  "eventually_nonneg F (\<lambda>_. c) \<longleftrightarrow> F = bot \<or> c \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eventually_nonneg F (\<lambda>_. c) = (F = bot \<or> (0::'b) \<le> c)
[PROOF STEP]
unfolding eventually_nonneg_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>\<^sub>F x in F. (0::'b) \<le> c) = (F = bot \<or> (0::'b) \<le> c)
[PROOF STEP]
by (auto simp: eventually_False)


[STATEMENT]
lemma powr_closureE:
  assumes "g \<in> powr_closure f"
  obtains p where "g = (\<lambda>x. f x powr p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. g = (\<lambda>x. f x powr p) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
g \<in> powr_closure f

goal (1 subgoal):
 1. (\<And>p. g = (\<lambda>x. f x powr p) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding powr_closure_def
[PROOF STATE]
proof (prove)
using this:
g \<in> {\<lambda>x. f x powr p |p. True}

goal (1 subgoal):
 1. (\<And>p. g = (\<lambda>x. f x powr p) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force


[STATEMENT]
lemma rreqs_increase:
  "paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, _), _, (\<xi>', _)). rreqs \<xi> \<subseteq> rreqs \<xi>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), uu_, \<xi>', uu_). rreqs \<xi> \<subseteq> rreqs \<xi>')
[PROOF STEP]
by (inv_cterms simp add: subset_insertI)


[STATEMENT]
lemma inputCases[consumes 1, case_names cInput]:
  fixes a  :: name
  and   x  :: name
  and   P  :: pi
  and   P' :: pi

  assumes Input: "a<x>.P \<longmapsto>\<alpha> \<prec> P'"
  and     A: "\<And>u. Prop (a<u>) (P[x::=u])"

  shows "Prop \<alpha> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
fix x P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
assume "a<x>.P \<longmapsto>\<alpha> \<prec> P'"
[PROOF STATE]
proof (state)
this:
a<x>.P \<longmapsto> \<alpha> \<prec> P'

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a<x>.P \<longmapsto> \<alpha> \<prec> P'

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
assume "(x::name) \<sharp> \<alpha>" and "x \<sharp> P'" and "x \<noteq> a"
[PROOF STATE]
proof (state)
this:
x \<sharp> \<alpha>
x \<sharp> P'
x \<noteq> a

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<sharp> \<alpha>
x \<sharp> P'
x \<noteq> a

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
assume "\<And>u. Prop (a<u>) (P[x::=u])"
[PROOF STATE]
proof (state)
this:
Prop (a<?u>) (P[x::=?u])

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Prop (a<?u>) (P[x::=?u])

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
obtain z::name where "z \<noteq> x" and "z \<sharp> P" and "z \<sharp> \<alpha>" and "z \<sharp> P'"  and "z \<noteq> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<noteq> x; z \<sharp> P; z \<sharp> \<alpha>; z \<sharp> P'; z \<noteq> a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(generate_fresh "name", auto simp add: fresh_prod)
[PROOF STATE]
proof (state)
this:
z \<noteq> x
z \<sharp> P
z \<sharp> \<alpha>
z \<sharp> P'
z \<noteq> a

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
z \<noteq> x
z \<sharp> P
z \<sharp> \<alpha>
z \<sharp> P'
z \<noteq> a

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
obtain z'::name where "z' \<noteq> x" and "z' \<noteq> z" and "z' \<sharp> P" and "z' \<sharp> \<alpha>" and "z' \<sharp> P'" and "z' \<noteq> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>z'. \<lbrakk>z' \<noteq> x; z' \<noteq> z; z' \<sharp> P; z' \<sharp> \<alpha>; z' \<sharp> P'; z' \<noteq> a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(generate_fresh "name", auto simp add: fresh_prod)
[PROOF STATE]
proof (state)
this:
z' \<noteq> x
z' \<noteq> z
z' \<sharp> P
z' \<sharp> \<alpha>
z' \<sharp> P'
z' \<noteq> a

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a<x>.P \<longmapsto> \<alpha> \<prec> P'
x \<sharp> \<alpha>
x \<sharp> P'
x \<noteq> a
Prop (a<?u>) (P[x::=?u])
z \<noteq> x
z \<sharp> P
z \<sharp> \<alpha>
z \<sharp> P'
z \<noteq> a
z' \<noteq> x
z' \<noteq> z
z' \<sharp> P
z' \<sharp> \<alpha>
z' \<sharp> P'
z' \<noteq> a
[PROOF STEP]
have "Prop \<alpha> P'"
[PROOF STATE]
proof (prove)
using this:
a<x>.P \<longmapsto> \<alpha> \<prec> P'
x \<sharp> \<alpha>
x \<sharp> P'
x \<noteq> a
Prop (a<?u>) (P[x::=?u])
z \<noteq> x
z \<sharp> P
z \<sharp> \<alpha>
z \<sharp> P'
z \<noteq> a
z' \<noteq> x
z' \<noteq> z
z' \<sharp> P
z' \<sharp> \<alpha>
z' \<sharp> P'
z' \<noteq> a

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
by(cases rule: TransitionsEarly.strong_cases[where x=x and b=z and xa=z and xb=z and xc=z and xd=z and xe=z
                                                   and y=z' and ya=z'])
        (auto simp add: pi.inject residual.inject abs_fresh alpha)
[PROOF STATE]
proof (state)
this:
Prop \<alpha> P'

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>a<?xa2>.?Pa2 \<longmapsto> \<alpha> \<prec> P'; ?xa2 \<sharp> \<alpha>; ?xa2 \<sharp> P'; ?xa2 \<noteq> a; \<And>u. Prop (a<u>) (?Pa2[?xa2::=u])\<rbrakk> \<Longrightarrow> Prop \<alpha> P'

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
note Goal = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>a<?xa2>.?Pa2 \<longmapsto> \<alpha> \<prec> P'; ?xa2 \<sharp> \<alpha>; ?xa2 \<sharp> P'; ?xa2 \<noteq> a; \<And>u. Prop (a<u>) (?Pa2[?xa2::=u])\<rbrakk> \<Longrightarrow> Prop \<alpha> P'

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
obtain y::name where "y \<sharp> P" and "y \<sharp> \<alpha>" and "y \<sharp> P'" and "y \<noteq> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<sharp> P; y \<sharp> \<alpha>; y \<sharp> P'; y \<noteq> a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(generate_fresh "name") (auto simp add: fresh_prod)
[PROOF STATE]
proof (state)
this:
y \<sharp> P
y \<sharp> \<alpha>
y \<sharp> P'
y \<noteq> a

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
from Input \<open>y \<sharp> P\<close>
[PROOF STATE]
proof (chain)
picking this:
a<x>.P \<longmapsto> \<alpha> \<prec> P'
y \<sharp> P
[PROOF STEP]
have "a<y>.([(x, y)] \<bullet> P) \<longmapsto>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
a<x>.P \<longmapsto> \<alpha> \<prec> P'
y \<sharp> P

goal (1 subgoal):
 1. a<y>.([(x, y)] \<bullet> P) \<longmapsto> \<alpha> \<prec> P'
[PROOF STEP]
by(simp add: alphaInput)
[PROOF STATE]
proof (state)
this:
a<y>.([(x, y)] \<bullet> P) \<longmapsto> \<alpha> \<prec> P'

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a<y>.([(x, y)] \<bullet> P) \<longmapsto> \<alpha> \<prec> P'

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
note \<open>y \<sharp> \<alpha>\<close> \<open>y \<sharp> P'\<close> \<open>y \<noteq> a\<close>
[PROOF STATE]
proof (state)
this:
y \<sharp> \<alpha>
y \<sharp> P'
y \<noteq> a

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y \<sharp> \<alpha>
y \<sharp> P'
y \<noteq> a

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
from A \<open>y \<sharp> P\<close>
[PROOF STATE]
proof (chain)
picking this:
Prop (a<?u>) (P[x::=?u])
y \<sharp> P
[PROOF STEP]
have "\<And>u. Prop (a<u>) (([(x, y)] \<bullet> P)[y::=u])"
[PROOF STATE]
proof (prove)
using this:
Prop (a<?u>) (P[x::=?u])
y \<sharp> P

goal (1 subgoal):
 1. \<And>u. Prop (a<u>) (([(x, y)] \<bullet> P)[y::=u])
[PROOF STEP]
by(simp add: renaming name_swap)
[PROOF STATE]
proof (state)
this:
Prop (a<?u>) (([(x, y)] \<bullet> P)[y::=?u])

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a<y>.([(x, y)] \<bullet> P) \<longmapsto> \<alpha> \<prec> P'
y \<sharp> \<alpha>
y \<sharp> P'
y \<noteq> a
Prop (a<?u>) (([(x, y)] \<bullet> P)[y::=?u])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a<y>.([(x, y)] \<bullet> P) \<longmapsto> \<alpha> \<prec> P'
y \<sharp> \<alpha>
y \<sharp> P'
y \<noteq> a
Prop (a<?u>) (([(x, y)] \<bullet> P)[y::=?u])

goal (1 subgoal):
 1. Prop \<alpha> P'
[PROOF STEP]
by(rule Goal)
[PROOF STATE]
proof (state)
this:
Prop \<alpha> P'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma smc_CAT_Comp_vdomain: "\<D>\<^sub>\<circ> (smc_CAT \<alpha>\<lparr>Comp\<rparr>) = composable_arrs (smc_CAT \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (smc_CAT \<alpha>\<lparr>Comp\<rparr>) = composable_arrs (smc_CAT \<alpha>)
[PROOF STEP]
unfolding smc_CAT_Comp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<lambda>\<GG>\<FF>\<in>\<^sub>\<circ>composable_arrs (smc_CAT \<alpha>). \<GG>\<FF>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>\<FF>\<lparr>1\<^sub>\<nat>\<rparr>) = composable_arrs (smc_CAT \<alpha>)
[PROOF STEP]
by auto


[STATEMENT]
lemma (in \<Z>) smc_CAT_obj_initialI: "obj_initial (smc_CAT \<alpha>) cat_0"
  \<comment>\<open>
  See \cite{noauthor_nlab_nodate}\footnote{\url{
  https://ncatlab.org/nlab/show/initial+object
  }}).
  \<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obj_initial (smc_CAT \<alpha>) cat_0
[PROOF STEP]
unfolding obj_initial_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obj_terminal (op_smc (smc_CAT \<alpha>)) cat_0
[PROOF STEP]
proof(intro obj_terminalI, unfold smc_op_simps smc_CAT_is_arr_iff smc_CAT_Obj_iff)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. category \<alpha> cat_0
 2. \<And>a. category \<alpha> a \<Longrightarrow> Ex1 (is_functor \<alpha> cat_0 a)
[PROOF STEP]
show "category \<alpha> cat_0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category \<alpha> cat_0
[PROOF STEP]
by (intro category_cat_0)
[PROOF STATE]
proof (state)
this:
category \<alpha> cat_0

goal (1 subgoal):
 1. \<And>a. category \<alpha> a \<Longrightarrow> Ex1 (is_functor \<alpha> cat_0 a)
[PROOF STEP]
fix \<AA>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. category \<alpha> a \<Longrightarrow> Ex1 (is_functor \<alpha> cat_0 a)
[PROOF STEP]
assume "category \<alpha> \<AA>"
[PROOF STATE]
proof (state)
this:
category \<alpha> \<AA>

goal (1 subgoal):
 1. \<And>a. category \<alpha> a \<Longrightarrow> Ex1 (is_functor \<alpha> cat_0 a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
category \<alpha> \<AA>
[PROOF STEP]
interpret category \<alpha> \<AA>
[PROOF STATE]
proof (prove)
using this:
category \<alpha> \<AA>

goal (1 subgoal):
 1. category \<alpha> \<AA>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. category \<alpha> a \<Longrightarrow> Ex1 (is_functor \<alpha> cat_0 a)
[PROOF STEP]
show "\<exists>!f. f : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!f. f : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?a : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 2. \<And>f. f : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<Longrightarrow> f = ?a
[PROOF STEP]
show cf_0: "cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (simp add: cf_0_is_ft_functor category_axioms is_ft_functor.axioms(1))
[PROOF STATE]
proof (state)
this:
cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<And>f. f : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<Longrightarrow> f = cf_0 \<AA>
[PROOF STEP]
fix \<FF>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. f : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<Longrightarrow> f = cf_0 \<AA>
[PROOF STEP]
assume prems: "\<FF> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (state)
this:
\<FF> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<And>f. f : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<Longrightarrow> f = cf_0 \<AA>
[PROOF STEP]
interpret \<FF>: is_functor \<alpha> cat_0 \<AA> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
using prems
[PROOF STATE]
proof (prove)
using this:
\<FF> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<FF> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. f : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<Longrightarrow> f = cf_0 \<AA>
[PROOF STEP]
show "\<FF> = cf_0 \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> = cf_0 \<AA>
[PROOF STEP]
proof(rule cf_eqI)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<FF> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. cf_0 \<AA> : ?\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\

 3. \<FF>\<lparr>ObjMap\<rparr> = cf_0 \<AA>\<lparr>ObjMap\<rparr>
 4. \<FF>\<lparr>ArrMap\<rparr> = cf_0 \<AA>\<lparr>ArrMap\<rparr>
 5. ?\<AA> = ?\<CC>
 6. ?\<BB> = ?\

[PROOF STEP]
show "\<FF> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (simp add: prems)
[PROOF STATE]
proof (state)
this:
\<FF> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (5 subgoals):
 1. cf_0 \<AA> : ?\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\

 2. \<FF>\<lparr>ObjMap\<rparr> = cf_0 \<AA>\<lparr>ObjMap\<rparr>
 3. \<FF>\<lparr>ArrMap\<rparr> = cf_0 \<AA>\<lparr>ArrMap\<rparr>
 4. cat_0 = ?\<CC>
 5. \<AA> = ?\

[PROOF STEP]
from cf_0
[PROOF STATE]
proof (chain)
picking this:
cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show "cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
unfolding smc_CAT_is_arr_iff
[PROOF STATE]
proof (prove)
using this:
cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (4 subgoals):
 1. \<FF>\<lparr>ObjMap\<rparr> = cf_0 \<AA>\<lparr>ObjMap\<rparr>
 2. \<FF>\<lparr>ArrMap\<rparr> = cf_0 \<AA>\<lparr>ArrMap\<rparr>
 3. cat_0 = cat_0
 4. \<AA> = \<AA>
[PROOF STEP]
have "\<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = []\<^sub>\<circ>
[PROOF STEP]
by (auto simp: cat_0_components cat_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = []\<^sub>\<circ>

goal (4 subgoals):
 1. \<FF>\<lparr>ObjMap\<rparr> = cf_0 \<AA>\<lparr>ObjMap\<rparr>
 2. \<FF>\<lparr>ArrMap\<rparr> = cf_0 \<AA>\<lparr>ArrMap\<rparr>
 3. cat_0 = cat_0
 4. \<AA> = \<AA>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = []\<^sub>\<circ>
[PROOF STEP]
show "\<FF>\<lparr>ObjMap\<rparr> = cf_0 \<AA>\<lparr>ObjMap\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = []\<^sub>\<circ>

goal (1 subgoal):
 1. \<FF>\<lparr>ObjMap\<rparr> = cf_0 \<AA>\<lparr>ObjMap\<rparr>
[PROOF STEP]
using \<FF>.ObjMap.vbrelation_vintersection_vdomain
[PROOF STATE]
proof (prove)
using this:
\<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = []\<^sub>\<circ>
\<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) \<inter>\<^sub>\<circ> \<D>\<^sub>\<circ> ?s = []\<^sub>\<circ> \<Longrightarrow> \<FF>\<lparr>ObjMap\<rparr> \<inter>\<^sub>\<circ> ?s = []\<^sub>\<circ>

goal (1 subgoal):
 1. \<FF>\<lparr>ObjMap\<rparr> = cf_0 \<AA>\<lparr>ObjMap\<rparr>
[PROOF STEP]
by (auto simp: cf_0_components)
[PROOF STATE]
proof (state)
this:
\<FF>\<lparr>ObjMap\<rparr> = cf_0 \<AA>\<lparr>ObjMap\<rparr>

goal (3 subgoals):
 1. \<FF>\<lparr>ArrMap\<rparr> = cf_0 \<AA>\<lparr>ArrMap\<rparr>
 2. cat_0 = cat_0
 3. \<AA> = \<AA>
[PROOF STEP]
have "\<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = []\<^sub>\<circ>
[PROOF STEP]
by (auto simp: cat_0_components cat_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = []\<^sub>\<circ>

goal (3 subgoals):
 1. \<FF>\<lparr>ArrMap\<rparr> = cf_0 \<AA>\<lparr>ArrMap\<rparr>
 2. cat_0 = cat_0
 3. \<AA> = \<AA>
[PROOF STEP]
with \<FF>.ArrMap.vbrelation_vintersection_vdomain
[PROOF STATE]
proof (chain)
picking this:
\<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) \<inter>\<^sub>\<circ> \<D>\<^sub>\<circ> ?s = []\<^sub>\<circ> \<Longrightarrow> \<FF>\<lparr>ArrMap\<rparr> \<inter>\<^sub>\<circ> ?s = []\<^sub>\<circ>
\<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = []\<^sub>\<circ>
[PROOF STEP]
show
        "\<FF>\<lparr>ArrMap\<rparr> = cf_0 \<AA>\<lparr>ArrMap\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) \<inter>\<^sub>\<circ> \<D>\<^sub>\<circ> ?s = []\<^sub>\<circ> \<Longrightarrow> \<FF>\<lparr>ArrMap\<rparr> \<inter>\<^sub>\<circ> ?s = []\<^sub>\<circ>
\<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = []\<^sub>\<circ>

goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr> = cf_0 \<AA>\<lparr>ArrMap\<rparr>
[PROOF STEP]
by (auto simp: cf_0_components)
[PROOF STATE]
proof (state)
this:
\<FF>\<lparr>ArrMap\<rparr> = cf_0 \<AA>\<lparr>ArrMap\<rparr>

goal (2 subgoals):
 1. cat_0 = cat_0
 2. \<AA> = \<AA>
[PROOF STEP]
qed (simp_all add: cf_0_components)
[PROOF STATE]
proof (state)
this:
\<FF> = cf_0 \<AA>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!f. f : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cblinfun_sum_image_distr:
  \<open>(\<Sum>i\<in>I. A i) *\<^sub>S S \<le> (SUP i\<in>I. A i *\<^sub>S S)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum A I *\<^sub>S S \<le> (\<Squnion>i\<in>I. A i *\<^sub>S S)
[PROOF STEP]
proof (cases \<open>finite I\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite I \<Longrightarrow> sum A I *\<^sub>S S \<le> (\<Squnion>i\<in>I. A i *\<^sub>S S)
 2. infinite I \<Longrightarrow> sum A I *\<^sub>S S \<le> (\<Squnion>i\<in>I. A i *\<^sub>S S)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
finite I

goal (2 subgoals):
 1. finite I \<Longrightarrow> sum A I *\<^sub>S S \<le> (\<Squnion>i\<in>I. A i *\<^sub>S S)
 2. infinite I \<Longrightarrow> sum A I *\<^sub>S S \<le> (\<Squnion>i\<in>I. A i *\<^sub>S S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite I
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite I

goal (1 subgoal):
 1. sum A I *\<^sub>S S \<le> (\<Squnion>i\<in>I. A i *\<^sub>S S)
[PROOF STEP]
proof induction
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sum A {} *\<^sub>S S \<le> (\<Squnion>i\<in>{}. A i *\<^sub>S S)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; sum A F *\<^sub>S S \<le> (\<Squnion>i\<in>F. A i *\<^sub>S S)\<rbrakk> \<Longrightarrow> sum A (insert x F) *\<^sub>S S \<le> (\<Squnion>i\<in>insert x F. A i *\<^sub>S S)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. sum A {} *\<^sub>S S \<le> (\<Squnion>i\<in>{}. A i *\<^sub>S S)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; sum A F *\<^sub>S S \<le> (\<Squnion>i\<in>F. A i *\<^sub>S S)\<rbrakk> \<Longrightarrow> sum A (insert x F) *\<^sub>S S \<le> (\<Squnion>i\<in>insert x F. A i *\<^sub>S S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum A {} *\<^sub>S S \<le> (\<Squnion>i\<in>{}. A i *\<^sub>S S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum A {} *\<^sub>S S \<le> (\<Squnion>i\<in>{}. A i *\<^sub>S S)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; sum A F *\<^sub>S S \<le> (\<Squnion>i\<in>F. A i *\<^sub>S S)\<rbrakk> \<Longrightarrow> sum A (insert x F) *\<^sub>S S \<le> (\<Squnion>i\<in>insert x F. A i *\<^sub>S S)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; sum A F *\<^sub>S S \<le> (\<Squnion>i\<in>F. A i *\<^sub>S S)\<rbrakk> \<Longrightarrow> sum A (insert x F) *\<^sub>S S \<le> (\<Squnion>i\<in>insert x F. A i *\<^sub>S S)
[PROOF STEP]
case (insert x F)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
sum A F *\<^sub>S S \<le> (\<Squnion>i\<in>F. A i *\<^sub>S S)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; sum A F *\<^sub>S S \<le> (\<Squnion>i\<in>F. A i *\<^sub>S S)\<rbrakk> \<Longrightarrow> sum A (insert x F) *\<^sub>S S \<le> (\<Squnion>i\<in>insert x F. A i *\<^sub>S S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite F
x \<notin> F
sum A F *\<^sub>S S \<le> (\<Squnion>i\<in>F. A i *\<^sub>S S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
sum A F *\<^sub>S S \<le> (\<Squnion>i\<in>F. A i *\<^sub>S S)

goal (1 subgoal):
 1. sum A (insert x F) *\<^sub>S S \<le> (\<Squnion>i\<in>insert x F. A i *\<^sub>S S)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite F; x \<notin> F; sum A F *\<^sub>S S \<le> (\<Squnion>i\<in>F. A i *\<^sub>S S)\<rbrakk> \<Longrightarrow> (A x + sum A F) *\<^sub>S S \<le> A x *\<^sub>S S \<squnion> (\<Squnion>i\<in>F. A i *\<^sub>S S)
[PROOF STEP]
by (smt (z3) cblinfun_plus_image_distr inf_sup_aci(6) le_iff_sup)
[PROOF STATE]
proof (state)
this:
sum A (insert x F) *\<^sub>S S \<le> (\<Squnion>i\<in>insert x F. A i *\<^sub>S S)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum A I *\<^sub>S S \<le> (\<Squnion>i\<in>I. A i *\<^sub>S S)

goal (1 subgoal):
 1. infinite I \<Longrightarrow> sum A I *\<^sub>S S \<le> (\<Squnion>i\<in>I. A i *\<^sub>S S)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite I \<Longrightarrow> sum A I *\<^sub>S S \<le> (\<Squnion>i\<in>I. A i *\<^sub>S S)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
infinite I

goal (1 subgoal):
 1. infinite I \<Longrightarrow> sum A I *\<^sub>S S \<le> (\<Squnion>i\<in>I. A i *\<^sub>S S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infinite I
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
infinite I

goal (1 subgoal):
 1. sum A I *\<^sub>S S \<le> (\<Squnion>i\<in>I. A i *\<^sub>S S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum A I *\<^sub>S S \<le> (\<Squnion>i\<in>I. A i *\<^sub>S S)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cut_less_Max_eq_Diff: "finite I \<Longrightarrow> I \<down>< (Max I) = I - {Max I}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite I \<Longrightarrow> I \<down>< Max I = I - {Max I}
[PROOF STEP]
by blast


[STATEMENT]
lemma tree_of_zipper_id[iff]: "tree_of_zipper (zipper_of_tree t) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tree_of_zipper (zipper_of_tree t) = t
[PROOF STEP]
by(simp add: zipper_of_tree_def)