[STATEMENT]
lemma rel_eventually_llbound:
  assumes "x \<sim> y"
  shows "\<forall>\<^sub>F w in llbound. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
have xy:"fst x \<in> I" "fst y \<in> I" "snd x \<in> \<FF> (fst x)" "snd y \<in> \<FF> (fst y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst x \<in> I &&& fst y \<in> I) &&& snd x \<in> \<FF> (fst x) &&& snd y \<in> \<FF> (fst y)
[PROOF STEP]
using \<open>x \<sim> y\<close>
[PROOF STATE]
proof (prove)
using this:
x \<sim> y

goal (1 subgoal):
 1. (fst x \<in> I &&& fst y \<in> I) &&& snd x \<in> \<FF> (fst x) &&& snd y \<in> \<FF> (fst y)
[PROOF STEP]
unfolding rel_def
[PROOF STATE]
proof (prove)
using this:
(fst x \<in> I \<and> fst y \<in> I) \<and> (snd x \<in> \<FF> (fst x) \<and> snd y \<in> \<FF> (fst y)) \<and> (\<exists>W. W \<in> I \<and> W \<subseteq> fst x \<inter> fst y \<and> \<rho> (fst x) W (snd x) = \<rho> (fst y) W (snd y))

goal (1 subgoal):
 1. (fst x \<in> I &&& fst y \<in> I) &&& snd x \<in> \<FF> (fst x) &&& snd y \<in> \<FF> (fst y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst x \<in> I
fst y \<in> I
snd x \<in> \<FF> (fst x)
snd y \<in> \<FF> (fst y)

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
obtain w0 where w0:"w0 \<in> I" "w0 \<subseteq> fst x \<inter> fst y" "\<rho> (fst x) w0 (snd x) = \<rho> (fst y) w0 (snd y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>w0. \<lbrakk>w0 \<in> I; w0 \<subseteq> fst x \<inter> fst y; \<rho> (fst x) w0 (snd x) = \<rho> (fst y) w0 (snd y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>x \<sim> y\<close>
[PROOF STATE]
proof (prove)
using this:
x \<sim> y

goal (1 subgoal):
 1. (\<And>w0. \<lbrakk>w0 \<in> I; w0 \<subseteq> fst x \<inter> fst y; \<rho> (fst x) w0 (snd x) = \<rho> (fst y) w0 (snd y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding rel_def
[PROOF STATE]
proof (prove)
using this:
(fst x \<in> I \<and> fst y \<in> I) \<and> (snd x \<in> \<FF> (fst x) \<and> snd y \<in> \<FF> (fst y)) \<and> (\<exists>W. W \<in> I \<and> W \<subseteq> fst x \<inter> fst y \<and> \<rho> (fst x) W (snd x) = \<rho> (fst y) W (snd y))

goal (1 subgoal):
 1. (\<And>w0. \<lbrakk>w0 \<in> I; w0 \<subseteq> fst x \<inter> fst y; \<rho> (fst x) w0 (snd x) = \<rho> (fst y) w0 (snd y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w0 \<in> I
w0 \<subseteq> fst x \<inter> fst y
\<rho> (fst x) w0 (snd x) = \<rho> (fst y) w0 (snd y)

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
interpret xw0:ring_homomorphism "\<rho> (fst x) w0" "\<FF> (fst x)" "+\<^bsub>fst x\<^esub>" "\<cdot>\<^bsub>fst x\<^esub>" "\<zero>\<^bsub>fst x\<^esub>"
        "\<one>\<^bsub>fst x\<^esub>" "\<FF> w0" "+\<^bsub>w0\<^esub>" "\<cdot>\<^bsub>w0\<^esub>" "\<zero>\<^bsub>w0\<^esub>" "\<one>\<^bsub>w0\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism (\<rho> (fst x) w0) (\<FF> (fst x)) +\<^bsub>fst x\<^esub> \<cdot>\<^bsub>fst x\<^esub> \<zero>\<^bsub>fst x\<^esub> \<one>\<^bsub>fst x\<^esub> (\<FF> w0) +\<^bsub>w0\<^esub> \<cdot>\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub>
[PROOF STEP]
by (meson is_ring_morphism le_inf_iff subset_of_opens w0 xy(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
interpret yw0:ring_homomorphism "\<rho> (fst y) w0" "\<FF> (fst y)" "+\<^bsub>fst y\<^esub>" "\<cdot>\<^bsub>fst y\<^esub>" "\<zero>\<^bsub>fst y\<^esub>"
        "\<one>\<^bsub>fst y\<^esub>" "\<FF> w0" "+\<^bsub>w0\<^esub>" "\<cdot>\<^bsub>w0\<^esub>" "\<zero>\<^bsub>w0\<^esub>" "\<one>\<^bsub>w0\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism (\<rho> (fst y) w0) (\<FF> (fst y)) +\<^bsub>fst y\<^esub> \<cdot>\<^bsub>fst y\<^esub> \<zero>\<^bsub>fst y\<^esub> \<one>\<^bsub>fst y\<^esub> (\<FF> w0) +\<^bsub>w0\<^esub> \<cdot>\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub>
[PROOF STEP]
using w0
[PROOF STATE]
proof (prove)
using this:
w0 \<in> I
w0 \<subseteq> fst x \<inter> fst y
\<rho> (fst x) w0 (snd x) = \<rho> (fst y) w0 (snd y)

goal (1 subgoal):
 1. ring_homomorphism (\<rho> (fst y) w0) (\<FF> (fst y)) +\<^bsub>fst y\<^esub> \<cdot>\<^bsub>fst y\<^esub> \<zero>\<^bsub>fst y\<^esub> \<one>\<^bsub>fst y\<^esub> (\<FF> w0) +\<^bsub>w0\<^esub> \<cdot>\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub>
[PROOF STEP]
by (metis is_ring_morphism le_inf_iff subset_of_opens  xy(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
have "\<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)" if "w \<subseteq> w0" "w \<in> I" for w
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
interpret w0w:ring_homomorphism "\<rho> w0 w" "\<FF> w0" "+\<^bsub>w0\<^esub>" "\<cdot>\<^bsub>w0\<^esub>" "\<zero>\<^bsub>w0\<^esub>" "\<one>\<^bsub>w0\<^esub>" "\<FF> w"
                  "+\<^bsub>w\<^esub>" "\<cdot>\<^bsub>w\<^esub>" "\<zero>\<^bsub>w\<^esub>" "\<one>\<^bsub>w\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism (\<rho> w0 w) (\<FF> w0) +\<^bsub>w0\<^esub> \<cdot>\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub> (\<FF> w) +\<^bsub>w\<^esub> \<cdot>\<^bsub>w\<^esub> \<zero>\<^bsub>w\<^esub> \<one>\<^bsub>w\<^esub>
[PROOF STEP]
using is_ring_morphism subset_of_opens that w0(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_open ?U; is_open ?V; ?V \<subseteq> ?U\<rbrakk> \<Longrightarrow> ring_homomorphism (\<rho> ?U ?V) (\<FF> ?U) +\<^bsub>?U\<^esub> \<cdot>\<^bsub>?U\<^esub> \<zero>\<^bsub>?U\<^esub> \<one>\<^bsub>?U\<^esub> (\<FF> ?V) +\<^bsub>?V\<^esub> \<cdot>\<^bsub>?V\<^esub> \<zero>\<^bsub>?V\<^esub> \<one>\<^bsub>?V\<^esub>
?U \<in> I \<Longrightarrow> is_open ?U
w \<subseteq> w0
w \<in> I
w0 \<in> I

goal (1 subgoal):
 1. ring_homomorphism (\<rho> w0 w) (\<FF> w0) +\<^bsub>w0\<^esub> \<cdot>\<^bsub>w0\<^esub> \<zero>\<^bsub>w0\<^esub> \<one>\<^bsub>w0\<^esub> (\<FF> w) +\<^bsub>w\<^esub> \<cdot>\<^bsub>w\<^esub> \<zero>\<^bsub>w\<^esub> \<one>\<^bsub>w\<^esub>
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
have "\<rho> (fst x) w (snd x) = (\<rho> w0 w \<circ> \<rho> (fst x) w0) (snd x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho> (fst x) w (snd x) = (\<rho> w0 w \<circ> \<rho> (fst x) w0) (snd x)
[PROOF STEP]
by (meson assoc_comp le_inf_iff subset_of_opens that w0 xy)
[PROOF STATE]
proof (state)
this:
\<rho> (fst x) w (snd x) = (\<rho> w0 w \<circ> \<rho> (fst x) w0) (snd x)

goal (1 subgoal):
 1. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<rho> (fst x) w (snd x) = (\<rho> w0 w \<circ> \<rho> (fst x) w0) (snd x)

goal (1 subgoal):
 1. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
have "... = (\<rho> w0 w \<circ> \<rho> (fst y) w0) (snd y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<rho> w0 w \<circ> \<rho> (fst x) w0) (snd x) = (\<rho> w0 w \<circ> \<rho> (fst y) w0) (snd y)
[PROOF STEP]
unfolding comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho> w0 w (\<rho> (fst x) w0 (snd x)) = \<rho> w0 w (\<rho> (fst y) w0 (snd y))
[PROOF STEP]
using w0(3)
[PROOF STATE]
proof (prove)
using this:
\<rho> (fst x) w0 (snd x) = \<rho> (fst y) w0 (snd y)

goal (1 subgoal):
 1. \<rho> w0 w (\<rho> (fst x) w0 (snd x)) = \<rho> w0 w (\<rho> (fst y) w0 (snd y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<rho> w0 w \<circ> \<rho> (fst x) w0) (snd x) = (\<rho> w0 w \<circ> \<rho> (fst y) w0) (snd y)

goal (1 subgoal):
 1. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<rho> w0 w \<circ> \<rho> (fst x) w0) (snd x) = (\<rho> w0 w \<circ> \<rho> (fst y) w0) (snd y)

goal (1 subgoal):
 1. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
have "... = \<rho> (fst y) w (snd y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<rho> w0 w \<circ> \<rho> (fst y) w0) (snd y) = \<rho> (fst y) w (snd y)
[PROOF STEP]
using w0 xy
[PROOF STATE]
proof (prove)
using this:
w0 \<in> I
w0 \<subseteq> fst x \<inter> fst y
\<rho> (fst x) w0 (snd x) = \<rho> (fst y) w0 (snd y)
fst x \<in> I
fst y \<in> I
snd x \<in> \<FF> (fst x)
snd y \<in> \<FF> (fst y)

goal (1 subgoal):
 1. (\<rho> w0 w \<circ> \<rho> (fst y) w0) (snd y) = \<rho> (fst y) w (snd y)
[PROOF STEP]
by (metis Int_subset_iff assoc_comp subset_of_opens that)
[PROOF STATE]
proof (state)
this:
(\<rho> w0 w \<circ> \<rho> (fst y) w0) (snd y) = \<rho> (fst y) w (snd y)

goal (1 subgoal):
 1. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)

goal (1 subgoal):
 1. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?w1 \<subseteq> w0; ?w1 \<in> I\<rbrakk> \<Longrightarrow> \<rho> (fst x) ?w1 (snd x) = \<rho> (fst y) ?w1 (snd y)

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
with w0
[PROOF STATE]
proof (chain)
picking this:
w0 \<in> I
w0 \<subseteq> fst x \<inter> fst y
\<rho> (fst x) w0 (snd x) = \<rho> (fst y) w0 (snd y)
\<lbrakk>?w1 \<subseteq> w0; ?w1 \<in> I\<rbrakk> \<Longrightarrow> \<rho> (fst x) ?w1 (snd x) = \<rho> (fst y) ?w1 (snd y)
[PROOF STEP]
have "\<exists>w0. w0 \<in> I \<and> w0 \<subseteq> fst x \<inter> fst y
            \<and> (\<forall>w. (w\<subseteq>w0 \<and> w\<in>I) \<longrightarrow> \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y))"
[PROOF STATE]
proof (prove)
using this:
w0 \<in> I
w0 \<subseteq> fst x \<inter> fst y
\<rho> (fst x) w0 (snd x) = \<rho> (fst y) w0 (snd y)
\<lbrakk>?w1 \<subseteq> w0; ?w1 \<in> I\<rbrakk> \<Longrightarrow> \<rho> (fst x) ?w1 (snd x) = \<rho> (fst y) ?w1 (snd y)

goal (1 subgoal):
 1. \<exists>w0. w0 \<in> I \<and> w0 \<subseteq> fst x \<inter> fst y \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>w0. w0 \<in> I \<and> w0 \<subseteq> fst x \<inter> fst y \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y))

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>w0. w0 \<in> I \<and> w0 \<subseteq> fst x \<inter> fst y \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y))
[PROOF STEP]
have "\<forall>\<^sub>F w in lbound {fst x,fst y}. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)"
[PROOF STATE]
proof (prove)
using this:
\<exists>w0. w0 \<in> I \<and> w0 \<subseteq> fst x \<inter> fst y \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y))

goal (1 subgoal):
 1. \<forall>\<^sub>F w in lbound {fst x, fst y}. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
apply (subst eventually_lbound_finite)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<exists>w0. w0 \<in> I \<and> w0 \<subseteq> fst x \<inter> fst y \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)) \<Longrightarrow> finite {fst x, fst y}
 2. \<exists>w0. w0 \<in> I \<and> w0 \<subseteq> fst x \<inter> fst y \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)) \<Longrightarrow> {fst x, fst y} \<noteq> {}
 3. \<exists>w0. w0 \<in> I \<and> w0 \<subseteq> fst x \<inter> fst y \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)) \<Longrightarrow> {fst x, fst y} \<subseteq> I
 4. \<exists>w0. w0 \<in> I \<and> w0 \<subseteq> fst x \<inter> fst y \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)) \<Longrightarrow> \<exists>w0. w0 \<in> I \<and> Ball {fst x, fst y} ((\<subseteq>) w0) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y))
