[STATEMENT]
theorem assumes fin: "finite (UNIV :: 'a set)"
  and xs: "sorted xs" "distinct xs"
  and ys: "sorted ys" "distinct ys"
  shows set_less_eq_aux_Compl2_conv_set_less_eq_aux_Compl:
  "set xs \<sqsubseteq>' - set ys \<longleftrightarrow> set_less_eq_aux_Compl None xs ys" (is ?Compl2)
  and Compl1_set_less_eq_aux_conv_Compl_set_less_eq_aux:
  "- set xs \<sqsubseteq>' set ys \<longleftrightarrow> Compl_set_less_eq_aux None xs ys" (is ?Compl1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys &&& (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
note fin' [simp] = finite_subset[OF subset_UNIV fin]
[PROOF STATE]
proof (state)
this:
finite ?A

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs 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 (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs 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)"
    and proper_interval_None2: "\<And>ao. proper_interval ao None \<longleftrightarrow> above ao \<noteq> {}"
[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)) &&& (\<And>ao. proper_interval ao None = (above ao \<noteq> {}))
[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)
proper_interval ?ao None = (above ?ao \<noteq> {})

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs 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)
proper_interval ?ao None = (above ?ao \<noteq> {})

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
fix ao x A B
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
assume ex: "proper_interval ao (Some x)"
      and A: "\<forall>a \<in> A. x \<le> a"
      and B: "\<forall>b \<in> B. x \<le> b"
[PROOF STATE]
proof (state)
this:
proper_interval ao (Some x)
\<forall>a\<in>A. x \<le> a
\<forall>b\<in>B. x \<le> b

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
from ex
[PROOF STATE]
proof (chain)
picking this:
proper_interval ao (Some x)
[PROOF STEP]
obtain z where z_ao: "z \<in> above ao" and z: "z < x"
[PROOF STATE]
proof (prove)
using this:
proper_interval ao (Some x)

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

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>A. x \<le> a
z \<in> above ao
z < x
[PROOF STEP]
have A_eq: "A \<inter> above ao = A"
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>A. x \<le> a
z \<in> above ao
z < x

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

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
from z_ao z B
[PROOF STATE]
proof (chain)
picking this:
z \<in> above ao
z < x
\<forall>b\<in>B. x \<le> b
[PROOF STEP]
have B_eq: "B \<inter> above ao = B"
[PROOF STATE]
proof (prove)
using this:
z \<in> above ao
z < x
\<forall>b\<in>B. x \<le> b

goal (1 subgoal):
 1. B \<inter> above ao = B
[PROOF STEP]
by(auto simp add: above_upclosed)
[PROOF STATE]
proof (state)
this:
B \<inter> above ao = B

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
define w where "w = Min (above ao)"
[PROOF STATE]
proof (state)
this:
w = Min (above ao)

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
with z_ao
[PROOF STATE]
proof (chain)
picking this:
z \<in> above ao
w = Min (above ao)
[PROOF STEP]
have "w \<le> z" "\<forall>z \<in> above ao. w \<le> z" "w \<in> above ao"
[PROOF STATE]
proof (prove)
using this:
z \<in> above ao
w = Min (above ao)

goal (1 subgoal):
 1. w \<le> z &&& \<forall>z\<in>above ao. w \<le> z &&& w \<in> above ao
[PROOF STEP]
by(auto simp add: Min_le_iff intro: Min_in)
[PROOF STATE]
proof (state)
this:
w \<le> z
\<forall>z\<in>above ao. w \<le> z
w \<in> above ao

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
hence "A \<inter> above ao \<sqsubset>' (- B) \<inter> above ao" (is "?lhs \<sqsubset>' ?rhs")
[PROOF STATE]
proof (prove)
using this:
w \<le> z
\<forall>z\<in>above ao. w \<le> z
w \<in> above ao

goal (1 subgoal):
 1. A \<inter> above ao \<sqsubset>' - B \<inter> above ao
[PROOF STEP]
using A B z
[PROOF STATE]
proof (prove)
using this:
w \<le> z
\<forall>z\<in>above ao. w \<le> z
w \<in> above ao
\<forall>a\<in>A. x \<le> a
\<forall>b\<in>B. x \<le> b
z < x

goal (1 subgoal):
 1. A \<inter> above ao \<sqsubset>' - B \<inter> above ao
[PROOF STEP]
by(auto simp add: set_less_aux_def intro!: bexI[where x="w"])
[PROOF STATE]
proof (state)
this:
A \<inter> above ao \<sqsubset>' - B \<inter> above ao

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
hence "A \<sqsubseteq>' ?rhs"
[PROOF STATE]
proof (prove)
using this:
A \<inter> above ao \<sqsubset>' - B \<inter> above ao

goal (1 subgoal):
 1. A \<sqsubseteq>' - B \<inter> above ao
[PROOF STEP]
unfolding A_eq
[PROOF STATE]
proof (prove)
using this:
A \<sqsubset>' - B \<inter> above ao

goal (1 subgoal):
 1. A \<sqsubseteq>' - B \<inter> above ao
[PROOF STEP]
by(simp add: set_less_eq_aux_def)
[PROOF STATE]
proof (state)
this:
A \<sqsubseteq>' - B \<inter> above ao

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A \<sqsubseteq>' - B \<inter> above ao

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
from z_ao z A B
[PROOF STATE]
proof (chain)
picking this:
z \<in> above ao
z < x
\<forall>a\<in>A. x \<le> a
\<forall>b\<in>B. x \<le> b
[PROOF STEP]
have "z \<in> - A \<inter> above ao" "z \<notin> B"
[PROOF STATE]
proof (prove)
using this:
z \<in> above ao
z < x
\<forall>a\<in>A. x \<le> a
\<forall>b\<in>B. x \<le> b

goal (1 subgoal):
 1. z \<in> - A \<inter> above ao &&& z \<notin> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> - A \<inter> above ao
z \<notin> B

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
hence neq: "- A \<inter> above ao \<noteq> B \<inter> above ao"
[PROOF STATE]
proof (prove)
using this:
z \<in> - A \<inter> above ao
z \<notin> B

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

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
have "\<not> - A \<inter> above ao \<sqsubset>' B \<inter> above ao" (is "\<not> ?lhs' \<sqsubset>' ?rhs'")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> - A \<inter> above ao \<sqsubset>' B \<inter> above ao
[PROOF STEP]
using A B z z_ao
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>A. x \<le> a
\<forall>b\<in>B. x \<le> b
z < x
z \<in> above ao

goal (1 subgoal):
 1. \<not> - A \<inter> above ao \<sqsubset>' B \<inter> above ao
[PROOF STEP]
by(force simp add: set_less_aux_def not_less dest: bspec[where x=z])
[PROOF STATE]
proof (state)
this:
\<not> - A \<inter> above ao \<sqsubset>' B \<inter> above ao

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
with neq
[PROOF STATE]
proof (chain)
picking this:
- A \<inter> above ao \<noteq> B \<inter> above ao
\<not> - A \<inter> above ao \<sqsubset>' B \<inter> above ao
[PROOF STEP]
have "\<not> ?lhs' \<sqsubseteq>' B"
[PROOF STATE]
proof (prove)
using this:
- A \<inter> above ao \<noteq> B \<inter> above ao
\<not> - A \<inter> above ao \<sqsubset>' B \<inter> above ao

goal (1 subgoal):
 1. \<not> - A \<inter> above ao \<sqsubseteq>' B
