[STATEMENT]
lemma proper_interval_Compl_set_aux:
  assumes fin: "finite (UNIV :: 'a set)"
  and xs: "sorted xs" "distinct xs"
  and ys: "sorted ys" "distinct ys"
  shows "proper_interval_Compl_set_aux None xs ys \<longleftrightarrow> (\<exists>A. - set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_interval_Compl_set_aux None xs ys = (\<exists>A. - set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proper_interval_Compl_set_aux None xs ys = (\<exists>A. - set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)
[PROOF STEP]
note [simp] = finite_subset[OF subset_UNIV fin]
[PROOF STATE]
proof (state)
this:
finite ?A

goal (1 subgoal):
 1. proper_interval_Compl_set_aux None xs ys = (\<exists>A. - set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)
[PROOF STEP]
define above where "above = case_option UNIV (Collect \<circ> less)"
[PROOF STATE]
proof (state)
this:
above = case_option UNIV (Collect \<circ> (<))

goal (1 subgoal):
 1. proper_interval_Compl_set_aux None xs ys = (\<exists>A. - set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)
[PROOF STEP]
have above_simps [simp]: "above None = UNIV" "\<And>x. above (Some x) = {y. x < y}"
    and above_upclosed: "\<And>x y ao. \<lbrakk> x \<in> above ao; x < y \<rbrakk> \<Longrightarrow> y \<in> above ao"
    and proper_interval_Some2: "\<And>x ao. proper_interval ao (Some x) \<longleftrightarrow> (\<exists>z\<in>above ao. z < x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (above None = UNIV &&& (\<And>x. above (Some x) = {y. x < y})) &&& (\<And>x y ao. \<lbrakk>x \<in> above ao; x < y\<rbrakk> \<Longrightarrow> y \<in> above ao) &&& (\<And>x ao. proper_interval ao (Some x) = (\<exists>z\<in>above ao. z < x))
[PROOF STEP]
by(simp_all add: proper_interval_simps above_def split: option.splits)
[PROOF STATE]
proof (state)
this:
above None = UNIV
above (Some ?x) = {y. ?x < y}
\<lbrakk>?x \<in> above ?ao; ?x < ?y\<rbrakk> \<Longrightarrow> ?y \<in> above ?ao
proper_interval ?ao (Some ?x) = (\<exists>z\<in>above ?ao. z < ?x)