[PROOF STEP]
using xy(1,2)
[PROOF STATE]
proof (prove)
using this:
fst x \<in> I
fst y \<in> I

goal (4 subgoals):
 1. \<exists>w0. w0 \<in> I \<and> w0 \<subseteq> fst x \<inter> fst y \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)) \<Longrightarrow> finite {fst x, fst y}
 2. \<exists>w0. w0 \<in> I \<and> w0 \<subseteq> fst x \<inter> fst y \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)) \<Longrightarrow> {fst x, fst y} \<noteq> {}
 3. \<exists>w0. w0 \<in> I \<and> w0 \<subseteq> fst x \<inter> fst y \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)) \<Longrightarrow> {fst x, fst y} \<subseteq> I
 4. \<exists>w0. w0 \<in> I \<and> w0 \<subseteq> fst x \<inter> fst y \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)) \<Longrightarrow> \<exists>w0. w0 \<in> I \<and> Ball {fst x, fst y} ((\<subseteq>) w0) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in lbound {fst x, fst y}. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F w in lbound {fst x, fst y}. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F w in lbound {fst x, fst y}. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
using llbound_lbound[of "{fst x,fst y}"] xy(1,2)
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F w in lbound {fst x, fst y}. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
\<lbrakk>finite {fst x, fst y}; {fst x, fst y} \<noteq> {}; {fst x, fst y} \<subseteq> I\<rbrakk> \<Longrightarrow> lbound {fst x, fst y} = llbound
fst x \<in> I
fst y \<in> I

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. \<rho> (fst x) w (snd x) = \<rho> (fst y) w (snd y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_rel_well_defined_llbound:
  fixes x y:: "'a set \<times> 'b" and z z':: "'a set"
  assumes "x \<in> Sigma I \<FF>" "y \<in> Sigma I \<FF>"
  assumes z:"z\<in>I" "z \<subseteq> fst x" "z \<subseteq> fst y"
  shows "\<forall>\<^sub>F w in llbound. \<lfloor>z, add_str z (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> =
          \<lfloor>w, add_str w (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>" (is "\<forall>\<^sub>F w in _. ?P w")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
[PROOF STEP]
have  "\<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow>?P w "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
[PROOF STEP]
by (meson add_rel_well_defined assms(1) assms(2) dual_order.trans z(1) z(2) z(3))
[PROOF STATE]
proof (state)
this:
\<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
[PROOF STEP]
have "\<forall>\<^sub>F w in lbound {fst x,fst y}. ?P w"
[PROOF STATE]
proof (prove)
using this:
\<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>

goal (1 subgoal):
 1. \<forall>\<^sub>F w in lbound {fst x, fst y}. \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
[PROOF STEP]
apply (subst eventually_lbound_finite)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor> \<Longrightarrow> finite {fst x, fst y}
 2. \<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor> \<Longrightarrow> {fst x, fst y} \<noteq> {}
 3. \<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor> \<Longrightarrow> {fst x, fst y} \<subseteq> I
 4. \<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor> \<Longrightarrow> \<exists>w0. w0 \<in> I \<and> Ball {fst x, fst y} ((\<subseteq>) w0) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> Sigma I \<FF>
y \<in> Sigma I \<FF>
z \<in> I
z \<subseteq> fst x
z \<subseteq> fst y

goal (4 subgoals):
 1. \<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor> \<Longrightarrow> finite {fst x, fst y}
 2. \<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor> \<Longrightarrow> {fst x, fst y} \<noteq> {}
 3. \<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor> \<Longrightarrow> {fst x, fst y} \<subseteq> I
 4. \<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor> \<Longrightarrow> \<exists>w0. w0 \<in> I \<and> Ball {fst x, fst y} ((\<subseteq>) w0) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in lbound {fst x, fst y}. \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F w in lbound {fst x, fst y}. \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F w in lbound {fst x, fst y}. \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
[PROOF STEP]
using llbound_lbound[of "{fst x,fst y}"] assms(1,2)
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F w in lbound {fst x, fst y}. \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
\<lbrakk>finite {fst x, fst y}; {fst x, fst y} \<noteq> {}; {fst x, fst y} \<subseteq> I\<rbrakk> \<Longrightarrow> lbound {fst x, fst y} = llbound
x \<in> Sigma I \<FF>
y \<in> Sigma I \<FF>

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. \<lfloor>z, +\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_rel_well_defined_llbound:
  fixes x y:: "'a set \<times> 'b" and z z':: "'a set"
  assumes "x \<in> Sigma I \<FF>" "y \<in> Sigma I \<FF>"
  assumes z:"z\<in>I" "z \<subseteq> fst x" "z \<subseteq> fst y"
  shows "\<forall>\<^sub>F w in llbound. \<lfloor>z, mult_str z (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> =
          \<lfloor>w, mult_str w (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>" (is "\<forall>\<^sub>F w in _. ?P w")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
[PROOF STEP]
have  "\<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow>?P w "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
[PROOF STEP]
by (meson mult_rel_well_defined assms(1) assms(2) dual_order.trans z(1) z(2) z(3))
[PROOF STATE]
proof (state)
this:
\<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
[PROOF STEP]
have "\<forall>\<^sub>F w in lbound {fst x,fst y}. ?P w"
[PROOF STATE]
proof (prove)
using this:
\<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>

goal (1 subgoal):
 1. \<forall>\<^sub>F w in lbound {fst x, fst y}. \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
[PROOF STEP]
apply (subst eventually_lbound_finite)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor> \<Longrightarrow> finite {fst x, fst y}
 2. \<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor> \<Longrightarrow> {fst x, fst y} \<noteq> {}
 3. \<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor> \<Longrightarrow> {fst x, fst y} \<subseteq> I
 4. \<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor> \<Longrightarrow> \<exists>w0. w0 \<in> I \<and> Ball {fst x, fst y} ((\<subseteq>) w0) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> Sigma I \<FF>
y \<in> Sigma I \<FF>
z \<in> I
z \<subseteq> fst x
z \<subseteq> fst y

goal (4 subgoals):
 1. \<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor> \<Longrightarrow> finite {fst x, fst y}
 2. \<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor> \<Longrightarrow> {fst x, fst y} \<noteq> {}
 3. \<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor> \<Longrightarrow> {fst x, fst y} \<subseteq> I
 4. \<forall>w. w \<subseteq> z \<and> w \<in> I \<longrightarrow> \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor> \<Longrightarrow> \<exists>w0. w0 \<in> I \<and> Ball {fst x, fst y} ((\<subseteq>) w0) \<and> (\<forall>w. w \<subseteq> w0 \<and> w \<in> I \<longrightarrow> \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in lbound {fst x, fst y}. \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F w in lbound {fst x, fst y}. \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F w in lbound {fst x, fst y}. \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
[PROOF STEP]
using llbound_lbound[of "{fst x,fst y}"] assms(1,2)
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F w in lbound {fst x, fst y}. \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
\<lbrakk>finite {fst x, fst y}; {fst x, fst y} \<noteq> {}; {fst x, fst y} \<subseteq> I\<rbrakk> \<Longrightarrow> lbound {fst x, fst y} = llbound
x \<in> Sigma I \<FF>
y \<in> Sigma I \<FF>

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_rel_class_of:
  fixes U V W :: "'a set" and x y :: 'b
  assumes uv_sigma:"(U, x) \<in> Sigma I \<FF>" "(V, y) \<in> Sigma I \<FF>"
  assumes w:"W \<in> I" "W \<subseteq> U" "W \<subseteq> V"
  shows "add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
define ux where "ux = (SOME ux. ux \<in> \<lfloor>U, x\<rfloor>)"
[PROOF STATE]
proof (state)
this:
ux = (SOME ux. ux \<in> \<lfloor>U, x\<rfloor>)

goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
define vy where "vy = (SOME ux. ux \<in> \<lfloor>V, y\<rfloor>)"
[PROOF STATE]
proof (state)
this:
vy = (SOME ux. ux \<in> \<lfloor>V, y\<rfloor>)

goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
have "ux \<in> \<lfloor>U, x\<rfloor>" "vy \<in> \<lfloor>V, y\<rfloor> "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ux \<in> \<lfloor>U, x\<rfloor> &&& vy \<in> \<lfloor>V, y\<rfloor>
[PROOF STEP]
unfolding ux_def vy_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME ux. ux \<in> \<lfloor>U, x\<rfloor>) \<in> \<lfloor>U, x\<rfloor> &&& (SOME ux. ux \<in> \<lfloor>V, y\<rfloor>) \<in> \<lfloor>V, y\<rfloor>
[PROOF STEP]
using uv_sigma class_of_def some_in_eq
[PROOF STATE]
proof (prove)
using this:
(U, x) \<in> Sigma I \<FF>
(V, y) \<in> Sigma I \<FF>
\<lfloor>?U, ?s\<rfloor> \<equiv> rel.Class (?U, ?s)
((SOME x. x \<in> ?A) \<in> ?A) = (?A \<noteq> {})

goal (1 subgoal):
 1. (SOME ux. ux \<in> \<lfloor>U, x\<rfloor>) \<in> \<lfloor>U, x\<rfloor> &&& (SOME ux. ux \<in> \<lfloor>V, y\<rfloor>) \<in> \<lfloor>V, y\<rfloor>
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
ux \<in> \<lfloor>U, x\<rfloor>
vy \<in> \<lfloor>V, y\<rfloor>

goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ux \<in> \<lfloor>U, x\<rfloor>
vy \<in> \<lfloor>V, y\<rfloor>
[PROOF STEP]
have "ux \<in> Sigma I \<FF>" "vy \<in> Sigma I \<FF>"
[PROOF STATE]
proof (prove)
using this:
ux \<in> \<lfloor>U, x\<rfloor>
vy \<in> \<lfloor>V, y\<rfloor>

goal (1 subgoal):
 1. ux \<in> Sigma I \<FF> &&& vy \<in> Sigma I \<FF>
[PROOF STEP]
using class_of_def uv_sigma
[PROOF STATE]
proof (prove)
using this:
ux \<in> \<lfloor>U, x\<rfloor>
vy \<in> \<lfloor>V, y\<rfloor>
\<lfloor>?U, ?s\<rfloor> \<equiv> rel.Class (?U, ?s)
(U, x) \<in> Sigma I \<FF>
(V, y) \<in> Sigma I \<FF>

goal (1 subgoal):
 1. ux \<in> Sigma I \<FF> &&& vy \<in> Sigma I \<FF>
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
ux \<in> Sigma I \<FF>
vy \<in> Sigma I \<FF>

goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ux \<in> Sigma I \<FF>
vy \<in> Sigma I \<FF>
[PROOF STEP]
have "fst ux \<in> I" "fst vy \<in> I"
[PROOF STATE]
proof (prove)
using this:
ux \<in> Sigma I \<FF>
vy \<in> Sigma I \<FF>

goal (1 subgoal):
 1. fst ux \<in> I &&& fst vy \<in> I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst ux \<in> I
fst vy \<in> I

goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
define w1 where "w1 = get_lower_bound (fst ux) (fst vy)"
[PROOF STATE]
proof (state)
this:
w1 = get_lower_bound (fst ux) (fst vy)

goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
have w1:"w1 \<in> I" "w1 \<subseteq> fst ux" "w1 \<subseteq> fst vy"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w1 \<in> I &&& w1 \<subseteq> fst ux &&& w1 \<subseteq> fst vy
[PROOF STEP]
using get_lower_bound[OF \<open>fst ux \<in> I\<close> \<open>fst vy \<in> I\<close>]
[PROOF STATE]
proof (prove)
using this:
get_lower_bound (fst ux) (fst vy) \<in> I
get_lower_bound (fst ux) (fst vy) \<subseteq> fst ux
get_lower_bound (fst ux) (fst vy) \<subseteq> fst vy

goal (1 subgoal):
 1. w1 \<in> I &&& w1 \<subseteq> fst ux &&& w1 \<subseteq> fst vy
[PROOF STEP]
unfolding w1_def
[PROOF STATE]
proof (prove)
using this:
get_lower_bound (fst ux) (fst vy) \<in> I
get_lower_bound (fst ux) (fst vy) \<subseteq> fst ux
get_lower_bound (fst ux) (fst vy) \<subseteq> fst vy

goal (1 subgoal):
 1. get_lower_bound (fst ux) (fst vy) \<in> I &&& get_lower_bound (fst ux) (fst vy) \<subseteq> fst ux &&& get_lower_bound (fst ux) (fst vy) \<subseteq> fst vy
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w1 \<in> I
w1 \<subseteq> fst ux
w1 \<subseteq> fst vy

goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
have "add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w1, +\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w1, +\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor>
[PROOF STEP]
unfolding add_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let x = SOME xa. xa \<in> \<lfloor>U, x\<rfloor>; y = SOME ya. ya \<in> \<lfloor>V, y\<rfloor>; w = get_lower_bound (fst x) (fst y) in \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>) = \<lfloor>w1, +\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor>
[PROOF STEP]
apply (fold ux_def vy_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let x = ux; y = vy; w = get_lower_bound (fst x) (fst y) in \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>) = \<lfloor>w1, +\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor>
[PROOF STEP]
by (simp add:Let_def w1_def)
[PROOF STATE]
proof (state)
this:
add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w1, +\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor>

goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w1, +\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor>

goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
have "\<forall>\<^sub>F w in llbound.
            ... = \<lfloor>w, add_str w (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<lfloor>w1, +\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>
[PROOF STEP]
apply (rule add_rel_well_defined_llbound)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. ux \<in> Sigma I \<FF>
 2. vy \<in> Sigma I \<FF>
 3. w1 \<in> I
 4. w1 \<subseteq> fst ux
 5. w1 \<subseteq> fst vy
[PROOF STEP]
using \<open>ux \<in> Sigma I \<FF>\<close> \<open>vy \<in> Sigma I \<FF>\<close> w1
[PROOF STATE]
proof (prove)
using this:
ux \<in> Sigma I \<FF>
vy \<in> Sigma I \<FF>
w1 \<in> I
w1 \<subseteq> fst ux
w1 \<subseteq> fst vy

goal (5 subgoals):
 1. ux \<in> Sigma I \<FF>
 2. vy \<in> Sigma I \<FF>
 3. w1 \<in> I
 4. w1 \<subseteq> fst ux
 5. w1 \<subseteq> fst vy
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. \<lfloor>w1, +\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>

goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w1, +\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor>
\<forall>\<^sub>F w in llbound. \<lfloor>w1, +\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>
[PROOF STEP]
have "\<forall>\<^sub>F w in llbound. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor>
      = \<lfloor>w, add_str w (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w1, +\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor>
\<forall>\<^sub>F w in llbound. \<lfloor>w1, +\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>

goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>

goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
have
    "\<forall>\<^sub>F w in llbound. \<rho> (fst ux) w (snd ux) = \<rho> (fst (U, x)) w (snd (U, x))"
    "\<forall>\<^sub>F w in llbound. \<rho> (fst vy) w (snd vy) = \<rho> (fst (V, y)) w (snd (V, y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<rho> (fst ux) w (snd ux) = \<rho> (fst (U, x)) w (snd (U, x)) &&& \<forall>\<^sub>F w in llbound. \<rho> (fst vy) w (snd vy) = \<rho> (fst (V, y)) w (snd (V, y))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<rho> (fst ux) w (snd ux) = \<rho> (fst (U, x)) w (snd (U, x))
[PROOF STEP]
apply (rule rel_eventually_llbound)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ux \<sim> (U, x)
[PROOF STEP]
using \<open>ux \<in> \<lfloor>U, x\<rfloor>\<close> class_of_def uv_sigma(1)
[PROOF STATE]
proof (prove)
using this:
ux \<in> \<lfloor>U, x\<rfloor>
\<lfloor>?U, ?s\<rfloor> \<equiv> rel.Class (?U, ?s)
(U, x) \<in> Sigma I \<FF>

goal (1 subgoal):
 1. ux \<sim> (U, x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<rho> (fst vy) w (snd vy) = \<rho> (fst (V, y)) w (snd (V, y))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<rho> (fst vy) w (snd vy) = \<rho> (fst (V, y)) w (snd (V, y))
[PROOF STEP]
apply (rule rel_eventually_llbound)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vy \<sim> (V, y)
[PROOF STEP]
using \<open>vy \<in> \<lfloor>V, y\<rfloor>\<close> class_of_def uv_sigma(2)
[PROOF STATE]
proof (prove)
using this:
vy \<in> \<lfloor>V, y\<rfloor>
\<lfloor>?U, ?s\<rfloor> \<equiv> rel.Class (?U, ?s)
(V, y) \<in> Sigma I \<FF>

goal (1 subgoal):
 1. vy \<sim> (V, y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. \<rho> (fst ux) w (snd ux) = \<rho> (fst (U, x)) w (snd (U, x))
\<forall>\<^sub>F w in llbound. \<rho> (fst vy) w (snd vy) = \<rho> (fst (V, y)) w (snd (V, y))

goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F w in llbound. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>
\<forall>\<^sub>F w in llbound. \<rho> (fst ux) w (snd ux) = \<rho> (fst (U, x)) w (snd (U, x))
\<forall>\<^sub>F w in llbound. \<rho> (fst vy) w (snd vy) = \<rho> (fst (V, y)) w (snd (V, y))
[PROOF STEP]
have "\<forall>\<^sub>F w in llbound. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor>
      = \<lfloor>w, add_str w (\<rho> U w x) (\<rho> V w y)\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F w in llbound. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>
\<forall>\<^sub>F w in llbound. \<rho> (fst ux) w (snd ux) = \<rho> (fst (U, x)) w (snd (U, x))
\<forall>\<^sub>F w in llbound. \<rho> (fst vy) w (snd vy) = \<rho> (fst (V, y)) w (snd (V, y))

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>
[PROOF STEP]
apply eventually_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>; \<rho> (fst ux) w (snd ux) = \<rho> (fst (U, x)) w (snd (U, x)); \<rho> (fst vy) w (snd vy) = \<rho> (fst (V, y)) w (snd (V, y))\<rbrakk> \<Longrightarrow> add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>

goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>

goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
have "\<forall>\<^sub>F w in llbound. \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>
[PROOF STEP]
apply (rule add_rel_well_defined_llbound[of "(U,x)" "(V,y)" W,simplified])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. U \<in> I \<and> x \<in> \<FF> U
 2. V \<in> I \<and> y \<in> \<FF> V
 3. W \<in> I
 4. W \<subseteq> U
 5. W \<subseteq> V
[PROOF STEP]
using w uv_sigma
[PROOF STATE]
proof (prove)
using this:
W \<in> I
W \<subseteq> U
W \<subseteq> V
(U, x) \<in> Sigma I \<FF>
(V, y) \<in> Sigma I \<FF>

goal (5 subgoals):
 1. U \<in> I \<and> x \<in> \<FF> U
 2. V \<in> I \<and> y \<in> \<FF> V
 3. W \<in> I
 4. W \<subseteq> U
 5. W \<subseteq> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>

goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F w in llbound. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>
\<forall>\<^sub>F w in llbound. \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>
[PROOF STEP]
have "\<forall>\<^sub>F w in llbound.
      add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F w in llbound. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>
\<forall>\<^sub>F w in llbound. \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
apply eventually_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>; \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor> = \<lfloor>w, +\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>\<rbrakk> \<Longrightarrow> add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>

goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>

goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
have "llbound\<noteq>bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llbound \<noteq> bot
[PROOF STEP]
using llbound_not_bot w(1)
[PROOF STATE]
proof (prove)
using this:
I \<noteq> {} \<Longrightarrow> llbound \<noteq> bot
W \<in> I

goal (1 subgoal):
 1. llbound \<noteq> bot
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
llbound \<noteq> bot

goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F w in llbound. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
llbound \<noteq> bot
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F w in llbound. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
llbound \<noteq> bot

goal (1 subgoal):
 1. add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
add_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, +\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_rel_class_of:
  fixes U V W :: "'a set" and x y :: 'b
  assumes uv_sigma:"(U, x) \<in> Sigma I \<FF>" "(V, y) \<in> Sigma I \<FF>"
  assumes w:"W \<in> I" "W \<subseteq> U" "W \<subseteq> V"
  shows "mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
define ux where "ux = (SOME ux. ux \<in> \<lfloor>U, x\<rfloor>)"
[PROOF STATE]
proof (state)
this:
ux = (SOME ux. ux \<in> \<lfloor>U, x\<rfloor>)

goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
define vy where "vy = (SOME ux. ux \<in> \<lfloor>V, y\<rfloor>)"
[PROOF STATE]
proof (state)
this:
vy = (SOME ux. ux \<in> \<lfloor>V, y\<rfloor>)

goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
have "ux \<in> \<lfloor>U, x\<rfloor>" "vy \<in> \<lfloor>V, y\<rfloor> "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ux \<in> \<lfloor>U, x\<rfloor> &&& vy \<in> \<lfloor>V, y\<rfloor>
[PROOF STEP]
unfolding ux_def vy_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME ux. ux \<in> \<lfloor>U, x\<rfloor>) \<in> \<lfloor>U, x\<rfloor> &&& (SOME ux. ux \<in> \<lfloor>V, y\<rfloor>) \<in> \<lfloor>V, y\<rfloor>
[PROOF STEP]
using uv_sigma class_of_def some_in_eq
[PROOF STATE]
proof (prove)
using this:
(U, x) \<in> Sigma I \<FF>
(V, y) \<in> Sigma I \<FF>
\<lfloor>?U, ?s\<rfloor> \<equiv> rel.Class (?U, ?s)
((SOME x. x \<in> ?A) \<in> ?A) = (?A \<noteq> {})

goal (1 subgoal):
 1. (SOME ux. ux \<in> \<lfloor>U, x\<rfloor>) \<in> \<lfloor>U, x\<rfloor> &&& (SOME ux. ux \<in> \<lfloor>V, y\<rfloor>) \<in> \<lfloor>V, y\<rfloor>
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
ux \<in> \<lfloor>U, x\<rfloor>
vy \<in> \<lfloor>V, y\<rfloor>

goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ux \<in> \<lfloor>U, x\<rfloor>
vy \<in> \<lfloor>V, y\<rfloor>
[PROOF STEP]
have "ux \<in> Sigma I \<FF>" "vy \<in> Sigma I \<FF>"
[PROOF STATE]
proof (prove)
using this:
ux \<in> \<lfloor>U, x\<rfloor>
vy \<in> \<lfloor>V, y\<rfloor>

goal (1 subgoal):
 1. ux \<in> Sigma I \<FF> &&& vy \<in> Sigma I \<FF>
[PROOF STEP]
using class_of_def uv_sigma
[PROOF STATE]
proof (prove)
using this:
ux \<in> \<lfloor>U, x\<rfloor>
vy \<in> \<lfloor>V, y\<rfloor>
\<lfloor>?U, ?s\<rfloor> \<equiv> rel.Class (?U, ?s)
(U, x) \<in> Sigma I \<FF>
(V, y) \<in> Sigma I \<FF>

goal (1 subgoal):
 1. ux \<in> Sigma I \<FF> &&& vy \<in> Sigma I \<FF>
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
ux \<in> Sigma I \<FF>
vy \<in> Sigma I \<FF>

goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ux \<in> Sigma I \<FF>
vy \<in> Sigma I \<FF>
[PROOF STEP]
have "fst ux \<in> I" "fst vy \<in> I"
[PROOF STATE]
proof (prove)
using this:
ux \<in> Sigma I \<FF>
vy \<in> Sigma I \<FF>

goal (1 subgoal):
 1. fst ux \<in> I &&& fst vy \<in> I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst ux \<in> I
fst vy \<in> I

goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
define w1 where "w1 = get_lower_bound (fst ux) (fst vy)"
[PROOF STATE]
proof (state)
this:
w1 = get_lower_bound (fst ux) (fst vy)

goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
have w1:"w1 \<in> I" "w1 \<subseteq> fst ux" "w1 \<subseteq> fst vy"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w1 \<in> I &&& w1 \<subseteq> fst ux &&& w1 \<subseteq> fst vy
[PROOF STEP]
using get_lower_bound[OF \<open>fst ux \<in> I\<close> \<open>fst vy \<in> I\<close>]
[PROOF STATE]
proof (prove)
using this:
get_lower_bound (fst ux) (fst vy) \<in> I
get_lower_bound (fst ux) (fst vy) \<subseteq> fst ux
get_lower_bound (fst ux) (fst vy) \<subseteq> fst vy

goal (1 subgoal):
 1. w1 \<in> I &&& w1 \<subseteq> fst ux &&& w1 \<subseteq> fst vy
[PROOF STEP]
unfolding w1_def
[PROOF STATE]
proof (prove)
using this:
get_lower_bound (fst ux) (fst vy) \<in> I
get_lower_bound (fst ux) (fst vy) \<subseteq> fst ux
get_lower_bound (fst ux) (fst vy) \<subseteq> fst vy

goal (1 subgoal):
 1. get_lower_bound (fst ux) (fst vy) \<in> I &&& get_lower_bound (fst ux) (fst vy) \<subseteq> fst ux &&& get_lower_bound (fst ux) (fst vy) \<subseteq> fst vy
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w1 \<in> I
w1 \<subseteq> fst ux
w1 \<subseteq> fst vy

goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
have "mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w1, \<cdot>\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w1, \<cdot>\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor>
[PROOF STEP]
unfolding mult_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let x = SOME xa. xa \<in> \<lfloor>U, x\<rfloor>; y = SOME ya. ya \<in> \<lfloor>V, y\<rfloor>; w = get_lower_bound (fst x) (fst y) in \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>) = \<lfloor>w1, \<cdot>\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor>
[PROOF STEP]
apply (fold ux_def vy_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let x = ux; y = vy; w = get_lower_bound (fst x) (fst y) in \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst x) w (snd x)) (\<rho> (fst y) w (snd y))\<rfloor>) = \<lfloor>w1, \<cdot>\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor>
[PROOF STEP]
by (simp add:Let_def w1_def)
[PROOF STATE]
proof (state)
this:
mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w1, \<cdot>\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor>

goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w1, \<cdot>\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor>

goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
have "\<forall>\<^sub>F w in llbound.
            ... = \<lfloor>w, mult_str w (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<lfloor>w1, \<cdot>\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>
[PROOF STEP]
apply (rule mult_rel_well_defined_llbound)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. ux \<in> Sigma I \<FF>
 2. vy \<in> Sigma I \<FF>
 3. w1 \<in> I
 4. w1 \<subseteq> fst ux
 5. w1 \<subseteq> fst vy
[PROOF STEP]
using \<open>ux \<in> Sigma I \<FF>\<close> \<open>vy \<in> Sigma I \<FF>\<close> w1
[PROOF STATE]
proof (prove)
using this:
ux \<in> Sigma I \<FF>
vy \<in> Sigma I \<FF>
w1 \<in> I
w1 \<subseteq> fst ux
w1 \<subseteq> fst vy

goal (5 subgoals):
 1. ux \<in> Sigma I \<FF>
 2. vy \<in> Sigma I \<FF>
 3. w1 \<in> I
 4. w1 \<subseteq> fst ux
 5. w1 \<subseteq> fst vy
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. \<lfloor>w1, \<cdot>\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>

goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w1, \<cdot>\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor>
\<forall>\<^sub>F w in llbound. \<lfloor>w1, \<cdot>\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>
[PROOF STEP]
have "\<forall>\<^sub>F w in llbound. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor>
      = \<lfloor>w, mult_str w (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w1, \<cdot>\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor>
\<forall>\<^sub>F w in llbound. \<lfloor>w1, \<cdot>\<^bsub>w1\<^esub> (\<rho> (fst ux) w1 (snd ux)) (\<rho> (fst vy) w1 (snd vy))\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>

goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>

goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
have
    "\<forall>\<^sub>F w in llbound. \<rho> (fst ux) w (snd ux) = \<rho> (fst (U, x)) w (snd (U, x))"
    "\<forall>\<^sub>F w in llbound. \<rho> (fst vy) w (snd vy) = \<rho> (fst (V, y)) w (snd (V, y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<rho> (fst ux) w (snd ux) = \<rho> (fst (U, x)) w (snd (U, x)) &&& \<forall>\<^sub>F w in llbound. \<rho> (fst vy) w (snd vy) = \<rho> (fst (V, y)) w (snd (V, y))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<rho> (fst ux) w (snd ux) = \<rho> (fst (U, x)) w (snd (U, x))
[PROOF STEP]
apply (rule rel_eventually_llbound)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ux \<sim> (U, x)
[PROOF STEP]
using \<open>ux \<in> \<lfloor>U, x\<rfloor>\<close> class_of_def uv_sigma(1)
[PROOF STATE]
proof (prove)
using this:
ux \<in> \<lfloor>U, x\<rfloor>
\<lfloor>?U, ?s\<rfloor> \<equiv> rel.Class (?U, ?s)
(U, x) \<in> Sigma I \<FF>

goal (1 subgoal):
 1. ux \<sim> (U, x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<rho> (fst vy) w (snd vy) = \<rho> (fst (V, y)) w (snd (V, y))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<rho> (fst vy) w (snd vy) = \<rho> (fst (V, y)) w (snd (V, y))
[PROOF STEP]
apply (rule rel_eventually_llbound)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vy \<sim> (V, y)
[PROOF STEP]
using \<open>vy \<in> \<lfloor>V, y\<rfloor>\<close> class_of_def uv_sigma(2)
[PROOF STATE]
proof (prove)
using this:
vy \<in> \<lfloor>V, y\<rfloor>
\<lfloor>?U, ?s\<rfloor> \<equiv> rel.Class (?U, ?s)
(V, y) \<in> Sigma I \<FF>

goal (1 subgoal):
 1. vy \<sim> (V, y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. \<rho> (fst ux) w (snd ux) = \<rho> (fst (U, x)) w (snd (U, x))
\<forall>\<^sub>F w in llbound. \<rho> (fst vy) w (snd vy) = \<rho> (fst (V, y)) w (snd (V, y))

goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F w in llbound. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>
\<forall>\<^sub>F w in llbound. \<rho> (fst ux) w (snd ux) = \<rho> (fst (U, x)) w (snd (U, x))
\<forall>\<^sub>F w in llbound. \<rho> (fst vy) w (snd vy) = \<rho> (fst (V, y)) w (snd (V, y))
[PROOF STEP]
have "\<forall>\<^sub>F w in llbound. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor>
      = \<lfloor>w, mult_str w (\<rho> U w x) (\<rho> V w y)\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F w in llbound. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>
\<forall>\<^sub>F w in llbound. \<rho> (fst ux) w (snd ux) = \<rho> (fst (U, x)) w (snd (U, x))
\<forall>\<^sub>F w in llbound. \<rho> (fst vy) w (snd vy) = \<rho> (fst (V, y)) w (snd (V, y))

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>
[PROOF STEP]
apply eventually_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> (fst ux) w (snd ux)) (\<rho> (fst vy) w (snd vy))\<rfloor>; \<rho> (fst ux) w (snd ux) = \<rho> (fst (U, x)) w (snd (U, x)); \<rho> (fst vy) w (snd vy) = \<rho> (fst (V, y)) w (snd (V, y))\<rbrakk> \<Longrightarrow> mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>

goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>

goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
have "\<forall>\<^sub>F w in llbound. \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>
[PROOF STEP]
apply (rule mult_rel_well_defined_llbound[of "(U,x)" "(V,y)" W,simplified])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. U \<in> I \<and> x \<in> \<FF> U
 2. V \<in> I \<and> y \<in> \<FF> V
 3. W \<in> I
 4. W \<subseteq> U
 5. W \<subseteq> V
[PROOF STEP]
using w uv_sigma
[PROOF STATE]
proof (prove)
using this:
W \<in> I
W \<subseteq> U
W \<subseteq> V
(U, x) \<in> Sigma I \<FF>
(V, y) \<in> Sigma I \<FF>

goal (5 subgoals):
 1. U \<in> I \<and> x \<in> \<FF> U
 2. V \<in> I \<and> y \<in> \<FF> V
 3. W \<in> I
 4. W \<subseteq> U
 5. W \<subseteq> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>

goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F w in llbound. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>
\<forall>\<^sub>F w in llbound. \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>
[PROOF STEP]
have "\<forall>\<^sub>F w in llbound.
      mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F w in llbound. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>
\<forall>\<^sub>F w in llbound. \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>

goal (1 subgoal):
 1. \<forall>\<^sub>F w in llbound. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
apply eventually_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>; \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor> = \<lfloor>w, \<cdot>\<^bsub>w\<^esub> (\<rho> U w x) (\<rho> V w y)\<rfloor>\<rbrakk> \<Longrightarrow> mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>

goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F w in llbound. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>

goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
have "llbound\<noteq>bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llbound \<noteq> bot
[PROOF STEP]
using llbound_not_bot w(1)
[PROOF STATE]
proof (prove)
using this:
I \<noteq> {} \<Longrightarrow> llbound \<noteq> bot
W \<in> I

goal (1 subgoal):
 1. llbound \<noteq> bot
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
llbound \<noteq> bot

goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F w in llbound. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
llbound \<noteq> bot
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F w in llbound. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
llbound \<noteq> bot

goal (1 subgoal):
 1. mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mult_rel \<lfloor>U, x\<rfloor> \<lfloor>V, y\<rfloor> = \<lfloor>W, \<cdot>\<^bsub>W\<^esub> (\<rho> U W x) (\<rho> V W y)\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_rel_carrier[intro]:
  assumes "X \<in> carrier_direct_lim" "Y \<in> carrier_direct_lim"
  shows "mult_rel X Y \<in> carrier_direct_lim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mult_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
define x where "x=(SOME x. x \<in> X)"
[PROOF STATE]
proof (state)
this:
x = (SOME x. x \<in> X)

goal (1 subgoal):
 1. mult_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
define y where "y=(SOME y. y \<in> Y)"
[PROOF STATE]
proof (state)
this:
y = (SOME y. y \<in> Y)

goal (1 subgoal):
 1. mult_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
have "x\<in>X" "x\<in>Sigma I \<FF>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> X &&& x \<in> Sigma I \<FF>
[PROOF STEP]
using rel_carrier_Eps_in[OF \<open>X \<in> carrier_direct_lim\<close>]
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> X) \<in> X
(SOME x. x \<in> X) \<in> Sigma I \<FF>
X = \<lfloor>fst (SOME x. x \<in> X), snd (SOME x. x \<in> X)\<rfloor>

goal (1 subgoal):
 1. x \<in> X &&& x \<in> Sigma I \<FF>
[PROOF STEP]
unfolding x_def
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> X) \<in> X
(SOME x. x \<in> X) \<in> Sigma I \<FF>
X = \<lfloor>fst (SOME x. x \<in> X), snd (SOME x. x \<in> X)\<rfloor>

goal (1 subgoal):
 1. (SOME x. x \<in> X) \<in> X &&& (SOME x. x \<in> X) \<in> Sigma I \<FF>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> X
x \<in> Sigma I \<FF>

goal (1 subgoal):
 1. mult_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
have "y\<in>Y" "y \<in> Sigma I \<FF>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> Y &&& y \<in> Sigma I \<FF>
[PROOF STEP]
using rel_carrier_Eps_in[OF \<open>Y \<in> carrier_direct_lim\<close>]
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> Y) \<in> Y
(SOME x. x \<in> Y) \<in> Sigma I \<FF>
Y = \<lfloor>fst (SOME x. x \<in> Y), snd (SOME x. x \<in> Y)\<rfloor>

goal (1 subgoal):
 1. y \<in> Y &&& y \<in> Sigma I \<FF>
[PROOF STEP]
unfolding y_def
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> Y) \<in> Y
(SOME x. x \<in> Y) \<in> Sigma I \<FF>
Y = \<lfloor>fst (SOME x. x \<in> Y), snd (SOME x. x \<in> Y)\<rfloor>

goal (1 subgoal):
 1. (SOME y. y \<in> Y) \<in> Y &&& (SOME y. y \<in> Y) \<in> Sigma I \<FF>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> Y
y \<in> Sigma I \<FF>

goal (1 subgoal):
 1. mult_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
define z where "z=get_lower_bound (fst x) (fst y)"
[PROOF STATE]
proof (state)
this:
z = get_lower_bound (fst x) (fst y)

goal (1 subgoal):
 1. mult_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
have "z \<in> I" "z \<subseteq> fst x" "z \<subseteq> fst y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> I &&& z \<subseteq> fst x &&& z \<subseteq> fst y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. z \<in> I
 2. z \<subseteq> fst x
 3. z \<subseteq> fst y
[PROOF STEP]
have "fst x \<in> I" "fst y \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst x \<in> I &&& fst y \<in> I
[PROOF STEP]
using \<open>x \<in> Sigma I \<FF>\<close> \<open>y \<in> Sigma I \<FF>\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> Sigma I \<FF>
y \<in> Sigma I \<FF>

goal (1 subgoal):
 1. fst x \<in> I &&& fst y \<in> I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst x \<in> I
fst y \<in> I

goal (3 subgoals):
 1. z \<in> I
 2. z \<subseteq> fst x
 3. z \<subseteq> fst y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst x \<in> I
fst y \<in> I
[PROOF STEP]
show "z \<in> I" "z \<subseteq> fst x" "z \<subseteq> fst y"
[PROOF STATE]
proof (prove)
using this:
fst x \<in> I
fst y \<in> I

goal (1 subgoal):
 1. z \<in> I &&& z \<subseteq> fst x &&& z \<subseteq> fst y
[PROOF STEP]
using get_lower_bound[of "fst x" "fst y",folded z_def]
[PROOF STATE]
proof (prove)
using this:
fst x \<in> I
fst y \<in> I
\<lbrakk>fst x \<in> I; fst y \<in> I\<rbrakk> \<Longrightarrow> z \<in> I
\<lbrakk>fst x \<in> I; fst y \<in> I\<rbrakk> \<Longrightarrow> z \<subseteq> fst x
\<lbrakk>fst x \<in> I; fst y \<in> I\<rbrakk> \<Longrightarrow> z \<subseteq> fst y

goal (1 subgoal):
 1. z \<in> I &&& z \<subseteq> fst x &&& z \<subseteq> fst y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> I
z \<subseteq> fst x
z \<subseteq> fst y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
z \<in> I
z \<subseteq> fst x
z \<subseteq> fst y

goal (1 subgoal):
 1. mult_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
have "mult_rel X Y = \<lfloor>z, mult_str z (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_rel X Y = \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor>
[PROOF STEP]
unfolding mult_rel_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>get_lower_bound (fst (SOME x. x \<in> X)) (fst (SOME y. y \<in> Y)), \<cdot>\<^bsub>get_lower_bound (fst (SOME x. x \<in> X)) (fst (SOME y. y \<in> Y))\<^esub> (\<rho> (fst (SOME x. x \<in> X)) (get_lower_bound (fst (SOME x. x \<in> X)) (fst (SOME y. y \<in> Y))) (snd (SOME x. x \<in> X))) (\<rho> (fst (SOME y. y \<in> Y)) (get_lower_bound (fst (SOME x. x \<in> X)) (fst (SOME y. y \<in> Y))) (snd (SOME y. y \<in> Y)))\<rfloor> = \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor>
[PROOF STEP]
by (fold x_def y_def z_def,rule)
[PROOF STATE]
proof (state)
this:
mult_rel X Y = \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor>

goal (1 subgoal):
 1. mult_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mult_rel X Y = \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor>

goal (1 subgoal):
 1. mult_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
have "... \<in> carrier_direct_lim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> \<in> carrier_direct_lim
[PROOF STEP]
unfolding carrier_direct_lim_def class_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel.Class (z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))) \<in> rel.Partition
[PROOF STEP]
proof (rule rel.Block_closed)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))) \<in> Sigma I \<FF>
[PROOF STEP]
interpret ring "(\<FF> z)" "+\<^bsub>z\<^esub>" "\<cdot>\<^bsub>z\<^esub>" "\<zero>\<^bsub>z\<^esub>" "\<one>\<^bsub>z\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring (\<FF> z) +\<^bsub>z\<^esub> \<cdot>\<^bsub>z\<^esub> \<zero>\<^bsub>z\<^esub> \<one>\<^bsub>z\<^esub>
[PROOF STEP]
by (simp add: \<open>z \<in> I\<close> is_ring_from_is_homomorphism subset_of_opens)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))) \<in> Sigma I \<FF>
[PROOF STEP]
show "(z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))) \<in> Sigma I \<FF>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))) \<in> Sigma I \<FF>
[PROOF STEP]
by (metis SigmaE SigmaI \<open>x \<in> Sigma I \<FF>\<close> \<open>y \<in> Sigma I \<FF>\<close> \<open>z \<in> I\<close> \<open>z \<subseteq> fst x\<close> \<open>z \<subseteq> fst y\<close>
          direct_lim.subset_of_opens direct_lim_axioms fst_conv
          is_map_from_is_homomorphism map.map_closed multiplicative.composition_closed snd_conv)
[PROOF STATE]
proof (state)
this:
(z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))) \<in> Sigma I \<FF>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lfloor>z, \<cdot>\<^bsub>z\<^esub> (\<rho> (fst x) z (snd x)) (\<rho> (fst y) z (snd y))\<rfloor> \<in> carrier_direct_lim

goal (1 subgoal):
 1. mult_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mult_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mult_rel X Y \<in> carrier_direct_lim

goal (1 subgoal):
 1. mult_rel X Y \<in> carrier_direct_lim
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
mult_rel X Y \<in> carrier_direct_lim

goal:
No subgoals!
[PROOF STEP]
qed