[STATEMENT]
lemma mk_doubleton_image_vsubset_veqpoll:
  assumes "X \<subseteq>\<^sub>\<circ> Y"
  shows "mk_doubleton_image X X \<approx>\<^sub>\<circ> mk_doubleton_image X Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_doubleton_image X X \<approx>\<^sub>\<circ> mk_doubleton_image X Y
[PROOF STEP]
unfolding eqpoll_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. bij_betw f (elts (mk_doubleton_image X X)) (elts (mk_doubleton_image X Y))
[PROOF STEP]
proof(intro exI[of _ \<open>\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})\<close>] bij_betw_imageI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) (elts (mk_doubleton_image X X))
 2. (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X) = elts (mk_doubleton_image X Y)
[PROOF STEP]
show "inj_on (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) (elts (mk_doubleton_image X X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) (elts (mk_doubleton_image X X))
[PROOF STEP]
unfolding mk_doubleton_image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) (elts (set (mk_doubleton X ` elts X)))
[PROOF STEP]
proof(intro inj_onI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X); y \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X); vinsert Y (x -\<^sub>\<circ> set {X}) = vinsert Y (y -\<^sub>\<circ> set {X})\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix y y'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X); y \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X); vinsert Y (x -\<^sub>\<circ> set {X}) = vinsert Y (y -\<^sub>\<circ> set {X})\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume prems:
      "y \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X)"
      "y' \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X)"
      "vinsert Y (y -\<^sub>\<circ> set {X}) = vinsert Y (y' -\<^sub>\<circ> set {X})"
[PROOF STATE]
proof (state)
this:
y \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X)
y' \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X)
vinsert Y (y -\<^sub>\<circ> set {X}) = vinsert Y (y' -\<^sub>\<circ> set {X})

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X); y \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X); vinsert Y (x -\<^sub>\<circ> set {X}) = vinsert Y (y -\<^sub>\<circ> set {X})\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X)
y' \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X)
vinsert Y (y -\<^sub>\<circ> set {X}) = vinsert Y (y' -\<^sub>\<circ> set {X})
[PROOF STEP]
obtain x x'
      where "x \<in>\<^sub>\<circ> X"
        and "x' \<in>\<^sub>\<circ> X"
        and y_def: "y = set {x, X}"
        and y'_def: "y' = set {x', X}"
[PROOF STATE]
proof (prove)
using this:
y \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X)
y' \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X)
vinsert Y (y -\<^sub>\<circ> set {X}) = vinsert Y (y' -\<^sub>\<circ> set {X})

goal (1 subgoal):
 1. (\<And>x x'. \<lbrakk>x \<in>\<^sub>\<circ> X; x' \<in>\<^sub>\<circ> X; y = set {x, X}; y' = set {x', X}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (clarsimp simp: mk_doubleton_def)
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>\<circ> X
x' \<in>\<^sub>\<circ> X
y = set {x, X}
y' = set {x', X}

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X); y \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X); vinsert Y (x -\<^sub>\<circ> set {X}) = vinsert Y (y -\<^sub>\<circ> set {X})\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
X \<subseteq>\<^sub>\<circ> Y
x \<in>\<^sub>\<circ> X
x' \<in>\<^sub>\<circ> X
y = set {x, X}
y' = set {x', X}
[PROOF STEP]
have xX_X: "set {x, X} -\<^sub>\<circ> set {X} = set {x}"
      and x'X_X: "set {x', X} -\<^sub>\<circ> set {X} = set {x'}"
[PROOF STATE]
proof (prove)
using this:
X \<subseteq>\<^sub>\<circ> Y
x \<in>\<^sub>\<circ> X
x' \<in>\<^sub>\<circ> X
y = set {x, X}
y' = set {x', X}

goal (1 subgoal):
 1. set {x, X} -\<^sub>\<circ> set {X} = set {x} &&& set {x', X} -\<^sub>\<circ> set {X} = set {x'}
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
set {x, X} -\<^sub>\<circ> set {X} = set {x}
set {x', X} -\<^sub>\<circ> set {X} = set {x'}

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X); y \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X); vinsert Y (x -\<^sub>\<circ> set {X}) = vinsert Y (y -\<^sub>\<circ> set {X})\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
from prems(3)[unfolded y_def y'_def]
[PROOF STATE]
proof (chain)
picking this:
vinsert Y (set {x, X} -\<^sub>\<circ> set {X}) = vinsert Y (set {x', X} -\<^sub>\<circ> set {X})
[PROOF STEP]
have "set {x, Y} = set {x', Y}"
[PROOF STATE]
proof (prove)
using this:
vinsert Y (set {x, X} -\<^sub>\<circ> set {X}) = vinsert Y (set {x', X} -\<^sub>\<circ> set {X})

goal (1 subgoal):
 1. set {x, Y} = set {x', Y}
[PROOF STEP]
unfolding xX_X x'X_X
[PROOF STATE]
proof (prove)
using this:
vinsert Y (set {x}) = vinsert Y (set {x'})

goal (1 subgoal):
 1. set {x, Y} = set {x', Y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set {x, Y} = set {x', Y}

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X); y \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X); vinsert Y (x -\<^sub>\<circ> set {X}) = vinsert Y (y -\<^sub>\<circ> set {X})\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set {x, Y} = set {x', Y}
[PROOF STEP]
have "x = x'"
[PROOF STATE]
proof (prove)
using this:
set {x, Y} = set {x', Y}

goal (1 subgoal):
 1. x = x'
[PROOF STEP]
by (auto simp: doubleton_eq_iff)
[PROOF STATE]
proof (state)
this:
x = x'

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X); y \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X); vinsert Y (x -\<^sub>\<circ> set {X}) = vinsert Y (y -\<^sub>\<circ> set {X})\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = x'
[PROOF STEP]
show "y = y'"
[PROOF STATE]
proof (prove)
using this:
x = x'

goal (1 subgoal):
 1. y = y'
[PROOF STEP]
unfolding y_def y'_def
[PROOF STATE]
proof (prove)
using this:
x = x'

goal (1 subgoal):
 1. set {x, X} = set {x', X}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y = y'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) (elts (mk_doubleton_image X X))

goal (1 subgoal):
 1. (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X) = elts (mk_doubleton_image X Y)
[PROOF STEP]
show
    "(\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` (elts (mk_doubleton_image X X)) =
      (elts (mk_doubleton_image X Y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X) = elts (mk_doubleton_image X Y)
[PROOF STEP]
proof(intro subset_antisym subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X) \<Longrightarrow> x \<in>\<^sub>\<circ> mk_doubleton_image X Y
 2. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X) \<Longrightarrow> x \<in>\<^sub>\<circ> mk_doubleton_image X Y
 2. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X)
[PROOF STEP]
assume prems:
      "z \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` (elts (mk_doubleton_image X X))"
[PROOF STATE]
proof (state)
this:
z \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X)

goal (2 subgoals):
 1. \<And>x. x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X) \<Longrightarrow> x \<in>\<^sub>\<circ> mk_doubleton_image X Y
 2. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X)
[PROOF STEP]
obtain y
      where "y \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X)"
        and z_def: "z = vinsert Y (y -\<^sub>\<circ> set {X})"
[PROOF STATE]
proof (prove)
using this:
z \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X); z = vinsert Y (y -\<^sub>\<circ> set {X})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding mk_doubleton_image_def
[PROOF STATE]
proof (prove)
using this:
z \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (set (mk_doubleton X ` elts X))

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X); z = vinsert Y (y -\<^sub>\<circ> set {X})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X)
z = vinsert Y (y -\<^sub>\<circ> set {X})

goal (2 subgoals):
 1. \<And>x. x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X) \<Longrightarrow> x \<in>\<^sub>\<circ> mk_doubleton_image X Y
 2. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X)
z = vinsert Y (y -\<^sub>\<circ> set {X})
[PROOF STEP]
obtain x where xX: "x \<in>\<^sub>\<circ> X" and y_def: "y = set {x, X}"
[PROOF STATE]
proof (prove)
using this:
y \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X)
z = vinsert Y (y -\<^sub>\<circ> set {X})

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in>\<^sub>\<circ> X; y = set {x, X}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding mk_doubleton_def
[PROOF STATE]
proof (prove)
using this:
y \<in>\<^sub>\<circ> set ((\<lambda>a. set {a, X}) ` elts X)
z = vinsert Y (y -\<^sub>\<circ> set {X})

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in>\<^sub>\<circ> X; y = set {x, X}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>\<circ> X
y = set {x, X}

goal (2 subgoals):
 1. \<And>x. x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X) \<Longrightarrow> x \<in>\<^sub>\<circ> mk_doubleton_image X Y
 2. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X)
[PROOF STEP]
from xX
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>\<circ> X
[PROOF STEP]
have y_X: "y -\<^sub>\<circ> set {X} = set {x}"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> X

goal (1 subgoal):
 1. y -\<^sub>\<circ> set {X} = set {x}
[PROOF STEP]
unfolding y_def
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> X

goal (1 subgoal):
 1. set {x, X} -\<^sub>\<circ> set {X} = set {x}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
y -\<^sub>\<circ> set {X} = set {x}

goal (2 subgoals):
 1. \<And>x. x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X) \<Longrightarrow> x \<in>\<^sub>\<circ> mk_doubleton_image X Y
 2. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X)
[PROOF STEP]
from z_def
[PROOF STATE]
proof (chain)
picking this:
z = vinsert Y (y -\<^sub>\<circ> set {X})
[PROOF STEP]
have z_def': "z = set {x, Y}"
[PROOF STATE]
proof (prove)
using this:
z = vinsert Y (y -\<^sub>\<circ> set {X})

goal (1 subgoal):
 1. z = set {x, Y}
[PROOF STEP]
unfolding y_X
[PROOF STATE]
proof (prove)
using this:
z = vinsert Y (set {x})

goal (1 subgoal):
 1. z = set {x, Y}
[PROOF STEP]
by (simp add: doubleton_eq_iff vinsert_vsingleton)
[PROOF STATE]
proof (state)
this:
z = set {x, Y}

goal (2 subgoals):
 1. \<And>x. x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X) \<Longrightarrow> x \<in>\<^sub>\<circ> mk_doubleton_image X Y
 2. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X)
[PROOF STEP]
from xX
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>\<circ> X
[PROOF STEP]
show "z \<in>\<^sub>\<circ> mk_doubleton_image X Y"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> X

goal (1 subgoal):
 1. z \<in>\<^sub>\<circ> mk_doubleton_image X Y
[PROOF STEP]
unfolding z_def' mk_doubleton_def mk_doubleton_image_def
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> X

goal (1 subgoal):
 1. set {x, Y} \<in>\<^sub>\<circ> set ((\<lambda>a. set {a, Y}) ` elts X)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z \<in>\<^sub>\<circ> mk_doubleton_image X Y

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X)
[PROOF STEP]
assume prems: "z \<in>\<^sub>\<circ> mk_doubleton_image X Y"
[PROOF STATE]
proof (state)
this:
z \<in>\<^sub>\<circ> mk_doubleton_image X Y

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in>\<^sub>\<circ> mk_doubleton_image X Y
[PROOF STEP]
obtain x where xX: "x \<in>\<^sub>\<circ> X" and z_def: "z = set {x, Y}"
[PROOF STATE]
proof (prove)
using this:
z \<in>\<^sub>\<circ> mk_doubleton_image X Y

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in>\<^sub>\<circ> X; z = set {x, Y}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding mk_doubleton_def mk_doubleton_image_def
[PROOF STATE]
proof (prove)
using this:
z \<in>\<^sub>\<circ> set ((\<lambda>a. set {a, Y}) ` elts X)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in>\<^sub>\<circ> X; z = set {x, Y}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>\<circ> X
z = set {x, Y}

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X)
[PROOF STEP]
from xX
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>\<circ> X
[PROOF STEP]
have xX_XX: "set {x, X} \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X)"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> X