goal (1 subgoal):
 1. proper_interval_Compl_set_aux None xs ys = (\<exists>A. - set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
above None = UNIV
above (Some ?x) = {y. ?x < y}
\<lbrakk>?x \<in> above ?ao; ?x < ?y\<rbrakk> \<Longrightarrow> ?y \<in> above ?ao
proper_interval ?ao (Some ?x) = (\<exists>z\<in>above ?ao. z < ?x)

goal (1 subgoal):
 1. proper_interval_Compl_set_aux None xs ys = (\<exists>A. - set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)
[PROOF STEP]
fix ao n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proper_interval_Compl_set_aux None xs ys = (\<exists>A. - set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)
[PROOF STEP]
assume "set xs \<subseteq> above ao" "set ys \<subseteq> above ao"
[PROOF STATE]
proof (state)
this:
set xs \<subseteq> above ao
set ys \<subseteq> above ao

goal (1 subgoal):
 1. proper_interval_Compl_set_aux None xs ys = (\<exists>A. - set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)
[PROOF STEP]
from xs \<open>set xs \<subseteq> above ao\<close> ys \<open>set ys \<subseteq> above ao\<close>
[PROOF STATE]
proof (chain)
picking this:
sorted xs
distinct xs
set xs \<subseteq> above ao
sorted ys
distinct ys
set ys \<subseteq> above ao
[PROOF STEP]
have "proper_interval_Compl_set_aux ao xs ys \<longleftrightarrow>
          (\<exists>A. - set xs \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set ys \<inter> above ao)"
[PROOF STATE]
proof (prove)
using this:
sorted xs
distinct xs
set xs \<subseteq> above ao
sorted ys
distinct ys
set ys \<subseteq> above ao

goal (1 subgoal):
 1. proper_interval_Compl_set_aux ao xs ys = (\<exists>A. - set xs \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set ys \<inter> above ao)
[PROOF STEP]
proof(induction ao xs ys rule: proper_interval_Compl_set_aux.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<And>ao uv_. \<lbrakk>sorted []; distinct []; set [] \<subseteq> above ao; sorted uv_; distinct uv_; set uv_ \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao [] uv_ = (\<exists>A. - set [] \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set uv_ \<inter> above ao)
 3. \<And>ao uu_. \<lbrakk>sorted uu_; distinct uu_; set uu_ \<subseteq> above ao; sorted []; distinct []; set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao uu_ [] = (\<exists>A. - set uu_ \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set [] \<inter> above ao)
[PROOF STEP]
case ("2_1" ao ys)
[PROOF STATE]
proof (state)
this:
sorted []
distinct []
set [] \<subseteq> above ao
sorted ys
distinct ys
set ys \<subseteq> above ao

goal (3 subgoals):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<And>ao uv_. \<lbrakk>sorted []; distinct []; set [] \<subseteq> above ao; sorted uv_; distinct uv_; set uv_ \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao [] uv_ = (\<exists>A. - set [] \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set uv_ \<inter> above ao)
 3. \<And>ao uu_. \<lbrakk>sorted uu_; distinct uu_; set uu_ \<subseteq> above ao; sorted []; distinct []; set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao uu_ [] = (\<exists>A. - set uu_ \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set [] \<inter> above ao)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
sorted []
distinct []
set [] \<subseteq> above ao
sorted ys
distinct ys
set ys \<subseteq> above ao

goal (3 subgoals):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<And>ao uv_. \<lbrakk>sorted []; distinct []; set [] \<subseteq> above ao; sorted uv_; distinct uv_; set uv_ \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao [] uv_ = (\<exists>A. - set [] \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set uv_ \<inter> above ao)
 3. \<And>ao uu_. \<lbrakk>sorted uu_; distinct uu_; set uu_ \<subseteq> above ao; sorted []; distinct []; set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao uu_ [] = (\<exists>A. - set uu_ \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set [] \<inter> above ao)
[PROOF STEP]
fix A
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<And>ao uv_. \<lbrakk>sorted []; distinct []; set [] \<subseteq> above ao; sorted uv_; distinct uv_; set uv_ \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao [] uv_ = (\<exists>A. - set [] \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set uv_ \<inter> above ao)
 3. \<And>ao uu_. \<lbrakk>sorted uu_; distinct uu_; set uu_ \<subseteq> above ao; sorted []; distinct []; set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao uu_ [] = (\<exists>A. - set uu_ \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set [] \<inter> above ao)
[PROOF STEP]
assume "above ao \<sqsubset>' A \<inter> above ao"
[PROOF STATE]
proof (state)
this:
above ao \<sqsubset>' A \<inter> above ao

goal (3 subgoals):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<And>ao uv_. \<lbrakk>sorted []; distinct []; set [] \<subseteq> above ao; sorted uv_; distinct uv_; set uv_ \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao [] uv_ = (\<exists>A. - set [] \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set uv_ \<inter> above ao)
 3. \<And>ao uu_. \<lbrakk>sorted uu_; distinct uu_; set uu_ \<subseteq> above ao; sorted []; distinct []; set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao uu_ [] = (\<exists>A. - set uu_ \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set [] \<inter> above ao)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
above ao \<sqsubset>' A \<inter> above ao

goal (3 subgoals):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<And>ao uv_. \<lbrakk>sorted []; distinct []; set [] \<subseteq> above ao; sorted uv_; distinct uv_; set uv_ \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao [] uv_ = (\<exists>A. - set [] \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set uv_ \<inter> above ao)
 3. \<And>ao uu_. \<lbrakk>sorted uu_; distinct uu_; set uu_ \<subseteq> above ao; sorted []; distinct []; set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao uu_ [] = (\<exists>A. - set uu_ \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set [] \<inter> above ao)
[PROOF STEP]
have "\<dots> \<subseteq> above ao"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> above ao \<subseteq> above ao
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A \<inter> above ao \<subseteq> above ao

goal (3 subgoals):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<And>ao uv_. \<lbrakk>sorted []; distinct []; set [] \<subseteq> above ao; sorted uv_; distinct uv_; set uv_ \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao [] uv_ = (\<exists>A. - set [] \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set uv_ \<inter> above ao)
 3. \<And>ao uu_. \<lbrakk>sorted uu_; distinct uu_; set uu_ \<subseteq> above ao; sorted []; distinct []; set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao uu_ [] = (\<exists>A. - set uu_ \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set [] \<inter> above ao)
[PROOF STEP]
hence "A \<inter> above ao \<sqsubseteq>' above ao"
[PROOF STATE]
proof (prove)
using this:
A \<inter> above ao \<subseteq> above ao

goal (1 subgoal):
 1. A \<inter> above ao \<sqsubseteq>' above ao
[PROOF STEP]
by(auto intro: subset_finite_imp_set_less_eq_aux)
[PROOF STATE]
proof (state)
this:
A \<inter> above ao \<sqsubseteq>' above ao

goal (3 subgoals):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<And>ao uv_. \<lbrakk>sorted []; distinct []; set [] \<subseteq> above ao; sorted uv_; distinct uv_; set uv_ \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao [] uv_ = (\<exists>A. - set [] \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set uv_ \<inter> above ao)
 3. \<And>ao uu_. \<lbrakk>sorted uu_; distinct uu_; set uu_ \<subseteq> above ao; sorted []; distinct []; set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao uu_ [] = (\<exists>A. - set uu_ \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set [] \<inter> above ao)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
above ao \<sqsubset>' above ao
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
above ao \<sqsubset>' above ao

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

goal (3 subgoals):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<And>ao uv_. \<lbrakk>sorted []; distinct []; set [] \<subseteq> above ao; sorted uv_; distinct uv_; set uv_ \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao [] uv_ = (\<exists>A. - set [] \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set uv_ \<inter> above ao)
 3. \<And>ao uu_. \<lbrakk>sorted uu_; distinct uu_; set uu_ \<subseteq> above ao; sorted []; distinct []; set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao uu_ [] = (\<exists>A. - set uu_ \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set [] \<inter> above ao)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
above ao \<sqsubset>' ?A2 \<inter> above ao \<Longrightarrow> False

goal (3 subgoals):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<And>ao uv_. \<lbrakk>sorted []; distinct []; set [] \<subseteq> above ao; sorted uv_; distinct uv_; set uv_ \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao [] uv_ = (\<exists>A. - set [] \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set uv_ \<inter> above ao)
 3. \<And>ao uu_. \<lbrakk>sorted uu_; distinct uu_; set uu_ \<subseteq> above ao; sorted []; distinct []; set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao uu_ [] = (\<exists>A. - set uu_ \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set [] \<inter> above ao)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
above ao \<sqsubset>' ?A2 \<inter> above ao \<Longrightarrow> False

goal (1 subgoal):
 1. proper_interval_Compl_set_aux ao [] ys = (\<exists>A. - set [] \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set ys \<inter> above ao)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proper_interval_Compl_set_aux ao [] ys = (\<exists>A. - set [] \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set ys \<inter> above ao)

goal (2 subgoals):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<And>ao uu_. \<lbrakk>sorted uu_; distinct uu_; set uu_ \<subseteq> above ao; sorted []; distinct []; set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao uu_ [] = (\<exists>A. - set uu_ \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set [] \<inter> above ao)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<And>ao uu_. \<lbrakk>sorted uu_; distinct uu_; set uu_ \<subseteq> above ao; sorted []; distinct []; set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao uu_ [] = (\<exists>A. - set uu_ \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set [] \<inter> above ao)
[PROOF STEP]
case ("2_2" ao xs)
[PROOF STATE]
proof (state)
this:
sorted xs
distinct xs
set xs \<subseteq> above ao
sorted []
distinct []
set [] \<subseteq> above ao

goal (2 subgoals):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<And>ao uu_. \<lbrakk>sorted uu_; distinct uu_; set uu_ \<subseteq> above ao; sorted []; distinct []; set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao uu_ [] = (\<exists>A. - set uu_ \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set [] \<inter> above ao)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
sorted xs
distinct xs
set xs \<subseteq> above ao
sorted []
distinct []
set [] \<subseteq> above ao

goal (1 subgoal):
 1. proper_interval_Compl_set_aux ao xs [] = (\<exists>A. - set xs \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set [] \<inter> above ao)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proper_interval_Compl_set_aux ao xs [] = (\<exists>A. - set xs \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set [] \<inter> above ao)

goal (1 subgoal):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
case (1 ao x xs y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x))
\<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y))
sorted (x # xs)
distinct (x # xs)
set (x # xs) \<subseteq> above ao
sorted (y # ys)
distinct (y # ys)
set (y # ys) \<subseteq> above ao

goal (1 subgoal):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
note xxs = \<open>sorted (x # xs)\<close> \<open>distinct (x # xs)\<close>
[PROOF STATE]
proof (state)
this:
sorted (x # xs)
distinct (x # xs)

goal (1 subgoal):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
hence xs: "sorted xs" "distinct xs" and x_Min: "\<forall>x' \<in> set xs. x < x'"
[PROOF STATE]
proof (prove)
using this:
sorted (x # xs)
distinct (x # xs)

goal (1 subgoal):
 1. (sorted xs &&& distinct xs) &&& \<forall>x'\<in>set xs. x < x'
[PROOF STEP]
by(auto simp add: less_le)
[PROOF STATE]
proof (state)
this:
sorted xs
distinct xs
\<forall>x'\<in>set xs. x < x'

goal (1 subgoal):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
note yys = \<open>sorted (y # ys)\<close> \<open>distinct (y # ys)\<close>
[PROOF STATE]
proof (state)
this:
sorted (y # ys)
distinct (y # ys)

goal (1 subgoal):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
hence ys: "sorted ys" "distinct ys" and y_Min: "\<forall>y'\<in>set ys. y < y'"
[PROOF STATE]
proof (prove)
using this:
sorted (y # ys)
distinct (y # ys)

goal (1 subgoal):
 1. (sorted ys &&& distinct ys) &&& \<forall>y'\<in>set ys. y < y'
[PROOF STEP]
by(auto simp add: less_le)
[PROOF STATE]
proof (state)
this:
sorted ys
distinct ys
\<forall>y'\<in>set ys. y < y'

goal (1 subgoal):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
note xxs_above = \<open>set (x # xs) \<subseteq> above ao\<close>
[PROOF STATE]
proof (state)
this:
set (x # xs) \<subseteq> above ao

goal (1 subgoal):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
note yys_above = \<open>set (y # ys) \<subseteq> above ao\<close>
[PROOF STATE]
proof (state)
this:
set (y # ys) \<subseteq> above ao

goal (1 subgoal):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; set xs \<subseteq> above (Some x); sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above (Some y); sorted ys; distinct ys; set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); set (x # xs) \<subseteq> above ao; sorted (y # ys); distinct (y # ys); set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
proof(cases "x < y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x < y \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<not> x < y \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x < y

goal (2 subgoals):
 1. x < y \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<not> x < y \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
have "\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys) \<longleftrightarrow>
              (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)"
          (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
proof(cases "proper_interval ao (Some x)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<not> proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
proper_interval ao (Some x)

goal (2 subgoals):
 1. proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<not> proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
proper_interval ao (Some x)
[PROOF STEP]
obtain z where z: "z < x" "z \<in> above ao"
[PROOF STATE]
proof (prove)
using this:
proper_interval ao (Some x)

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z < x; z \<in> above ao\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: proper_interval_Some2)
[PROOF STATE]
proof (state)
this:
z < x
z \<in> above ao

goal (2 subgoals):
 1. proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<not> proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
hence nempty: "above ao \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
z < x
z \<in> above ao

goal (1 subgoal):
 1. above ao \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
above ao \<noteq> {}

goal (2 subgoals):
 1. proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<not> proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
with z
[PROOF STATE]
proof (chain)
picking this:
z < x
z \<in> above ao
above ao \<noteq> {}
[PROOF STEP]
have "Min (above ao) \<le> z"
[PROOF STATE]
proof (prove)
using this:
z < x
z \<in> above ao
above ao \<noteq> {}

goal (1 subgoal):
 1. Min (above ao) \<le> z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Min (above ao) \<le> z

goal (2 subgoals):
 1. proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<not> proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
hence "Min (above ao) < x"
[PROOF STATE]
proof (prove)
using this:
Min (above ao) \<le> z

goal (1 subgoal):
 1. Min (above ao) < x
[PROOF STEP]
using \<open>z < x\<close>
[PROOF STATE]
proof (prove)
using this:
Min (above ao) \<le> z
z < x

goal (1 subgoal):
 1. Min (above ao) < x
[PROOF STEP]
by(rule le_less_trans)
[PROOF STATE]
proof (state)
this:
Min (above ao) < x

goal (2 subgoals):
 1. proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<not> proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
hence "set (y # ys) \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao"
[PROOF STATE]
proof (prove)
using this:
Min (above ao) < x

goal (1 subgoal):
 1. set (y # ys) \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao
[PROOF STEP]
using y_Min x_Min z \<open>x < y\<close>
[PROOF STATE]
proof (prove)
using this:
Min (above ao) < x
\<forall>y'\<in>set ys. y < y'
\<forall>x'\<in>set xs. x < x'
z < x
z \<in> above ao
x < y

goal (1 subgoal):
 1. set (y # ys) \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao
[PROOF STEP]
by(fastforce simp add: set_less_aux_def nempty intro!: Min_eqI bexI[where x="Min (above ao)"])
[PROOF STATE]
proof (state)
this:
set (y # ys) \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao

goal (2 subgoals):
 1. proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<not> proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
set (y # ys) \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao

goal (1 subgoal):
 1. (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
set (y # ys) \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao
proper_interval ao (Some x)

goal (1 subgoal):
 1. (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
by(auto dest: set_less_aux_trans set_less_aux_antisym)
[PROOF STATE]
proof (state)
this:
(\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> proper_interval ao (Some x)

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
hence above_eq: "above ao = insert x (above (Some x))"
[PROOF STATE]
proof (prove)
using this:
\<not> proper_interval ao (Some x)

goal (1 subgoal):
 1. above ao = insert x (above (Some x))
[PROOF STEP]
using xxs_above
[PROOF STATE]
proof (prove)
using this:
\<not> proper_interval ao (Some x)
set (x # xs) \<subseteq> above ao

goal (1 subgoal):
 1. above ao = insert x (above (Some x))
[PROOF STEP]
by(auto simp add: proper_interval_Some2 intro: above_upclosed)
[PROOF STATE]
proof (state)
this:
above ao = insert x (above (Some x))

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
from x_Min
[PROOF STATE]
proof (chain)
picking this:
\<forall>x'\<in>set xs. x < x'
[PROOF STEP]
have xs_above: "set xs \<subseteq> above (Some x)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x'\<in>set xs. x < x'

goal (1 subgoal):
 1. set xs \<subseteq> above (Some x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set xs \<subseteq> above (Some x)

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
from \<open>x < y\<close> y_Min
[PROOF STATE]
proof (chain)
picking this:
x < y
\<forall>y'\<in>set ys. y < y'
[PROOF STEP]
have ys_above: "set (y # ys) \<subseteq> above (Some x)"
[PROOF STATE]
proof (prove)
using this:
x < y
\<forall>y'\<in>set ys. y < y'

goal (1 subgoal):
 1. set (y # ys) \<subseteq> above (Some x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (y # ys) \<subseteq> above (Some x)

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
have eq_xs: "- set xs \<inter> above (Some x) = - set (x # xs) \<inter> above ao"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - set xs \<inter> above (Some x) = - set (x # xs) \<inter> above ao
[PROOF STEP]
using above_eq
[PROOF STATE]
proof (prove)
using this:
above ao = insert x (above (Some x))

goal (1 subgoal):
 1. - set xs \<inter> above (Some x) = - set (x # xs) \<inter> above ao
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- set xs \<inter> above (Some x) = - set (x # xs) \<inter> above ao

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
have eq_ys: "set (y # ys) \<inter> above (Some x) = set (y # ys) \<inter> above ao"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (y # ys) \<inter> above (Some x) = set (y # ys) \<inter> above ao
[PROOF STEP]
using y_Min \<open>x < y\<close> xxs_above
[PROOF STATE]
proof (prove)
using this:
\<forall>y'\<in>set ys. y < y'
x < y
set (x # xs) \<subseteq> above ao

goal (1 subgoal):
 1. set (y # ys) \<inter> above (Some x) = set (y # ys) \<inter> above ao
[PROOF STEP]
by(auto intro: above_upclosed)
[PROOF STATE]
proof (state)
this:
set (y # ys) \<inter> above (Some x) = set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
from \<open>x < y\<close> xs xs_above yys ys_above
[PROOF STATE]
proof (chain)
picking this:
x < y
sorted xs
distinct xs
set xs \<subseteq> above (Some x)
sorted (y # ys)
distinct (y # ys)
set (y # ys) \<subseteq> above (Some x)
[PROOF STEP]
have "proper_interval_Compl_set_aux (Some x) xs (y # ys) \<longleftrightarrow>
               (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and>
                    A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x))"
[PROOF STATE]
proof (prove)
using this:
x < y
sorted xs
distinct xs
set xs \<subseteq> above (Some x)
sorted (y # ys)
distinct (y # ys)
set (y # ys) \<subseteq> above (Some x)

goal (1 subgoal):
 1. proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x))
[PROOF STEP]
by(rule "1.IH")
[PROOF STATE]
proof (state)
this:
proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x))

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x))

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
have "\<dots> \<longleftrightarrow> ?rhs" (is "?lhs \<longleftrightarrow> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x) \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)

goal (2 subgoals):
 1. \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x) \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)
[PROOF STEP]
obtain A where "- set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x)"
              and "A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)"
[PROOF STATE]
proof (prove)
using this:
\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>- set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x); A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
- set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x)
A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)

goal (2 subgoals):
 1. \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x) \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
- set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x)
A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)

goal (2 subgoals):
 1. \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x) \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)
[PROOF STEP]
have "A \<inter> above (Some x) = (A - {x}) \<inter> above ao"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> above (Some x) = (A - {x}) \<inter> above ao
[PROOF STEP]
using above_eq
[PROOF STATE]
proof (prove)
using this:
above ao = insert x (above (Some x))

goal (1 subgoal):
 1. A \<inter> above (Some x) = (A - {x}) \<inter> above ao
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<inter> above (Some x) = (A - {x}) \<inter> above ao

goal (2 subgoals):
 1. \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x) \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
- set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x)
A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)
A \<inter> above (Some x) = (A - {x}) \<inter> above ao
[PROOF STEP]
have "- set (x # xs) \<inter> above ao \<sqsubset>' (A - {x}) \<inter> above ao"
              and "(A - {x}) \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao"
[PROOF STATE]
proof (prove)
using this:
- set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x)
A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)
A \<inter> above (Some x) = (A - {x}) \<inter> above ao

goal (1 subgoal):
 1. - set (x # xs) \<inter> above ao \<sqsubset>' (A - {x}) \<inter> above ao &&& (A - {x}) \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
using eq_xs eq_ys
[PROOF STATE]
proof (prove)
using this:
- set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x)
A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)
A \<inter> above (Some x) = (A - {x}) \<inter> above ao
- set xs \<inter> above (Some x) = - set (x # xs) \<inter> above ao
set (y # ys) \<inter> above (Some x) = set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. - set (x # xs) \<inter> above ao \<sqsubset>' (A - {x}) \<inter> above ao &&& (A - {x}) \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
- set (x # xs) \<inter> above ao \<sqsubset>' (A - {x}) \<inter> above ao
(A - {x}) \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (2 subgoals):
 1. \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x) \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)
[PROOF STEP]
thus ?rhs
[PROOF STATE]
proof (prove)
using this:
- set (x # xs) \<inter> above ao \<sqsubset>' (A - {x}) \<inter> above ao
(A - {x}) \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
obtain A where "- set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao"
              and A_less: "A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao"
[PROOF STATE]
proof (prove)
using this:
\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>- set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao; A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
- set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao
A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
- set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao
A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)
[PROOF STEP]
have "x \<notin> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> False
[PROOF STEP]
assume "x \<in> A"
[PROOF STATE]
proof (state)
this:
x \<in> A

goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> False
[PROOF STEP]
hence "set (y # ys) \<inter> above ao \<sqsubset>' A \<inter> above ao"
[PROOF STATE]
proof (prove)
using this:
x \<in> A

goal (1 subgoal):
 1. set (y # ys) \<inter> above ao \<sqsubset>' A \<inter> above ao
[PROOF STEP]
using y_Min \<open>x < y\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> A
\<forall>y'\<in>set ys. y < y'
x < y

goal (1 subgoal):
 1. set (y # ys) \<inter> above ao \<sqsubset>' A \<inter> above ao
[PROOF STEP]
by(auto simp add: above_eq set_less_aux_def intro!: bexI[where x=x])
[PROOF STATE]
proof (state)
this:
set (y # ys) \<inter> above ao \<sqsubset>' A \<inter> above ao

goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> False
[PROOF STEP]
with A_less
[PROOF STATE]
proof (chain)
picking this:
A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
set (y # ys) \<inter> above ao \<sqsubset>' A \<inter> above ao
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
set (y # ys) \<inter> above ao \<sqsubset>' A \<inter> above ao

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

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

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)
[PROOF STEP]
hence "A \<inter> above ao = A \<inter> above (Some x)"
[PROOF STATE]
proof (prove)
using this:
x \<notin> A

goal (1 subgoal):
 1. A \<inter> above ao = A \<inter> above (Some x)
[PROOF STEP]
using above_eq
[PROOF STATE]
proof (prove)
using this:
x \<notin> A
above ao = insert x (above (Some x))

goal (1 subgoal):
 1. A \<inter> above ao = A \<inter> above (Some x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<inter> above ao = A \<inter> above (Some x)

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
- set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao
A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
A \<inter> above ao = A \<inter> above (Some x)
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
- set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao
A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
A \<inter> above ao = A \<inter> above (Some x)

goal (1 subgoal):
 1. \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)
[PROOF STEP]
using eq_xs eq_ys
[PROOF STATE]
proof (prove)
using this:
- set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao
A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
A \<inter> above ao = A \<inter> above (Some x)
- set xs \<inter> above (Some x) = - set (x # xs) \<inter> above ao
set (y # ys) \<inter> above (Some x) = set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>A. - set xs \<inter> above (Some x) \<sqsubset>' A \<inter> above (Some x) \<and> A \<inter> above (Some x) \<sqsubset>' set (y # ys) \<inter> above (Some x)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)

goal (1 subgoal):
 1. (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
proper_interval_Compl_set_aux (Some x) xs (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
\<not> proper_interval ao (Some x)

goal (1 subgoal):
 1. (\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)

goal (2 subgoals):
 1. x < y \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<not> x < y \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)

goal (1 subgoal):
 1. proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
(\<not> proper_interval ao (Some x) \<and> proper_interval_Compl_set_aux (Some x) xs (y # ys)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
x < y

goal (1 subgoal):
 1. proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)

goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> x < y

goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
proof(cases "y < x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<not> y < x \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y < x

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<not> y < x \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
show ?thesis (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
proof(cases "proper_interval ao (Some y)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
proper_interval ao (Some y)

goal (2 subgoals):
 1. proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
proper_interval ao (Some y)
[PROOF STEP]
obtain z where z: "z < y" "z \<in> above ao"
[PROOF STATE]
proof (prove)
using this:
proper_interval ao (Some y)

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z < y; z \<in> above ao\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: proper_interval_Some2)
[PROOF STATE]
proof (state)
this:
z < y
z \<in> above ao

goal (2 subgoals):
 1. proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
hence nempty: "above ao \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
z < y
z \<in> above ao

goal (1 subgoal):
 1. above ao \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
above ao \<noteq> {}

goal (2 subgoals):
 1. proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
with z
[PROOF STATE]
proof (chain)
picking this:
z < y
z \<in> above ao
above ao \<noteq> {}
[PROOF STEP]
have "Min (above ao) \<le> z"
[PROOF STATE]
proof (prove)
using this:
z < y
z \<in> above ao
above ao \<noteq> {}

goal (1 subgoal):
 1. Min (above ao) \<le> z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Min (above ao) \<le> z

goal (2 subgoals):
 1. proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
hence "Min (above ao) < y"
[PROOF STATE]
proof (prove)
using this:
Min (above ao) \<le> z

goal (1 subgoal):
 1. Min (above ao) < y
[PROOF STEP]
using \<open>z < y\<close>
[PROOF STATE]
proof (prove)
using this:
Min (above ao) \<le> z
z < y

goal (1 subgoal):
 1. Min (above ao) < y
[PROOF STEP]
by(rule le_less_trans)
[PROOF STATE]
proof (state)
this:
Min (above ao) < y

goal (2 subgoals):
 1. proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
hence "set (y # ys) \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao"
[PROOF STATE]
proof (prove)
using this:
Min (above ao) < y

goal (1 subgoal):
 1. set (y # ys) \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao
[PROOF STEP]
using y_Min x_Min z \<open>y < x\<close>
[PROOF STATE]
proof (prove)
using this:
Min (above ao) < y
\<forall>y'\<in>set ys. y < y'
\<forall>x'\<in>set xs. x < x'
z < y
z \<in> above ao
y < x

goal (1 subgoal):
 1. set (y # ys) \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao
[PROOF STEP]
by(fastforce simp add: set_less_aux_def nempty intro!: Min_eqI bexI[where x="Min (above ao)"])
[PROOF STATE]
proof (state)
this:
set (y # ys) \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao

goal (2 subgoals):
 1. proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
set (y # ys) \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao

goal (1 subgoal):
 1. proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
using True \<open>y < x\<close>
[PROOF STATE]
proof (prove)
using this:
set (y # ys) \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao
proper_interval ao (Some y)
y < x

goal (1 subgoal):
 1. proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
by(auto dest: set_less_aux_trans set_less_aux_antisym)
[PROOF STATE]
proof (state)
this:
proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> proper_interval ao (Some y)

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
hence above_eq: "above ao = insert y (above (Some y))"
[PROOF STATE]
proof (prove)
using this:
\<not> proper_interval ao (Some y)

goal (1 subgoal):
 1. above ao = insert y (above (Some y))
[PROOF STEP]
using yys_above
[PROOF STATE]
proof (prove)
using this:
\<not> proper_interval ao (Some y)
set (y # ys) \<subseteq> above ao

goal (1 subgoal):
 1. above ao = insert y (above (Some y))
[PROOF STEP]
by(auto simp add: proper_interval_Some2 intro: above_upclosed)
[PROOF STATE]
proof (state)
this:
above ao = insert y (above (Some y))

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
from y_Min
[PROOF STATE]
proof (chain)
picking this:
\<forall>y'\<in>set ys. y < y'
[PROOF STEP]
have ys_above: "set ys \<subseteq> above (Some y)"
[PROOF STATE]
proof (prove)
using this:
\<forall>y'\<in>set ys. y < y'

goal (1 subgoal):
 1. set ys \<subseteq> above (Some y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set ys \<subseteq> above (Some y)

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
from \<open>y < x\<close> x_Min
[PROOF STATE]
proof (chain)
picking this:
y < x
\<forall>x'\<in>set xs. x < x'
[PROOF STEP]
have xs_above: "set (x # xs) \<subseteq> above (Some y)"
[PROOF STATE]
proof (prove)
using this:
y < x
\<forall>x'\<in>set xs. x < x'

goal (1 subgoal):
 1. set (x # xs) \<subseteq> above (Some y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (x # xs) \<subseteq> above (Some y)

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
have "y \<in> - set (x # xs) \<inter> above ao"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> - set (x # xs) \<inter> above ao
[PROOF STEP]
using \<open>y < x\<close> x_Min yys_above
[PROOF STATE]
proof (prove)
using this:
y < x
\<forall>x'\<in>set xs. x < x'
set (y # ys) \<subseteq> above ao

goal (1 subgoal):
 1. y \<in> - set (x # xs) \<inter> above ao
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> - set (x # xs) \<inter> above ao

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
hence nempty: "- set (x # xs) \<inter> above ao \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
y \<in> - set (x # xs) \<inter> above ao

goal (1 subgoal):
 1. - set (x # xs) \<inter> above ao \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- set (x # xs) \<inter> above ao \<noteq> {}

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
have Min_x: "Min (- set (x # xs) \<inter> above ao) = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (- set (x # xs) \<inter> above ao) = y
[PROOF STEP]
using above_eq \<open>y < x\<close> x_Min
[PROOF STATE]
proof (prove)
using this:
above ao = insert y (above (Some y))
y < x
\<forall>x'\<in>set xs. x < x'

goal (1 subgoal):
 1. Min (- set (x # xs) \<inter> above ao) = y
[PROOF STEP]
by(auto intro!: Min_eqI)
[PROOF STATE]
proof (state)
this:
Min (- set (x # xs) \<inter> above ao) = y

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
have Min_y: "Min (set (y # ys) \<inter> above ao) = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (set (y # ys) \<inter> above ao) = y
[PROOF STEP]
using y_Min above_eq
[PROOF STATE]
proof (prove)
using this:
\<forall>y'\<in>set ys. y < y'
above ao = insert y (above (Some y))

goal (1 subgoal):
 1. Min (set (y # ys) \<inter> above ao) = y
[PROOF STEP]
by(auto intro!: Min_eqI)
[PROOF STATE]
proof (state)
this:
Min (set (y # ys) \<inter> above ao) = y

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
have eq_xs: "- set (x # xs) \<inter> above ao - {y} = - set (x # xs) \<inter> above (Some y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - set (x # xs) \<inter> above ao - {y} = - set (x # xs) \<inter> above (Some y)
[PROOF STEP]
by(auto simp add: above_eq)
[PROOF STATE]
proof (state)
this:
- set (x # xs) \<inter> above ao - {y} = - set (x # xs) \<inter> above (Some y)

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
have eq_ys: "set ys \<inter> above ao - {y} = set ys \<inter> above (Some y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ys \<inter> above ao - {y} = set ys \<inter> above (Some y)
[PROOF STEP]
using y_Min above_eq
[PROOF STATE]
proof (prove)
using this:
\<forall>y'\<in>set ys. y < y'
above ao = insert y (above (Some y))

goal (1 subgoal):
 1. set ys \<inter> above ao - {y} = set ys \<inter> above (Some y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set ys \<inter> above ao - {y} = set ys \<inter> above (Some y)

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
from \<open>\<not> x < y\<close> \<open>y < x\<close> xxs xs_above ys ys_above
[PROOF STATE]
proof (chain)
picking this:
\<not> x < y
y < x
sorted (x # xs)
distinct (x # xs)
set (x # xs) \<subseteq> above (Some y)
sorted ys
distinct ys
set ys \<subseteq> above (Some y)
[PROOF STEP]
have "proper_interval_Compl_set_aux (Some y) (x # xs) ys \<longleftrightarrow>
                 (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and>
                      A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y))"
[PROOF STATE]
proof (prove)
using this:
\<not> x < y
y < x
sorted (x # xs)
distinct (x # xs)
set (x # xs) \<subseteq> above (Some y)
sorted ys
distinct ys
set ys \<subseteq> above (Some y)

goal (1 subgoal):
 1. proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y))
[PROOF STEP]
by(rule "1.IH")
[PROOF STATE]
proof (state)
this:
proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y))

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y))

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
have "\<dots> \<longleftrightarrow> ?rhs" (is "?lhs' \<longleftrightarrow> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y) \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
assume ?lhs'
[PROOF STATE]
proof (state)
this:
\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)

goal (2 subgoals):
 1. \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y) \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
obtain A where less_A: "- set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y)"
                and A_less: "A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)"
[PROOF STATE]
proof (prove)
using this:
\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>- set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y); A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
- set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y)
A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)

goal (2 subgoals):
 1. \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y) \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
let ?A = "insert y A"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y) \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
have Min_A: "Min (?A \<inter> above ao) = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (insert y A \<inter> above ao) = y
[PROOF STEP]
using above_eq
[PROOF STATE]
proof (prove)
using this:
above ao = insert y (above (Some y))

goal (1 subgoal):
 1. Min (insert y A \<inter> above ao) = y
[PROOF STEP]
by(auto intro!: Min_eqI)
[PROOF STATE]
proof (state)
this:
Min (insert y A \<inter> above ao) = y

goal (2 subgoals):
 1. \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y) \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Min (insert y A \<inter> above ao) = y

goal (2 subgoals):
 1. \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y) \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
have A_eq: "A \<inter> above ao - {y} = A \<inter> above (Some y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> above ao - {y} = A \<inter> above (Some y)
[PROOF STEP]
using above_eq
[PROOF STATE]
proof (prove)
using this:
above ao = insert y (above (Some y))

goal (1 subgoal):
 1. A \<inter> above ao - {y} = A \<inter> above (Some y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<inter> above ao - {y} = A \<inter> above (Some y)

goal (2 subgoals):
 1. \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y) \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Min (insert y A \<inter> above ao) = y
A \<inter> above ao - {y} = A \<inter> above (Some y)
[PROOF STEP]
have less_A': "- set (x # xs) \<inter> above ao \<sqsubset>' ?A \<inter> above ao"
[PROOF STATE]
proof (prove)
using this:
Min (insert y A \<inter> above ao) = y
A \<inter> above ao - {y} = A \<inter> above (Some y)

goal (1 subgoal):
 1. - set (x # xs) \<inter> above ao \<sqsubset>' insert y A \<inter> above ao
[PROOF STEP]
using nempty yys_above less_A Min_x eq_xs
[PROOF STATE]
proof (prove)
using this:
Min (insert y A \<inter> above ao) = y
A \<inter> above ao - {y} = A \<inter> above (Some y)
- set (x # xs) \<inter> above ao \<noteq> {}
set (y # ys) \<subseteq> above ao
- set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y)
Min (- set (x # xs) \<inter> above ao) = y
- set (x # xs) \<inter> above ao - {y} = - set (x # xs) \<inter> above (Some y)

goal (1 subgoal):
 1. - set (x # xs) \<inter> above ao \<sqsubset>' insert y A \<inter> above ao
[PROOF STEP]
by(subst set_less_aux_rec) simp_all
[PROOF STATE]
proof (state)
this:
- set (x # xs) \<inter> above ao \<sqsubset>' insert y A \<inter> above ao

goal (2 subgoals):
 1. \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y) \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
have A'_less: "?A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert y A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
using yys_above nempty Min_A A_eq A_less Min_y eq_ys
[PROOF STATE]
proof (prove)
using this:
set (y # ys) \<subseteq> above ao
- set (x # xs) \<inter> above ao \<noteq> {}
Min (insert y A \<inter> above ao) = y
A \<inter> above ao - {y} = A \<inter> above (Some y)
A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
Min (set (y # ys) \<inter> above ao) = y
set ys \<inter> above ao - {y} = set ys \<inter> above (Some y)

goal (1 subgoal):
 1. insert y A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
by(subst set_less_aux_rec) simp_all
[PROOF STATE]
proof (state)
this:
insert y A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (2 subgoals):
 1. \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y) \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
with less_A'
[PROOF STATE]
proof (chain)
picking this:
- set (x # xs) \<inter> above ao \<sqsubset>' insert y A \<inter> above ao
insert y A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
- set (x # xs) \<inter> above ao \<sqsubset>' insert y A \<inter> above ao
insert y A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
obtain A where less_A: "- set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao"
                and A_less: "A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao"
[PROOF STATE]
proof (prove)
using this:
\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>- set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao; A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
- set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao
A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
from less_A
[PROOF STATE]
proof (chain)
picking this:
- set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao
[PROOF STEP]
have nempty': "A \<inter> above ao \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
- set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao

goal (1 subgoal):
 1. A \<inter> above ao \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<inter> above ao \<noteq> {}

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A \<inter> above ao \<noteq> {}

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
have A_eq: "A \<inter> above ao - {y} = A \<inter> above (Some y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> above ao - {y} = A \<inter> above (Some y)
[PROOF STEP]
using above_eq
[PROOF STATE]
proof (prove)
using this:
above ao = insert y (above (Some y))

goal (1 subgoal):
 1. A \<inter> above ao - {y} = A \<inter> above (Some y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<inter> above ao - {y} = A \<inter> above (Some y)

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A \<inter> above ao - {y} = A \<inter> above (Some y)

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
have y_in_xxs: "y \<in> - set (x # xs) \<inter> above ao"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> - set (x # xs) \<inter> above ao
[PROOF STEP]
using \<open>y < x\<close> x_Min yys_above
[PROOF STATE]
proof (prove)
using this:
y < x
\<forall>x'\<in>set xs. x < x'
set (y # ys) \<subseteq> above ao

goal (1 subgoal):
 1. y \<in> - set (x # xs) \<inter> above ao
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> - set (x # xs) \<inter> above ao

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y \<in> - set (x # xs) \<inter> above ao

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
have "y \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> A
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<notin> A \<Longrightarrow> False
[PROOF STEP]
assume "y \<notin> A"
[PROOF STATE]
proof (state)
this:
y \<notin> A

goal (1 subgoal):
 1. y \<notin> A \<Longrightarrow> False
[PROOF STEP]
hence "A \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao"
[PROOF STATE]
proof (prove)
using this:
y \<notin> A

goal (1 subgoal):
 1. A \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao
[PROOF STEP]
using \<open>y < x\<close> x_Min y_in_xxs
[PROOF STATE]
proof (prove)
using this:
y \<notin> A
y < x
\<forall>x'\<in>set xs. x < x'
y \<in> - set (x # xs) \<inter> above ao

goal (1 subgoal):
 1. A \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao
[PROOF STEP]
by(auto simp add: set_less_aux_def above_eq intro: bexI[where x=y])
[PROOF STATE]
proof (state)
this:
A \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao

goal (1 subgoal):
 1. y \<notin> A \<Longrightarrow> False
[PROOF STEP]
with less_A
[PROOF STATE]
proof (chain)
picking this:
- set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao
A \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
- set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao
A \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
y \<in> A

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
hence Min_A: "Min (A \<inter> above ao) = y"
[PROOF STATE]
proof (prove)
using this:
y \<in> A

goal (1 subgoal):
 1. Min (A \<inter> above ao) = y
[PROOF STEP]
using above_eq y_Min
[PROOF STATE]
proof (prove)
using this:
y \<in> A
above ao = insert y (above (Some y))
\<forall>y'\<in>set ys. y < y'

goal (1 subgoal):
 1. Min (A \<inter> above ao) = y
[PROOF STEP]
by(auto intro!: Min_eqI)
[PROOF STATE]
proof (state)
this:
Min (A \<inter> above ao) = y

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A \<inter> above ao \<noteq> {}
A \<inter> above ao - {y} = A \<inter> above (Some y)
y \<in> - set (x # xs) \<inter> above ao
Min (A \<inter> above ao) = y
[PROOF STEP]
have less_A': "- set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y)"
[PROOF STATE]
proof (prove)
using this:
A \<inter> above ao \<noteq> {}
A \<inter> above ao - {y} = A \<inter> above (Some y)
y \<in> - set (x # xs) \<inter> above ao
Min (A \<inter> above ao) = y

goal (1 subgoal):
 1. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y)
[PROOF STEP]
using nempty less_A Min_x eq_xs
[PROOF STATE]
proof (prove)
using this:
A \<inter> above ao \<noteq> {}
A \<inter> above ao - {y} = A \<inter> above (Some y)
y \<in> - set (x # xs) \<inter> above ao
Min (A \<inter> above ao) = y
- set (x # xs) \<inter> above ao \<noteq> {}
- set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao
Min (- set (x # xs) \<inter> above ao) = y
- set (x # xs) \<inter> above ao - {y} = - set (x # xs) \<inter> above (Some y)

goal (1 subgoal):
 1. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y)
[PROOF STEP]
by(subst (asm) set_less_aux_rec)(auto dest: bspec[where x=y])
[PROOF STATE]
proof (state)
this:
- set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y)

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
have A'_less: "A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
using A_less nempty' yys_above Min_A Min_y A_eq eq_ys
[PROOF STATE]
proof (prove)
using this:
A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
A \<inter> above ao \<noteq> {}
set (y # ys) \<subseteq> above ao
Min (A \<inter> above ao) = y
Min (set (y # ys) \<inter> above ao) = y
A \<inter> above ao - {y} = A \<inter> above (Some y)
set ys \<inter> above ao - {y} = set ys \<inter> above (Some y)

goal (1 subgoal):
 1. A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
by(subst (asm) set_less_aux_rec) simp_all
[PROOF STATE]
proof (state)
this:
A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
with less_A'
[PROOF STATE]
proof (chain)
picking this:
- set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y)
A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
show ?lhs'
[PROOF STATE]
proof (prove)
using this:
- set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y)
A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>A. - set (x # xs) \<inter> above (Some y) \<sqsubset>' A \<inter> above (Some y) \<and> A \<inter> above (Some y) \<sqsubset>' set ys \<inter> above (Some y)) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)

goal (1 subgoal):
 1. proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
using \<open>\<not> x < y\<close> \<open>y < x\<close> False
[PROOF STATE]
proof (prove)
using this:
proper_interval_Compl_set_aux (Some y) (x # xs) ys = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
\<not> x < y
y < x
\<not> proper_interval ao (Some y)

goal (1 subgoal):
 1. proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> y < x

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
with \<open>\<not> x < y\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> x < y
\<not> y < x
[PROOF STEP]
have "x = y"
[PROOF STATE]
proof (prove)
using this:
\<not> x < y
\<not> y < x

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

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
thus ?thesis (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
using this:
x = y

goal (1 subgoal):
 1. proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
proof(cases "proper_interval ao (Some x)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x = y; proper_interval ao (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<lbrakk>x = y; \<not> proper_interval ao (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
proper_interval ao (Some x)

goal (2 subgoals):
 1. \<lbrakk>x = y; proper_interval ao (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<lbrakk>x = y; \<not> proper_interval ao (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
proper_interval ao (Some x)
[PROOF STEP]
obtain z where z: "z < x" "z \<in> above ao"
[PROOF STATE]
proof (prove)
using this:
proper_interval ao (Some x)

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z < x; z \<in> above ao\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: proper_interval_Some2)
[PROOF STATE]
proof (state)
this:
z < x
z \<in> above ao

goal (2 subgoals):
 1. \<lbrakk>x = y; proper_interval ao (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<lbrakk>x = y; \<not> proper_interval ao (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
hence nempty: "above ao \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
z < x
z \<in> above ao

goal (1 subgoal):
 1. above ao \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
above ao \<noteq> {}

goal (2 subgoals):
 1. \<lbrakk>x = y; proper_interval ao (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<lbrakk>x = y; \<not> proper_interval ao (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
with z
[PROOF STATE]
proof (chain)
picking this:
z < x
z \<in> above ao
above ao \<noteq> {}
[PROOF STEP]
have "Min (above ao) \<le> z"
[PROOF STATE]
proof (prove)
using this:
z < x
z \<in> above ao
above ao \<noteq> {}

goal (1 subgoal):
 1. Min (above ao) \<le> z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Min (above ao) \<le> z

goal (2 subgoals):
 1. \<lbrakk>x = y; proper_interval ao (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<lbrakk>x = y; \<not> proper_interval ao (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
hence "Min (above ao) < x"
[PROOF STATE]
proof (prove)
using this:
Min (above ao) \<le> z

goal (1 subgoal):
 1. Min (above ao) < x
[PROOF STEP]
using \<open>z < x\<close>
[PROOF STATE]
proof (prove)
using this:
Min (above ao) \<le> z
z < x

goal (1 subgoal):
 1. Min (above ao) < x
[PROOF STEP]
by(rule le_less_trans)
[PROOF STATE]
proof (state)
this:
Min (above ao) < x

goal (2 subgoals):
 1. \<lbrakk>x = y; proper_interval ao (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<lbrakk>x = y; \<not> proper_interval ao (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
hence "set (y # ys) \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao"
[PROOF STATE]
proof (prove)
using this:
Min (above ao) < x

goal (1 subgoal):
 1. set (y # ys) \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao
[PROOF STEP]
using y_Min x_Min z \<open>x = y\<close>
[PROOF STATE]
proof (prove)
using this:
Min (above ao) < x
\<forall>y'\<in>set ys. y < y'
\<forall>x'\<in>set xs. x < x'
z < x
z \<in> above ao
x = y

goal (1 subgoal):
 1. set (y # ys) \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao
[PROOF STEP]
by(fastforce simp add: set_less_aux_def nempty intro!: Min_eqI bexI[where x="Min (above ao)"])
[PROOF STATE]
proof (state)
this:
set (y # ys) \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao

goal (2 subgoals):
 1. \<lbrakk>x = y; proper_interval ao (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
 2. \<lbrakk>x = y; \<not> proper_interval ao (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
set (y # ys) \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao

goal (1 subgoal):
 1. proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
using True \<open>x = y\<close>
[PROOF STATE]
proof (prove)
using this:
set (y # ys) \<inter> above ao \<sqsubset>' - set (x # xs) \<inter> above ao
proper_interval ao (Some x)
x = y

goal (1 subgoal):
 1. proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
by(auto dest: set_less_aux_trans set_less_aux_antisym)
[PROOF STATE]
proof (state)
this:
proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)

goal (1 subgoal):
 1. \<lbrakk>x = y; \<not> proper_interval ao (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x = y; \<not> proper_interval ao (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> proper_interval ao (Some x)

goal (1 subgoal):
 1. \<lbrakk>x = y; \<not> proper_interval ao (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
hence above_eq: "above ao = insert x (above (Some x))"
[PROOF STATE]
proof (prove)
using this:
\<not> proper_interval ao (Some x)

goal (1 subgoal):
 1. above ao = insert x (above (Some x))
[PROOF STEP]
using xxs_above
[PROOF STATE]
proof (prove)
using this:
\<not> proper_interval ao (Some x)
set (x # xs) \<subseteq> above ao

goal (1 subgoal):
 1. above ao = insert x (above (Some x))
[PROOF STEP]
by(auto simp add: proper_interval_Some2 intro: above_upclosed)
[PROOF STATE]
proof (state)
this:
above ao = insert x (above (Some x))

goal (1 subgoal):
 1. \<lbrakk>x = y; \<not> proper_interval ao (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
have "(ys = [] \<longrightarrow> xs \<noteq> []) \<longleftrightarrow> ?rhs" (is "?lhs' \<longleftrightarrow> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ys = [] \<longrightarrow> xs \<noteq> []) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
proof(intro iffI strip notI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ys = [] \<longrightarrow> xs \<noteq> [] \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<lbrakk>\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao; ys = []; xs = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume ?lhs'
[PROOF STATE]
proof (state)
this:
ys = [] \<longrightarrow> xs \<noteq> []

goal (2 subgoals):
 1. ys = [] \<longrightarrow> xs \<noteq> [] \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<lbrakk>\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao; ys = []; xs = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
proof(cases ys)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ys = [] \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<And>a list. ys = a # list \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
ys = []

goal (2 subgoals):
 1. ys = [] \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<And>a list. ys = a # list \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
with \<open>?lhs'\<close>
[PROOF STATE]
proof (chain)
picking this:
ys = [] \<longrightarrow> xs \<noteq> []
ys = []
[PROOF STEP]
obtain x' xs' where xs_eq: "xs = x' # xs'"
[PROOF STATE]
proof (prove)
using this:
ys = [] \<longrightarrow> xs \<noteq> []
ys = []

goal (1 subgoal):
 1. (\<And>x' xs'. xs = x' # xs' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: neq_Nil_conv)
[PROOF STATE]
proof (state)
this:
xs = x' # xs'

goal (2 subgoals):
 1. ys = [] \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<And>a list. ys = a # list \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
with xs
[PROOF STATE]
proof (chain)
picking this:
sorted xs
distinct xs
xs = x' # xs'
[PROOF STEP]
have x'_Min: "\<forall>x'' \<in> set xs'. x' < x''"
[PROOF STATE]
proof (prove)
using this:
sorted xs
distinct xs
xs = x' # xs'

goal (1 subgoal):
 1. \<forall>x''\<in>set xs'. x' < x''
[PROOF STEP]
by(auto simp add: less_le)
[PROOF STATE]
proof (state)
this:
\<forall>x''\<in>set xs'. x' < x''

goal (2 subgoals):
 1. ys = [] \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<And>a list. ys = a # list \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
let ?A = "- set (x # xs')"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ys = [] \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<And>a list. ys = a # list \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
have "- set (x # xs) \<inter> above ao \<subseteq> ?A \<inter> above ao"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - set (x # xs) \<inter> above ao \<subseteq> - set (x # xs') \<inter> above ao
[PROOF STEP]
using xs_eq
[PROOF STATE]
proof (prove)
using this:
xs = x' # xs'

goal (1 subgoal):
 1. - set (x # xs) \<inter> above ao \<subseteq> - set (x # xs') \<inter> above ao
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- set (x # xs) \<inter> above ao \<subseteq> - set (x # xs') \<inter> above ao

goal (2 subgoals):
 1. ys = [] \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<And>a list. ys = a # list \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
- set (x # xs) \<inter> above ao \<subseteq> - set (x # xs') \<inter> above ao

goal (2 subgoals):
 1. ys = [] \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<And>a list. ys = a # list \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
have "x' \<notin> - set (x # xs) \<inter> above ao" "x' \<in> ?A \<inter> above ao"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x' \<notin> - set (x # xs) \<inter> above ao &&& x' \<in> - set (x # xs') \<inter> above ao
[PROOF STEP]
using xs_eq xxs_above x'_Min x_Min
[PROOF STATE]
proof (prove)
using this:
xs = x' # xs'
set (x # xs) \<subseteq> above ao
\<forall>x''\<in>set xs'. x' < x''
\<forall>x'\<in>set xs. x < x'

goal (1 subgoal):
 1. x' \<notin> - set (x # xs) \<inter> above ao &&& x' \<in> - set (x # xs') \<inter> above ao
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x' \<notin> - set (x # xs) \<inter> above ao
x' \<in> - set (x # xs') \<inter> above ao

goal (2 subgoals):
 1. ys = [] \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<And>a list. ys = a # list \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
- set (x # xs) \<inter> above ao \<subseteq> - set (x # xs') \<inter> above ao
x' \<notin> - set (x # xs) \<inter> above ao
x' \<in> - set (x # xs') \<inter> above ao
[PROOF STEP]
have "- set (x # xs) \<inter> above ao \<subset> ?A \<inter> above ao"
[PROOF STATE]
proof (prove)
using this:
- set (x # xs) \<inter> above ao \<subseteq> - set (x # xs') \<inter> above ao
x' \<notin> - set (x # xs) \<inter> above ao
x' \<in> - set (x # xs') \<inter> above ao

goal (1 subgoal):
 1. - set (x # xs) \<inter> above ao \<subset> - set (x # xs') \<inter> above ao
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
- set (x # xs) \<inter> above ao \<subset> - set (x # xs') \<inter> above ao

goal (2 subgoals):
 1. ys = [] \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<And>a list. ys = a # list \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
hence "- set (x # xs) \<inter> above ao \<sqsubset>' \<dots> "
[PROOF STATE]
proof (prove)
using this:
- set (x # xs) \<inter> above ao \<subset> - set (x # xs') \<inter> above ao

goal (1 subgoal):
 1. - set (x # xs) \<inter> above ao \<sqsubset>' - set (x # xs') \<inter> above ao
[PROOF STEP]
by(fastforce intro: psubset_finite_imp_set_less_aux)
[PROOF STATE]
proof (state)
this:
- set (x # xs) \<inter> above ao \<sqsubset>' - set (x # xs') \<inter> above ao

goal (2 subgoals):
 1. ys = [] \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<And>a list. ys = a # list \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
- set (x # xs) \<inter> above ao \<sqsubset>' - set (x # xs') \<inter> above ao

goal (2 subgoals):
 1. ys = [] \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<And>a list. ys = a # list \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
have "\<dots> \<sqsubset>' set (y # ys) \<inter> above ao"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - set (x # xs') \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
using Nil \<open>x = y\<close>
[PROOF STATE]
proof (prove)
using this:
ys = []
x = y

goal (1 subgoal):
 1. - set (x # xs') \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
by(auto simp add: set_less_aux_def above_eq)
[PROOF STATE]
proof (state)
this:
- set (x # xs') \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (2 subgoals):
 1. ys = [] \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
 2. \<And>a list. ys = a # list \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
- set (x # xs) \<inter> above ao \<sqsubset>' - set (x # xs') \<inter> above ao
- set (x # xs') \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
- set (x # xs) \<inter> above ao \<sqsubset>' - set (x # xs') \<inter> above ao
- set (x # xs') \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
case (Cons y' ys')
[PROOF STATE]
proof (state)
this:
ys = y' # ys'

goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
let ?A = "{y}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
have "- set (x # xs) \<inter> above ao \<sqsubset>' ?A \<inter> above ao"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - set (x # xs) \<inter> above ao \<sqsubset>' {y} \<inter> above ao
[PROOF STEP]
using \<open>x = y\<close> x_Min
[PROOF STATE]
proof (prove)
using this:
x = y
\<forall>x'\<in>set xs. x < x'

goal (1 subgoal):
 1. - set (x # xs) \<inter> above ao \<sqsubset>' {y} \<inter> above ao
[PROOF STEP]
by(auto simp add: set_less_aux_def above_eq)
[PROOF STATE]
proof (state)
this:
- set (x # xs) \<inter> above ao \<sqsubset>' {y} \<inter> above ao

goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
- set (x # xs) \<inter> above ao \<sqsubset>' {y} \<inter> above ao

goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
have "\<dots> \<subset> set (y # ys) \<inter> above ao"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y} \<inter> above ao \<subset> set (y # ys) \<inter> above ao
[PROOF STEP]
using yys_above yys Cons
[PROOF STATE]
proof (prove)
using this:
set (y # ys) \<subseteq> above ao
sorted (y # ys)
distinct (y # ys)
ys = y' # ys'

goal (1 subgoal):
 1. {y} \<inter> above ao \<subset> set (y # ys) \<inter> above ao
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{y} \<inter> above ao \<subset> set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
hence "?A \<inter> above ao \<sqsubset>' \<dots>"
[PROOF STATE]
proof (prove)
using this:
{y} \<inter> above ao \<subset> set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. {y} \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
by(fastforce intro: psubset_finite_imp_set_less_aux)
[PROOF STATE]
proof (state)
this:
{y} \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
- set (x # xs) \<inter> above ao \<sqsubset>' {y} \<inter> above ao
{y} \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
- set (x # xs) \<inter> above ao \<sqsubset>' {y} \<inter> above ao
{y} \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<lbrakk>\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao; ys = []; xs = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao; ys = []; xs = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume Nil: "ys = []" "xs = []" and ?rhs
[PROOF STATE]
proof (state)
this:
ys = []
xs = []
\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<lbrakk>\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao; ys = []; xs = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ys = []
xs = []
\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
[PROOF STEP]
obtain A where less_A: "- {x} \<inter> above ao \<sqsubset>' A \<inter> above ao"
                and A_less: "A \<inter> above ao \<sqsubset>' {x}"
[PROOF STATE]
proof (prove)
using this:
ys = []
xs = []
\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>- {x} \<inter> above ao \<sqsubset>' A \<inter> above ao; A \<inter> above ao \<sqsubset>' {x}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>x = y\<close> above_eq
[PROOF STATE]
proof (prove)
using this:
ys = []
xs = []
\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao
x = y
above ao = insert x (above (Some x))

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>- {x} \<inter> above ao \<sqsubset>' A \<inter> above ao; A \<inter> above ao \<sqsubset>' {x}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- {x} \<inter> above ao \<sqsubset>' A \<inter> above ao
A \<inter> above ao \<sqsubset>' {x}

goal (1 subgoal):
 1. \<lbrakk>\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao; ys = []; xs = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "x \<notin> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> A
[PROOF STEP]
using A_less
[PROOF STATE]
proof (prove)
using this:
A \<inter> above ao \<sqsubset>' {x}

goal (1 subgoal):
 1. x \<notin> A
[PROOF STEP]
by(auto simp add: set_less_aux_def above_eq)
[PROOF STATE]
proof (state)
this:
x \<notin> A

goal (1 subgoal):
 1. \<lbrakk>\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao; ys = []; xs = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "A \<inter> above ao \<subseteq> - {x} \<inter> above ao"
[PROOF STATE]
proof (prove)
using this:
x \<notin> A

goal (1 subgoal):
 1. A \<inter> above ao \<subseteq> - {x} \<inter> above ao
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<inter> above ao \<subseteq> - {x} \<inter> above ao

goal (1 subgoal):
 1. \<lbrakk>\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao; ys = []; xs = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "A \<inter> above ao \<sqsubseteq>' \<dots>"
[PROOF STATE]
proof (prove)
using this:
A \<inter> above ao \<subseteq> - {x} \<inter> above ao

goal (1 subgoal):
 1. A \<inter> above ao \<sqsubseteq>' - {x} \<inter> above ao
[PROOF STEP]
by(auto intro: subset_finite_imp_set_less_eq_aux)
[PROOF STATE]
proof (state)
this:
A \<inter> above ao \<sqsubseteq>' - {x} \<inter> above ao

goal (1 subgoal):
 1. \<lbrakk>\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao; ys = []; xs = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with less_A
[PROOF STATE]
proof (chain)
picking this:
- {x} \<inter> above ao \<sqsubset>' A \<inter> above ao
A \<inter> above ao \<sqsubseteq>' - {x} \<inter> above ao
[PROOF STEP]
have "\<dots> \<sqsubset>' \<dots>"
[PROOF STATE]
proof (prove)
using this:
- {x} \<inter> above ao \<sqsubset>' A \<inter> above ao
A \<inter> above ao \<sqsubseteq>' - {x} \<inter> above ao

goal (1 subgoal):
 1. - {x} \<inter> above ao \<sqsubset>' - {x} \<inter> above ao
[PROOF STEP]
by(rule set_less_trans_set_less_eq)
[PROOF STATE]
proof (state)
this:
- {x} \<inter> above ao \<sqsubset>' - {x} \<inter> above ao

goal (1 subgoal):
 1. \<lbrakk>\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao; ys = []; xs = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
- {x} \<inter> above ao \<sqsubset>' - {x} \<inter> above ao

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(ys = [] \<longrightarrow> xs \<noteq> []) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)

goal (1 subgoal):
 1. \<lbrakk>x = y; \<not> proper_interval ao (Some x)\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
with \<open>x = y\<close> False
[PROOF STATE]
proof (chain)
picking this:
x = y
\<not> proper_interval ao (Some x)
(ys = [] \<longrightarrow> xs \<noteq> []) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = y
\<not> proper_interval ao (Some x)
(ys = [] \<longrightarrow> xs \<noteq> []) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)

goal (1 subgoal):
 1. proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
proper_interval_Compl_set_aux ao (x # xs) (y # ys) = (\<exists>A. - set (x # xs) \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set (y # ys) \<inter> above ao)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
proper_interval_Compl_set_aux ao xs ys = (\<exists>A. - set xs \<inter> above ao \<sqsubset>' A \<inter> above ao \<and> A \<inter> above ao \<sqsubset>' set ys \<inter> above ao)

goal (1 subgoal):
 1. proper_interval_Compl_set_aux None xs ys = (\<exists>A. - set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>set xs \<subseteq> above ?ao2; set ys \<subseteq> above ?ao2\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux ?ao2 xs ys = (\<exists>A. - set xs \<inter> above ?ao2 \<sqsubset>' A \<inter> above ?ao2 \<and> A \<inter> above ?ao2 \<sqsubset>' set ys \<inter> above ?ao2)

goal (1 subgoal):
 1. proper_interval_Compl_set_aux None xs ys = (\<exists>A. - set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)
[PROOF STEP]
from this[of None]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>set xs \<subseteq> above None; set ys \<subseteq> above None\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux None xs ys = (\<exists>A. - set xs \<inter> above None \<sqsubset>' A \<inter> above None \<and> A \<inter> above None \<sqsubset>' set ys \<inter> above None)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set xs \<subseteq> above None; set ys \<subseteq> above None\<rbrakk> \<Longrightarrow> proper_interval_Compl_set_aux None xs ys = (\<exists>A. - set xs \<inter> above None \<sqsubset>' A \<inter> above None \<and> A \<inter> above None \<sqsubset>' set ys \<inter> above None)

goal (1 subgoal):
 1. proper_interval_Compl_set_aux None xs ys = (\<exists>A. - set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proper_interval_Compl_set_aux None xs ys = (\<exists>A. - set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)

goal:
No subgoals!
[PROOF STEP]
qed