[PROOF STEP]
unfolding B_eq
[PROOF STATE]
proof (prove)
using this:
- A \<inter> above ao \<noteq> B
\<not> - A \<inter> above ao \<sqsubset>' B

goal (1 subgoal):
 1. \<not> - A \<inter> above ao \<sqsubseteq>' B
[PROOF STEP]
by(auto simp add: set_less_eq_aux_def)
[PROOF STATE]
proof (state)
this:
\<not> - A \<inter> above ao \<sqsubseteq>' B

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> - A \<inter> above ao \<sqsubseteq>' B

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
note calculation
[PROOF STATE]
proof (state)
this:
A \<sqsubseteq>' - B \<inter> above ao
\<not> - A \<inter> above ao \<sqsubseteq>' B

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>proper_interval ?ao2 (Some ?x2); \<forall>a\<in>?A2. ?x2 \<le> a; \<forall>b\<in>?B2. ?x2 \<le> b\<rbrakk> \<Longrightarrow> ?A2 \<sqsubseteq>' - ?B2 \<inter> above ?ao2
\<lbrakk>proper_interval ?ao2 (Some ?x2); \<forall>a\<in>?A2. ?x2 \<le> a; \<forall>b\<in>?B2. ?x2 \<le> b\<rbrakk> \<Longrightarrow> \<not> - ?A2 \<inter> above ?ao2 \<sqsubseteq>' ?B2

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
note proper_interval_set_less_eqI = this(1)
    and proper_interval_not_set_less_eq_auxI = this(2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>proper_interval ?ao2 (Some ?x2); \<forall>a\<in>?A2. ?x2 \<le> a; \<forall>b\<in>?B2. ?x2 \<le> b\<rbrakk> \<Longrightarrow> ?A2 \<sqsubseteq>' - ?B2 \<inter> above ?ao2
\<lbrakk>proper_interval ?ao2 (Some ?x2); \<forall>a\<in>?A2. ?x2 \<le> a; \<forall>b\<in>?B2. ?x2 \<le> b\<rbrakk> \<Longrightarrow> \<not> - ?A2 \<inter> above ?ao2 \<sqsubseteq>' ?B2

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>proper_interval ?ao2 (Some ?x2); \<forall>a\<in>?A2. ?x2 \<le> a; \<forall>b\<in>?B2. ?x2 \<le> b\<rbrakk> \<Longrightarrow> ?A2 \<sqsubseteq>' - ?B2 \<inter> above ?ao2
\<lbrakk>proper_interval ?ao2 (Some ?x2); \<forall>a\<in>?A2. ?x2 \<le> a; \<forall>b\<in>?B2. ?x2 \<le> b\<rbrakk> \<Longrightarrow> \<not> - ?A2 \<inter> above ?ao2 \<sqsubseteq>' ?B2

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
fix ao
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
assume "set xs \<union> set ys \<subseteq> above ao"
[PROOF STATE]
proof (state)
this:
set xs \<union> set ys \<subseteq> above ao

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
with xs ys
[PROOF STATE]
proof (chain)
picking this:
sorted xs
distinct xs
sorted ys
distinct ys
set xs \<union> set ys \<subseteq> above ao
[PROOF STEP]
have "set_less_eq_aux_Compl ao xs ys \<longleftrightarrow> set xs \<sqsubseteq>' (- set ys) \<inter> above ao"
[PROOF STATE]
proof (prove)
using this:
sorted xs
distinct xs
sorted ys
distinct ys
set xs \<union> set ys \<subseteq> above ao

goal (1 subgoal):
 1. set_less_eq_aux_Compl ao xs ys = (set xs \<sqsubseteq>' - set ys \<inter> above ao)
[PROOF STEP]
proof(induction ao xs ys rule: set_less_eq_aux_Compl.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ao ys. \<lbrakk>sorted []; distinct []; sorted ys; distinct ys; set [] \<union> set ys \<subseteq> above ao\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl ao [] ys = (set [] \<sqsubseteq>' - set ys \<inter> above ao)
 2. \<And>ao xs. \<lbrakk>sorted xs; distinct xs; sorted []; distinct []; set xs \<union> set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl ao xs [] = (set xs \<sqsubseteq>' - set [] \<inter> above ao)
 3. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some x) xs (y # ys) = (set xs \<sqsubseteq>' - set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some y) (x # xs) ys = (set (x # xs) \<sqsubseteq>' - set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
sorted []
distinct []
sorted ys_
distinct ys_
set [] \<union> set ys_ \<subseteq> above ao_

goal (3 subgoals):
 1. \<And>ao ys. \<lbrakk>sorted []; distinct []; sorted ys; distinct ys; set [] \<union> set ys \<subseteq> above ao\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl ao [] ys = (set [] \<sqsubseteq>' - set ys \<inter> above ao)
 2. \<And>ao xs. \<lbrakk>sorted xs; distinct xs; sorted []; distinct []; set xs \<union> set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl ao xs [] = (set xs \<sqsubseteq>' - set [] \<inter> above ao)
 3. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some x) xs (y # ys) = (set xs \<sqsubseteq>' - set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some y) (x # xs) ys = (set (x # xs) \<sqsubseteq>' - set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
sorted []
distinct []
sorted ys_
distinct ys_
set [] \<union> set ys_ \<subseteq> above ao_

goal (1 subgoal):
 1. set_less_eq_aux_Compl ao_ [] ys_ = (set [] \<sqsubseteq>' - set ys_ \<inter> above ao_)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set_less_eq_aux_Compl ao_ [] ys_ = (set [] \<sqsubseteq>' - set ys_ \<inter> above ao_)

goal (2 subgoals):
 1. \<And>ao xs. \<lbrakk>sorted xs; distinct xs; sorted []; distinct []; set xs \<union> set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl ao xs [] = (set xs \<sqsubseteq>' - set [] \<inter> above ao)
 2. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some x) xs (y # ys) = (set xs \<sqsubseteq>' - set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some y) (x # xs) ys = (set (x # xs) \<sqsubseteq>' - set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ao xs. \<lbrakk>sorted xs; distinct xs; sorted []; distinct []; set xs \<union> set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl ao xs [] = (set xs \<sqsubseteq>' - set [] \<inter> above ao)
 2. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some x) xs (y # ys) = (set xs \<sqsubseteq>' - set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some y) (x # xs) ys = (set (x # xs) \<sqsubseteq>' - set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
sorted xs_
distinct xs_
sorted []
distinct []
set xs_ \<union> set [] \<subseteq> above ao_

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

goal (1 subgoal):
 1. set_less_eq_aux_Compl ao_ xs_ [] = (set xs_ \<sqsubseteq>' - set [] \<inter> above ao_)
[PROOF STEP]
by(auto intro: subset_finite_imp_set_less_eq_aux)
[PROOF STATE]
proof (state)
this:
set_less_eq_aux_Compl ao_ xs_ [] = (set xs_ \<sqsubseteq>' - set [] \<inter> above ao_)

goal (1 subgoal):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some x) xs (y # ys) = (set xs \<sqsubseteq>' - set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some y) (x # xs) ys = (set (x # xs) \<sqsubseteq>' - set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - 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; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some x) xs (y # ys) = (set xs \<sqsubseteq>' - set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some y) (x # xs) ys = (set (x # xs) \<sqsubseteq>' - set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
case (3 ao x xs y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some x) xs (y # ys) = (set xs \<sqsubseteq>' - set (y # ys) \<inter> above (Some x))
\<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some y) (x # xs) ys = (set (x # xs) \<sqsubseteq>' - set ys \<inter> above (Some y))
sorted (x # xs)
distinct (x # xs)
sorted (y # ys)
distinct (y # ys)
set (x # xs) \<union> set (y # ys) \<subseteq> above ao

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

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

goal (1 subgoal):
 1. x \<in> above ao &&& y \<in> above ao
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
x \<in> above ao
y \<in> above ao

goal (1 subgoal):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some x) xs (y # ys) = (set xs \<sqsubseteq>' - set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some y) (x # xs) ys = (set (x # xs) \<sqsubseteq>' - set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - 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; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some x) xs (y # ys) = (set xs \<sqsubseteq>' - set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some y) (x # xs) ys = (set (x # xs) \<sqsubseteq>' - set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - 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; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some x) xs (y # ys) = (set xs \<sqsubseteq>' - set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some y) (x # xs) ys = (set (x # xs) \<sqsubseteq>' - set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - 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; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some x) xs (y # ys) = (set xs \<sqsubseteq>' - set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some y) (x # xs) ys = (set (x # xs) \<sqsubseteq>' - set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - 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; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some x) xs (y # ys) = (set xs \<sqsubseteq>' - set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some y) (x # xs) ys = (set (x # xs) \<sqsubseteq>' - set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
let ?lhs = "set (x # xs)" and ?rhs = "- set (y # ys) \<inter> above ao"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some x) xs (y # ys) = (set xs \<sqsubseteq>' - set (y # ys) \<inter> above (Some x)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl (Some y) (x # xs) ys = (set (x # xs) \<sqsubseteq>' - set ys \<inter> above (Some y)); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
proof(cases "x < y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x < y \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
 2. \<not> x < y \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x < y

goal (2 subgoals):
 1. x < y \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
 2. \<not> x < y \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - 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> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
 2. \<not> proper_interval ao (Some x) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - 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> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
 2. \<not> proper_interval ao (Some x) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
hence "?lhs \<sqsubseteq>' ?rhs"
[PROOF STATE]
proof (prove)
using this:
proper_interval ao (Some x)

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

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

goal (2 subgoals):
 1. proper_interval ao (Some x) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
 2. \<not> proper_interval ao (Some x) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
proper_interval ao (Some x)
set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
proper_interval ao (Some x)
set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao

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

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - 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> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
have "set xs \<union> set (y # ys) \<subseteq> above (Some x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs \<union> set (y # ys) \<subseteq> above (Some x)
[PROOF STEP]
using True x_Min y_Min
[PROOF STATE]
proof (prove)
using this:
x < y
\<forall>x'\<in>set xs. x < x'
\<forall>y'\<in>set ys. y < y'

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
with True xs yys
[PROOF STATE]
proof (chain)
picking this:
x < y
sorted xs
distinct xs
sorted (y # ys)
distinct (y # ys)
set xs \<union> set (y # ys) \<subseteq> above (Some x)
[PROOF STEP]
have IH: "set_less_eq_aux_Compl (Some x) xs (y # ys) =
            (set xs \<sqsubseteq>' - set (y # ys) \<inter> above (Some x))"
[PROOF STATE]
proof (prove)
using this:
x < y
sorted xs
distinct xs
sorted (y # ys)
distinct (y # ys)
set xs \<union> set (y # ys) \<subseteq> above (Some x)

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
from True y_Min x_ao
[PROOF STATE]
proof (chain)
picking this:
x < y
\<forall>y'\<in>set ys. y < y'
x \<in> above ao
[PROOF STEP]
have "x \<in> - set (y # ys) \<inter> above ao"
[PROOF STATE]
proof (prove)
using this:
x < y
\<forall>y'\<in>set ys. y < y'
x \<in> above ao

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

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

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
- set (y # ys) \<inter> above ao \<noteq> {}

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
have "Min ?lhs = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (set (x # xs)) = x
[PROOF STEP]
using x_Min x_ao
[PROOF STATE]
proof (prove)
using this:
\<forall>x'\<in>set xs. x < x'
x \<in> above ao

goal (1 subgoal):
 1. Min (set (x # xs)) = x
[PROOF STEP]
by(auto intro!: Min_eqI)
[PROOF STATE]
proof (state)
this:
Min (set (x # xs)) = x

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Min (set (x # xs)) = x

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
have "Min ?rhs = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (- set (y # ys) \<inter> above ao) = x
[PROOF STEP]
using \<open>x < y\<close> y_Min x_ao False
[PROOF STATE]
proof (prove)
using this:
x < y
\<forall>y'\<in>set ys. y < y'
x \<in> above ao
\<not> proper_interval ao (Some x)

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Min (- set (y # ys) \<inter> above ao) = x

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
have "set xs = set xs - {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs = set xs - {x}
[PROOF STEP]
using ao x_Min
[PROOF STATE]
proof (prove)
using this:
set (x # xs) \<union> set (y # ys) \<subseteq> above ao
\<forall>x'\<in>set xs. x < x'

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

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
have "- set (y # ys) \<inter> above (Some x) = - set (y # ys) \<inter> above ao - {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - set (y # ys) \<inter> above (Some x) = - set (y # ys) \<inter> above ao - {x}
[PROOF STEP]
using False x_ao
[PROOF STATE]
proof (prove)
using this:
\<not> proper_interval ao (Some x)
x \<in> above ao

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
- set (y # ys) \<inter> above ao \<noteq> {}
Min (set (x # xs)) = x
Min (- set (y # ys) \<inter> above ao) = x
set xs = set xs - {x}
- set (y # ys) \<inter> above (Some x) = - set (y # ys) \<inter> above ao - {x}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
- set (y # ys) \<inter> above ao \<noteq> {}
Min (set (x # xs)) = x
Min (- set (y # ys) \<inter> above ao) = x
set xs = set xs - {x}
- set (y # ys) \<inter> above (Some x) = - set (y # ys) \<inter> above ao - {x}

goal (1 subgoal):
 1. set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
using True False IH
[PROOF STATE]
proof (prove)
using this:
- set (y # ys) \<inter> above ao \<noteq> {}
Min (set (x # xs)) = x
Min (- set (y # ys) \<inter> above ao) = x
set xs = set xs - {x}
- set (y # ys) \<inter> above (Some x) = - set (y # ys) \<inter> above ao - {x}
x < y
\<not> proper_interval ao (Some x)
set_less_eq_aux_Compl (Some x) xs (y # ys) = (set xs \<sqsubseteq>' - set (y # ys) \<inter> above (Some x))

goal (1 subgoal):
 1. set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
by(simp del: set_simps)(subst (2) set_less_eq_aux_rec, simp_all add: x_ao)
[PROOF STATE]
proof (state)
this:
set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)

goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - 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> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
proof(cases "y < x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y < x \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
 2. \<not> y < x \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y < x

goal (2 subgoals):
 1. y < x \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
 2. \<not> y < x \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - 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> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
 2. \<not> proper_interval ao (Some y) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - 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> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
 2. \<not> proper_interval ao (Some y) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
hence "?lhs \<sqsubseteq>' ?rhs"
[PROOF STATE]
proof (prove)
using this:
proper_interval ao (Some y)

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

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

goal (2 subgoals):
 1. proper_interval ao (Some y) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
 2. \<not> proper_interval ao (Some y) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
proper_interval ao (Some y)
set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
proper_interval ao (Some y)
set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao

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

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - 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> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
have "set (x # xs) \<union> set ys \<subseteq> above (Some y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (x # xs) \<union> set ys \<subseteq> above (Some y)
[PROOF STEP]
using \<open>y < x\<close> x_Min y_Min
[PROOF STATE]
proof (prove)
using this:
y < x
\<forall>x'\<in>set xs. x < x'
\<forall>y'\<in>set ys. y < y'

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
with \<open>\<not> x < y\<close> \<open>y < x\<close> xxs ys
[PROOF STATE]
proof (chain)
picking this:
\<not> x < y
y < x
sorted (x # xs)
distinct (x # xs)
sorted ys
distinct ys
set (x # xs) \<union> set ys \<subseteq> above (Some y)
[PROOF STEP]
have IH: "set_less_eq_aux_Compl (Some y) (x # xs) ys =
              (set (x # xs) \<sqsubseteq>' - set ys \<inter> above (Some y))"
[PROOF STATE]
proof (prove)
using this:
\<not> x < y
y < x
sorted (x # xs)
distinct (x # xs)
sorted ys
distinct ys
set (x # xs) \<union> set ys \<subseteq> above (Some y)

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set_less_eq_aux_Compl (Some y) (x # xs) ys = (set (x # xs) \<sqsubseteq>' - set ys \<inter> above (Some y))

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
have "- set ys \<inter> above (Some y) = ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - set ys \<inter> above (Some y) = - set (y # ys) \<inter> above ao
[PROOF STEP]
using y_ao False
[PROOF STATE]
proof (prove)
using this:
y \<in> above ao
\<not> proper_interval ao (Some y)

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - 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> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - 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> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
assume "proper_interval ao (Some y)"
[PROOF STATE]
proof (state)
this:
proper_interval ao (Some y)

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
hence "?lhs \<sqsubseteq>' ?rhs"
[PROOF STATE]
proof (prove)
using this:
proper_interval ao (Some y)

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

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

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
proper_interval ao (Some y) \<Longrightarrow> set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
proper_interval ao (Some y) \<Longrightarrow> set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
proper_interval ao (Some y) \<Longrightarrow> set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
assume "?lhs \<sqsubseteq>' ?rhs"
[PROOF STATE]
proof (state)
this:
set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
have "?lhs \<noteq> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (x # xs) \<noteq> - set (y # ys) \<inter> above ao
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (x # xs) = - set (y # ys) \<inter> above ao \<Longrightarrow> False
[PROOF STEP]
assume eq: "?lhs = ?rhs"
[PROOF STATE]
proof (state)
this:
set (x # xs) = - set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. set (x # xs) = - set (y # ys) \<inter> above ao \<Longrightarrow> False
[PROOF STEP]
have "x \<in> ?lhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set (x # xs)
[PROOF STEP]
using x_ao
[PROOF STATE]
proof (prove)
using this:
x \<in> above ao

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

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

goal (1 subgoal):
 1. set (x # xs) = - set (y # ys) \<inter> above ao \<Longrightarrow> False
[PROOF STEP]
note eq
[PROOF STATE]
proof (state)
this:
set (x # xs) = - set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. set (x # xs) = - set (y # ys) \<inter> above ao \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (x # xs) = - set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. set (x # xs) = - set (y # ys) \<inter> above ao \<Longrightarrow> False
[PROOF STEP]
note \<open>x = y\<close>
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. set (x # xs) = - set (y # ys) \<inter> above ao \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
y \<in> - set (y # ys) \<inter> above ao
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
y \<in> - set (y # ys) \<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:
set (x # xs) \<noteq> - set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao
set (x # xs) \<noteq> - set (y # ys) \<inter> above ao
[PROOF STEP]
obtain z where "z \<in> above ao" "z < y"
[PROOF STATE]
proof (prove)
using this:
set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao
set (x # xs) \<noteq> - set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> above ao; z < y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>x = y\<close> y_ao
[PROOF STATE]
proof (prove)
using this:
set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao
set (x # xs) \<noteq> - set (y # ys) \<inter> above ao
x = y
y \<in> above ao

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> above ao; z < y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce simp add: set_less_eq_aux_def set_less_aux_def not_le dest!: bspec[where x=y])
[PROOF STATE]
proof (state)
this:
z \<in> above ao
z < y

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
hence "proper_interval ao (Some y)"
[PROOF STATE]
proof (prove)
using this:
z \<in> above ao
z < y

goal (1 subgoal):
 1. proper_interval ao (Some y)
[PROOF STEP]
by(auto simp add: proper_interval_Some2)
[PROOF STATE]
proof (state)
this:
proper_interval ao (Some y)

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao \<Longrightarrow> proper_interval ao (Some y)

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set_less_eq_aux_Compl ao (x # xs) (y # ys) = (set (x # xs) \<sqsubseteq>' - set (y # ys) \<inter> above ao)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set_less_eq_aux_Compl ao xs ys = (set xs \<sqsubseteq>' - set ys \<inter> above ao)

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
set xs \<union> set ys \<subseteq> above ?ao2 \<Longrightarrow> set_less_eq_aux_Compl ?ao2 xs ys = (set xs \<sqsubseteq>' - set ys \<inter> above ?ao2)

goal (2 subgoals):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
 2. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
from this[of None]
[PROOF STATE]
proof (chain)
picking this:
set xs \<union> set ys \<subseteq> above None \<Longrightarrow> set_less_eq_aux_Compl None xs ys = (set xs \<sqsubseteq>' - set ys \<inter> above None)
[PROOF STEP]
show ?Compl2
[PROOF STATE]
proof (prove)
using this:
set xs \<union> set ys \<subseteq> above None \<Longrightarrow> set_less_eq_aux_Compl None xs ys = (set xs \<sqsubseteq>' - set ys \<inter> above None)

goal (1 subgoal):
 1. (set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys

goal (1 subgoal):
 1. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(set xs \<sqsubseteq>' - set ys) = set_less_eq_aux_Compl None xs ys

goal (1 subgoal):
 1. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
fix ao
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
assume "set xs \<union> set ys \<subseteq> above ao"
[PROOF STATE]
proof (state)
this:
set xs \<union> set ys \<subseteq> above ao

goal (1 subgoal):
 1. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
with xs ys
[PROOF STATE]
proof (chain)
picking this:
sorted xs
distinct xs
sorted ys
distinct ys
set xs \<union> set ys \<subseteq> above ao
[PROOF STEP]
have "Compl_set_less_eq_aux ao xs ys \<longleftrightarrow> (- set xs) \<inter> above ao \<sqsubseteq>' set ys"
[PROOF STATE]
proof (prove)
using this:
sorted xs
distinct xs
sorted ys
distinct ys
set xs \<union> set ys \<subseteq> above ao

goal (1 subgoal):
 1. Compl_set_less_eq_aux ao xs ys = (- set xs \<inter> above ao \<sqsubseteq>' set ys)
[PROOF STEP]
proof(induction ao xs ys rule: Compl_set_less_eq_aux.induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>ao. \<lbrakk>sorted []; distinct []; sorted []; distinct []; set [] \<union> set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao [] [] = (- set [] \<inter> above ao \<sqsubseteq>' set [])
 2. \<And>ao y ys. \<lbrakk>\<lbrakk>sorted []; distinct []; sorted ys; distinct ys; set [] \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) [] ys = (- set [] \<inter> above (Some y) \<sqsubseteq>' set ys); sorted []; distinct []; sorted (y # ys); distinct (y # ys); set [] \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
 3. \<And>ao x xs. \<lbrakk>\<lbrakk>sorted xs; distinct xs; sorted []; distinct []; set xs \<union> set [] \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs [] = (- set xs \<inter> above (Some x) \<sqsubseteq>' set []); sorted (x # xs); distinct (x # xs); sorted []; distinct []; set (x # xs) \<union> set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
 4. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
sorted []
distinct []
sorted []
distinct []
set [] \<union> set [] \<subseteq> above ao_

goal (4 subgoals):
 1. \<And>ao. \<lbrakk>sorted []; distinct []; sorted []; distinct []; set [] \<union> set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao [] [] = (- set [] \<inter> above ao \<sqsubseteq>' set [])
 2. \<And>ao y ys. \<lbrakk>\<lbrakk>sorted []; distinct []; sorted ys; distinct ys; set [] \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) [] ys = (- set [] \<inter> above (Some y) \<sqsubseteq>' set ys); sorted []; distinct []; sorted (y # ys); distinct (y # ys); set [] \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
 3. \<And>ao x xs. \<lbrakk>\<lbrakk>sorted xs; distinct xs; sorted []; distinct []; set xs \<union> set [] \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs [] = (- set xs \<inter> above (Some x) \<sqsubseteq>' set []); sorted (x # xs); distinct (x # xs); sorted []; distinct []; set (x # xs) \<union> set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
 4. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
sorted []
distinct []
sorted []
distinct []
set [] \<union> set [] \<subseteq> above ao_

goal (1 subgoal):
 1. Compl_set_less_eq_aux ao_ [] [] = (- set [] \<inter> above ao_ \<sqsubseteq>' set [])
[PROOF STEP]
by(simp add: proper_interval_None2)
[PROOF STATE]
proof (state)
this:
Compl_set_less_eq_aux ao_ [] [] = (- set [] \<inter> above ao_ \<sqsubseteq>' set [])

goal (3 subgoals):
 1. \<And>ao y ys. \<lbrakk>\<lbrakk>sorted []; distinct []; sorted ys; distinct ys; set [] \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) [] ys = (- set [] \<inter> above (Some y) \<sqsubseteq>' set ys); sorted []; distinct []; sorted (y # ys); distinct (y # ys); set [] \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
 2. \<And>ao x xs. \<lbrakk>\<lbrakk>sorted xs; distinct xs; sorted []; distinct []; set xs \<union> set [] \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs [] = (- set xs \<inter> above (Some x) \<sqsubseteq>' set []); sorted (x # xs); distinct (x # xs); sorted []; distinct []; set (x # xs) \<union> set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
 3. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ao y ys. \<lbrakk>\<lbrakk>sorted []; distinct []; sorted ys; distinct ys; set [] \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) [] ys = (- set [] \<inter> above (Some y) \<sqsubseteq>' set ys); sorted []; distinct []; sorted (y # ys); distinct (y # ys); set [] \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
 2. \<And>ao x xs. \<lbrakk>\<lbrakk>sorted xs; distinct xs; sorted []; distinct []; set xs \<union> set [] \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs [] = (- set xs \<inter> above (Some x) \<sqsubseteq>' set []); sorted (x # xs); distinct (x # xs); sorted []; distinct []; set (x # xs) \<union> set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
 3. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
case (2 ao y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>sorted []; distinct []; sorted ys; distinct ys; set [] \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) [] ys = (- set [] \<inter> above (Some y) \<sqsubseteq>' set ys)
sorted []
distinct []
sorted (y # ys)
distinct (y # ys)
set [] \<union> set (y # ys) \<subseteq> above ao

goal (3 subgoals):
 1. \<And>ao y ys. \<lbrakk>\<lbrakk>sorted []; distinct []; sorted ys; distinct ys; set [] \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) [] ys = (- set [] \<inter> above (Some y) \<sqsubseteq>' set ys); sorted []; distinct []; sorted (y # ys); distinct (y # ys); set [] \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
 2. \<And>ao x xs. \<lbrakk>\<lbrakk>sorted xs; distinct xs; sorted []; distinct []; set xs \<union> set [] \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs [] = (- set xs \<inter> above (Some x) \<sqsubseteq>' set []); sorted (x # xs); distinct (x # xs); sorted []; distinct []; set (x # xs) \<union> set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
 3. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
from \<open>sorted (y # ys)\<close> \<open>distinct (y # ys)\<close>
[PROOF STATE]
proof (chain)
picking this:
sorted (y # ys)
distinct (y # ys)
[PROOF STEP]
have 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 (3 subgoals):
 1. \<And>ao y ys. \<lbrakk>\<lbrakk>sorted []; distinct []; sorted ys; distinct ys; set [] \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) [] ys = (- set [] \<inter> above (Some y) \<sqsubseteq>' set ys); sorted []; distinct []; sorted (y # ys); distinct (y # ys); set [] \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
 2. \<And>ao x xs. \<lbrakk>\<lbrakk>sorted xs; distinct xs; sorted []; distinct []; set xs \<union> set [] \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs [] = (- set xs \<inter> above (Some x) \<sqsubseteq>' set []); sorted (x # xs); distinct (x # xs); sorted []; distinct []; set (x # xs) \<union> set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
 3. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
proof(cases "proper_interval ao (Some y)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
 2. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
proper_interval ao (Some y)

goal (2 subgoals):
 1. proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
 2. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
hence "\<not> - set [] \<inter> above ao \<sqsubseteq>' set (y # ys)"
[PROOF STATE]
proof (prove)
using this:
proper_interval ao (Some y)

goal (1 subgoal):
 1. \<not> - set [] \<inter> above ao \<sqsubseteq>' set (y # ys)
[PROOF STEP]
using y_Min
[PROOF STATE]
proof (prove)
using this:
proper_interval ao (Some y)
\<forall>y'\<in>set ys. y < y'

goal (1 subgoal):
 1. \<not> - set [] \<inter> above ao \<sqsubseteq>' set (y # ys)
[PROOF STEP]
by -(erule proper_interval_not_set_less_eq_auxI, auto)
[PROOF STATE]
proof (state)
this:
\<not> - set [] \<inter> above ao \<sqsubseteq>' set (y # ys)

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

goal (1 subgoal):
 1. Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
\<not> - set [] \<inter> above ao \<sqsubseteq>' set (y # ys)
proper_interval ao (Some y)

goal (1 subgoal):
 1. Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[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> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
note ao = \<open>set [] \<union> set (y # ys) \<subseteq> above ao\<close>
[PROOF STATE]
proof (state)
this:
set [] \<union> set (y # ys) \<subseteq> above ao

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
hence y_ao: "y \<in> above ao"
[PROOF STATE]
proof (prove)
using this:
set [] \<union> set (y # ys) \<subseteq> above ao

goal (1 subgoal):
 1. y \<in> above ao
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y \<in> above ao

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
from ao y_Min
[PROOF STATE]
proof (chain)
picking this:
set [] \<union> set (y # ys) \<subseteq> above ao
\<forall>y'\<in>set ys. y < y'
[PROOF STEP]
have "set [] \<union> set ys \<subseteq> above (Some y)"
[PROOF STATE]
proof (prove)
using this:
set [] \<union> set (y # ys) \<subseteq> above ao
\<forall>y'\<in>set ys. y < y'

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
with \<open>sorted []\<close> \<open>distinct []\<close> ys
[PROOF STATE]
proof (chain)
picking this:
sorted []
distinct []
sorted ys
distinct ys
set [] \<union> set ys \<subseteq> above (Some y)
[PROOF STEP]
have "Compl_set_less_eq_aux (Some y) [] ys \<longleftrightarrow> - set [] \<inter> above (Some y) \<sqsubseteq>' set ys"
[PROOF STATE]
proof (prove)
using this:
sorted []
distinct []
sorted ys
distinct ys
set [] \<union> set ys \<subseteq> above (Some y)

goal (1 subgoal):
 1. Compl_set_less_eq_aux (Some y) [] ys = (- set [] \<inter> above (Some y) \<sqsubseteq>' set ys)
[PROOF STEP]
by(rule "2.IH")
[PROOF STATE]
proof (state)
this:
Compl_set_less_eq_aux (Some y) [] ys = (- set [] \<inter> above (Some y) \<sqsubseteq>' set ys)

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Compl_set_less_eq_aux (Some y) [] ys = (- set [] \<inter> above (Some y) \<sqsubseteq>' set ys)

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
have "above ao \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. above ao \<noteq> {}
[PROOF STEP]
using y_ao
[PROOF STATE]
proof (prove)
using this:
y \<in> above ao

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
above ao \<noteq> {}

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
have "Min (above ao) = y"
          and "Min (set (y # ys)) = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (above ao) = y &&& Min (set (y # ys)) = y
[PROOF STEP]
using y_ao False ao
[PROOF STATE]
proof (prove)
using this:
y \<in> above ao
\<not> proper_interval ao (Some y)
set [] \<union> set (y # ys) \<subseteq> above ao

goal (1 subgoal):
 1. Min (above ao) = y &&& Min (set (y # ys)) = y
[PROOF STEP]
by(auto intro!: Min_eqI simp add: proper_interval_Some2 not_less)
[PROOF STATE]
proof (state)
this:
Min (above ao) = y
Min (set (y # ys)) = y

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Min (above ao) = y
Min (set (y # ys)) = y

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
have "above ao - {y} = above (Some y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. above ao - {y} = above (Some y)
[PROOF STEP]
using False y_ao
[PROOF STATE]
proof (prove)
using this:
\<not> proper_interval ao (Some y)
y \<in> above ao

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
above ao - {y} = above (Some y)

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
have "set ys - {y} = set ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ys - {y} = set ys
[PROOF STEP]
using y_Min y_ao
[PROOF STATE]
proof (prove)
using this:
\<forall>y'\<in>set ys. y < y'
y \<in> above ao

goal (1 subgoal):
 1. set ys - {y} = set ys
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
set ys - {y} = set ys

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Compl_set_less_eq_aux (Some y) [] ys = (- set [] \<inter> above (Some y) \<sqsubseteq>' set ys)
above ao \<noteq> {}
Min (above ao) = y
Min (set (y # ys)) = y
above ao - {y} = above (Some y)
set ys - {y} = set ys
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Compl_set_less_eq_aux (Some y) [] ys = (- set [] \<inter> above (Some y) \<sqsubseteq>' set ys)
above ao \<noteq> {}
Min (above ao) = y
Min (set (y # ys)) = y
above ao - {y} = above (Some y)
set ys - {y} = set ys

goal (1 subgoal):
 1. Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
using False y_ao
[PROOF STATE]
proof (prove)
using this:
Compl_set_less_eq_aux (Some y) [] ys = (- set [] \<inter> above (Some y) \<sqsubseteq>' set ys)
above ao \<noteq> {}
Min (above ao) = y
Min (set (y # ys)) = y
above ao - {y} = above (Some y)
set ys - {y} = set ys
\<not> proper_interval ao (Some y)
y \<in> above ao

goal (1 subgoal):
 1. Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
by(simp)(subst (2) set_less_eq_aux_rec, simp_all)
[PROOF STATE]
proof (state)
this:
Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Compl_set_less_eq_aux ao [] (y # ys) = (- set [] \<inter> above ao \<sqsubseteq>' set (y # ys))

goal (2 subgoals):
 1. \<And>ao x xs. \<lbrakk>\<lbrakk>sorted xs; distinct xs; sorted []; distinct []; set xs \<union> set [] \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs [] = (- set xs \<inter> above (Some x) \<sqsubseteq>' set []); sorted (x # xs); distinct (x # xs); sorted []; distinct []; set (x # xs) \<union> set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
 2. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ao x xs. \<lbrakk>\<lbrakk>sorted xs; distinct xs; sorted []; distinct []; set xs \<union> set [] \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs [] = (- set xs \<inter> above (Some x) \<sqsubseteq>' set []); sorted (x # xs); distinct (x # xs); sorted []; distinct []; set (x # xs) \<union> set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
 2. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
case (3 ao x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>sorted xs; distinct xs; sorted []; distinct []; set xs \<union> set [] \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs [] = (- set xs \<inter> above (Some x) \<sqsubseteq>' set [])
sorted (x # xs)
distinct (x # xs)
sorted []
distinct []
set (x # xs) \<union> set [] \<subseteq> above ao

goal (2 subgoals):
 1. \<And>ao x xs. \<lbrakk>\<lbrakk>sorted xs; distinct xs; sorted []; distinct []; set xs \<union> set [] \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs [] = (- set xs \<inter> above (Some x) \<sqsubseteq>' set []); sorted (x # xs); distinct (x # xs); sorted []; distinct []; set (x # xs) \<union> set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
 2. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
from \<open>sorted (x # xs)\<close> \<open>distinct (x # xs)\<close>
[PROOF STATE]
proof (chain)
picking this:
sorted (x # xs)
distinct (x # xs)
[PROOF STEP]
have 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 (2 subgoals):
 1. \<And>ao x xs. \<lbrakk>\<lbrakk>sorted xs; distinct xs; sorted []; distinct []; set xs \<union> set [] \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs [] = (- set xs \<inter> above (Some x) \<sqsubseteq>' set []); sorted (x # xs); distinct (x # xs); sorted []; distinct []; set (x # xs) \<union> set [] \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
 2. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
[PROOF STEP]
proof(cases "proper_interval ao (Some x)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
 2. \<not> proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
proper_interval ao (Some x)

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

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

goal (2 subgoals):
 1. proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
 2. \<not> proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
[PROOF STEP]
hence "z \<in> - set (x # xs) \<inter> above ao"
[PROOF STATE]
proof (prove)
using this:
z \<in> above ao
z < x

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

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

goal (2 subgoals):
 1. proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
 2. \<not> proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
z \<in> - set (x # xs) \<inter> above ao

goal (1 subgoal):
 1. Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
z \<in> - set (x # xs) \<inter> above ao
proper_interval ao (Some x)

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
[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> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
[PROOF STEP]
note ao = \<open>set (x # xs) \<union> set [] \<subseteq> above ao\<close>
[PROOF STATE]
proof (state)
this:
set (x # xs) \<union> set [] \<subseteq> above ao

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
[PROOF STEP]
hence x_ao: "x \<in> above ao"
[PROOF STATE]
proof (prove)
using this:
set (x # xs) \<union> set [] \<subseteq> above ao

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
[PROOF STEP]
from ao
[PROOF STATE]
proof (chain)
picking this:
set (x # xs) \<union> set [] \<subseteq> above ao
[PROOF STEP]
have "set xs \<union> set [] \<subseteq> above (Some x)"
[PROOF STATE]
proof (prove)
using this:
set (x # xs) \<union> set [] \<subseteq> above ao

goal (1 subgoal):
 1. set xs \<union> set [] \<subseteq> above (Some x)
[PROOF STEP]
using x_Min
[PROOF STATE]
proof (prove)
using this:
set (x # xs) \<union> set [] \<subseteq> above ao
\<forall>x'\<in>set xs. x < x'

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
[PROOF STEP]
with xs \<open>sorted []\<close> \<open>distinct []\<close>
[PROOF STATE]
proof (chain)
picking this:
sorted xs
distinct xs
sorted []
distinct []
set xs \<union> set [] \<subseteq> above (Some x)
[PROOF STEP]
have "Compl_set_less_eq_aux (Some x) xs [] \<longleftrightarrow>
          - set xs \<inter> above (Some x) \<sqsubseteq>' set []"
[PROOF STATE]
proof (prove)
using this:
sorted xs
distinct xs
sorted []
distinct []
set xs \<union> set [] \<subseteq> above (Some x)

goal (1 subgoal):
 1. Compl_set_less_eq_aux (Some x) xs [] = (- set xs \<inter> above (Some x) \<sqsubseteq>' set [])
[PROOF STEP]
by(rule "3.IH")
[PROOF STATE]
proof (state)
this:
Compl_set_less_eq_aux (Some x) xs [] = (- set xs \<inter> above (Some x) \<sqsubseteq>' set [])

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Compl_set_less_eq_aux (Some x) xs [] = (- set xs \<inter> above (Some x) \<sqsubseteq>' set [])

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
[PROOF STEP]
have "- set (x # xs) \<inter> above ao = - set xs \<inter> above (Some x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - set (x # xs) \<inter> above ao = - set xs \<inter> above (Some x)
[PROOF STEP]
using False x_ao
[PROOF STATE]
proof (prove)
using this:
\<not> proper_interval ao (Some x)
x \<in> above ao

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Compl_set_less_eq_aux (Some x) xs [] = (- set xs \<inter> above (Some x) \<sqsubseteq>' set [])
- set (x # xs) \<inter> above ao = - set xs \<inter> above (Some x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Compl_set_less_eq_aux (Some x) xs [] = (- set xs \<inter> above (Some x) \<sqsubseteq>' set [])
- set (x # xs) \<inter> above ao = - set xs \<inter> above (Some x)

goal (1 subgoal):
 1. Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
Compl_set_less_eq_aux (Some x) xs [] = (- set xs \<inter> above (Some x) \<sqsubseteq>' set [])
- set (x # xs) \<inter> above ao = - set xs \<inter> above (Some x)
\<not> proper_interval ao (Some x)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Compl_set_less_eq_aux ao (x # xs) [] = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set [])

goal (1 subgoal):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[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; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
case (4 ao x xs y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys))
\<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys)
sorted (x # xs)
distinct (x # xs)
sorted (y # ys)
distinct (y # ys)
set (x # xs) \<union> set (y # ys) \<subseteq> above ao

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

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

goal (1 subgoal):
 1. x \<in> above ao &&& y \<in> above ao
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
x \<in> above ao
y \<in> above ao

goal (1 subgoal):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[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; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[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; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[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; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[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; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
let ?lhs = "- set (x # xs) \<inter> above ao" and ?rhs = "set (y # ys)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ao x xs y ys. \<lbrakk>\<lbrakk>x < y; sorted xs; distinct xs; sorted (y # ys); distinct (y # ys); set xs \<union> set (y # ys) \<subseteq> above (Some x)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys)); \<lbrakk>\<not> x < y; y < x; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys; set (x # xs) \<union> set ys \<subseteq> above (Some y)\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys); set (x # xs) \<union> set (y # ys) \<subseteq> above ao\<rbrakk> \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
proof(cases "x < y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x < y \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
 2. \<not> x < y \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x < y

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

goal (2 subgoals):
 1. proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
 2. \<not> proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
hence "\<not> ?lhs \<sqsubseteq>' ?rhs"
[PROOF STATE]
proof (prove)
using this:
proper_interval ao (Some x)

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

goal (1 subgoal):
 1. \<not> - set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys)
[PROOF STEP]
by -(erule proper_interval_not_set_less_eq_auxI, auto)
[PROOF STATE]
proof (state)
this:
\<not> - set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys)

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

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

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[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> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
have "set xs \<union> set (y # ys) \<subseteq> above (Some x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs \<union> set (y # ys) \<subseteq> above (Some x)
[PROOF STEP]
using ao x_Min y_Min True
[PROOF STATE]
proof (prove)
using this:
set (x # xs) \<union> set (y # ys) \<subseteq> above ao
\<forall>x'\<in>set xs. x < x'
\<forall>y'\<in>set ys. y < y'
x < y

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
with True xs yys
[PROOF STATE]
proof (chain)
picking this:
x < y
sorted xs
distinct xs
sorted (y # ys)
distinct (y # ys)
set xs \<union> set (y # ys) \<subseteq> above (Some x)
[PROOF STEP]
have "Compl_set_less_eq_aux (Some x) xs (y # ys) \<longleftrightarrow>
            - set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys)"
[PROOF STATE]
proof (prove)
using this:
x < y
sorted xs
distinct xs
sorted (y # ys)
distinct (y # ys)
set xs \<union> set (y # ys) \<subseteq> above (Some x)

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys))

goal (1 subgoal):
 1. \<not> proper_interval ao (Some x) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
have "- set xs \<inter> above (Some x) = ?lhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - set xs \<inter> above (Some x) = - set (x # xs) \<inter> above ao
[PROOF STEP]
using x_ao False
[PROOF STATE]
proof (prove)
using this:
x \<in> above ao
\<not> proper_interval ao (Some x)

goal (1 subgoal):
 1. - set xs \<inter> above (Some x) = - set (x # xs) \<inter> above ao
[PROOF STEP]
by(auto intro: above_upclosed simp add: proper_interval_Some2)
[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> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys))
- set xs \<inter> above (Some x) = - set (x # xs) \<inter> above ao
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Compl_set_less_eq_aux (Some x) xs (y # ys) = (- set xs \<inter> above (Some x) \<sqsubseteq>' set (y # ys))
- set xs \<inter> above (Some x) = - set (x # xs) \<inter> above ao

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))

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

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

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

goal (2 subgoals):
 1. proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
 2. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
hence "\<not> ?lhs \<sqsubseteq>' ?rhs"
[PROOF STATE]
proof (prove)
using this:
proper_interval ao (Some y)

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

goal (1 subgoal):
 1. \<not> - set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys)
[PROOF STEP]
by -(erule proper_interval_not_set_less_eq_auxI, auto)
[PROOF STATE]
proof (state)
this:
\<not> - set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys)

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

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

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[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> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
from ao True x_Min y_Min
[PROOF STATE]
proof (chain)
picking this:
set (x # xs) \<union> set (y # ys) \<subseteq> above ao
y < x
\<forall>x'\<in>set xs. x < x'
\<forall>y'\<in>set ys. y < y'
[PROOF STEP]
have "set (x # xs) \<union> set ys \<subseteq> above (Some y)"
[PROOF STATE]
proof (prove)
using this:
set (x # xs) \<union> set (y # ys) \<subseteq> above ao
y < x
\<forall>x'\<in>set xs. x < x'
\<forall>y'\<in>set ys. y < y'

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
with \<open>\<not> x < y\<close> True xxs ys
[PROOF STATE]
proof (chain)
picking this:
\<not> x < y
y < x
sorted (x # xs)
distinct (x # xs)
sorted ys
distinct ys
set (x # xs) \<union> set ys \<subseteq> above (Some y)
[PROOF STEP]
have "Compl_set_less_eq_aux (Some y) (x # xs) ys \<longleftrightarrow>
              - set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys"
[PROOF STATE]
proof (prove)
using this:
\<not> x < y
y < x
sorted (x # xs)
distinct (x # xs)
sorted ys
distinct ys
set (x # xs) \<union> set ys \<subseteq> above (Some y)

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys)

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
have "y \<in> ?lhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> - set (x # xs) \<inter> above ao
[PROOF STEP]
using True x_Min y_ao
[PROOF STATE]
proof (prove)
using this:
y < x
\<forall>x'\<in>set xs. x < x'
y \<in> 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> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
hence "?lhs \<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> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
- set (x # xs) \<inter> above ao \<noteq> {}

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
have "Min ?lhs = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (- set (x # xs) \<inter> above ao) = y
[PROOF STEP]
using True False x_Min y_ao
[PROOF STATE]
proof (prove)
using this:
y < x
\<not> proper_interval ao (Some y)
\<forall>x'\<in>set xs. x < x'
y \<in> above ao

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Min (- set (x # xs) \<inter> above ao) = y

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
have "Min ?rhs = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (set (y # ys)) = y
[PROOF STEP]
using y_Min y_ao
[PROOF STATE]
proof (prove)
using this:
\<forall>y'\<in>set ys. y < y'
y \<in> above ao

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Min (set (y # ys)) = y

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
have "- set (x # xs) \<inter> above (Some y) = ?lhs - {y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - set (x # xs) \<inter> above (Some y) = - set (x # xs) \<inter> above ao - {y}
[PROOF STEP]
using y_ao False
[PROOF STATE]
proof (prove)
using this:
y \<in> above ao
\<not> proper_interval ao (Some y)

goal (1 subgoal):
 1. - set (x # xs) \<inter> above (Some y) = - set (x # xs) \<inter> above ao - {y}
[PROOF STEP]
by(auto intro: above_upclosed simp add: proper_interval_Some2)
[PROOF STATE]
proof (state)
this:
- set (x # xs) \<inter> above (Some y) = - set (x # xs) \<inter> above ao - {y}

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

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
have "set ys = set ys - {y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ys = set ys - {y}
[PROOF STEP]
using y_ao y_Min
[PROOF STATE]
proof (prove)
using this:
y \<in> above ao
\<forall>y'\<in>set ys. y < y'

goal (1 subgoal):
 1. set ys = set ys - {y}
[PROOF STEP]
by(auto intro: above_upclosed)
[PROOF STATE]
proof (state)
this:
set ys = set ys - {y}

goal (1 subgoal):
 1. \<not> proper_interval ao (Some y) \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys)
- set (x # xs) \<inter> above ao \<noteq> {}
Min (- set (x # xs) \<inter> above ao) = y
Min (set (y # ys)) = y
- set (x # xs) \<inter> above (Some y) = - set (x # xs) \<inter> above ao - {y}
set ys = set ys - {y}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys)
- set (x # xs) \<inter> above ao \<noteq> {}
Min (- set (x # xs) \<inter> above ao) = y
Min (set (y # ys)) = y
- set (x # xs) \<inter> above (Some y) = - set (x # xs) \<inter> above ao - {y}
set ys = set ys - {y}

goal (1 subgoal):
 1. Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
using True False \<open>\<not> x < y\<close> y_ao
[PROOF STATE]
proof (prove)
using this:
Compl_set_less_eq_aux (Some y) (x # xs) ys = (- set (x # xs) \<inter> above (Some y) \<sqsubseteq>' set ys)
- set (x # xs) \<inter> above ao \<noteq> {}
Min (- set (x # xs) \<inter> above ao) = y
Min (set (y # ys)) = y
- set (x # xs) \<inter> above (Some y) = - set (x # xs) \<inter> above ao - {y}
set ys = set ys - {y}
y < x
\<not> proper_interval ao (Some y)
\<not> x < y
y \<in> above ao

goal (1 subgoal):
 1. Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
by(simp)(subst (2) set_less_eq_aux_rec, simp_all)
[PROOF STATE]
proof (state)
this:
Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))

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

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[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> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
assume "proper_interval ao (Some y)"
[PROOF STATE]
proof (state)
this:
proper_interval ao (Some y)

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
hence "\<not> ?lhs \<sqsubseteq>' ?rhs"
[PROOF STATE]
proof (prove)
using this:
proper_interval ao (Some y)

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

goal (1 subgoal):
 1. \<not> - set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys)
[PROOF STEP]
by -(erule proper_interval_not_set_less_eq_auxI, auto)
[PROOF STATE]
proof (state)
this:
\<not> - set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys)

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
proper_interval ao (Some y) \<Longrightarrow> \<not> - set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys)

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
proper_interval ao (Some y) \<Longrightarrow> \<not> - set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys)

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
proper_interval ao (Some y) \<Longrightarrow> \<not> - set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys)

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
assume "\<not> ?lhs \<sqsubseteq>' ?rhs"
[PROOF STATE]
proof (state)
this:
\<not> - set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys)

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<not> - set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys)

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
have "?rhs = set (y # ys) \<inter> above ao"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (y # ys) = set (y # ys) \<inter> above ao
[PROOF STEP]
using ao
[PROOF STATE]
proof (prove)
using this:
set (x # xs) \<union> set (y # ys) \<subseteq> above ao

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

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<not> - set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys) \<inter> above ao
[PROOF STEP]
obtain z where "z \<in> above ao" "z < y"
[PROOF STATE]
proof (prove)
using this:
\<not> - set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys) \<inter> above ao

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> above ao; z < y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>x = y\<close> x_ao x_Min[unfolded Ball_def]
[PROOF STATE]
proof (prove)
using this:
\<not> - set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys) \<inter> above ao
x = y
x \<in> above ao
\<forall>xa. xa \<in> set xs \<longrightarrow> x < xa

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> above ao; z < y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce simp add: set_less_eq_aux_def set_less_aux_def simp add: less_le not_le dest!: bspec[where x=y])
[PROOF STATE]
proof (state)
this:
z \<in> above ao
z < y

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
hence "proper_interval ao (Some y)"
[PROOF STATE]
proof (prove)
using this:
z \<in> above ao
z < y

goal (1 subgoal):
 1. proper_interval ao (Some y)
[PROOF STEP]
by(auto simp add: proper_interval_Some2)
[PROOF STATE]
proof (state)
this:
proper_interval ao (Some y)

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> - set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys) \<Longrightarrow> proper_interval ao (Some y)

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Compl_set_less_eq_aux ao (x # xs) (y # ys) = (- set (x # xs) \<inter> above ao \<sqsubseteq>' set (y # ys))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Compl_set_less_eq_aux ao xs ys = (- set xs \<inter> above ao \<sqsubseteq>' set ys)

goal (1 subgoal):
 1. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
set xs \<union> set ys \<subseteq> above ?ao2 \<Longrightarrow> Compl_set_less_eq_aux ?ao2 xs ys = (- set xs \<inter> above ?ao2 \<sqsubseteq>' set ys)

goal (1 subgoal):
 1. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
from this[of None]
[PROOF STATE]
proof (chain)
picking this:
set xs \<union> set ys \<subseteq> above None \<Longrightarrow> Compl_set_less_eq_aux None xs ys = (- set xs \<inter> above None \<sqsubseteq>' set ys)
[PROOF STEP]
show ?Compl1
[PROOF STATE]
proof (prove)
using this:
set xs \<union> set ys \<subseteq> above None \<Longrightarrow> Compl_set_less_eq_aux None xs ys = (- set xs \<inter> above None \<sqsubseteq>' set ys)

goal (1 subgoal):
 1. (- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(- set xs \<sqsubseteq>' set ys) = Compl_set_less_eq_aux None xs ys

goal:
No subgoals!
[PROOF STEP]
qed