goal (1 subgoal):
 1. set {x, X} \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X)
[PROOF STEP]
unfolding mk_doubleton_def
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> X

goal (1 subgoal):
 1. set {x, X} \<in>\<^sub>\<circ> set ((\<lambda>a. set {a, X}) ` elts X)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set {x, X} \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X)
[PROOF STEP]
from xX
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>\<circ> X
[PROOF STEP]
have xX_X: "set {x, X} -\<^sub>\<circ> set {X} = set {x}"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> X

goal (1 subgoal):
 1. set {x, X} -\<^sub>\<circ> set {X} = set {x}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
set {x, X} -\<^sub>\<circ> set {X} = set {x}

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X)
[PROOF STEP]
have z_def': "z = vinsert Y (set {x, X} -\<^sub>\<circ> set {X})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z = vinsert Y (set {x, X} -\<^sub>\<circ> set {X})
[PROOF STEP]
unfolding xX_X z_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set {x, Y} = vinsert Y (set {x})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z = vinsert Y (set {x, X} -\<^sub>\<circ> set {X})

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X)
[PROOF STEP]
with xX_XX
[PROOF STATE]
proof (chain)
picking this:
set {x, X} \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X)
z = vinsert Y (set {x, X} -\<^sub>\<circ> set {X})
[PROOF STEP]
show
      "z \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` (elts (mk_doubleton_image X X))"
[PROOF STATE]
proof (prove)
using this:
set {x, X} \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X)
z = vinsert Y (set {x, X} -\<^sub>\<circ> set {X})

goal (1 subgoal):
 1. z \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X)
[PROOF STEP]
unfolding z_def' mk_doubleton_image_def
[PROOF STATE]
proof (prove)
using this:
set {x, X} \<in>\<^sub>\<circ> set (mk_doubleton X ` elts X)
vinsert Y (set {x, X} -\<^sub>\<circ> set {X}) = vinsert Y (set {x, X} -\<^sub>\<circ> set {X})

goal (1 subgoal):
 1. vinsert Y (set {x, X} -\<^sub>\<circ> set {X}) \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (set (mk_doubleton X ` elts X))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z \<in> (\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>A. vinsert Y (A -\<^sub>\<circ> set {X})) ` elts (mk_doubleton_image X X) = elts (mk_doubleton_image X Y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mk_doubleton_image_veqpoll:
  assumes "X \<subseteq>\<^sub>\<circ> Y"
  shows "X \<approx>\<^sub>\<circ> mk_doubleton_image X Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<approx>\<^sub>\<circ> mk_doubleton_image X Y
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. X \<approx>\<^sub>\<circ> mk_doubleton_image X Y
[PROOF STEP]
have "X \<approx>\<^sub>\<circ> mk_doubleton_image X X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<approx>\<^sub>\<circ> mk_doubleton_image X X
[PROOF STEP]
unfolding mk_doubleton_image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<approx>\<^sub>\<circ> set (mk_doubleton X ` elts X)
[PROOF STEP]
by (auto simp: inj_on_mk_doubleton)
[PROOF STATE]
proof (state)
this:
X \<approx>\<^sub>\<circ> mk_doubleton_image X X

goal (1 subgoal):
 1. X \<approx>\<^sub>\<circ> mk_doubleton_image X Y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
X \<approx>\<^sub>\<circ> mk_doubleton_image X X

goal (1 subgoal):
 1. X \<approx>\<^sub>\<circ> mk_doubleton_image X Y
[PROOF STEP]
have "\<dots> \<approx> elts (mk_doubleton_image X Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_doubleton_image X X \<approx>\<^sub>\<circ> mk_doubleton_image X Y
[PROOF STEP]
by (rule mk_doubleton_image_vsubset_veqpoll[OF assms])
[PROOF STATE]
proof (state)
this:
mk_doubleton_image X X \<approx>\<^sub>\<circ> mk_doubleton_image X Y

goal (1 subgoal):
 1. X \<approx>\<^sub>\<circ> mk_doubleton_image X Y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
X \<approx>\<^sub>\<circ> mk_doubleton_image X Y
[PROOF STEP]
show "X \<approx>\<^sub>\<circ> mk_doubleton_image X Y"
[PROOF STATE]
proof (prove)
using this:
X \<approx>\<^sub>\<circ> mk_doubleton_image X Y

goal (1 subgoal):
 1. X \<approx>\<^sub>\<circ> mk_doubleton_image X Y
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
X \<approx>\<^sub>\<circ> mk_doubleton_image X Y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vdisjnt_mk_doubleton_image: "vdisjnt (mk_doubleton_image X Y) Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_doubleton_image X Y \<inter>\<^sub>\<circ> Y = []\<^sub>\<circ>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in>\<^sub>\<circ> mk_doubleton_image X Y; x \<in>\<^sub>\<circ> Y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in>\<^sub>\<circ> mk_doubleton_image X Y; x \<in>\<^sub>\<circ> Y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume prems: "b \<in>\<^sub>\<circ> Y" "b \<in>\<^sub>\<circ> mk_doubleton_image X Y"
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> Y
b \<in>\<^sub>\<circ> mk_doubleton_image X Y

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in>\<^sub>\<circ> mk_doubleton_image X Y; x \<in>\<^sub>\<circ> Y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in>\<^sub>\<circ> Y
b \<in>\<^sub>\<circ> mk_doubleton_image X Y
[PROOF STEP]
obtain a where "a \<in>\<^sub>\<circ> X" and "set {a, Y} = b"
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> Y
b \<in>\<^sub>\<circ> mk_doubleton_image X Y

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in>\<^sub>\<circ> X; set {a, Y} = b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding mk_doubleton_def mk_doubleton_image_def
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> Y
b \<in>\<^sub>\<circ> set ((\<lambda>a. set {a, Y}) ` elts X)

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in>\<^sub>\<circ> X; set {a, Y} = b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> X
set {a, Y} = b

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in>\<^sub>\<circ> mk_doubleton_image X Y; x \<in>\<^sub>\<circ> Y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> X
set {a, Y} = b
[PROOF STEP]
have "Y \<in>\<^sub>\<circ> b"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> X
set {a, Y} = b

goal (1 subgoal):
 1. Y \<in>\<^sub>\<circ> b
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
Y \<in>\<^sub>\<circ> b

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in>\<^sub>\<circ> mk_doubleton_image X Y; x \<in>\<^sub>\<circ> Y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with mem_not_sym
[PROOF STATE]
proof (chain)
picking this:
\<not> (?x \<in>\<^sub>\<circ> ?y \<and> ?y \<in>\<^sub>\<circ> ?x)
Y \<in>\<^sub>\<circ> b
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> (?x \<in>\<^sub>\<circ> ?y \<and> ?y \<in>\<^sub>\<circ> ?x)
Y \<in>\<^sub>\<circ> b

goal (1 subgoal):
 1. False
[PROOF STEP]
by (simp add: prems)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Limit_mk_doubleton_image_vsubset_Vset:
  assumes "Limit \<alpha>" and "X \<subseteq>\<^sub>\<circ> Y" and "Y \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "mk_doubleton_image X Y \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_doubleton_image X Y \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof(intro vsubsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
assume "b \<in>\<^sub>\<circ> mk_doubleton_image X Y"
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> mk_doubleton_image X Y

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in>\<^sub>\<circ> mk_doubleton_image X Y
[PROOF STEP]
obtain a where "b = mk_doubleton Y a" and "a \<in>\<^sub>\<circ> X"
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> mk_doubleton_image X Y

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>b = mk_doubleton Y a; a \<in>\<^sub>\<circ> X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding mk_doubleton_image_def
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> set (mk_doubleton Y ` elts X)

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>b = mk_doubleton Y a; a \<in>\<^sub>\<circ> X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
b = mk_doubleton Y a
a \<in>\<^sub>\<circ> X

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
Limit \<alpha>
X \<subseteq>\<^sub>\<circ> Y
Y \<in>\<^sub>\<circ> Vset \<alpha>
b = mk_doubleton Y a
a \<in>\<^sub>\<circ> X
[PROOF STEP]
have b_def: "b = set {a, Y}" and a\<alpha>: "a \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
X \<subseteq>\<^sub>\<circ> Y
Y \<in>\<^sub>\<circ> Vset \<alpha>
b = mk_doubleton Y a
a \<in>\<^sub>\<circ> X

goal (1 subgoal):
 1. b = set {a, Y} &&& a \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (auto simp: mk_doubleton_def)
[PROOF STATE]
proof (state)
this:
b = set {a, Y}
a \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from this(2) assms
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> Vset \<alpha>
Limit \<alpha>
X \<subseteq>\<^sub>\<circ> Y
Y \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "b \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> Vset \<alpha>
Limit \<alpha>
X \<subseteq>\<^sub>\<circ> Y
Y \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. b \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
unfolding b_def
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> Vset \<alpha>
Limit \<alpha>
X \<subseteq>\<^sub>\<circ> Y
Y \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. set {a, Y} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (simp add: Limit_vdoubleton_in_VsetI)
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Ord_mk_doubleton_image_vsubset_Vset_succ:
  assumes "Ord \<alpha>" and "X \<subseteq>\<^sub>\<circ> Y" and "Y \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "mk_doubleton_image X Y \<subseteq>\<^sub>\<circ> Vset (succ \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_doubleton_image X Y \<subseteq>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
proof(intro vsubsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
assume "b \<in>\<^sub>\<circ> mk_doubleton_image X Y"
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> mk_doubleton_image X Y

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in>\<^sub>\<circ> mk_doubleton_image X Y
[PROOF STEP]
obtain a where "b = mk_doubleton Y a" and "a \<in>\<^sub>\<circ> X"
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> mk_doubleton_image X Y

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>b = mk_doubleton Y a; a \<in>\<^sub>\<circ> X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding mk_doubleton_image_def
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> set (mk_doubleton Y ` elts X)

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>b = mk_doubleton Y a; a \<in>\<^sub>\<circ> X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
b = mk_doubleton Y a
a \<in>\<^sub>\<circ> X

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
Ord \<alpha>
X \<subseteq>\<^sub>\<circ> Y
Y \<in>\<^sub>\<circ> Vset \<alpha>
b = mk_doubleton Y a
a \<in>\<^sub>\<circ> X
[PROOF STEP]
have b_def: "b = set {a, Y}" and a\<alpha>: "a \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Ord \<alpha>
X \<subseteq>\<^sub>\<circ> Y
Y \<in>\<^sub>\<circ> Vset \<alpha>
b = mk_doubleton Y a
a \<in>\<^sub>\<circ> X

goal (1 subgoal):
 1. b = set {a, Y} &&& a \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (auto simp: mk_doubleton_def)
[PROOF STATE]
proof (state)
this:
b = set {a, Y}
a \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> mk_doubleton_image X Y \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
from this(2) assms
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> Vset \<alpha>
Ord \<alpha>
X \<subseteq>\<^sub>\<circ> Y
Y \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "b \<in>\<^sub>\<circ> Vset (succ \<alpha>)"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> Vset \<alpha>
Ord \<alpha>
X \<subseteq>\<^sub>\<circ> Y
Y \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
unfolding b_def
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> Vset \<alpha>
Ord \<alpha>
X \<subseteq>\<^sub>\<circ> Y
Y \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. set {a, Y} \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
[PROOF STEP]
by (simp add: Ord_vdoubleton_in_Vset_succI)
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Limit_ex_eqpoll_vdisjnt:
  assumes "Limit \<alpha>" and "X \<subseteq>\<^sub>\<circ> Y" and "Y \<in>\<^sub>\<circ> Vset \<alpha>"
  obtains Z where "X \<approx>\<^sub>\<circ> Z" and "vdisjnt Z Y" and "Z \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Z. \<lbrakk>X \<approx>\<^sub>\<circ> Z; Z \<inter>\<^sub>\<circ> Y = []\<^sub>\<circ>; Z \<subseteq>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Limit \<alpha>
X \<subseteq>\<^sub>\<circ> Y
Y \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. (\<And>Z. \<lbrakk>X \<approx>\<^sub>\<circ> Z; Z \<inter>\<^sub>\<circ> Y = []\<^sub>\<circ>; Z \<subseteq>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (intro that[of \<open>mk_doubleton_image X Y\<close>])
    (
      simp_all add:
        mk_doubleton_image_veqpoll
        vdisjnt_mk_doubleton_image
        Limit_mk_doubleton_image_vsubset_Vset
    )


[STATEMENT]
lemma Ord_ex_eqpoll_vdisjnt:
  assumes "Ord \<alpha>" and "X \<subseteq>\<^sub>\<circ> Y" and "Y \<in>\<^sub>\<circ> Vset \<alpha>"
  obtains Z where "X \<approx>\<^sub>\<circ> Z" and "vdisjnt Z Y" and "Z \<subseteq>\<^sub>\<circ> Vset (succ \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Z. \<lbrakk>X \<approx>\<^sub>\<circ> Z; Z \<inter>\<^sub>\<circ> Y = []\<^sub>\<circ>; Z \<subseteq>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Ord \<alpha>
X \<subseteq>\<^sub>\<circ> Y
Y \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. (\<And>Z. \<lbrakk>X \<approx>\<^sub>\<circ> Z; Z \<inter>\<^sub>\<circ> Y = []\<^sub>\<circ>; Z \<subseteq>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (intro that[of \<open>mk_doubleton_image X Y\<close>])
    (
      simp_all add:
        mk_doubleton_image_veqpoll
        vdisjnt_mk_doubleton_image
        Ord_mk_doubleton_image_vsubset_Vset_succ
    )


[STATEMENT]
lemma Q_hit_exists: obtains Q_hit Q_hit_pre Q_hit_post where
  "Q_hit \<in> Q" "y \<in> set Q_hit" "Q_hit = Q_hit_pre @ y # Q_hit_post"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Q_hit Q_hit_pre Q_hit_post. \<lbrakk>Q_hit \<in> Q; y \<in> set Q_hit; Q_hit = Q_hit_pre @ y # Q_hit_post\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>Q_hit Q_hit_pre Q_hit_post. \<lbrakk>Q_hit \<in> Q; y \<in> set Q_hit; Q_hit = Q_hit_pre @ y # Q_hit_post\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain Q_hit where "Q_hit \<in> Q" "y \<in> set Q_hit"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Q_hit. \<lbrakk>Q_hit \<in> Q; y \<in> set Q_hit\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using hitting_Q_or_new_last_def y y_neq_v1 y_neq_new_last
[PROOF STATE]
proof (prove)
using this:
hitting_Q_or_new_last \<equiv> \<lambda>y. y \<noteq> v0 \<and> (y = new_last \<or> (\<exists>Q_hit\<in>Q. y \<in> set Q_hit))
hitting_Q_or_new_last y
y \<noteq> v1
y \<noteq> new_last

goal (1 subgoal):
 1. (\<And>Q_hit. \<lbrakk>Q_hit \<in> Q; y \<in> set Q_hit\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Q_hit \<in> Q
y \<in> set Q_hit

goal (1 subgoal):
 1. (\<And>Q_hit Q_hit_pre Q_hit_post. \<lbrakk>Q_hit \<in> Q; y \<in> set Q_hit; Q_hit = Q_hit_pre @ y # Q_hit_post\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Q_hit \<in> Q
y \<in> set Q_hit
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Q_hit \<in> Q
y \<in> set Q_hit

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
Q_hit \<in> Q
y \<in> set Q_hit
\<lbrakk>?Q_hit \<in> Q; y \<in> set ?Q_hit; ?Q_hit = ?Q_hit_pre @ y # ?Q_hit_post\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (meson split_list)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Q_hit_v0_v1: "v0 \<leadsto>Q_hit\<leadsto>\<^bsub>H_x\<^esub> v1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v0 \<leadsto>Q_hit\<leadsto>\<^bsub>H_x\<^esub> v1
[PROOF STEP]
using Q.paths Q_hit(1)
[PROOF STATE]
proof (prove)
using this:
?xs \<in> Q \<Longrightarrow> v0 \<leadsto>?xs\<leadsto>\<^bsub>H_x\<^esub> v1
Q_hit \<in> Q

goal (1 subgoal):
 1. v0 \<leadsto>Q_hit\<leadsto>\<^bsub>H_x\<^esub> v1
[PROOF STEP]
by blast


[STATEMENT]
lemma Q_hit_vertices: "set Q_hit \<subseteq> V - {new_last}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set Q_hit \<subseteq> V - {new_last}
[PROOF STEP]
using Q.walk_in_V H_x_def path_from_to_def remove_vertex_V Q_hit_v0_v1
[PROOF STATE]
proof (prove)
using this:
Q.walk ?xs \<Longrightarrow> set ?xs \<subseteq> V\<^bsub>H_x\<^esub>
H_x \<equiv> remove_vertex new_last
?v \<leadsto>?xs\<leadsto>\<^bsub>?G\<^esub> ?w \<equiv> (Digraph.walk ?G ?xs \<and> distinct ?xs) \<and> ?xs \<noteq> [] \<and> hd ?xs = ?v \<and> last ?xs = ?w
V\<^bsub>remove_vertex ?x\<^esub> = V - {?x}
v0 \<leadsto>Q_hit\<leadsto>\<^bsub>H_x\<^esub> v1

goal (1 subgoal):
 1. set Q_hit \<subseteq> V - {new_last}
[PROOF STEP]
by fastforce


[STATEMENT]
lemma Q_hit_pre_not_Nil: "Q_hit_pre \<noteq> Nil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q_hit_pre \<noteq> []
[PROOF STEP]
using Q_hit_v0_v1 y_neq_v0
[PROOF STATE]
proof (prove)
using this:
v0 \<leadsto>Q_hit\<leadsto>\<^bsub>H_x\<^esub> v1
y \<noteq> v0

goal (1 subgoal):
 1. Q_hit_pre \<noteq> []
[PROOF STEP]
unfolding Q_hit_decomp
[PROOF STATE]
proof (prove)
using this:
v0 \<leadsto>(Q_hit_pre @ y # Q_hit_post)\<leadsto>\<^bsub>H_x\<^esub> v1
y \<noteq> v0

goal (1 subgoal):
 1. Q_hit_pre \<noteq> []
[PROOF STEP]
by auto


[STATEMENT]
lemma tl_Q_hit_pre: "tl (Q_hit_pre @ [y]) \<noteq> Nil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl (Q_hit_pre @ [y]) \<noteq> []
[PROOF STEP]
using Q_hit_pre_not_Nil
[PROOF STATE]
proof (prove)
using this:
Q_hit_pre \<noteq> []

goal (1 subgoal):
 1. tl (Q_hit_pre @ [y]) \<noteq> []
[PROOF STEP]
by simp


[STATEMENT]
lemma Q_hit_pre_edges: "edges_of_walk (Q_hit_pre @ [y]) \<inter> B \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B \<noteq> {}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
assume "edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {}"
[PROOF STATE]
proof (state)
this:
H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {}

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {}

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
have "edges_of_walk (Q_hit_pre @ [y]) \<subseteq> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<subseteq> E
[PROOF STEP]
by (metis Q.paths H_x_def Q_hit(1) Q_hit_decomp edges_of_walk_in_E path_decomp'
          path_from_to_def remove_vertex_walk_add)
[PROOF STATE]
proof (state)
this:
H.edges_of_walk (Q_hit_pre @ [y]) \<subseteq> E

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {}
H.edges_of_walk (Q_hit_pre @ [y]) \<subseteq> E
[PROOF STEP]
have Q_hit_pre_edges:
      "edges_of_walk (Q_hit_pre @ [y]) \<subseteq> \<Union>(edges_of_walk ` paths_with_new)"
[PROOF STATE]
proof (prove)
using this:
H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {}
H.edges_of_walk (Q_hit_pre @ [y]) \<subseteq> E

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
H.edges_of_walk (Q_hit_pre @ [y]) \<inter> (E - \<Union> (H.edges_of_walk ` paths_with_new)) = {}
H.edges_of_walk (Q_hit_pre @ [y]) \<subseteq> E

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
H.edges_of_walk (Q_hit_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
H.edges_of_walk (Q_hit_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)
[PROOF STEP]
have *: "first_edge_of_walk (Q_hit_pre @ [y]) \<in> \<Union>(edges_of_walk ` paths_with_new)"
[PROOF STATE]
proof (prove)
using this:
H.edges_of_walk (Q_hit_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)

goal (1 subgoal):
 1. H.first_edge_of_walk (Q_hit_pre @ [y]) \<in> \<Union> (H.edges_of_walk ` paths_with_new)
[PROOF STEP]
using tl_Q_hit_pre first_edge_in_edges
[PROOF STATE]
proof (prove)
using this:
H.edges_of_walk (Q_hit_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)
tl (Q_hit_pre @ [y]) \<noteq> []
tl ?xs \<noteq> [] \<Longrightarrow> H.first_edge_of_walk ?xs \<in> H.edges_of_walk ?xs

goal (1 subgoal):
 1. H.first_edge_of_walk (Q_hit_pre @ [y]) \<in> \<Union> (H.edges_of_walk ` paths_with_new)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
H.first_edge_of_walk (Q_hit_pre @ [y]) \<in> \<Union> (H.edges_of_walk ` paths_with_new)

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
define v' where "v' \<equiv> hd (tl (Q_hit_pre @ [y]))"
[PROOF STATE]
proof (state)
this:
v' \<equiv> hd (tl (Q_hit_pre @ [y]))

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v' \<equiv> hd (tl (Q_hit_pre @ [y]))
[PROOF STEP]
have v': "(v0, v') = first_edge_of_walk (Q_hit_pre @ [y])"
[PROOF STATE]
proof (prove)
using this:
v' \<equiv> hd (tl (Q_hit_pre @ [y]))

goal (1 subgoal):
 1. (v0, v') = H.first_edge_of_walk (Q_hit_pre @ [y])
[PROOF STEP]
using first_edge_hd_tl Q_hit_pre_not_Nil tl_Q_hit_pre
[PROOF STATE]
proof (prove)
using this:
v' \<equiv> hd (tl (Q_hit_pre @ [y]))
\<lbrakk>?v \<leadsto>?xs\<leadsto> ?w; tl ?xs \<noteq> []\<rbrakk> \<Longrightarrow> H.first_edge_of_walk ?xs = (?v, hd (tl ?xs))
Q_hit_pre \<noteq> []
tl (Q_hit_pre @ [y]) \<noteq> []

goal (1 subgoal):
 1. (v0, v') = H.first_edge_of_walk (Q_hit_pre @ [y])
[PROOF STEP]
by (metis Q.path_from_toE Q_hit_decomp Q_hit_v0_v1 first_edge_of_walk.simps(1)
          hd_Cons_tl hd_append snoc_eq_iff_butlast)
[PROOF STATE]
proof (state)
this:
(v0, v') = H.first_edge_of_walk (Q_hit_pre @ [y])

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(v0, v') = H.first_edge_of_walk (Q_hit_pre @ [y])
[PROOF STEP]
obtain P_i where
      P_i: "P_i \<in> paths_with_new" "(v0, v') \<in> edges_of_walk P_i"
[PROOF STATE]
proof (prove)
using this:
(v0, v') = H.first_edge_of_walk (Q_hit_pre @ [y])

goal (1 subgoal):
 1. (\<And>P_i. \<lbrakk>P_i \<in> paths_with_new; (v0, v') \<in> H.edges_of_walk P_i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
(v0, v') = H.first_edge_of_walk (Q_hit_pre @ [y])
H.first_edge_of_walk (Q_hit_pre @ [y]) \<in> \<Union> (H.edges_of_walk ` paths_with_new)

goal (1 subgoal):
 1. (\<And>P_i. \<lbrakk>P_i \<in> paths_with_new; (v0, v') \<in> H.edges_of_walk P_i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P_i \<in> paths_with_new
(v0, v') \<in> H.edges_of_walk P_i

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P_i \<in> paths_with_new
(v0, v') \<in> H.edges_of_walk P_i
[PROOF STEP]
have P_i_first: "first_edge_of_walk P_i = (v0, v')"
[PROOF STATE]
proof (prove)
using this:
P_i \<in> paths_with_new
(v0, v') \<in> H.edges_of_walk P_i

goal (1 subgoal):
 1. H.first_edge_of_walk P_i = (v0, v')
[PROOF STEP]
using first_edge_first paths_with_new_def paths P_new
[PROOF STATE]
proof (prove)
using this:
P_i \<in> paths_with_new
(v0, v') \<in> H.edges_of_walk P_i
\<lbrakk>?v \<leadsto>?xs\<leadsto> ?w; (?v, ?w') \<in> H.edges_of_walk ?xs\<rbrakk> \<Longrightarrow> H.first_edge_of_walk ?xs = (?v, ?w')
paths_with_new \<equiv> insert P_new paths
?xs \<in> paths \<Longrightarrow> v0 \<leadsto>?xs\<leadsto> v1
v0 \<leadsto>P_new\<leadsto> last P_new

goal (1 subgoal):
 1. H.first_edge_of_walk P_i = (v0, v')
[PROOF STEP]
by (metis insert_iff)
[PROOF STATE]
proof (state)
this:
H.first_edge_of_walk P_i = (v0, v')

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
H.first_edge_of_walk P_i = (v0, v')

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
have "first_edge_of_walk P_k = (v0, hd (tl P_k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H.first_edge_of_walk P_k = (v0, hd (tl P_k))
[PROOF STEP]
by (metis P_k_decomp P_k_pre_not_Nil append_is_Nil_conv first_edge_of_walk.simps(1)
          hd_P_k_v0 list.distinct(1) list.exhaust_sel tl_append2)
[PROOF STATE]
proof (state)
this:
H.first_edge_of_walk P_k = (v0, hd (tl P_k))

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
H.first_edge_of_walk P_i = (v0, v')
H.first_edge_of_walk P_k = (v0, hd (tl P_k))
[PROOF STEP]
have "P_i \<noteq> P_k"
[PROOF STATE]
proof (prove)
using this:
H.first_edge_of_walk P_i = (v0, v')
H.first_edge_of_walk P_k = (v0, hd (tl P_k))

goal (1 subgoal):
 1. P_i \<noteq> P_k
[PROOF STEP]
by (metis Q.first_edge_first P_k(2) Q.second_vertices_first_edge Q_hit(1) Q_hit_decomp
          Q_hit_v0_v1 Un_iff v' tl_Q_hit_pre first_edge_in_edges walk_edges_decomp)
[PROOF STATE]
proof (state)
this:
P_i \<noteq> P_k

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
text \<open>
      Then @{term P_k} and @{term P_i} intersect in @{term y}, which is not one of @{term v0},
      @{term v1}, or @{term new_last}.  So we get a contradiction because these two paths should be
      disjoint on all other vertices.
\<close>
[PROOF STATE]
proof (state)
this:
P_i \<noteq> P_k

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P_i \<noteq> P_k

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
have "v1 \<notin> set (Q_hit_pre @ [y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v1 \<notin> set (Q_hit_pre @ [y])
[PROOF STEP]
using Q_hit_v0_v1 Q_hit_decomp y_neq_v1
[PROOF STATE]
proof (prove)
using this:
v0 \<leadsto>Q_hit\<leadsto>\<^bsub>H_x\<^esub> v1
Q_hit = Q_hit_pre @ y # Q_hit_post
y \<noteq> v1

goal (1 subgoal):
 1. v1 \<notin> set (Q_hit_pre @ [y])
[PROOF STEP]
by (simp add: Q.path_from_to_last')
[PROOF STATE]
proof (state)
this:
v1 \<notin> set (Q_hit_pre @ [y])

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v1 \<notin> set (Q_hit_pre @ [y])

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
have "new_last \<notin> set (Q_hit_pre @ [y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_last \<notin> set (Q_hit_pre @ [y])
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. new_last \<notin> set (Q_hit_pre @ [y])
[PROOF STEP]
have "new_last \<notin> set Q_hit_pre"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_last \<notin> set Q_hit_pre
[PROOF STEP]
using Q_hit_decomp Q_hit_vertices
[PROOF STATE]
proof (prove)
using this:
Q_hit = Q_hit_pre @ y # Q_hit_post
set Q_hit \<subseteq> V - {new_last}

goal (1 subgoal):
 1. new_last \<notin> set Q_hit_pre
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
new_last \<notin> set Q_hit_pre

goal (1 subgoal):
 1. new_last \<notin> set (Q_hit_pre @ [y])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
new_last \<notin> set Q_hit_pre
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
new_last \<notin> set Q_hit_pre

goal (1 subgoal):
 1. new_last \<notin> set (Q_hit_pre @ [y])
[PROOF STEP]
using y_neq_new_last
[PROOF STATE]
proof (prove)
using this:
new_last \<notin> set Q_hit_pre
y \<noteq> new_last

goal (1 subgoal):
 1. new_last \<notin> set (Q_hit_pre @ [y])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
new_last \<notin> set (Q_hit_pre @ [y])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
new_last \<notin> set (Q_hit_pre @ [y])

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
new_last \<notin> set (Q_hit_pre @ [y])

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
have "hd (tl (Q_hit_pre @ [y])) = hd (tl P_i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (tl (Q_hit_pre @ [y])) = hd (tl P_i)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hd (tl (Q_hit_pre @ [y])) = hd (tl P_i)
[PROOF STEP]
have "hd (tl P_i) = v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (tl P_i) = v'
[PROOF STEP]
using P_i_first P_i(1) tl_P_new(1)
[PROOF STATE]
proof (prove)
using this:
H.first_edge_of_walk P_i = (v0, v')
P_i \<in> paths_with_new
tl P_new \<noteq> []

goal (1 subgoal):
 1. hd (tl P_i) = v'
[PROOF STEP]
by (metis Pair_inject first_edge_of_walk.simps(1) insert_iff list.collapse
            paths_tl_notnil paths_with_new_def tl_Nil)
[PROOF STATE]
proof (state)
this:
hd (tl P_i) = v'

goal (1 subgoal):
 1. hd (tl (Q_hit_pre @ [y])) = hd (tl P_i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd (tl P_i) = v'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hd (tl P_i) = v'

goal (1 subgoal):
 1. hd (tl (Q_hit_pre @ [y])) = hd (tl P_i)
[PROOF STEP]
using v'_def
[PROOF STATE]
proof (prove)
using this:
hd (tl P_i) = v'
v' \<equiv> hd (tl (Q_hit_pre @ [y]))

goal (1 subgoal):
 1. hd (tl (Q_hit_pre @ [y])) = hd (tl P_i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hd (tl (Q_hit_pre @ [y])) = hd (tl P_i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
hd (tl (Q_hit_pre @ [y])) = hd (tl P_i)

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hd (tl (Q_hit_pre @ [y])) = hd (tl P_i)

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
have "v0 \<leadsto>(Q_hit_pre @ [y])\<leadsto> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v0 \<leadsto>(Q_hit_pre @ [y])\<leadsto> y
[PROOF STEP]
by (metis Q.path_decomp' H_x_def Q_hit_decomp Q_hit_v0_v1 Q_hit_pre_not_Nil
          hd_append2 path_from_to_def remove_vertex_walk_add snoc_eq_iff_butlast)
[PROOF STATE]
proof (state)
this:
v0 \<leadsto>(Q_hit_pre @ [y])\<leadsto> y

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P_i \<noteq> P_k
v1 \<notin> set (Q_hit_pre @ [y])
new_last \<notin> set (Q_hit_pre @ [y])
hd (tl (Q_hit_pre @ [y])) = hd (tl P_i)
v0 \<leadsto>(Q_hit_pre @ [y])\<leadsto> y
[PROOF STEP]
have "edges_of_walk (Q_hit_pre @ [y]) \<subseteq> edges_of_walk P_i"
[PROOF STATE]
proof (prove)
using this:
P_i \<noteq> P_k
v1 \<notin> set (Q_hit_pre @ [y])
new_last \<notin> set (Q_hit_pre @ [y])
hd (tl (Q_hit_pre @ [y])) = hd (tl P_i)
v0 \<leadsto>(Q_hit_pre @ [y])\<leadsto> y

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<subseteq> H.edges_of_walk P_i
[PROOF STEP]
using new_path_follows_old_paths tl_Q_hit_pre P_i(1) Q_hit_pre_edges
[PROOF STATE]
proof (prove)
using this:
P_i \<noteq> P_k
v1 \<notin> set (Q_hit_pre @ [y])
new_last \<notin> set (Q_hit_pre @ [y])
hd (tl (Q_hit_pre @ [y])) = hd (tl P_i)
v0 \<leadsto>(Q_hit_pre @ [y])\<leadsto> y
\<lbrakk>v0 \<leadsto>?xs\<leadsto> ?w; tl ?xs \<noteq> []; v1 \<notin> set ?xs; new_last \<notin> set ?xs; ?P \<in> paths_with_new; hd (tl ?xs) = hd (tl ?P); H.edges_of_walk ?xs \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)\<rbrakk> \<Longrightarrow> H.edges_of_walk ?xs \<subseteq> H.edges_of_walk ?P
tl (Q_hit_pre @ [y]) \<noteq> []
P_i \<in> paths_with_new
H.edges_of_walk (Q_hit_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<subseteq> H.edges_of_walk P_i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
H.edges_of_walk (Q_hit_pre @ [y]) \<subseteq> H.edges_of_walk P_i

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
from walk_edges_subset[OF this]
[PROOF STATE]
proof (chain)
picking this:
tl (Q_hit_pre @ [y]) \<noteq> [] \<Longrightarrow> set (Q_hit_pre @ [y]) \<subseteq> set P_i
[PROOF STEP]
have "y \<in> set P_i"
[PROOF STATE]
proof (prove)
using this:
tl (Q_hit_pre @ [y]) \<noteq> [] \<Longrightarrow> set (Q_hit_pre @ [y]) \<subseteq> set P_i

goal (1 subgoal):
 1. y \<in> set P_i
[PROOF STEP]
by (simp add: tl_Q_hit_pre)
[PROOF STATE]
proof (state)
this:
y \<in> set P_i

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y \<in> set P_i

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
have "y \<in> set P_k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> set P_k
[PROOF STEP]
using P_k_decomp
[PROOF STATE]
proof (prove)
using this:
P_k = P_k_pre @ y # P_k_post

goal (1 subgoal):
 1. y \<in> set P_k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> set P_k

goal (1 subgoal):
 1. H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B = {} \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
y \<in> set P_i
y \<in> set P_k
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
y \<in> set P_i
y \<in> set P_k

goal (1 subgoal):
 1. False
[PROOF STEP]
using y_neq_v0 y_neq_v1 y_neq_new_last \<open>P_i \<noteq> P_k\<close>
        paths_plus_one_disjoint[OF P_i(1), of P_k y] P_k(1) P_new_decomp
[PROOF STATE]
proof (prove)
using this:
y \<in> set P_i
y \<in> set P_k
y \<noteq> v0
y \<noteq> v1
y \<noteq> new_last
P_i \<noteq> P_k
\<lbrakk>P_k \<in> paths_with_new; P_i \<noteq> P_k; y \<in> set P_i; y \<in> set P_k\<rbrakk> \<Longrightarrow> y = v0 \<or> y = v1 \<or> y = new_last
P_k \<in> paths_with_new
P_new = new_pre @ [new_last]

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma P_k_pre_edges: "edges_of_walk (P_k_pre @ [y]) \<inter> B = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H.edges_of_walk (P_k_pre @ [y]) \<inter> B = {}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H.edges_of_walk (P_k_pre @ [y]) \<inter> B = {}
[PROOF STEP]
have "edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union>(edges_of_walk ` paths_with_new)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)
 2. \<not> ?P \<Longrightarrow> H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)
[PROOF STEP]
assume "P_k = P_new"
[PROOF STATE]
proof (state)
this:
P_k = P_new

goal (2 subgoals):
 1. ?P \<Longrightarrow> H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)
 2. \<not> ?P \<Longrightarrow> H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P_k = P_new
[PROOF STEP]
have "edges_of_walk (P_k_pre @ [y]) \<subseteq> edges_of_walk P_new"
[PROOF STATE]
proof (prove)
using this:
P_k = P_new

goal (1 subgoal):
 1. H.edges_of_walk (P_k_pre @ [y]) \<subseteq> H.edges_of_walk P_new
[PROOF STEP]
using P_k_decomp edges_of_comp1
[PROOF STATE]
proof (prove)
using this:
P_k = P_new
P_k = P_k_pre @ y # P_k_post
H.edges_of_walk ?xs \<subseteq> H.edges_of_walk (?xs @ ?ys)

goal (1 subgoal):
 1. H.edges_of_walk (P_k_pre @ [y]) \<subseteq> H.edges_of_walk P_new
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
H.edges_of_walk (P_k_pre @ [y]) \<subseteq> H.edges_of_walk P_new

goal (2 subgoals):
 1. ?P \<Longrightarrow> H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)
 2. \<not> ?P \<Longrightarrow> H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
H.edges_of_walk (P_k_pre @ [y]) \<subseteq> H.edges_of_walk P_new
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
H.edges_of_walk (P_k_pre @ [y]) \<subseteq> H.edges_of_walk P_new

goal (1 subgoal):
 1. H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)
[PROOF STEP]
unfolding paths_with_new_def
[PROOF STATE]
proof (prove)
using this:
H.edges_of_walk (P_k_pre @ [y]) \<subseteq> H.edges_of_walk P_new

goal (1 subgoal):
 1. H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` insert P_new paths)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)

goal (1 subgoal):
 1. P_k \<noteq> P_new \<Longrightarrow> H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P_k \<noteq> P_new \<Longrightarrow> H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)
[PROOF STEP]
assume "P_k \<noteq> P_new"
[PROOF STATE]
proof (state)
this:
P_k \<noteq> P_new

goal (1 subgoal):
 1. P_k \<noteq> P_new \<Longrightarrow> H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P_k \<noteq> P_new
[PROOF STEP]
have "P_k \<in> paths"
[PROOF STATE]
proof (prove)
using this:
P_k \<noteq> P_new

goal (1 subgoal):
 1. P_k \<in> paths
[PROOF STEP]
using P_k(1) paths_with_new_def
[PROOF STATE]
proof (prove)
using this:
P_k \<noteq> P_new
P_k \<in> paths_with_new
paths_with_new \<equiv> insert P_new paths

goal (1 subgoal):
 1. P_k \<in> paths
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P_k \<in> paths

goal (1 subgoal):
 1. P_k \<noteq> P_new \<Longrightarrow> H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P_k \<in> paths
[PROOF STEP]
have "edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union>(edges_of_walk ` paths)"
[PROOF STATE]
proof (prove)
using this:
P_k \<in> paths

goal (1 subgoal):
 1. H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths)
[PROOF STEP]
using edges_of_comp1[of "P_k_pre @ [y]"] P_k_decomp
[PROOF STATE]
proof (prove)
using this:
P_k \<in> paths
H.edges_of_walk (P_k_pre @ [y]) \<subseteq> H.edges_of_walk ((P_k_pre @ [y]) @ ?ys)
P_k = P_k_pre @ y # P_k_post

goal (1 subgoal):
 1. H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths)

goal (1 subgoal):
 1. P_k \<noteq> P_new \<Longrightarrow> H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths)

goal (1 subgoal):
 1. H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)
[PROOF STEP]
unfolding paths_with_new_def
[PROOF STATE]
proof (prove)
using this:
H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths)

goal (1 subgoal):
 1. H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` insert P_new paths)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)

goal (1 subgoal):
 1. H.edges_of_walk (P_k_pre @ [y]) \<inter> B = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)

goal (1 subgoal):
 1. H.edges_of_walk (P_k_pre @ [y]) \<inter> B = {}
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
H.edges_of_walk (P_k_pre @ [y]) \<subseteq> \<Union> (H.edges_of_walk ` paths_with_new)

goal (1 subgoal):
 1. H.edges_of_walk (P_k_pre @ [y]) \<inter> (E - \<Union> (H.edges_of_walk ` paths_with_new)) = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
H.edges_of_walk (P_k_pre @ [y]) \<inter> B = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Q_hit'_v0_v1_H_x: "v0 \<leadsto>Q_hit'\<leadsto>\<^bsub>H_x\<^esub> v1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v0 \<leadsto>Q_hit'\<leadsto>\<^bsub>H_x\<^esub> v1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v0 \<leadsto>Q_hit'\<leadsto>\<^bsub>H_x\<^esub> v1
[PROOF STEP]
have "new_last \<notin> set P_k_pre"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_last \<notin> set P_k_pre
[PROOF STEP]
using new_last_neq_v0 hitting_Q_or_new_last_def y_min
[PROOF STATE]
proof (prove)
using this:
new_last \<noteq> v0
hitting_Q_or_new_last \<equiv> \<lambda>y. y \<noteq> v0 \<and> (y = new_last \<or> (\<exists>Q_hit\<in>Q. y \<in> set Q_hit))
?y' \<in> set P_k_pre \<Longrightarrow> \<not> hitting_Q_or_new_last ?y'

goal (1 subgoal):
 1. new_last \<notin> set P_k_pre
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
new_last \<notin> set P_k_pre

goal (1 subgoal):
 1. v0 \<leadsto>Q_hit'\<leadsto>\<^bsub>H_x\<^esub> v1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
new_last \<notin> set P_k_pre

goal (1 subgoal):
 1. v0 \<leadsto>Q_hit'\<leadsto>\<^bsub>H_x\<^esub> v1
[PROOF STEP]
have "new_last \<notin> set Q_hit_post"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_last \<notin> set Q_hit_post
[PROOF STEP]
using Q_hit_vertices
[PROOF STATE]
proof (prove)
using this:
set Q_hit \<subseteq> V - {new_last}

goal (1 subgoal):
 1. new_last \<notin> set Q_hit_post
[PROOF STEP]
unfolding Q_hit_decomp
[PROOF STATE]
proof (prove)
using this:
set (Q_hit_pre @ y # Q_hit_post) \<subseteq> V - {new_last}

goal (1 subgoal):
 1. new_last \<notin> set Q_hit_post
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
new_last \<notin> set Q_hit_post

goal (1 subgoal):
 1. v0 \<leadsto>Q_hit'\<leadsto>\<^bsub>H_x\<^esub> v1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
new_last \<notin> set P_k_pre
new_last \<notin> set Q_hit_post
[PROOF STEP]
have "new_last \<notin> set Q_hit'"
[PROOF STATE]
proof (prove)
using this:
new_last \<notin> set P_k_pre
new_last \<notin> set Q_hit_post

goal (1 subgoal):
 1. new_last \<notin> set Q_hit'
[PROOF STEP]
using y_neq_new_last Q_hit'_def
[PROOF STATE]
proof (prove)
using this:
new_last \<notin> set P_k_pre
new_last \<notin> set Q_hit_post
y \<noteq> new_last
Q_hit' \<equiv> P_k_pre @ y # Q_hit_post

goal (1 subgoal):
 1. new_last \<notin> set Q_hit'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
new_last \<notin> set Q_hit'

goal (1 subgoal):
 1. v0 \<leadsto>Q_hit'\<leadsto>\<^bsub>H_x\<^esub> v1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
new_last \<notin> set Q_hit'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
new_last \<notin> set Q_hit'

goal (1 subgoal):
 1. v0 \<leadsto>Q_hit'\<leadsto>\<^bsub>H_x\<^esub> v1
[PROOF STEP]
using remove_vertex_path_from_to[OF Q_hit'_v0_v1] H_x_def new_last_in_V
[PROOF STATE]
proof (prove)
using this:
new_last \<notin> set Q_hit'
\<lbrakk>?x \<in> V; ?x \<notin> set Q_hit'\<rbrakk> \<Longrightarrow> v0 \<leadsto>Q_hit'\<leadsto>\<^bsub>remove_vertex ?x\<^esub> v1
H_x \<equiv> remove_vertex new_last
new_last \<in> V

goal (1 subgoal):
 1. v0 \<leadsto>Q_hit'\<leadsto>\<^bsub>H_x\<^esub> v1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v0 \<leadsto>Q_hit'\<leadsto>\<^bsub>H_x\<^esub> v1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Q_hit_edges_disjoint:
    "\<Union>(edges_of_walk ` (Q - {Q_hit})) \<inter> edges_of_walk Q_hit = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (H.edges_of_walk ` (Q - {Q_hit})) \<inter> H.edges_of_walk Q_hit = {}
[PROOF STEP]
using DiffD1 Q.paths_edge_disjoint Q_hit(1)
[PROOF STATE]
proof (prove)
using this:
?c \<in> ?A - ?B \<Longrightarrow> ?c \<in> ?A
\<lbrakk>?xs \<in> Q; ?ys \<in> Q; ?xs \<noteq> ?ys\<rbrakk> \<Longrightarrow> H.edges_of_walk ?xs \<inter> H.edges_of_walk ?ys = {}
Q_hit \<in> Q

goal (1 subgoal):
 1. \<Union> (H.edges_of_walk ` (Q - {Q_hit})) \<inter> H.edges_of_walk Q_hit = {}
[PROOF STEP]
by fastforce


[STATEMENT]
lemma Q_hit'_notin_Q_minus_Q_hit: "Q_hit' \<notin> Q - {Q_hit}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q_hit' \<notin> Q - {Q_hit}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Q_hit' \<notin> Q - {Q_hit}
[PROOF STEP]
have "hd (tl Q_hit') \<notin> Q.second_vertices"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (tl Q_hit') \<notin> Q.second_vertices
[PROOF STEP]
using P_k(2) P_k_decomp
[PROOF STATE]
proof (prove)
using this:
hd (tl P_k) \<notin> Q.second_vertices
P_k = P_k_pre @ y # P_k_post

goal (1 subgoal):
 1. hd (tl Q_hit') \<notin> Q.second_vertices
[PROOF STEP]
by (metis P_k_pre_not_Nil Q_hit'_def append_eq_append_conv2 append_self_conv hd_append2
          list.sel(1) tl_append2)
[PROOF STATE]
proof (state)
this:
hd (tl Q_hit') \<notin> Q.second_vertices

goal (1 subgoal):
 1. Q_hit' \<notin> Q - {Q_hit}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd (tl Q_hit') \<notin> Q.second_vertices
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hd (tl Q_hit') \<notin> Q.second_vertices

goal (1 subgoal):
 1. Q_hit' \<notin> Q - {Q_hit}
[PROOF STEP]
using Q.second_vertices_new_path[of Q_hit']
[PROOF STATE]
proof (prove)
using this:
hd (tl Q_hit') \<notin> Q.second_vertices
hd (tl Q_hit') \<notin> Q.second_vertices \<Longrightarrow> Q_hit' \<notin> Q

goal (1 subgoal):
 1. Q_hit' \<notin> Q - {Q_hit}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Q_hit' \<notin> Q - {Q_hit}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Q_weight_smaller: "Q_weight Q' < Q_weight Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
define Q_edges where "Q_edges \<equiv> \<Union>(edges_of_walk ` Q) \<inter> B"
[PROOF STATE]
proof (state)
this:
Q_edges \<equiv> \<Union> (H.edges_of_walk ` Q) \<inter> B

goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
define Q'_edges where "Q'_edges \<equiv> \<Union>(edges_of_walk ` Q') \<inter> B"
[PROOF STATE]
proof (state)
this:
Q'_edges \<equiv> \<Union> (H.edges_of_walk ` Q') \<inter> B

goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Q'_edges \<equiv> \<Union> (H.edges_of_walk ` Q') \<inter> B

goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
fix v w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
assume *: "(v,w) \<in> Q'_edges" "(v,w) \<notin> Q_edges"
[PROOF STATE]
proof (state)
this:
(v, w) \<in> Q'_edges
(v, w) \<notin> Q_edges

goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(v, w) \<in> Q'_edges
(v, w) \<notin> Q_edges
[PROOF STEP]
have v_w_in_B: "(v,w) \<in> B"
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> Q'_edges
(v, w) \<notin> Q_edges

goal (1 subgoal):
 1. (v, w) \<in> B
[PROOF STEP]
unfolding Q'_edges_def
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> \<Union> (H.edges_of_walk ` Q') \<inter> B
(v, w) \<notin> Q_edges

goal (1 subgoal):
 1. (v, w) \<in> B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(v, w) \<in> B

goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
obtain Q'_v_w_witness where Q'_v_w_witness:
        "Q'_v_w_witness \<in> Q'" "(v,w) \<in> edges_of_walk Q'_v_w_witness"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Q'_v_w_witness. \<lbrakk>Q'_v_w_witness \<in> Q'; (v, w) \<in> H.edges_of_walk Q'_v_w_witness\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using *(1)
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> Q'_edges

goal (1 subgoal):
 1. (\<And>Q'_v_w_witness. \<lbrakk>Q'_v_w_witness \<in> Q'; (v, w) \<in> H.edges_of_walk Q'_v_w_witness\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Q'_edges_def
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> \<Union> (H.edges_of_walk ` Q') \<inter> B

goal (1 subgoal):
 1. (\<And>Q'_v_w_witness. \<lbrakk>Q'_v_w_witness \<in> Q'; (v, w) \<in> H.edges_of_walk Q'_v_w_witness\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Q'_v_w_witness \<in> Q'
(v, w) \<in> H.edges_of_walk Q'_v_w_witness

goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
have "Q'_v_w_witness \<noteq> Q_hit'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q'_v_w_witness \<noteq> Q_hit'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Q'_v_w_witness = Q_hit' \<Longrightarrow> False
[PROOF STEP]
assume "Q'_v_w_witness = Q_hit'"
[PROOF STATE]
proof (state)
this:
Q'_v_w_witness = Q_hit'

goal (1 subgoal):
 1. Q'_v_w_witness = Q_hit' \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Q'_v_w_witness = Q_hit'
[PROOF STEP]
have "edges_of_walk Q'_v_w_witness =
            edges_of_walk (P_k_pre @ [y]) \<union> edges_of_walk (y # Q_hit_post)"
[PROOF STATE]
proof (prove)
using this:
Q'_v_w_witness = Q_hit'

goal (1 subgoal):
 1. H.edges_of_walk Q'_v_w_witness = H.edges_of_walk (P_k_pre @ [y]) \<union> H.edges_of_walk (y # Q_hit_post)
[PROOF STEP]
unfolding Q_hit'_def
[PROOF STATE]
proof (prove)
using this:
Q'_v_w_witness = P_k_pre @ y # Q_hit_post

goal (1 subgoal):
 1. H.edges_of_walk Q'_v_w_witness = H.edges_of_walk (P_k_pre @ [y]) \<union> H.edges_of_walk (y # Q_hit_post)
[PROOF STEP]
using walk_edges_decomp[of P_k_pre y Q_hit_post]
[PROOF STATE]
proof (prove)
using this:
Q'_v_w_witness = P_k_pre @ y # Q_hit_post
H.edges_of_walk (P_k_pre @ y # Q_hit_post) = H.edges_of_walk (P_k_pre @ [y]) \<union> H.edges_of_walk (y # Q_hit_post)

goal (1 subgoal):
 1. H.edges_of_walk Q'_v_w_witness = H.edges_of_walk (P_k_pre @ [y]) \<union> H.edges_of_walk (y # Q_hit_post)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
H.edges_of_walk Q'_v_w_witness = H.edges_of_walk (P_k_pre @ [y]) \<union> H.edges_of_walk (y # Q_hit_post)

goal (1 subgoal):
 1. Q'_v_w_witness = Q_hit' \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
H.edges_of_walk Q'_v_w_witness = H.edges_of_walk (P_k_pre @ [y]) \<union> H.edges_of_walk (y # Q_hit_post)

goal (1 subgoal):
 1. Q'_v_w_witness = Q_hit' \<Longrightarrow> False
[PROOF STEP]
have "(v,w) \<notin> edges_of_walk (P_k_pre @ [y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, w) \<notin> H.edges_of_walk (P_k_pre @ [y])
[PROOF STEP]
using P_k_pre_edges v_w_in_B
[PROOF STATE]
proof (prove)
using this:
H.edges_of_walk (P_k_pre @ [y]) \<inter> B = {}
(v, w) \<in> B

goal (1 subgoal):
 1. (v, w) \<notin> H.edges_of_walk (P_k_pre @ [y])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(v, w) \<notin> H.edges_of_walk (P_k_pre @ [y])

goal (1 subgoal):
 1. Q'_v_w_witness = Q_hit' \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(v, w) \<notin> H.edges_of_walk (P_k_pre @ [y])

goal (1 subgoal):
 1. Q'_v_w_witness = Q_hit' \<Longrightarrow> False
[PROOF STEP]
have "(v,w) \<notin> edges_of_walk (y # Q_hit_post)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, w) \<notin> H.edges_of_walk (y # Q_hit_post)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (v, w) \<in> H.edges_of_walk (y # Q_hit_post) \<Longrightarrow> False
[PROOF STEP]
assume "(v,w) \<in> edges_of_walk (y # Q_hit_post)"
[PROOF STATE]
proof (state)
this:
(v, w) \<in> H.edges_of_walk (y # Q_hit_post)

goal (1 subgoal):
 1. (v, w) \<in> H.edges_of_walk (y # Q_hit_post) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(v, w) \<in> H.edges_of_walk (y # Q_hit_post)
[PROOF STEP]
have "(v,w) \<in> edges_of_walk Q_hit"
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> H.edges_of_walk (y # Q_hit_post)

goal (1 subgoal):
 1. (v, w) \<in> H.edges_of_walk Q_hit
[PROOF STEP]
unfolding Q_hit_decomp
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> H.edges_of_walk (y # Q_hit_post)

goal (1 subgoal):
 1. (v, w) \<in> H.edges_of_walk (Q_hit_pre @ y # Q_hit_post)
[PROOF STEP]
by (metis UnCI walk_edges_decomp)
[PROOF STATE]
proof (state)
this:
(v, w) \<in> H.edges_of_walk Q_hit

goal (1 subgoal):
 1. (v, w) \<in> H.edges_of_walk (y # Q_hit_post) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(v, w) \<in> H.edges_of_walk Q_hit
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> H.edges_of_walk Q_hit

goal (1 subgoal):
 1. False
[PROOF STEP]
using *(2) v_w_in_B Q_hit(1)
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> H.edges_of_walk Q_hit
(v, w) \<notin> Q_edges
(v, w) \<in> B
Q_hit \<in> Q

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding Q_edges_def
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> H.edges_of_walk Q_hit
(v, w) \<notin> \<Union> (H.edges_of_walk ` Q) \<inter> B
(v, w) \<in> B
Q_hit \<in> Q

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(v, w) \<notin> H.edges_of_walk (y # Q_hit_post)

goal (1 subgoal):
 1. Q'_v_w_witness = Q_hit' \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
H.edges_of_walk Q'_v_w_witness = H.edges_of_walk (P_k_pre @ [y]) \<union> H.edges_of_walk (y # Q_hit_post)
(v, w) \<notin> H.edges_of_walk (P_k_pre @ [y])
(v, w) \<notin> H.edges_of_walk (y # Q_hit_post)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
H.edges_of_walk Q'_v_w_witness = H.edges_of_walk (P_k_pre @ [y]) \<union> H.edges_of_walk (y # Q_hit_post)
(v, w) \<notin> H.edges_of_walk (P_k_pre @ [y])
(v, w) \<notin> H.edges_of_walk (y # Q_hit_post)

goal (1 subgoal):
 1. False
[PROOF STEP]
using Q'_v_w_witness(2)
[PROOF STATE]
proof (prove)
using this:
H.edges_of_walk Q'_v_w_witness = H.edges_of_walk (P_k_pre @ [y]) \<union> H.edges_of_walk (y # Q_hit_post)
(v, w) \<notin> H.edges_of_walk (P_k_pre @ [y])
(v, w) \<notin> H.edges_of_walk (y # Q_hit_post)
(v, w) \<in> H.edges_of_walk Q'_v_w_witness

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Q'_v_w_witness \<noteq> Q_hit'

goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Q'_v_w_witness \<noteq> Q_hit'
[PROOF STEP]
have "Q'_v_w_witness \<in> Q"
[PROOF STATE]
proof (prove)
using this:
Q'_v_w_witness \<noteq> Q_hit'

goal (1 subgoal):
 1. Q'_v_w_witness \<in> Q
[PROOF STEP]
using Q'_v_w_witness(1)
[PROOF STATE]
proof (prove)
using this:
Q'_v_w_witness \<noteq> Q_hit'
Q'_v_w_witness \<in> Q'

goal (1 subgoal):
 1. Q'_v_w_witness \<in> Q
[PROOF STEP]
unfolding Q'_def
[PROOF STATE]
proof (prove)
using this:
Q'_v_w_witness \<noteq> Q_hit'
Q'_v_w_witness \<in> insert Q_hit' (Q - {Q_hit})

goal (1 subgoal):
 1. Q'_v_w_witness \<in> Q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Q'_v_w_witness \<in> Q

goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Q'_v_w_witness \<in> Q
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
Q'_v_w_witness \<in> Q

goal (1 subgoal):
 1. False
[PROOF STEP]
using *(2) v_w_in_B Q'_v_w_witness(2)
[PROOF STATE]
proof (prove)
using this:
Q'_v_w_witness \<in> Q
(v, w) \<notin> Q_edges
(v, w) \<in> B
(v, w) \<in> H.edges_of_walk Q'_v_w_witness

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding Q_edges_def
[PROOF STATE]
proof (prove)
using this:
Q'_v_w_witness \<in> Q
(v, w) \<notin> \<Union> (H.edges_of_walk ` Q) \<inter> B
(v, w) \<in> B
(v, w) \<in> H.edges_of_walk Q'_v_w_witness

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?v2, ?w2) \<in> Q'_edges; (?v2, ?w2) \<notin> Q_edges\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?v2, ?w2) \<in> Q'_edges; (?v2, ?w2) \<notin> Q_edges\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
have "\<exists>e \<in> Q_edges. e \<notin> Q'_edges"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>e\<in>Q_edges. e \<notin> Q'_edges
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>e\<in>Q_edges. e \<notin> Q'_edges
[PROOF STEP]
obtain v w where v_w: "(v,w) \<in> edges_of_walk (Q_hit_pre @ [y]) \<inter> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v w. (v, w) \<in> H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Q_hit_pre_edges
[PROOF STATE]
proof (prove)
using this:
H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B \<noteq> {}

goal (1 subgoal):
 1. (\<And>v w. (v, w) \<in> H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(v, w) \<in> H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B

goal (1 subgoal):
 1. \<exists>e\<in>Q_edges. e \<notin> Q'_edges
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(v, w) \<in> H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B
[PROOF STEP]
have v_w_in_Q_hit: "(v,w) \<in> edges_of_walk Q_hit \<inter> B"
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B

goal (1 subgoal):
 1. (v, w) \<in> H.edges_of_walk Q_hit \<inter> B
[PROOF STEP]
unfolding Q_hit_decomp
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B

goal (1 subgoal):
 1. (v, w) \<in> H.edges_of_walk (Q_hit_pre @ y # Q_hit_post) \<inter> B
[PROOF STEP]
by (metis Int_iff UnCI walk_edges_decomp)
[PROOF STATE]
proof (state)
this:
(v, w) \<in> H.edges_of_walk Q_hit \<inter> B

goal (1 subgoal):
 1. \<exists>e\<in>Q_edges. e \<notin> Q'_edges
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(v, w) \<in> H.edges_of_walk Q_hit \<inter> B
[PROOF STEP]
have "(v,w) \<in> Q_edges"
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> H.edges_of_walk Q_hit \<inter> B

goal (1 subgoal):
 1. (v, w) \<in> Q_edges
[PROOF STEP]
unfolding Q_edges_def
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> H.edges_of_walk Q_hit \<inter> B

goal (1 subgoal):
 1. (v, w) \<in> \<Union> (H.edges_of_walk ` Q) \<inter> B
[PROOF STEP]
using Q_hit(1)
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> H.edges_of_walk Q_hit \<inter> B
Q_hit \<in> Q

goal (1 subgoal):
 1. (v, w) \<in> \<Union> (H.edges_of_walk ` Q) \<inter> B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(v, w) \<in> Q_edges

goal (1 subgoal):
 1. \<exists>e\<in>Q_edges. e \<notin> Q'_edges
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(v, w) \<in> Q_edges

goal (1 subgoal):
 1. \<exists>e\<in>Q_edges. e \<notin> Q'_edges
[PROOF STEP]
have "(v,w) \<notin> Q'_edges"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, w) \<notin> Q'_edges
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (v, w) \<in> Q'_edges \<Longrightarrow> False
[PROOF STEP]
assume "(v,w) \<in> Q'_edges"
[PROOF STATE]
proof (state)
this:
(v, w) \<in> Q'_edges

goal (1 subgoal):
 1. (v, w) \<in> Q'_edges \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(v, w) \<in> Q'_edges
[PROOF STEP]
have "(v,w) \<in> edges_of_walk Q_hit'"
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> Q'_edges

goal (1 subgoal):
 1. (v, w) \<in> H.edges_of_walk Q_hit'
[PROOF STEP]
unfolding Q'_edges_def Q'_def
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> \<Union> (H.edges_of_walk ` insert Q_hit' (Q - {Q_hit})) \<inter> B

goal (1 subgoal):
 1. (v, w) \<in> H.edges_of_walk Q_hit'
[PROOF STEP]
using IntD1 v_w_in_Q_hit Q_hit_edges_disjoint
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> \<Union> (H.edges_of_walk ` insert Q_hit' (Q - {Q_hit})) \<inter> B
?c \<in> ?A \<inter> ?B \<Longrightarrow> ?c \<in> ?A
(v, w) \<in> H.edges_of_walk Q_hit \<inter> B
\<Union> (H.edges_of_walk ` (Q - {Q_hit})) \<inter> H.edges_of_walk Q_hit = {}

goal (1 subgoal):
 1. (v, w) \<in> H.edges_of_walk Q_hit'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(v, w) \<in> H.edges_of_walk Q_hit'

goal (1 subgoal):
 1. (v, w) \<in> Q'_edges \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(v, w) \<in> H.edges_of_walk Q_hit'
[PROOF STEP]
have "(v,w) \<in> edges_of_walk (y # Q_hit_post)"
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> H.edges_of_walk Q_hit'

goal (1 subgoal):
 1. (v, w) \<in> H.edges_of_walk (y # Q_hit_post)
[PROOF STEP]
unfolding Q_hit'_def
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> H.edges_of_walk (P_k_pre @ y # Q_hit_post)

goal (1 subgoal):
 1. (v, w) \<in> H.edges_of_walk (y # Q_hit_post)
[PROOF STEP]
using v_w P_k_pre_edges
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> H.edges_of_walk (P_k_pre @ y # Q_hit_post)
(v, w) \<in> H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B
H.edges_of_walk (P_k_pre @ [y]) \<inter> B = {}

goal (1 subgoal):
 1. (v, w) \<in> H.edges_of_walk (y # Q_hit_post)
[PROOF STEP]
by (metis (no_types, lifting) IntD2 UnE disjoint_iff_not_equal walk_edges_decomp)
[PROOF STATE]
proof (state)
this:
(v, w) \<in> H.edges_of_walk (y # Q_hit_post)

goal (1 subgoal):
 1. (v, w) \<in> Q'_edges \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(v, w) \<in> H.edges_of_walk (y # Q_hit_post)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> H.edges_of_walk (y # Q_hit_post)

goal (1 subgoal):
 1. False
[PROOF STEP]
using v_w Q_hit(1) Q.paths Q_hit_decomp
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> H.edges_of_walk (y # Q_hit_post)
(v, w) \<in> H.edges_of_walk (Q_hit_pre @ [y]) \<inter> B
Q_hit \<in> Q
?xs \<in> Q \<Longrightarrow> v0 \<leadsto>?xs\<leadsto>\<^bsub>H_x\<^esub> v1
Q_hit = Q_hit_pre @ y # Q_hit_post

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis DiffE Q.path_edges_remove_prefix IntD1 path_from_to_def)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(v, w) \<notin> Q'_edges

goal (1 subgoal):
 1. \<exists>e\<in>Q_edges. e \<notin> Q'_edges
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(v, w) \<in> Q_edges
(v, w) \<notin> Q'_edges
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> Q_edges
(v, w) \<notin> Q'_edges

goal (1 subgoal):
 1. \<exists>e\<in>Q_edges. e \<notin> Q'_edges
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>e\<in>Q_edges. e \<notin> Q'_edges

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>e\<in>Q_edges. e \<notin> Q'_edges

goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>e\<in>Q_edges. e \<notin> Q'_edges

goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
have "finite Q_edges"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite Q_edges
[PROOF STEP]
unfolding Q_edges_def B_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (\<Union> (H.edges_of_walk ` Q) \<inter> (E - \<Union> (H.edges_of_walk ` paths_with_new)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite Q_edges

goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite Q_edges

goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
have "finite Q'_edges"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite Q'_edges
[PROOF STEP]
unfolding Q'_edges_def B_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (\<Union> (H.edges_of_walk ` Q') \<inter> (E - \<Union> (H.edges_of_walk ` paths_with_new)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite Q'_edges

goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(?v2, ?w2) \<in> Q'_edges; (?v2, ?w2) \<notin> Q_edges\<rbrakk> \<Longrightarrow> False
\<exists>e\<in>Q_edges. e \<notin> Q'_edges
finite Q_edges
finite Q'_edges
[PROOF STEP]
have "card Q'_edges < card Q_edges"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?v2, ?w2) \<in> Q'_edges; (?v2, ?w2) \<notin> Q_edges\<rbrakk> \<Longrightarrow> False
\<exists>e\<in>Q_edges. e \<notin> Q'_edges
finite Q_edges
finite Q'_edges

goal (1 subgoal):
 1. card Q'_edges < card Q_edges
[PROOF STEP]
by (metis card_seteq not_le subrelI)
[PROOF STATE]
proof (state)
this:
card Q'_edges < card Q_edges

goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card Q'_edges < card Q_edges
[PROOF STEP]
have "card (\<Union>(edges_of_walk ` Q') \<inter> B) < card (\<Union>(edges_of_walk ` Q) \<inter> B)"
[PROOF STATE]
proof (prove)
using this:
card Q'_edges < card Q_edges

goal (1 subgoal):
 1. card (\<Union> (H.edges_of_walk ` Q') \<inter> B) < card (\<Union> (H.edges_of_walk ` Q) \<inter> B)
[PROOF STEP]
unfolding Q_edges_def Q'_edges_def
[PROOF STATE]
proof (prove)
using this:
card (\<Union> (H.edges_of_walk ` Q') \<inter> B) < card (\<Union> (H.edges_of_walk ` Q) \<inter> B)

goal (1 subgoal):
 1. card (\<Union> (H.edges_of_walk ` Q') \<inter> B) < card (\<Union> (H.edges_of_walk ` Q) \<inter> B)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card (\<Union> (H.edges_of_walk ` Q') \<inter> B) < card (\<Union> (H.edges_of_walk ` Q) \<inter> B)

goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (\<Union> (H.edges_of_walk ` Q') \<inter> B) < card (\<Union> (H.edges_of_walk ` Q) \<inter> B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (\<Union> (H.edges_of_walk ` Q') \<inter> B) < card (\<Union> (H.edges_of_walk ` Q) \<inter> B)

goal (1 subgoal):
 1. Q_weight Q' < Q_weight Q
[PROOF STEP]
unfolding Q_weight_def
[PROOF STATE]
proof (prove)
using this:
card (\<Union> (H.edges_of_walk ` Q') \<inter> B) < card (\<Union> (H.edges_of_walk ` Q) \<inter> B)

goal (1 subgoal):
 1. card (\<Union> (H.edges_of_walk ` Q') \<inter> B) < card (\<Union> (H.edges_of_walk ` Q) \<inter> B)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Q_weight Q' < Q_weight Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma DisjointPaths_Q': "DisjointPaths H_x v0 v1 Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DisjointPaths H_x v0 v1 Q'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. DisjointPaths H_x v0 v1 Q'
[PROOF STEP]
interpret Q_reduced: DisjointPaths H_x v0 v1 "Q - {Q_hit}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DisjointPaths H_x v0 v1 (Q - {Q_hit})
[PROOF STEP]
using Q.DisjointPaths_reduce[of "Q - {Q_hit}"]
[PROOF STATE]
proof (prove)
using this:
Q - {Q_hit} \<subseteq> Q \<Longrightarrow> DisjointPaths H_x v0 v1 (Q - {Q_hit})

goal (1 subgoal):
 1. DisjointPaths H_x v0 v1 (Q - {Q_hit})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. DisjointPaths H_x v0 v1 Q'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. DisjointPaths H_x v0 v1 Q'
[PROOF STEP]
fix xs v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. DisjointPaths H_x v0 v1 Q'
[PROOF STEP]
assume xs: "xs \<in> Q - {Q_hit}"
          and v: "v \<in> set xs" "v \<in> set Q_hit'" "v \<noteq> v0" "v \<noteq> v1"
[PROOF STATE]
proof (state)
this:
xs \<in> Q - {Q_hit}
v \<in> set xs
v \<in> set Q_hit'
v \<noteq> v0
v \<noteq> v1

goal (1 subgoal):
 1. DisjointPaths H_x v0 v1 Q'
[PROOF STEP]
have "v \<notin> set P_k_pre"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<notin> set P_k_pre
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<in> set P_k_pre \<Longrightarrow> False
[PROOF STEP]
assume "v \<in> set P_k_pre"
[PROOF STATE]
proof (state)
this:
v \<in> set P_k_pre

goal (1 subgoal):
 1. v \<in> set P_k_pre \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> set P_k_pre
[PROOF STEP]
have "\<not>hitting_Q_or_new_last v"
[PROOF STATE]
proof (prove)
using this:
v \<in> set P_k_pre

goal (1 subgoal):
 1. \<not> hitting_Q_or_new_last v
[PROOF STEP]
using y_min
[PROOF STATE]
proof (prove)
using this:
v \<in> set P_k_pre
?y' \<in> set P_k_pre \<Longrightarrow> \<not> hitting_Q_or_new_last ?y'

goal (1 subgoal):
 1. \<not> hitting_Q_or_new_last v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> hitting_Q_or_new_last v

goal (1 subgoal):
 1. v \<in> set P_k_pre \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> hitting_Q_or_new_last v

goal (1 subgoal):
 1. v \<in> set P_k_pre \<Longrightarrow> False
[PROOF STEP]
have "v \<noteq> new_last"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<noteq> new_last
[PROOF STEP]
using v(2) calculation hitting_Q_or_new_last_def v(3)
[PROOF STATE]
proof (prove)
using this:
v \<in> set Q_hit'
\<not> hitting_Q_or_new_last v
hitting_Q_or_new_last \<equiv> \<lambda>y. y \<noteq> v0 \<and> (y = new_last \<or> (\<exists>Q_hit\<in>Q. y \<in> set Q_hit))
v \<noteq> v0

goal (1 subgoal):
 1. v \<noteq> new_last
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<noteq> new_last

goal (1 subgoal):
 1. v \<in> set P_k_pre \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> hitting_Q_or_new_last v
v \<noteq> new_last
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> hitting_Q_or_new_last v
v \<noteq> new_last

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding hitting_Q_or_new_last_def
[PROOF STATE]
proof (prove)
using this:
\<not> (v \<noteq> v0 \<and> (v = new_last \<or> (\<exists>Q_hit\<in>Q. v \<in> set Q_hit)))
v \<noteq> new_last

goal (1 subgoal):
 1. False
[PROOF STEP]
using v(1,3) xs
[PROOF STATE]
proof (prove)
using this:
\<not> (v \<noteq> v0 \<and> (v = new_last \<or> (\<exists>Q_hit\<in>Q. v \<in> set Q_hit)))
v \<noteq> new_last
v \<in> set xs
v \<noteq> v0
xs \<in> Q - {Q_hit}

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v \<notin> set P_k_pre

goal (1 subgoal):
 1. DisjointPaths H_x v0 v1 Q'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v \<notin> set P_k_pre

goal (1 subgoal):
 1. DisjointPaths H_x v0 v1 Q'
[PROOF STEP]
have "v \<noteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<noteq> y
[PROOF STEP]
by (metis DiffE Q.paths_disjoint Q_hit y_neq_v0 y_neq_v1 insert_iff v(1) xs)
[PROOF STATE]
proof (state)
this:
v \<noteq> y

goal (1 subgoal):
 1. DisjointPaths H_x v0 v1 Q'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v \<noteq> y

goal (1 subgoal):
 1. DisjointPaths H_x v0 v1 Q'
[PROOF STEP]
have "v \<notin> set Q_hit_post"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<notin> set Q_hit_post
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<in> set Q_hit_post \<Longrightarrow> False
[PROOF STEP]
assume "v \<in> set Q_hit_post"
[PROOF STATE]
proof (state)
this:
v \<in> set Q_hit_post

goal (1 subgoal):
 1. v \<in> set Q_hit_post \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> set Q_hit_post
[PROOF STEP]
have "v \<in> set Q_hit"
[PROOF STATE]
proof (prove)
using this:
v \<in> set Q_hit_post

goal (1 subgoal):
 1. v \<in> set Q_hit
[PROOF STEP]
unfolding Q_hit_decomp
[PROOF STATE]
proof (prove)
using this:
v \<in> set Q_hit_post

goal (1 subgoal):
 1. v \<in> set (Q_hit_pre @ y # Q_hit_post)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<in> set Q_hit

goal (1 subgoal):
 1. v \<in> set Q_hit_post \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> set Q_hit
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
v \<in> set Q_hit

goal (1 subgoal):
 1. False
[PROOF STEP]
using Q.paths_disjoint[of Q_hit xs] xs Q_hit(1) v
[PROOF STATE]
proof (prove)
using this:
v \<in> set Q_hit
\<lbrakk>Q_hit \<in> Q; xs \<in> Q; Q_hit \<noteq> xs; ?v \<in> set Q_hit; ?v \<in> set xs\<rbrakk> \<Longrightarrow> ?v = v0 \<or> ?v = v1
xs \<in> Q - {Q_hit}
Q_hit \<in> Q
v \<in> set xs
v \<in> set Q_hit'
v \<noteq> v0
v \<noteq> v1

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v \<notin> set Q_hit_post

goal (1 subgoal):
 1. DisjointPaths H_x v0 v1 Q'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v \<notin> set P_k_pre
v \<noteq> y
v \<notin> set Q_hit_post
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
v \<notin> set P_k_pre
v \<noteq> y
v \<notin> set Q_hit_post

goal (1 subgoal):
 1. False
[PROOF STEP]
using v(2)
[PROOF STATE]
proof (prove)
using this:
v \<notin> set P_k_pre
v \<noteq> y
v \<notin> set Q_hit_post
v \<in> set Q_hit'

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding Q_hit'_def
[PROOF STATE]
proof (prove)
using this:
v \<notin> set P_k_pre
v \<noteq> y
v \<notin> set Q_hit_post
v \<in> set (P_k_pre @ y # Q_hit_post)

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. DisjointPaths H_x v0 v1 Q'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?xs2 \<in> Q - {Q_hit}; ?v2 \<in> set ?xs2; ?v2 \<in> set Q_hit'; ?v2 \<noteq> v0; ?v2 \<noteq> v1\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. DisjointPaths H_x v0 v1 Q'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?xs2 \<in> Q - {Q_hit}; ?v2 \<in> set ?xs2; ?v2 \<in> set Q_hit'; ?v2 \<noteq> v0; ?v2 \<noteq> v1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?xs2 \<in> Q - {Q_hit}; ?v2 \<in> set ?xs2; ?v2 \<in> set Q_hit'; ?v2 \<noteq> v0; ?v2 \<noteq> v1\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. DisjointPaths H_x v0 v1 Q'
[PROOF STEP]
using Q_reduced.DisjointPaths_extend Q_hit'_v0_v1_H_x
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?xs2 \<in> Q - {Q_hit}; ?v2 \<in> set ?xs2; ?v2 \<in> set Q_hit'; ?v2 \<noteq> v0; ?v2 \<noteq> v1\<rbrakk> \<Longrightarrow> False
\<lbrakk>v0 \<leadsto>?P\<leadsto>\<^bsub>H_x\<^esub> v1; \<And>xs v. \<lbrakk>xs \<in> Q - {Q_hit}; xs \<noteq> ?P; v \<in> set xs; v \<in> set ?P\<rbrakk> \<Longrightarrow> v = v0 \<or> v = v1\<rbrakk> \<Longrightarrow> DisjointPaths H_x v0 v1 (insert ?P (Q - {Q_hit}))
v0 \<leadsto>Q_hit'\<leadsto>\<^bsub>H_x\<^esub> v1

goal (1 subgoal):
 1. DisjointPaths H_x v0 v1 Q'
[PROOF STEP]
unfolding Q'_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?xs2 \<in> Q - {Q_hit}; ?v2 \<in> set ?xs2; ?v2 \<in> set Q_hit'; ?v2 \<noteq> v0; ?v2 \<noteq> v1\<rbrakk> \<Longrightarrow> False
\<lbrakk>v0 \<leadsto>?P\<leadsto>\<^bsub>H_x\<^esub> v1; \<And>xs v. \<lbrakk>xs \<in> Q - {Q_hit}; xs \<noteq> ?P; v \<in> set xs; v \<in> set ?P\<rbrakk> \<Longrightarrow> v = v0 \<or> v = v1\<rbrakk> \<Longrightarrow> DisjointPaths H_x v0 v1 (insert ?P (Q - {Q_hit}))
v0 \<leadsto>Q_hit'\<leadsto>\<^bsub>H_x\<^esub> v1

goal (1 subgoal):
 1. DisjointPaths H_x v0 v1 (insert Q_hit' (Q - {Q_hit}))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
DisjointPaths H_x v0 v1 Q'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_Q': "card Q' = sep_size"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card Q' = sep_size
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card Q' = sep_size
[PROOF STEP]
have "Suc (card (Q - {Q_hit})) = card Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (card (Q - {Q_hit})) = card Q
[PROOF STEP]
using Q_hit(1) Q.finite_paths
[PROOF STATE]
proof (prove)
using this:
Q_hit \<in> Q
finite Q

goal (1 subgoal):
 1. Suc (card (Q - {Q_hit})) = card Q
[PROOF STEP]
by (meson card_Suc_Diff1)
[PROOF STATE]
proof (state)
this:
Suc (card (Q - {Q_hit})) = card Q

goal (1 subgoal):
 1. card Q' = sep_size
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Suc (card (Q - {Q_hit})) = card Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Suc (card (Q - {Q_hit})) = card Q

goal (1 subgoal):
 1. card Q' = sep_size
[PROOF STEP]
using Q(2) Q.finite_paths Q_hit'_notin_Q_minus_Q_hit
[PROOF STATE]
proof (prove)
using this:
Suc (card (Q - {Q_hit})) = card Q
card Q = sep_size
finite Q
Q_hit' \<notin> Q - {Q_hit}

goal (1 subgoal):
 1. card Q' = sep_size
[PROOF STEP]
unfolding Q'_def
[PROOF STATE]
proof (prove)
using this:
Suc (card (Q - {Q_hit})) = card Q
card Q = sep_size
finite Q
Q_hit' \<notin> Q - {Q_hit}

goal (1 subgoal):
 1. card (insert Q_hit' (Q - {Q_hit})) = sep_size
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card Q' = sep_size

goal:
No subgoals!
[PROOF STEP]
qed