[STATEMENT]
lemma LLq_num:
assumes "\<phi> \<in> fmla" "q \<in> num" "Fvars \<phi> = {zz}" "\<forall> p \<in> num. prv (subst \<phi> p zz)"
shows "prv (all zz (imp (LLq (Var zz) q) \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prv (all zz (imp (LLq (Var zz) q) \<phi>))
[PROOF STEP]
using assms Lq_num
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
q \<in> num
Fvars \<phi> = {zz}
\<forall>p\<in>num. prv (subst \<phi> p zz)
let LLq = \<lambda>t1 t2. psubst Lq [(t1, zz), (t2, yy)] in \<forall>\<phi>\<in>fmla. \<forall>q\<in>num. Fvars \<phi> = {zz} \<and> (\<forall>p\<in>num. prv (subst \<phi> p zz)) \<longrightarrow> prv (all zz (imp (LLq (Var zz) q) \<phi>))

goal (1 subgoal):
 1. prv (all zz (imp (LLq (Var zz) q) \<phi>))
[PROOF STEP]
unfolding LLq_def
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> fmla
q \<in> num
Fvars \<phi> = {zz}
\<forall>p\<in>num. prv (subst \<phi> p zz)
let LLq = \<lambda>t1 t2. psubst Lq [(t1, zz), (t2, yy)] in \<forall>\<phi>\<in>fmla. \<forall>q\<in>num. Fvars \<phi> = {zz} \<and> (\<forall>p\<in>num. prv (subst \<phi> p zz)) \<longrightarrow> prv (all zz (imp (LLq (Var zz) q) \<phi>))

goal (1 subgoal):
 1. prv (all zz (imp (psubst Lq [(Var zz, zz), (q, yy)]) \<phi>))
[PROOF STEP]
by auto


[STATEMENT]
lemma LLq_num2:
assumes "p \<in> num"
shows "\<exists> P \<subseteq> num. finite P \<and> prv (dsj (sdsj {eql (Var yy) r | r. r \<in> P}) (LLq p (Var yy)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<subseteq>num. finite P \<and> prv (dsj (sdsj {eql (Var yy) r |r. r \<in> P}) (LLq p (Var yy)))
[PROOF STEP]
using assms Lq_num2
[PROOF STATE]
proof (prove)
using this:
p \<in> num
let LLq = \<lambda>t1 t2. psubst Lq [(t1, zz), (t2, yy)] in \<forall>p\<in>num. \<exists>P\<subseteq>num. finite P \<and> prv (dsj (sdsj {eql (Var yy) r |r. r \<in> P}) (LLq p (Var yy)))

goal (1 subgoal):
 1. \<exists>P\<subseteq>num. finite P \<and> prv (dsj (sdsj {eql (Var yy) r |r. r \<in> P}) (LLq p (Var yy)))
[PROOF STEP]
unfolding LLq_def
[PROOF STATE]
proof (prove)
using this:
p \<in> num
let LLq = \<lambda>t1 t2. psubst Lq [(t1, zz), (t2, yy)] in \<forall>p\<in>num. \<exists>P\<subseteq>num. finite P \<and> prv (dsj (sdsj {eql (Var yy) r |r. r \<in> P}) (LLq p (Var yy)))

goal (1 subgoal):
 1. \<exists>P\<subseteq>num. finite P \<and> prv (dsj (sdsj {eql (Var yy) r |r. r \<in> P}) (psubst Lq [(p, zz), (Var yy, yy)]))
[PROOF STEP]
by auto


[STATEMENT]
lemma not_in_complement_partition:
  "\<not> finite (UNIV :: 'a set)
  \<Longrightarrow> (A :: 'a set) \<notin> infinite_complement_partition \<longleftrightarrow> - A \<in> infinite_complement_partition"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite UNIV \<Longrightarrow> (A \<notin> infinite_complement_partition) = (- A \<in> infinite_complement_partition)
[PROOF STEP]
by(metis complement_partition)


[STATEMENT]
lemma not_in_complement_partition_False:
  "\<lbrakk> (A :: 'a set) \<in> infinite_complement_partition; \<not> finite (UNIV :: 'a set) \<rbrakk>
  \<Longrightarrow> - A \<in> infinite_complement_partition = False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> infinite_complement_partition; infinite UNIV\<rbrakk> \<Longrightarrow> (- A \<in> infinite_complement_partition) = False
[PROOF STEP]
by(simp add: not_in_complement_partition)


[STATEMENT]
lemma Compl_eq_empty_iff: "- A = {} \<longleftrightarrow> A = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- A = {}) = (A = UNIV)
[PROOF STEP]
by auto


[STATEMENT]
lemma set_less_aux_irrefl [iff]: "\<not> A \<sqsubset>' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> A \<sqsubset>' A
[PROOF STEP]
by(auto simp add: set_less_aux_def)


[STATEMENT]
lemma set_less_eq_aux_refl [iff]: "A \<sqsubseteq>' A \<longleftrightarrow> A \<in> infinite_complement_partition"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<sqsubseteq>' A) = (A \<in> infinite_complement_partition)
[PROOF STEP]
by(simp add: set_less_eq_aux_def)


[STATEMENT]
lemma set_less_aux_empty [simp]: "\<not> A \<sqsubset>' {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> A \<sqsubset>' {}
[PROOF STEP]
by(auto simp add: set_less_aux_def intro: finite_subset finite_complement_partition)


[STATEMENT]
lemma set_less_eq_aux_empty [simp]: "A \<sqsubseteq>' {} \<longleftrightarrow> A = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<sqsubseteq>' {}) = (A = {})
[PROOF STEP]
by(auto simp add: set_less_eq_aux_def finite_complement_partition)


[STATEMENT]
lemma set_less_aux_antisym: "\<lbrakk> A \<sqsubset>' B; B \<sqsubset>' A \<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<sqsubset>' B; B \<sqsubset>' A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by(auto simp add: set_less_aux_def split: if_split_asm)


[STATEMENT]
lemma set_less_aux_conv_set_less_eq_aux:
  "A \<sqsubset>' B \<longleftrightarrow> A \<sqsubseteq>' B \<and> \<not> B \<sqsubseteq>' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<sqsubset>' B) = (A \<sqsubseteq>' B \<and> \<not> B \<sqsubseteq>' A)
[PROOF STEP]
by(auto simp add: set_less_eq_aux_def dest: set_less_aux_antisym)


[STATEMENT]
lemma set_less_eq_aux_antisym: "\<lbrakk> A \<sqsubseteq>' B; B \<sqsubseteq>' A \<rbrakk> \<Longrightarrow> A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<sqsubseteq>' B; B \<sqsubseteq>' A\<rbrakk> \<Longrightarrow> A = B
[PROOF STEP]
by(auto simp add: set_less_eq_aux_def dest: set_less_aux_antisym)


[STATEMENT]
lemma set_less_aux_finiteD: "A \<sqsubset>' B \<Longrightarrow> finite A \<and> B \<in> infinite_complement_partition"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<sqsubset>' B \<Longrightarrow> finite A \<and> B \<in> infinite_complement_partition
[PROOF STEP]
by(auto simp add: set_less_aux_def finite_complement_partition)


[STATEMENT]
lemma set_less_eq_aux_infinite_complement_partitionD:
  "A \<sqsubseteq>' B \<Longrightarrow> A \<in> infinite_complement_partition \<and> B \<in> infinite_complement_partition"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<sqsubseteq>' B \<Longrightarrow> A \<in> infinite_complement_partition \<and> B \<in> infinite_complement_partition
[PROOF STEP]
by(auto simp add: set_less_eq_aux_def dest: set_less_aux_finiteD intro: finite_complement_partition)


[STATEMENT]
lemma Compl_set_less_aux_Compl:
  "finite (UNIV :: 'a set) \<Longrightarrow> - A \<sqsubset>' - B \<longleftrightarrow> B \<sqsubset>' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite UNIV \<Longrightarrow> (- A \<sqsubset>' - B) = (B \<sqsubset>' A)
[PROOF STEP]
by(auto simp add: set_less_aux_def finite_subset[OF subset_UNIV])


[STATEMENT]
lemma Compl_set_less_eq_aux_Compl:
  "finite (UNIV :: 'a set) \<Longrightarrow> - A \<sqsubseteq>' - B \<longleftrightarrow> B \<sqsubseteq>' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite UNIV \<Longrightarrow> (- A \<sqsubseteq>' - B) = (B \<sqsubseteq>' A)
[PROOF STEP]
by(auto simp add: set_less_eq_aux_def Compl_set_less_aux_Compl)


[STATEMENT]
lemma set_less_aux_insert_same:
  "x \<in> A \<longleftrightarrow> x \<in> B \<Longrightarrow> insert x A \<sqsubset>' insert x B \<longleftrightarrow> A \<sqsubset>' B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> A) = (x \<in> B) \<Longrightarrow> (insert x A \<sqsubset>' insert x B) = (A \<sqsubset>' B)
[PROOF STEP]
by(auto simp add: set_less_aux_def)


[STATEMENT]
lemma set_less_eq_aux_insert_same:
  "\<lbrakk> A \<in> infinite_complement_partition; insert x B \<in> infinite_complement_partition;
    x \<in> A \<longleftrightarrow> x \<in> B \<rbrakk>
  \<Longrightarrow> insert x A \<sqsubseteq>' insert x B \<longleftrightarrow> A \<sqsubseteq>' B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> infinite_complement_partition; insert x B \<in> infinite_complement_partition; (x \<in> A) = (x \<in> B)\<rbrakk> \<Longrightarrow> (insert x A \<sqsubseteq>' insert x B) = (A \<sqsubseteq>' B)
[PROOF STEP]
by(auto simp add: set_less_eq_aux_def set_less_aux_insert_same)


[STATEMENT]
lemma wlog_le [case_names sym le]:
  assumes "\<And>a b. P a b \<Longrightarrow> P b a"
  and "\<And>a b. a \<le> b \<Longrightarrow> P a b"
  shows "P b a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P b a
[PROOF STEP]
by (metis assms linear)


[STATEMENT]
lemma empty_set_less_aux [simp]: "{} \<sqsubset>' A \<longleftrightarrow> A \<noteq> {} \<and> finite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({} \<sqsubset>' A) = (A \<noteq> {} \<and> finite A)
[PROOF STEP]
by(auto 4 3 simp add: set_less_aux_def intro!: Min_eqI intro: bexI[where x="Min A"] order_trans[where y="Min A"] Min_in)


[STATEMENT]
lemma empty_set_less_eq_aux [simp]: "{} \<sqsubseteq>' A \<longleftrightarrow> finite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({} \<sqsubseteq>' A) = finite A
[PROOF STEP]
by(auto simp add: set_less_eq_aux_def finite_complement_partition)


[STATEMENT]
lemma set_less_eq_aux_trans [trans]:
  "\<lbrakk> A \<sqsubseteq>' B; B \<sqsubseteq>' C \<rbrakk> \<Longrightarrow> A \<sqsubseteq>' C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<sqsubseteq>' B; B \<sqsubseteq>' C\<rbrakk> \<Longrightarrow> A \<sqsubseteq>' C
[PROOF STEP]
by(auto simp add: set_less_eq_aux_def dest: set_less_aux_trans)


[STATEMENT]
lemma set_less_trans_set_less_eq [trans]:
  "\<lbrakk> A \<sqsubset>' B; B \<sqsubseteq>' C \<rbrakk> \<Longrightarrow> A \<sqsubset>' C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<sqsubset>' B; B \<sqsubseteq>' C\<rbrakk> \<Longrightarrow> A \<sqsubset>' C
[PROOF STEP]
by(auto simp add: set_less_eq_aux_def dest: set_less_aux_trans)


[STATEMENT]
lemma set_less_eq_aux_porder: "partial_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>' B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>' B}
[PROOF STEP]
by(auto simp add: preorder_on_def partial_order_on_def intro!: refl_onI transI antisymI dest: set_less_eq_aux_infinite_complement_partitionD intro: set_less_eq_aux_antisym set_less_eq_aux_trans del: equalityI)


[STATEMENT]
lemma psubset_finite_imp_set_less_aux:
  assumes AsB: "A \<subset> B" and B: "finite B"
  shows "A \<sqsubset>' B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<sqsubset>' B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<sqsubset>' B
[PROOF STEP]
from AsB B
[PROOF STATE]
proof (chain)
picking this:
A \<subset> B
finite B
[PROOF STEP]
have A: "finite A"
[PROOF STATE]
proof (prove)
using this:
A \<subset> B
finite B

goal (1 subgoal):
 1. finite A
[PROOF STEP]
by(auto intro: finite_subset)
[PROOF STATE]
proof (state)
this:
finite A

goal (1 subgoal):
 1. A \<sqsubset>' B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite A

goal (1 subgoal):
 1. A \<sqsubset>' B
[PROOF STEP]
from AsB B
[PROOF STATE]
proof (chain)
picking this:
A \<subset> B
finite B
[PROOF STEP]
have "Min (B - A) \<in> B - A"
[PROOF STATE]
proof (prove)
using this:
A \<subset> B
finite B

goal (1 subgoal):
 1. Min (B - A) \<in> B - A
[PROOF STEP]
by - (rule Min_in, auto)
[PROOF STATE]
proof (state)
this:
Min (B - A) \<in> B - A

goal (1 subgoal):
 1. A \<sqsubset>' B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite A
Min (B - A) \<in> B - A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite A
Min (B - A) \<in> B - A

goal (1 subgoal):
 1. A \<sqsubset>' B
[PROOF STEP]
using B AsB
[PROOF STATE]
proof (prove)
using this:
finite A
Min (B - A) \<in> B - A
finite B
A \<subset> B

goal (1 subgoal):
 1. A \<sqsubset>' B
[PROOF STEP]
by(auto simp add: set_less_aux_def intro!: rev_bexI[where x="Min (B - A)"] Min_eqI dest: Min_ge_iff[THEN iffD1, rotated 2])
[PROOF STATE]
proof (state)
this:
A \<sqsubset>' B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subset_finite_imp_set_less_eq_aux:
  "\<lbrakk> A \<subseteq> B; finite B \<rbrakk> \<Longrightarrow> A \<sqsubseteq>' B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> B; finite B\<rbrakk> \<Longrightarrow> A \<sqsubseteq>' B
[PROOF STEP]
by(cases "A = B")(auto simp add: set_less_eq_aux_def finite_complement_partition intro: psubset_finite_imp_set_less_aux)


[STATEMENT]
lemma empty_set_less_aux_finite_iff:
  "finite A \<Longrightarrow> {} \<sqsubset>' A \<longleftrightarrow> A \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> ({} \<sqsubset>' A) = (A \<noteq> {})
[PROOF STEP]
by(auto intro: psubset_finite_imp_set_less_aux)


[STATEMENT]
lemma set_less_aux_finite_total:
  assumes A: "finite A" and B: "finite B"
  shows "A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
proof(cases "A \<subseteq> B \<or> B \<subseteq> A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A \<subseteq> B \<or> B \<subseteq> A \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
 2. \<not> (A \<subseteq> B \<or> B \<subseteq> A) \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A \<subseteq> B \<or> B \<subseteq> A

goal (2 subgoals):
 1. A \<subseteq> B \<or> B \<subseteq> A \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
 2. \<not> (A \<subseteq> B \<or> B \<subseteq> A) \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> B \<or> B \<subseteq> A

goal (1 subgoal):
 1. A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
using A B psubset_finite_imp_set_less_aux[of A B] psubset_finite_imp_set_less_aux[of B A]
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> B \<or> B \<subseteq> A
finite A
finite B
\<lbrakk>A \<subset> B; finite B\<rbrakk> \<Longrightarrow> A \<sqsubset>' B
\<lbrakk>B \<subset> A; finite A\<rbrakk> \<Longrightarrow> B \<sqsubset>' A

goal (1 subgoal):
 1. A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A

goal (1 subgoal):
 1. \<not> (A \<subseteq> B \<or> B \<subseteq> A) \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (A \<subseteq> B \<or> B \<subseteq> A) \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (A \<subseteq> B \<or> B \<subseteq> A)

goal (1 subgoal):
 1. \<not> (A \<subseteq> B \<or> B \<subseteq> A) \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
hence A': "\<not> A \<subseteq> B" and B': "\<not> B \<subseteq> A" and AnB: "A \<noteq> B"
[PROOF STATE]
proof (prove)
using this:
\<not> (A \<subseteq> B \<or> B \<subseteq> A)

goal (1 subgoal):
 1. \<not> A \<subseteq> B &&& \<not> B \<subseteq> A &&& A \<noteq> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> A \<subseteq> B
\<not> B \<subseteq> A
A \<noteq> B

goal (1 subgoal):
 1. \<not> (A \<subseteq> B \<or> B \<subseteq> A) \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> A \<subseteq> B
\<not> B \<subseteq> A
A \<noteq> B

goal (1 subgoal):
 1. A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
using A B
[PROOF STATE]
proof (prove)
using this:
\<not> A \<subseteq> B
\<not> B \<subseteq> A
A \<noteq> B
finite A
finite B

goal (1 subgoal):
 1. A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
proof(induct "Min (B - A)" "Min (A - B)" arbitrary: A B rule: wlog_le)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A B. \<lbrakk>\<And>Aa Ba. \<lbrakk>Min (A - B) = Min (Ba - Aa); Min (B - A) = Min (Aa - Ba); \<not> Aa \<subseteq> Ba; \<not> Ba \<subseteq> Aa; Aa \<noteq> Ba; finite Aa; finite Ba\<rbrakk> \<Longrightarrow> Aa \<sqsubset>' Ba \<or> Aa = Ba \<or> Ba \<sqsubset>' Aa; \<not> A \<subseteq> B; \<not> B \<subseteq> A; A \<noteq> B; finite A; finite B\<rbrakk> \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
 2. \<And>A B. \<lbrakk>Min (B - A) \<le> Min (A - B); \<not> A \<subseteq> B; \<not> B \<subseteq> A; A \<noteq> B; finite A; finite B\<rbrakk> \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
case (sym m n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Min (m - n) = Min (?B - ?A); Min (n - m) = Min (?A - ?B); \<not> ?A \<subseteq> ?B; \<not> ?B \<subseteq> ?A; ?A \<noteq> ?B; finite ?A; finite ?B\<rbrakk> \<Longrightarrow> ?A \<sqsubset>' ?B \<or> ?A = ?B \<or> ?B \<sqsubset>' ?A
\<not> m \<subseteq> n
\<not> n \<subseteq> m
m \<noteq> n
finite m
finite n

goal (2 subgoals):
 1. \<And>A B. \<lbrakk>\<And>Aa Ba. \<lbrakk>Min (A - B) = Min (Ba - Aa); Min (B - A) = Min (Aa - Ba); \<not> Aa \<subseteq> Ba; \<not> Ba \<subseteq> Aa; Aa \<noteq> Ba; finite Aa; finite Ba\<rbrakk> \<Longrightarrow> Aa \<sqsubset>' Ba \<or> Aa = Ba \<or> Ba \<sqsubset>' Aa; \<not> A \<subseteq> B; \<not> B \<subseteq> A; A \<noteq> B; finite A; finite B\<rbrakk> \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
 2. \<And>A B. \<lbrakk>Min (B - A) \<le> Min (A - B); \<not> A \<subseteq> B; \<not> B \<subseteq> A; A \<noteq> B; finite A; finite B\<rbrakk> \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
from sym.hyps[OF refl refl] sym.prems
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> n \<subseteq> m; \<not> m \<subseteq> n; n \<noteq> m; finite n; finite m\<rbrakk> \<Longrightarrow> n \<sqsubset>' m \<or> n = m \<or> m \<sqsubset>' n
\<not> m \<subseteq> n
\<not> n \<subseteq> m
m \<noteq> n
finite m
finite n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> n \<subseteq> m; \<not> m \<subseteq> n; n \<noteq> m; finite n; finite m\<rbrakk> \<Longrightarrow> n \<sqsubset>' m \<or> n = m \<or> m \<sqsubset>' n
\<not> m \<subseteq> n
\<not> n \<subseteq> m
m \<noteq> n
finite m
finite n

goal (1 subgoal):
 1. m \<sqsubset>' n \<or> m = n \<or> n \<sqsubset>' m
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
m \<sqsubset>' n \<or> m = n \<or> n \<sqsubset>' m

goal (1 subgoal):
 1. \<And>A B. \<lbrakk>Min (B - A) \<le> Min (A - B); \<not> A \<subseteq> B; \<not> B \<subseteq> A; A \<noteq> B; finite A; finite B\<rbrakk> \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A B. \<lbrakk>Min (B - A) \<le> Min (A - B); \<not> A \<subseteq> B; \<not> B \<subseteq> A; A \<noteq> B; finite A; finite B\<rbrakk> \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
case (le A B)
[PROOF STATE]
proof (state)
this:
Min (B - A) \<le> Min (A - B)
\<not> A \<subseteq> B
\<not> B \<subseteq> A
A \<noteq> B
finite A
finite B

goal (1 subgoal):
 1. \<And>A B. \<lbrakk>Min (B - A) \<le> Min (A - B); \<not> A \<subseteq> B; \<not> B \<subseteq> A; A \<noteq> B; finite A; finite B\<rbrakk> \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
note A = \<open>finite A\<close> and B = \<open>finite B\<close>
      and A' = \<open>\<not> A \<subseteq> B\<close> and B' = \<open>\<not> B \<subseteq> A\<close>
[PROOF STATE]
proof (state)
this:
finite A
finite B
\<not> A \<subseteq> B
\<not> B \<subseteq> A

goal (1 subgoal):
 1. \<And>A B. \<lbrakk>Min (B - A) \<le> Min (A - B); \<not> A \<subseteq> B; \<not> B \<subseteq> A; A \<noteq> B; finite A; finite B\<rbrakk> \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
finite A
finite B
\<not> A \<subseteq> B
\<not> B \<subseteq> A

goal (1 subgoal):
 1. \<And>A B. \<lbrakk>Min (B - A) \<le> Min (A - B); \<not> A \<subseteq> B; \<not> B \<subseteq> A; A \<noteq> B; finite A; finite B\<rbrakk> \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A B. \<lbrakk>Min (B - A) \<le> Min (A - B); \<not> A \<subseteq> B; \<not> B \<subseteq> A; A \<noteq> B; finite A; finite B\<rbrakk> \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
assume z: "z \<in> (A - B) \<union> (B - A)"
[PROOF STATE]
proof (state)
this:
z \<in> A - B \<union> (B - A)

goal (1 subgoal):
 1. \<And>A B. \<lbrakk>Min (B - A) \<le> Min (A - B); \<not> A \<subseteq> B; \<not> B \<subseteq> A; A \<noteq> B; finite A; finite B\<rbrakk> \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
hence "Min (B - A) \<le> z \<and> (z \<le> Min (B - A) \<longrightarrow> Min (B - A) = z)"
[PROOF STATE]
proof (prove)
using this:
z \<in> A - B \<union> (B - A)

goal (1 subgoal):
 1. Min (B - A) \<le> z \<and> (z \<le> Min (B - A) \<longrightarrow> Min (B - A) = z)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z \<in> A - B \<Longrightarrow> Min (B - A) \<le> z \<and> (z \<le> Min (B - A) \<longrightarrow> Min (B - A) = z)
 2. z \<in> B - A \<Longrightarrow> Min (B - A) \<le> z \<and> (z \<le> Min (B - A) \<longrightarrow> Min (B - A) = z)
[PROOF STEP]
assume "z \<in> B - A"
[PROOF STATE]
proof (state)
this:
z \<in> B - A

goal (2 subgoals):
 1. z \<in> A - B \<Longrightarrow> Min (B - A) \<le> z \<and> (z \<le> Min (B - A) \<longrightarrow> Min (B - A) = z)
 2. z \<in> B - A \<Longrightarrow> Min (B - A) \<le> z \<and> (z \<le> Min (B - A) \<longrightarrow> Min (B - A) = z)
[PROOF STEP]
hence "Min (B - A) \<le> z"
[PROOF STATE]
proof (prove)
using this:
z \<in> B - A

goal (1 subgoal):
 1. Min (B - A) \<le> z
[PROOF STEP]
by(simp add: B)
[PROOF STATE]
proof (state)
this:
Min (B - A) \<le> z

goal (2 subgoals):
 1. z \<in> A - B \<Longrightarrow> Min (B - A) \<le> z \<and> (z \<le> Min (B - A) \<longrightarrow> Min (B - A) = z)
 2. z \<in> B - A \<Longrightarrow> Min (B - A) \<le> z \<and> (z \<le> Min (B - A) \<longrightarrow> Min (B - A) = z)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Min (B - A) \<le> z

goal (1 subgoal):
 1. Min (B - A) \<le> z \<and> (z \<le> Min (B - A) \<longrightarrow> Min (B - A) = z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Min (B - A) \<le> z \<and> (z \<le> Min (B - A) \<longrightarrow> Min (B - A) = z)

goal (1 subgoal):
 1. z \<in> A - B \<Longrightarrow> Min (B - A) \<le> z \<and> (z \<le> Min (B - A) \<longrightarrow> Min (B - A) = z)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<in> A - B \<Longrightarrow> Min (B - A) \<le> z \<and> (z \<le> Min (B - A) \<longrightarrow> Min (B - A) = z)
[PROOF STEP]
assume "z \<in> A - B"
[PROOF STATE]
proof (state)
this:
z \<in> A - B

goal (1 subgoal):
 1. z \<in> A - B \<Longrightarrow> Min (B - A) \<le> z \<and> (z \<le> Min (B - A) \<longrightarrow> Min (B - A) = z)
[PROOF STEP]
hence "Min (A - B) \<le> z"
[PROOF STATE]
proof (prove)
using this:
z \<in> A - B

goal (1 subgoal):
 1. Min (A - B) \<le> z
[PROOF STEP]
by(simp add: A)
[PROOF STATE]
proof (state)
this:
Min (A - B) \<le> z

goal (1 subgoal):
 1. z \<in> A - B \<Longrightarrow> Min (B - A) \<le> z \<and> (z \<le> Min (B - A) \<longrightarrow> Min (B - A) = z)
[PROOF STEP]
with le.hyps
[PROOF STATE]
proof (chain)
picking this:
Min (B - A) \<le> Min (A - B)
Min (A - B) \<le> z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Min (B - A) \<le> Min (A - B)
Min (A - B) \<le> z

goal (1 subgoal):
 1. Min (B - A) \<le> z \<and> (z \<le> Min (B - A) \<longrightarrow> Min (B - A) = z)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
Min (B - A) \<le> z \<and> (z \<le> Min (B - A) \<longrightarrow> Min (B - A) = z)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Min (B - A) \<le> z \<and> (z \<le> Min (B - A) \<longrightarrow> Min (B - A) = z)

goal (1 subgoal):
 1. \<And>A B. \<lbrakk>Min (B - A) \<le> Min (A - B); \<not> A \<subseteq> B; \<not> B \<subseteq> A; A \<noteq> B; finite A; finite B\<rbrakk> \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?z2 \<in> A - B \<union> (B - A) \<Longrightarrow> Min (B - A) \<le> ?z2 \<and> (?z2 \<le> Min (B - A) \<longrightarrow> Min (B - A) = ?z2)

goal (1 subgoal):
 1. \<And>A B. \<lbrakk>Min (B - A) \<le> Min (A - B); \<not> A \<subseteq> B; \<not> B \<subseteq> A; A \<noteq> B; finite A; finite B\<rbrakk> \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?z2 \<in> A - B \<union> (B - A) \<Longrightarrow> Min (B - A) \<le> ?z2 \<and> (?z2 \<le> Min (B - A) \<longrightarrow> Min (B - A) = ?z2)

goal (1 subgoal):
 1. \<And>A B. \<lbrakk>Min (B - A) \<le> Min (A - B); \<not> A \<subseteq> B; \<not> B \<subseteq> A; A \<noteq> B; finite A; finite B\<rbrakk> \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
have "Min (B - A) \<in> B - A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (B - A) \<in> B - A
[PROOF STEP]
by(rule Min_in)(simp_all add: B B')
[PROOF STATE]
proof (state)
this:
Min (B - A) \<in> B - A

goal (1 subgoal):
 1. \<And>A B. \<lbrakk>Min (B - A) \<le> Min (A - B); \<not> A \<subseteq> B; \<not> B \<subseteq> A; A \<noteq> B; finite A; finite B\<rbrakk> \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?z2 \<in> A - B \<union> (B - A) \<Longrightarrow> Min (B - A) \<le> ?z2 \<and> (?z2 \<le> Min (B - A) \<longrightarrow> Min (B - A) = ?z2)
Min (B - A) \<in> B - A
[PROOF STEP]
have "A \<sqsubset>' B"
[PROOF STATE]
proof (prove)
using this:
?z2 \<in> A - B \<union> (B - A) \<Longrightarrow> Min (B - A) \<le> ?z2 \<and> (?z2 \<le> Min (B - A) \<longrightarrow> Min (B - A) = ?z2)
Min (B - A) \<in> B - A

goal (1 subgoal):
 1. A \<sqsubset>' B
[PROOF STEP]
using A B
[PROOF STATE]
proof (prove)
using this:
?z2 \<in> A - B \<union> (B - A) \<Longrightarrow> Min (B - A) \<le> ?z2 \<and> (?z2 \<le> Min (B - A) \<longrightarrow> Min (B - A) = ?z2)
Min (B - A) \<in> B - A
finite A
finite B

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

goal (1 subgoal):
 1. \<And>A B. \<lbrakk>Min (B - A) \<le> Min (A - B); \<not> A \<subseteq> B; \<not> B \<subseteq> A; A \<noteq> B; finite A; finite B\<rbrakk> \<Longrightarrow> A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
A \<sqsubset>' B

goal (1 subgoal):
 1. A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A \<sqsubset>' B \<or> A = B \<or> B \<sqsubset>' A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_less_eq_aux_finite_total:
  "\<lbrakk> finite A; finite B \<rbrakk> \<Longrightarrow> A \<sqsubseteq>' B \<or> A = B \<or> B \<sqsubseteq>' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> A \<sqsubseteq>' B \<or> A = B \<or> B \<sqsubseteq>' A
[PROOF STEP]
by(drule (1) set_less_aux_finite_total)(auto simp add: set_less_eq_aux_def)


[STATEMENT]
lemma set_less_eq_aux_finite_total2:
  "\<lbrakk> finite A; finite B \<rbrakk> \<Longrightarrow> A \<sqsubseteq>' B \<or> B \<sqsubseteq>' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> A \<sqsubseteq>' B \<or> B \<sqsubseteq>' A
[PROOF STEP]
by(drule (1) set_less_eq_aux_finite_total)(auto simp add: finite_complement_partition)


[STATEMENT]
lemma set_less_aux_rec:
  assumes A: "finite A" and B: "finite B"
  and A': "A \<noteq> {}" and B': "B \<noteq> {}"
  shows "A \<sqsubset>' B \<longleftrightarrow> Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubset>' B - {Min A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<sqsubset>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubset>' B - {Min A})
[PROOF STEP]
proof(cases "Min A = Min B")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Min A = Min B \<Longrightarrow> (A \<sqsubset>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubset>' B - {Min A})
 2. Min A \<noteq> Min B \<Longrightarrow> (A \<sqsubset>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubset>' B - {Min A})
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Min A = Min B

goal (2 subgoals):
 1. Min A = Min B \<Longrightarrow> (A \<sqsubset>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubset>' B - {Min A})
 2. Min A \<noteq> Min B \<Longrightarrow> (A \<sqsubset>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubset>' B - {Min A})
[PROOF STEP]
from A A' B B'
[PROOF STATE]
proof (chain)
picking this:
finite A
A \<noteq> {}
finite B
B \<noteq> {}
[PROOF STEP]
have "insert (Min A) A = A" "insert (Min B) B = B"
[PROOF STATE]
proof (prove)
using this:
finite A
A \<noteq> {}
finite B
B \<noteq> {}

goal (1 subgoal):
 1. insert (Min A) A = A &&& insert (Min B) B = B
[PROOF STEP]
by(auto simp add: ex_in_conv[symmetric] exI)
[PROOF STATE]
proof (state)
this:
insert (Min A) A = A
insert (Min B) B = B

goal (2 subgoals):
 1. Min A = Min B \<Longrightarrow> (A \<sqsubset>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubset>' B - {Min A})
 2. Min A \<noteq> Min B \<Longrightarrow> (A \<sqsubset>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubset>' B - {Min A})
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
Min A = Min B
insert (Min A) A = A
insert (Min B) B = B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Min A = Min B
insert (Min A) A = A
insert (Min B) B = B

goal (1 subgoal):
 1. (A \<sqsubset>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubset>' B - {Min A})
[PROOF STEP]
by(subst (2) set_less_aux_insert_same[symmetric, where x="Min A"]) simp_all
[PROOF STATE]
proof (state)
this:
(A \<sqsubset>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubset>' B - {Min A})

goal (1 subgoal):
 1. Min A \<noteq> Min B \<Longrightarrow> (A \<sqsubset>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubset>' B - {Min A})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Min A \<noteq> Min B \<Longrightarrow> (A \<sqsubset>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubset>' B - {Min A})
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Min A \<noteq> Min B

goal (1 subgoal):
 1. Min A \<noteq> Min B \<Longrightarrow> (A \<sqsubset>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubset>' B - {Min A})
[PROOF STEP]
have "A \<sqsubset>' B \<longleftrightarrow> Min B < Min A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<sqsubset>' B) = (Min B < Min A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A \<sqsubset>' B \<Longrightarrow> Min B < Min A
 2. Min B < Min A \<Longrightarrow> A \<sqsubset>' B
[PROOF STEP]
assume AB: "A \<sqsubset>' B"
[PROOF STATE]
proof (state)
this:
A \<sqsubset>' B

goal (2 subgoals):
 1. A \<sqsubset>' B \<Longrightarrow> Min B < Min A
 2. Min B < Min A \<Longrightarrow> A \<sqsubset>' B
[PROOF STEP]
with B A
[PROOF STATE]
proof (chain)
picking this:
finite B
finite A
A \<sqsubset>' B
[PROOF STEP]
obtain ab where ab: "ab \<in> B - A"
      and AB: "\<And>x. \<lbrakk> x \<in> A; x \<notin> B \<rbrakk> \<Longrightarrow> ab \<le> x"
[PROOF STATE]
proof (prove)
using this:
finite B
finite A
A \<sqsubset>' B

goal (1 subgoal):
 1. (\<And>ab. \<lbrakk>ab \<in> B - A; \<And>x. \<lbrakk>x \<in> A; x \<notin> B\<rbrakk> \<Longrightarrow> ab \<le> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: set_less_aux_def)
[PROOF STATE]
proof (state)
this:
ab \<in> B - A
\<lbrakk>?x \<in> A; ?x \<notin> B\<rbrakk> \<Longrightarrow> ab \<le> ?x

goal (2 subgoals):
 1. A \<sqsubset>' B \<Longrightarrow> Min B < Min A
 2. Min B < Min A \<Longrightarrow> A \<sqsubset>' B
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ab \<in> B - A
\<lbrakk>?x \<in> A; ?x \<notin> B\<rbrakk> \<Longrightarrow> ab \<le> ?x

goal (2 subgoals):
 1. A \<sqsubset>' B \<Longrightarrow> Min B < Min A
 2. Min B < Min A \<Longrightarrow> A \<sqsubset>' B
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A \<sqsubset>' B \<Longrightarrow> Min B < Min A
 2. Min B < Min A \<Longrightarrow> A \<sqsubset>' B
[PROOF STEP]
assume "a \<in> A"
[PROOF STATE]
proof (state)
this:
a \<in> A

goal (2 subgoals):
 1. A \<sqsubset>' B \<Longrightarrow> Min B < Min A
 2. Min B < Min A \<Longrightarrow> A \<sqsubset>' B
[PROOF STEP]
hence "Min B \<le> a"
[PROOF STATE]
proof (prove)
using this:
a \<in> A

goal (1 subgoal):
 1. Min B \<le> a
[PROOF STEP]
using A A' B B' ab
[PROOF STATE]
proof (prove)
using this:
a \<in> A
finite A
A \<noteq> {}
finite B
B \<noteq> {}
ab \<in> B - A

goal (1 subgoal):
 1. Min B \<le> a
[PROOF STEP]
by(cases "a \<in> B")(auto intro: order_trans[where y=ab] dest: AB)
[PROOF STATE]
proof (state)
this:
Min B \<le> a

goal (2 subgoals):
 1. A \<sqsubset>' B \<Longrightarrow> Min B < Min A
 2. Min B < Min A \<Longrightarrow> A \<sqsubset>' B
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?a2 \<in> A \<Longrightarrow> Min B \<le> ?a2

goal (2 subgoals):
 1. A \<sqsubset>' B \<Longrightarrow> Min B < Min A
 2. Min B < Min A \<Longrightarrow> A \<sqsubset>' B
[PROOF STEP]
hence "Min B \<le> Min A"
[PROOF STATE]
proof (prove)
using this:
?a2 \<in> A \<Longrightarrow> Min B \<le> ?a2

goal (1 subgoal):
 1. Min B \<le> Min A
[PROOF STEP]
using A A'
[PROOF STATE]
proof (prove)
using this:
?a2 \<in> A \<Longrightarrow> Min B \<le> ?a2
finite A
A \<noteq> {}

goal (1 subgoal):
 1. Min B \<le> Min A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Min B \<le> Min A

goal (2 subgoals):
 1. A \<sqsubset>' B \<Longrightarrow> Min B < Min A
 2. Min B < Min A \<Longrightarrow> A \<sqsubset>' B
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
Min A \<noteq> Min B
Min B \<le> Min A
[PROOF STEP]
show "Min B < Min A"
[PROOF STATE]
proof (prove)
using this:
Min A \<noteq> Min B
Min B \<le> Min A

goal (1 subgoal):
 1. Min B < Min A
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
Min A \<noteq> Min B
Min B \<le> Min A
Min A \<noteq> Min B

goal (1 subgoal):
 1. Min B < Min A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Min B < Min A

goal (1 subgoal):
 1. Min B < Min A \<Longrightarrow> A \<sqsubset>' B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Min B < Min A \<Longrightarrow> A \<sqsubset>' B
[PROOF STEP]
assume "Min B < Min A"
[PROOF STATE]
proof (state)
this:
Min B < Min A

goal (1 subgoal):
 1. Min B < Min A \<Longrightarrow> A \<sqsubset>' B
[PROOF STEP]
hence "\<forall>z\<in>A - B \<union> (B - A). Min B \<le> z \<and> (z \<le> Min B \<longrightarrow> Min B = z)"
[PROOF STATE]
proof (prove)
using this:
Min B < Min A

goal (1 subgoal):
 1. \<forall>z\<in>A - B \<union> (B - A). Min B \<le> z \<and> (z \<le> Min B \<longrightarrow> Min B = z)
[PROOF STEP]
using A B A' B'
[PROOF STATE]
proof (prove)
using this:
Min B < Min A
finite A
finite B
A \<noteq> {}
B \<noteq> {}

goal (1 subgoal):
 1. \<forall>z\<in>A - B \<union> (B - A). Min B \<le> z \<and> (z \<le> Min B \<longrightarrow> Min B = z)
[PROOF STEP]
by(auto 4 4 intro: Min_in Min_eqI dest: bspec bspec[where x="Min B"])
[PROOF STATE]
proof (state)
this:
\<forall>z\<in>A - B \<union> (B - A). Min B \<le> z \<and> (z \<le> Min B \<longrightarrow> Min B = z)

goal (1 subgoal):
 1. Min B < Min A \<Longrightarrow> A \<sqsubset>' B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>z\<in>A - B \<union> (B - A). Min B \<le> z \<and> (z \<le> Min B \<longrightarrow> Min B = z)

goal (1 subgoal):
 1. Min B < Min A \<Longrightarrow> A \<sqsubset>' B
[PROOF STEP]
have "Min B \<notin> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min B \<notin> A
[PROOF STEP]
using \<open>Min B < Min A\<close>
[PROOF STATE]
proof (prove)
using this:
Min B < Min A

goal (1 subgoal):
 1. Min B \<notin> A
[PROOF STEP]
by (metis A Min_le not_less)
[PROOF STATE]
proof (state)
this:
Min B \<notin> A

goal (1 subgoal):
 1. Min B < Min A \<Longrightarrow> A \<sqsubset>' B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>z\<in>A - B \<union> (B - A). Min B \<le> z \<and> (z \<le> Min B \<longrightarrow> Min B = z)
Min B \<notin> A
[PROOF STEP]
show "A \<sqsubset>' B"
[PROOF STATE]
proof (prove)
using this:
\<forall>z\<in>A - B \<union> (B - A). Min B \<le> z \<and> (z \<le> Min B \<longrightarrow> Min B = z)
Min B \<notin> A

goal (1 subgoal):
 1. A \<sqsubset>' B
[PROOF STEP]
using A B A' B'
[PROOF STATE]
proof (prove)
using this:
\<forall>z\<in>A - B \<union> (B - A). Min B \<le> z \<and> (z \<le> Min B \<longrightarrow> Min B = z)
Min B \<notin> A
finite A
finite B
A \<noteq> {}
B \<noteq> {}

goal (1 subgoal):
 1. A \<sqsubset>' B
[PROOF STEP]
by(simp add: set_less_aux_def bexI[where x="Min B"])
[PROOF STATE]
proof (state)
this:
A \<sqsubset>' B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(A \<sqsubset>' B) = (Min B < Min A)

goal (1 subgoal):
 1. Min A \<noteq> Min B \<Longrightarrow> (A \<sqsubset>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubset>' B - {Min A})
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(A \<sqsubset>' B) = (Min B < Min A)

goal (1 subgoal):
 1. (A \<sqsubset>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubset>' B - {Min A})
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
(A \<sqsubset>' B) = (Min B < Min A)
Min A \<noteq> Min B

goal (1 subgoal):
 1. (A \<sqsubset>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubset>' B - {Min A})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(A \<sqsubset>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubset>' B - {Min A})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_less_eq_aux_rec:
  assumes "finite A" "finite B" "A \<noteq> {}" "B \<noteq> {}"
  shows "A \<sqsubseteq>' B \<longleftrightarrow> Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubseteq>' B - {Min A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<sqsubseteq>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubseteq>' B - {Min A})
[PROOF STEP]
proof(cases "A = B")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A = B \<Longrightarrow> (A \<sqsubseteq>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubseteq>' B - {Min A})
 2. A \<noteq> B \<Longrightarrow> (A \<sqsubseteq>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubseteq>' B - {Min A})
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A = B

goal (2 subgoals):
 1. A = B \<Longrightarrow> (A \<sqsubseteq>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubseteq>' B - {Min A})
 2. A \<noteq> B \<Longrightarrow> (A \<sqsubseteq>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubseteq>' B - {Min A})
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A = B

goal (1 subgoal):
 1. (A \<sqsubseteq>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubseteq>' B - {Min A})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A = B
finite A
finite B
A \<noteq> {}
B \<noteq> {}

goal (1 subgoal):
 1. (A \<sqsubseteq>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubseteq>' B - {Min A})
[PROOF STEP]
by(simp add: finite_complement_partition)
[PROOF STATE]
proof (state)
this:
(A \<sqsubseteq>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubseteq>' B - {Min A})

goal (1 subgoal):
 1. A \<noteq> B \<Longrightarrow> (A \<sqsubseteq>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubseteq>' B - {Min A})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<noteq> B \<Longrightarrow> (A \<sqsubseteq>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubseteq>' B - {Min A})
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
A \<noteq> B

goal (1 subgoal):
 1. A \<noteq> B \<Longrightarrow> (A \<sqsubseteq>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubseteq>' B - {Min A})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A \<noteq> B

goal (1 subgoal):
 1. A \<noteq> B \<Longrightarrow> (A \<sqsubseteq>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubseteq>' B - {Min A})
[PROOF STEP]
hence "Min A = Min B \<Longrightarrow> A - {Min A} \<noteq> B - {Min B}"
[PROOF STATE]
proof (prove)
using this:
A \<noteq> B

goal (1 subgoal):
 1. Min A = Min B \<Longrightarrow> A - {Min A} \<noteq> B - {Min B}
[PROOF STEP]
by (metis (lifting) assms Min_in insert_Diff)
[PROOF STATE]
proof (state)
this:
Min A = Min B \<Longrightarrow> A - {Min A} \<noteq> B - {Min B}

goal (1 subgoal):
 1. A \<noteq> B \<Longrightarrow> (A \<sqsubseteq>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubseteq>' B - {Min A})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A \<noteq> B
Min A = Min B \<Longrightarrow> A - {Min A} \<noteq> B - {Min B}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<noteq> B
Min A = Min B \<Longrightarrow> A - {Min A} \<noteq> B - {Min B}

goal (1 subgoal):
 1. (A \<sqsubseteq>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubseteq>' B - {Min A})
[PROOF STEP]
using set_less_aux_rec[OF assms]
[PROOF STATE]
proof (prove)
using this:
A \<noteq> B
Min A = Min B \<Longrightarrow> A - {Min A} \<noteq> B - {Min B}
(A \<sqsubset>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubset>' B - {Min A})

goal (1 subgoal):
 1. (A \<sqsubseteq>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubseteq>' B - {Min A})
[PROOF STEP]
by(simp add: set_less_eq_aux_def cong: conj_cong)
[PROOF STATE]
proof (state)
this:
(A \<sqsubseteq>' B) = (Min B < Min A \<or> Min A = Min B \<and> A - {Min A} \<sqsubseteq>' B - {Min A})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_less_aux_Min_antimono:
  "\<lbrakk> Min A < Min B;  finite A; finite B; A \<noteq> {} \<rbrakk> \<Longrightarrow> B \<sqsubset>' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Min A < Min B; finite A; finite B; A \<noteq> {}\<rbrakk> \<Longrightarrow> B \<sqsubset>' A
[PROOF STEP]
using set_less_aux_rec[of B A]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite B; finite A; B \<noteq> {}; A \<noteq> {}\<rbrakk> \<Longrightarrow> (B \<sqsubset>' A) = (Min A < Min B \<or> Min B = Min A \<and> B - {Min B} \<sqsubset>' A - {Min B})

goal (1 subgoal):
 1. \<lbrakk>Min A < Min B; finite A; finite B; A \<noteq> {}\<rbrakk> \<Longrightarrow> B \<sqsubset>' A
[PROOF STEP]
by(cases "B = {}")(simp_all add: empty_set_less_aux_finite_iff)


[STATEMENT]
lemma sorted_Cons_Min: "sorted (x # xs) \<Longrightarrow> Min (insert x (set xs)) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted (x # xs) \<Longrightarrow> Min (insert x (set xs)) = x
[PROOF STEP]
by(auto simp add: intro: Min_eqI)


[STATEMENT]
lemma set_less_aux_code:
  "\<lbrakk> sorted xs; distinct xs; sorted ys; distinct ys \<rbrakk>
  \<Longrightarrow> set xs \<sqsubset>' set ys \<longleftrightarrow> ord.lexordp (>) xs ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sorted xs; distinct xs; sorted ys; distinct ys\<rbrakk> \<Longrightarrow> (set xs \<sqsubset>' set ys) = ord.lexordp (\<lambda>x y. y < x) xs ys
[PROOF STEP]
apply(induct xs ys rule: list_induct2')
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>sorted []; distinct []; sorted []; distinct []\<rbrakk> \<Longrightarrow> (set [] \<sqsubset>' set []) = ord.lexordp (\<lambda>x y. y < x) [] []
 2. \<And>x xs. \<lbrakk>sorted (x # xs); distinct (x # xs); sorted []; distinct []\<rbrakk> \<Longrightarrow> (set (x # xs) \<sqsubset>' set []) = ord.lexordp (\<lambda>x y. y < x) (x # xs) []
 3. \<And>y ys. \<lbrakk>sorted []; distinct []; sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> (set [] \<sqsubset>' set (y # ys)) = ord.lexordp (\<lambda>x y. y < x) [] (y # ys)
 4. \<And>x xs y ys. \<lbrakk>\<lbrakk>sorted xs; distinct xs; sorted ys; distinct ys\<rbrakk> \<Longrightarrow> (set xs \<sqsubset>' set ys) = ord.lexordp (\<lambda>x y. y < x) xs ys; sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> (set (x # xs) \<sqsubset>' set (y # ys)) = ord.lexordp (\<lambda>x y. y < x) (x # xs) (y # ys)
[PROOF STEP]
apply(simp_all add: empty_set_less_aux_finite_iff sorted_Cons_Min set_less_aux_rec neq_Nil_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>(set xs \<sqsubset>' set ys) = ord.lexordp (\<lambda>x y. y < x) xs ys; (\<forall>xa\<in>set xs. x \<le> xa) \<and> sorted xs; x \<notin> set xs \<and> distinct xs; (\<forall>x\<in>set ys. y \<le> x) \<and> sorted ys; y \<notin> set ys \<and> distinct ys\<rbrakk> \<Longrightarrow> (y < x \<or> x = y \<and> set xs \<sqsubset>' insert y (set ys) - {x}) = (y < x \<or> \<not> x < y \<and> ord.lexordp (\<lambda>x y. y < x) xs ys)
[PROOF STEP]
apply(auto cong: conj_cong)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma set_less_eq_aux_code:
  assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys"
  shows "set xs \<sqsubseteq>' set ys \<longleftrightarrow> ord.lexordp_eq (>) xs ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set xs \<sqsubseteq>' set ys) = ord.lexordp_eq (\<lambda>x y. y < x) xs ys
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (set xs \<sqsubseteq>' set ys) = ord.lexordp_eq (\<lambda>x y. y < x) xs ys
[PROOF STEP]
have dual: "class.linorder (\<ge>) (>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.linorder (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x)
[PROOF STEP]
by(rule linorder.dual_linorder) unfold_locales
[PROOF STATE]
proof (state)
this:
class.linorder (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x)

goal (1 subgoal):
 1. (set xs \<sqsubseteq>' set ys) = ord.lexordp_eq (\<lambda>x y. y < x) xs ys
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
sorted xs
distinct xs
sorted ys
distinct ys
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sorted xs
distinct xs
sorted ys
distinct ys

goal (1 subgoal):
 1. (set xs \<sqsubseteq>' set ys) = ord.lexordp_eq (\<lambda>x y. y < x) xs ys
[PROOF STEP]
by(auto simp add: set_less_eq_aux_def finite_complement_partition linorder.lexordp_eq_conv_lexord[OF dual] set_less_aux_code intro: sorted_distinct_set_unique)
[PROOF STATE]
proof (state)
this:
(set xs \<sqsubseteq>' set ys) = ord.lexordp_eq (\<lambda>x y. y < x) xs ys

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_less_eq_aux'_refl:
  "A \<sqsubseteq>'' A \<longleftrightarrow> A \<in> infinite_complement_partition"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<sqsubseteq>'' A) = (A \<in> infinite_complement_partition)
[PROOF STEP]
by(auto simp add: set_less_eq_aux'_def)


[STATEMENT]
lemma set_less_eq_aux'_antisym: "\<lbrakk> A \<sqsubseteq>'' B; B \<sqsubseteq>'' A \<rbrakk> \<Longrightarrow> A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<sqsubseteq>'' B; B \<sqsubseteq>'' A\<rbrakk> \<Longrightarrow> A = B
[PROOF STEP]
by(auto simp add: set_less_eq_aux'_def intro: set_less_eq_aux_antisym del: equalityI)


[STATEMENT]
lemma set_less_eq_aux'_infinite_complement_partitionD:
  "A \<sqsubseteq>'' B \<Longrightarrow> A \<in> infinite_complement_partition \<and> B \<in> infinite_complement_partition"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<sqsubseteq>'' B \<Longrightarrow> A \<in> infinite_complement_partition \<and> B \<in> infinite_complement_partition
[PROOF STEP]
by(auto simp add: set_less_eq_aux'_def intro: finite_complement_partition dest: set_less_eq_aux_infinite_complement_partitionD)


[STATEMENT]
lemma empty_set_less_eq_def [simp]: "{} \<sqsubseteq>'' B \<longleftrightarrow> B \<in> infinite_complement_partition"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({} \<sqsubseteq>'' B) = (B \<in> infinite_complement_partition)
[PROOF STEP]
by(auto simp add: set_less_eq_aux'_def dest: set_less_eq_aux_infinite_complement_partitionD)


[STATEMENT]
lemma set_less_eq_aux'_trans: "\<lbrakk> A \<sqsubseteq>'' B; B \<sqsubseteq>'' C \<rbrakk> \<Longrightarrow> A \<sqsubseteq>'' C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<sqsubseteq>'' B; B \<sqsubseteq>'' C\<rbrakk> \<Longrightarrow> A \<sqsubseteq>'' C
[PROOF STEP]
by(auto simp add: set_less_eq_aux'_def del: equalityI intro: set_less_eq_aux_trans dest: set_less_eq_aux_infinite_complement_partitionD)


[STATEMENT]
lemma set_less_eq_aux'_porder: "partial_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>'' B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>'' B}
[PROOF STEP]
by(auto simp add: partial_order_on_def preorder_on_def intro!: refl_onI transI antisymI dest: set_less_eq_aux'_antisym set_less_eq_aux'_infinite_complement_partitionD simp add: set_less_eq_aux'_refl intro: set_less_eq_aux'_trans)


[STATEMENT]
lemma set_less_eq_aux''_spec:
  shows "linear_order {(a, b). a \<le> b} \<Longrightarrow> linear_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>''' B}"
  (is "PROP ?thesis1")
  and "order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). A \<sqsubseteq>''' B}" (is ?thesis2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (linear_order {(x, y). x \<le> y} \<Longrightarrow> linear_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>''' B}) &&& order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). A \<sqsubseteq>''' B}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. linear_order {(x, y). x \<le> y} \<Longrightarrow> linear_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>''' B}
 2. order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). A \<sqsubseteq>''' B}
[PROOF STEP]
let ?P = "\<lambda>sleq. (linear_order {(a, b). a \<le> b} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and>
                  order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. linear_order {(x, y). x \<le> y} \<Longrightarrow> linear_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>''' B}
 2. order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). A \<sqsubseteq>''' B}
[PROOF STEP]
have "Ex ?P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}
[PROOF STEP]
proof(cases "linear_order {(a, b). a \<le> b}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. linear_order {(x, y). x \<le> y} \<Longrightarrow> \<exists>sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}
 2. \<not> linear_order {(x, y). x \<le> y} \<Longrightarrow> \<exists>sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> linear_order {(x, y). x \<le> y}

goal (2 subgoals):
 1. linear_order {(x, y). x \<le> y} \<Longrightarrow> \<exists>sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}
 2. \<not> linear_order {(x, y). x \<le> y} \<Longrightarrow> \<exists>sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}
[PROOF STEP]
have "antisym {(a, b). a \<sqsubseteq>'' b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. antisym {(a, b). a \<sqsubseteq>'' b}
[PROOF STEP]
by (rule antisymI) (simp add: set_less_eq_aux'_antisym)
[PROOF STATE]
proof (state)
this:
antisym {(a, b). a \<sqsubseteq>'' b}

goal (2 subgoals):
 1. linear_order {(x, y). x \<le> y} \<Longrightarrow> \<exists>sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}
 2. \<not> linear_order {(x, y). x \<le> y} \<Longrightarrow> \<exists>sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
antisym {(a, b). a \<sqsubseteq>'' b}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
antisym {(a, b). a \<sqsubseteq>'' b}

goal (1 subgoal):
 1. \<exists>sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
antisym {(a, b). a \<sqsubseteq>'' b}
\<not> linear_order {(x, y). x \<le> y}

goal (1 subgoal):
 1. \<exists>sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}
[PROOF STEP]
by (auto intro: antisym_order_consistent_self)
[PROOF STATE]
proof (state)
this:
\<exists>sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}

goal (1 subgoal):
 1. linear_order {(x, y). x \<le> y} \<Longrightarrow> \<exists>sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. linear_order {(x, y). x \<le> y} \<Longrightarrow> \<exists>sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
linear_order {(x, y). x \<le> y}

goal (1 subgoal):
 1. linear_order {(x, y). x \<le> y} \<Longrightarrow> \<exists>sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}
[PROOF STEP]
hence "partial_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>'' B}"
[PROOF STATE]
proof (prove)
using this:
linear_order {(x, y). x \<le> y}

goal (1 subgoal):
 1. partial_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>'' B}
[PROOF STEP]
by(rule linorder.set_less_eq_aux'_porder[OF linear_order_imp_linorder])
[PROOF STATE]
proof (state)
this:
partial_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>'' B}

goal (1 subgoal):
 1. linear_order {(x, y). x \<le> y} \<Longrightarrow> \<exists>sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
partial_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>'' B}
[PROOF STEP]
obtain s where "linear_order_on infinite_complement_partition s"
      and "order_consistent {(A, B). A \<sqsubseteq>'' B} s"
[PROOF STATE]
proof (prove)
using this:
partial_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>'' B}

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>linear_order_on infinite_complement_partition s; order_consistent {(A, B). A \<sqsubseteq>'' B} s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule porder_extend_to_linorder)
[PROOF STATE]
proof (state)
this:
linear_order_on infinite_complement_partition s
order_consistent {(A, B). A \<sqsubseteq>'' B} s

goal (1 subgoal):
 1. linear_order {(x, y). x \<le> y} \<Longrightarrow> \<exists>sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
linear_order_on infinite_complement_partition s
order_consistent {(A, B). A \<sqsubseteq>'' B} s

goal (1 subgoal):
 1. \<exists>sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}
[PROOF STEP]
by(auto intro: exI[where x="\<lambda>A B. (A, B) \<in> s"])
[PROOF STATE]
proof (state)
this:
\<exists>sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}

goal (2 subgoals):
 1. linear_order {(x, y). x \<le> y} \<Longrightarrow> linear_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>''' B}
 2. order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). A \<sqsubseteq>''' B}
[PROOF STEP]
hence "?P (Eps ?P)"
[PROOF STATE]
proof (prove)
using this:
\<exists>sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}

goal (1 subgoal):
 1. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). (SOME sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}) A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). (SOME sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}) A B}
[PROOF STEP]
by(rule someI_ex)
[PROOF STATE]
proof (state)
this:
(linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). (SOME sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}) A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). (SOME sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}) A B}

goal (2 subgoals):
 1. linear_order {(x, y). x \<le> y} \<Longrightarrow> linear_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>''' B}
 2. order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). A \<sqsubseteq>''' B}
[PROOF STEP]
thus "PROP ?thesis1" ?thesis2
[PROOF STATE]
proof (prove)
using this:
(linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). (SOME sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}) A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). (SOME sleq. (linear_order {(x, y). x \<le> y} \<longrightarrow> linear_order_on infinite_complement_partition {(A, B). sleq A B}) \<and> order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). sleq A B}) A B}

goal (1 subgoal):
 1. (linear_order {(x, y). x \<le> y} \<Longrightarrow> linear_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>''' B}) &&& order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). A \<sqsubseteq>''' B}
[PROOF STEP]
by(simp_all add: set_less_eq_aux''_def)
[PROOF STATE]
proof (state)
this:
linear_order {(x, y). x \<le> y} \<Longrightarrow> linear_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>''' B}
order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). A \<sqsubseteq>''' B}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_less_eq_aux''_linear_order:
  "linear_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>''' B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>''' B}
[PROOF STEP]
by(rule set_less_eq_aux''_spec)(rule linear_order)


[STATEMENT]
lemma set_less_eq_aux''_refl [iff]: "A \<sqsubseteq>''' A \<longleftrightarrow> A \<in> infinite_complement_partition"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<sqsubseteq>''' A) = (A \<in> infinite_complement_partition)
[PROOF STEP]
using set_less_eq_aux''_linear_order
[PROOF STATE]
proof (prove)
using this:
linear_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>''' B}

goal (1 subgoal):
 1. (A \<sqsubseteq>''' A) = (A \<in> infinite_complement_partition)
[PROOF STEP]
by(auto simp add: linear_order_on_def partial_order_on_def preorder_on_def dest: refl_onD refl_onD1)


[STATEMENT]
lemma set_less_eq_aux'_into_set_less_eq_aux'':
  assumes "A \<sqsubseteq>'' B"
  shows "A \<sqsubseteq>''' B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<sqsubseteq>''' B
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> A \<sqsubseteq>''' B \<Longrightarrow> False
[PROOF STEP]
assume nleq: "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
\<not> A \<sqsubseteq>''' B

goal (1 subgoal):
 1. \<not> A \<sqsubseteq>''' B \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> A \<sqsubseteq>''' B

goal (1 subgoal):
 1. \<not> A \<sqsubseteq>''' B \<Longrightarrow> False
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
A \<sqsubseteq>'' B
[PROOF STEP]
have A: "A \<in> infinite_complement_partition"
    and B: "B \<in> infinite_complement_partition"
[PROOF STATE]
proof (prove)
using this:
A \<sqsubseteq>'' B

goal (1 subgoal):
 1. A \<in> infinite_complement_partition &&& B \<in> infinite_complement_partition
[PROOF STEP]
by(auto dest: set_less_eq_aux'_infinite_complement_partitionD)
[PROOF STATE]
proof (state)
this:
A \<in> infinite_complement_partition
B \<in> infinite_complement_partition

goal (1 subgoal):
 1. \<not> A \<sqsubseteq>''' B \<Longrightarrow> False
[PROOF STEP]
with set_less_eq_aux''_linear_order
[PROOF STATE]
proof (chain)
picking this:
linear_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>''' B}
A \<in> infinite_complement_partition
B \<in> infinite_complement_partition
[PROOF STEP]
have "A \<sqsubseteq>''' B \<or> A = B \<or> B \<sqsubseteq>''' A"
[PROOF STATE]
proof (prove)
using this:
linear_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>''' B}
A \<in> infinite_complement_partition
B \<in> infinite_complement_partition

goal (1 subgoal):
 1. A \<sqsubseteq>''' B \<or> A = B \<or> B \<sqsubseteq>''' A
[PROOF STEP]
by(auto simp add: linear_order_on_def dest: total_onD)
[PROOF STATE]
proof (state)
this:
A \<sqsubseteq>''' B \<or> A = B \<or> B \<sqsubseteq>''' A

goal (1 subgoal):
 1. \<not> A \<sqsubseteq>''' B \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> A \<sqsubseteq>''' B
A \<sqsubseteq>''' B \<or> A = B \<or> B \<sqsubseteq>''' A
[PROOF STEP]
have "B \<sqsubseteq>''' A"
[PROOF STATE]
proof (prove)
using this:
\<not> A \<sqsubseteq>''' B
A \<sqsubseteq>''' B \<or> A = B \<or> B \<sqsubseteq>''' A

goal (1 subgoal):
 1. B \<sqsubseteq>''' A
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
\<not> A \<sqsubseteq>''' B
A \<sqsubseteq>''' B \<or> A = B \<or> B \<sqsubseteq>''' A
B \<in> infinite_complement_partition

goal (1 subgoal):
 1. B \<sqsubseteq>''' A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B \<sqsubseteq>''' A

goal (1 subgoal):
 1. \<not> A \<sqsubseteq>''' B \<Longrightarrow> False
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
A \<sqsubseteq>'' B
B \<sqsubseteq>''' A
[PROOF STEP]
have "A = B"
[PROOF STATE]
proof (prove)
using this:
A \<sqsubseteq>'' B
B \<sqsubseteq>''' A

goal (1 subgoal):
 1. A = B
[PROOF STEP]
using set_less_eq_aux''_spec(2)
[PROOF STATE]
proof (prove)
using this:
A \<sqsubseteq>'' B
B \<sqsubseteq>''' A
order_consistent {(A, B). A \<sqsubseteq>'' B} {(A, B). A \<sqsubseteq>''' B}

goal (1 subgoal):
 1. A = B
[PROOF STEP]
by(simp add: order_consistent_def)
[PROOF STATE]
proof (state)
this:
A = B

goal (1 subgoal):
 1. \<not> A \<sqsubseteq>''' B \<Longrightarrow> False
[PROOF STEP]
with A nleq
[PROOF STATE]
proof (chain)
picking this:
A \<in> infinite_complement_partition
\<not> A \<sqsubseteq>''' B
A = B
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
A \<in> infinite_complement_partition
\<not> A \<sqsubseteq>''' B
A = B

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_set_less_eq_aux''_finite:
  assumes "finite A" and "finite B"
  shows "A \<sqsubseteq>''' B \<longleftrightarrow> A \<sqsubseteq>'' B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<sqsubseteq>''' B) = (A \<sqsubseteq>'' B)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A \<sqsubseteq>''' B \<Longrightarrow> A \<sqsubseteq>'' B
 2. A \<sqsubseteq>'' B \<Longrightarrow> A \<sqsubseteq>''' B
[PROOF STEP]
assume "A \<sqsubseteq>''' B"
[PROOF STATE]
proof (state)
this:
A \<sqsubseteq>''' B

goal (2 subgoals):
 1. A \<sqsubseteq>''' B \<Longrightarrow> A \<sqsubseteq>'' B
 2. A \<sqsubseteq>'' B \<Longrightarrow> A \<sqsubseteq>''' B
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
finite A
finite B
[PROOF STEP]
have "A \<sqsubseteq>' B \<or> B \<sqsubseteq>' A"
[PROOF STATE]
proof (prove)
using this:
finite A
finite B

goal (1 subgoal):
 1. A \<sqsubseteq>' B \<or> B \<sqsubseteq>' A
[PROOF STEP]
by(rule set_less_eq_aux_finite_total2)
[PROOF STATE]
proof (state)
this:
A \<sqsubseteq>' B \<or> B \<sqsubseteq>' A

goal (2 subgoals):
 1. A \<sqsubseteq>''' B \<Longrightarrow> A \<sqsubseteq>'' B
 2. A \<sqsubseteq>'' B \<Longrightarrow> A \<sqsubseteq>''' B
[PROOF STEP]
hence "A \<sqsubseteq>'' B \<or> B \<sqsubseteq>'' A"
[PROOF STATE]
proof (prove)
using this:
A \<sqsubseteq>' B \<or> B \<sqsubseteq>' A

goal (1 subgoal):
 1. A \<sqsubseteq>'' B \<or> B \<sqsubseteq>'' A
[PROOF STEP]
by(auto simp add: set_less_eq_aux'_def)
[PROOF STATE]
proof (state)
this:
A \<sqsubseteq>'' B \<or> B \<sqsubseteq>'' A

goal (2 subgoals):
 1. A \<sqsubseteq>''' B \<Longrightarrow> A \<sqsubseteq>'' B
 2. A \<sqsubseteq>'' B \<Longrightarrow> A \<sqsubseteq>''' B
[PROOF STEP]
thus "A \<sqsubseteq>'' B"
[PROOF STATE]
proof (prove)
using this:
A \<sqsubseteq>'' B \<or> B \<sqsubseteq>'' A

goal (1 subgoal):
 1. A \<sqsubseteq>'' B
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A \<sqsubseteq>'' B \<Longrightarrow> A \<sqsubseteq>'' B
 2. B \<sqsubseteq>'' A \<Longrightarrow> A \<sqsubseteq>'' B
[PROOF STEP]
assume "B \<sqsubseteq>'' A"
[PROOF STATE]
proof (state)
this:
B \<sqsubseteq>'' A

goal (2 subgoals):
 1. A \<sqsubseteq>'' B \<Longrightarrow> A \<sqsubseteq>'' B
 2. B \<sqsubseteq>'' A \<Longrightarrow> A \<sqsubseteq>'' B
[PROOF STEP]
hence "B \<sqsubseteq>''' A"
[PROOF STATE]
proof (prove)
using this:
B \<sqsubseteq>'' A

goal (1 subgoal):
 1. B \<sqsubseteq>''' A
[PROOF STEP]
by(rule set_less_eq_aux'_into_set_less_eq_aux'')
[PROOF STATE]
proof (state)
this:
B \<sqsubseteq>''' A

goal (2 subgoals):
 1. A \<sqsubseteq>'' B \<Longrightarrow> A \<sqsubseteq>'' B
 2. B \<sqsubseteq>'' A \<Longrightarrow> A \<sqsubseteq>'' B
[PROOF STEP]
with \<open>A \<sqsubseteq>''' B\<close> set_less_eq_aux''_linear_order
[PROOF STATE]
proof (chain)
picking this:
A \<sqsubseteq>''' B
linear_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>''' B}
B \<sqsubseteq>''' A
[PROOF STEP]
have "A = B"
[PROOF STATE]
proof (prove)
using this:
A \<sqsubseteq>''' B
linear_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>''' B}
B \<sqsubseteq>''' A

goal (1 subgoal):
 1. A = B
[PROOF STEP]
by(auto simp add: linear_order_on_def partial_order_on_def dest: antisymD)
[PROOF STATE]
proof (state)
this:
A = B

goal (2 subgoals):
 1. A \<sqsubseteq>'' B \<Longrightarrow> A \<sqsubseteq>'' B
 2. B \<sqsubseteq>'' A \<Longrightarrow> A \<sqsubseteq>'' B
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A = B

goal (1 subgoal):
 1. A \<sqsubseteq>'' B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A = B
finite A
finite B

goal (1 subgoal):
 1. A \<sqsubseteq>'' B
[PROOF STEP]
by(simp add: finite_complement_partition set_less_eq_aux'_def)
[PROOF STATE]
proof (state)
this:
A \<sqsubseteq>'' B

goal (1 subgoal):
 1. A \<sqsubseteq>'' B \<Longrightarrow> A \<sqsubseteq>'' B
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A \<sqsubseteq>'' B

goal (1 subgoal):
 1. A \<sqsubseteq>'' B \<Longrightarrow> A \<sqsubseteq>''' B
[PROOF STEP]
qed(rule set_less_eq_aux'_into_set_less_eq_aux'')


[STATEMENT]
lemma set_less_eq_aux''_finite:
  "finite (UNIV :: 'a set) \<Longrightarrow> set_less_eq_aux'' = set_less_eq_aux"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite UNIV \<Longrightarrow> (\<sqsubseteq>''') = (\<sqsubseteq>')
[PROOF STEP]
by(auto simp add: fun_eq_iff finite_set_less_eq_aux''_finite set_less_eq_aux'_def finite_subset[OF subset_UNIV])


[STATEMENT]
lemma set_less_eq_aux''_antisym:
  "\<lbrakk> A \<sqsubseteq>''' B; B \<sqsubseteq>''' A;
     A \<in> infinite_complement_partition; B \<in> infinite_complement_partition \<rbrakk>
  \<Longrightarrow> A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<sqsubseteq>''' B; B \<sqsubseteq>''' A; A \<in> infinite_complement_partition; B \<in> infinite_complement_partition\<rbrakk> \<Longrightarrow> A = B
[PROOF STEP]
using set_less_eq_aux''_linear_order
[PROOF STATE]
proof (prove)
using this:
linear_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>''' B}

goal (1 subgoal):
 1. \<lbrakk>A \<sqsubseteq>''' B; B \<sqsubseteq>''' A; A \<in> infinite_complement_partition; B \<in> infinite_complement_partition\<rbrakk> \<Longrightarrow> A = B
[PROOF STEP]
by(auto simp add: linear_order_on_def partial_order_on_def dest: antisymD del: equalityI)


[STATEMENT]
lemma set_less_eq_aux''_trans: "\<lbrakk> A \<sqsubseteq>''' B; B \<sqsubseteq>''' C \<rbrakk> \<Longrightarrow> A \<sqsubseteq>''' C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<sqsubseteq>''' B; B \<sqsubseteq>''' C\<rbrakk> \<Longrightarrow> A \<sqsubseteq>''' C
[PROOF STEP]
using set_less_eq_aux''_linear_order
[PROOF STATE]
proof (prove)
using this:
linear_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>''' B}

goal (1 subgoal):
 1. \<lbrakk>A \<sqsubseteq>''' B; B \<sqsubseteq>''' C\<rbrakk> \<Longrightarrow> A \<sqsubseteq>''' C
[PROOF STEP]
by(auto simp add: linear_order_on_def partial_order_on_def preorder_on_def dest: transD)


[STATEMENT]
lemma set_less_eq_aux''_total:
  "\<lbrakk> A \<in> infinite_complement_partition; B \<in> infinite_complement_partition \<rbrakk>
  \<Longrightarrow> A \<sqsubseteq>''' B \<or> B \<sqsubseteq>''' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> infinite_complement_partition; B \<in> infinite_complement_partition\<rbrakk> \<Longrightarrow> A \<sqsubseteq>''' B \<or> B \<sqsubseteq>''' A
[PROOF STEP]
using set_less_eq_aux''_linear_order
[PROOF STATE]
proof (prove)
using this:
linear_order_on infinite_complement_partition {(A, B). A \<sqsubseteq>''' B}

goal (1 subgoal):
 1. \<lbrakk>A \<in> infinite_complement_partition; B \<in> infinite_complement_partition\<rbrakk> \<Longrightarrow> A \<sqsubseteq>''' B \<or> B \<sqsubseteq>''' A
[PROOF STEP]
by(auto simp add: linear_order_on_def dest: total_onD)


[STATEMENT]
lemma set_less_eq_def2:
  "A \<sqsubseteq> B \<longleftrightarrow>
  (if finite (UNIV :: 'a set) then A \<sqsubseteq>''' B
   else if A \<in> infinite_complement_partition then A \<sqsubseteq>''' B \<or> B \<notin> infinite_complement_partition
   else B \<notin> infinite_complement_partition \<and> - B \<sqsubseteq>''' - A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<sqsubseteq> B) = (if finite UNIV then A \<sqsubseteq>''' B else if A \<in> infinite_complement_partition then A \<sqsubseteq>''' B \<or> B \<notin> infinite_complement_partition else B \<notin> infinite_complement_partition \<and> - B \<sqsubseteq>''' - A)
[PROOF STEP]
by(simp add: set_less_eq_def)


[STATEMENT]
lemma set_less_eq_antisym: "\<lbrakk> A \<sqsubseteq> B; B \<sqsubseteq> A \<rbrakk> \<Longrightarrow> A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<sqsubseteq> B; B \<sqsubseteq> A\<rbrakk> \<Longrightarrow> A = B
[PROOF STEP]
by(auto simp add: set_less_eq_def2 set_less_eq_aux''_finite not_in_complement_partition not_in_complement_partition_False del: equalityI split: if_split_asm dest: set_less_eq_aux_antisym set_less_eq_aux''_antisym)


[STATEMENT]
lemma set_less_eq_trans: "\<lbrakk> A \<sqsubseteq> B; B \<sqsubseteq> C \<rbrakk> \<Longrightarrow> A \<sqsubseteq> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<sqsubseteq> B; B \<sqsubseteq> C\<rbrakk> \<Longrightarrow> A \<sqsubseteq> C
[PROOF STEP]
by(auto simp add: set_less_eq_def split: if_split_asm intro: set_less_eq_aux''_trans)


[STATEMENT]
lemma set_less_eq_total: "A \<sqsubseteq> B \<or> B \<sqsubseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<sqsubseteq> B \<or> B \<sqsubseteq> A
[PROOF STEP]
by(auto simp add: set_less_eq_def2 set_less_eq_aux''_finite not_in_complement_partition not_in_complement_partition_False intro: set_less_eq_aux_finite_total2 finite_subset[OF subset_UNIV] del: disjCI dest: set_less_eq_aux''_total)


[STATEMENT]
lemma set_less_eq_linorder: "class.linorder (\<sqsubseteq>) (\<sqsubset>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.linorder (\<sqsubseteq>) (\<sqsubset>)
[PROOF STEP]
by(unfold_locales)(auto simp add: set_less_def set_less_eq_antisym set_less_eq_total intro: set_less_eq_trans)


[STATEMENT]
lemma set_less_eq_conv_set_less: "set_less_eq A B \<longleftrightarrow> A = B \<or> set_less A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<sqsubseteq> B) = (A = B \<or> A \<sqsubset> B)
[PROOF STEP]
by(auto simp add: set_less_def del: equalityI dest: set_less_eq_antisym)


[STATEMENT]
lemma Compl_set_less_eq_Compl: "- A \<sqsubseteq> - B \<longleftrightarrow> B \<sqsubseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- A \<sqsubseteq> - B) = (B \<sqsubseteq> A)
[PROOF STEP]
by(auto simp add: set_less_eq_def2 not_in_complement_partition_False not_in_complement_partition set_less_eq_aux''_finite Compl_set_less_eq_aux_Compl)


[STATEMENT]
lemma Compl_set_less_Compl: "- A \<sqsubset> - B \<longleftrightarrow> B \<sqsubset> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- A \<sqsubset> - B) = (B \<sqsubset> A)
[PROOF STEP]
by(simp add: set_less_def Compl_set_less_eq_Compl)


[STATEMENT]
lemma set_less_eq_finite_iff: "\<lbrakk> finite A; finite B \<rbrakk> \<Longrightarrow> A \<sqsubseteq> B \<longleftrightarrow> A \<sqsubseteq>' B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> (A \<sqsubseteq> B) = (A \<sqsubseteq>' B)
[PROOF STEP]
by(auto simp add: set_less_eq_def finite_complement_partition set_less_eq_aux'_def finite_set_less_eq_aux''_finite)


[STATEMENT]
lemma set_less_finite_iff: "\<lbrakk> finite A; finite B \<rbrakk> \<Longrightarrow> A \<sqsubset> B \<longleftrightarrow> A \<sqsubset>' B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> (A \<sqsubset> B) = (A \<sqsubset>' B)
[PROOF STEP]
by(simp add: set_less_def set_less_aux_conv_set_less_eq_aux set_less_eq_finite_iff)


[STATEMENT]
lemma infinite_set_less_eq_Complement:
  "\<lbrakk> finite A; finite B; \<not> finite (UNIV :: 'a set) \<rbrakk> \<Longrightarrow> A \<sqsubseteq> - B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; finite B; infinite UNIV\<rbrakk> \<Longrightarrow> A \<sqsubseteq> - B
[PROOF STEP]
by(simp add: set_less_eq_def finite_complement_partition not_in_complement_partition)


[STATEMENT]
lemma infinite_set_less_Complement:
  "\<lbrakk> finite A; finite B; \<not> finite (UNIV :: 'a set) \<rbrakk> \<Longrightarrow> A \<sqsubset> - B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; finite B; infinite UNIV\<rbrakk> \<Longrightarrow> A \<sqsubset> - B
[PROOF STEP]
by(auto simp add: set_less_def dest: set_less_eq_antisym intro: infinite_set_less_eq_Complement)


[STATEMENT]
lemma infinite_Complement_set_less_eq:
  "\<lbrakk> finite A; finite B; \<not> finite (UNIV :: 'a set) \<rbrakk> \<Longrightarrow> \<not> - A \<sqsubseteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; finite B; infinite UNIV\<rbrakk> \<Longrightarrow> \<not> - A \<sqsubseteq> B
[PROOF STEP]
using infinite_set_less_eq_Complement[of A B] Compl_set_less_eq_Compl[of A "- B"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite A; finite B; infinite UNIV\<rbrakk> \<Longrightarrow> A \<sqsubseteq> - B
(- A \<sqsubseteq> - (- B)) = (- B \<sqsubseteq> A)

goal (1 subgoal):
 1. \<lbrakk>finite A; finite B; infinite UNIV\<rbrakk> \<Longrightarrow> \<not> - A \<sqsubseteq> B
[PROOF STEP]
by(auto dest: set_less_eq_antisym)


[STATEMENT]
lemma infinite_Complement_set_less:
  "\<lbrakk> finite A; finite B; \<not> finite (UNIV :: 'a set) \<rbrakk> \<Longrightarrow> \<not> - A \<sqsubset> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; finite B; infinite UNIV\<rbrakk> \<Longrightarrow> \<not> - A \<sqsubset> B
[PROOF STEP]
using infinite_Complement_set_less_eq[of A B]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite A; finite B; infinite UNIV\<rbrakk> \<Longrightarrow> \<not> - A \<sqsubseteq> B

goal (1 subgoal):
 1. \<lbrakk>finite A; finite B; infinite UNIV\<rbrakk> \<Longrightarrow> \<not> - A \<sqsubset> B
[PROOF STEP]
by(simp add: set_less_def)


[STATEMENT]
lemma empty_set_less_eq [iff]: "{} \<sqsubseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<sqsubseteq> A
[PROOF STEP]
by(auto simp add: set_less_eq_def finite_complement_partition intro: set_less_eq_aux'_into_set_less_eq_aux'')


[STATEMENT]
lemma set_less_eq_empty [iff]: "A \<sqsubseteq> {} \<longleftrightarrow> A = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<sqsubseteq> {}) = (A = {})
[PROOF STEP]
by (metis empty_set_less_eq set_less_eq_antisym)


[STATEMENT]
lemma empty_set_less_iff [iff]: "{} \<sqsubset> A \<longleftrightarrow> A \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({} \<sqsubset> A) = (A \<noteq> {})
[PROOF STEP]
by(simp add: set_less_def)


[STATEMENT]
lemma not_set_less_empty [simp]: "\<not> A \<sqsubset> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> A \<sqsubset> {}
[PROOF STEP]
by(simp add: set_less_def)


[STATEMENT]
lemma set_less_eq_UNIV [iff]: "A \<sqsubseteq> UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<sqsubseteq> UNIV
[PROOF STEP]
using Compl_set_less_eq_Compl[of "- A" "{}"]
[PROOF STATE]
proof (prove)
using this:
(- (- A) \<sqsubseteq> - {}) = ({} \<sqsubseteq> - A)

goal (1 subgoal):
 1. A \<sqsubseteq> UNIV
[PROOF STEP]
by simp


[STATEMENT]
lemma UNIV_set_less_eq [iff]: "UNIV \<sqsubseteq> A \<longleftrightarrow> A = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (UNIV \<sqsubseteq> A) = (A = UNIV)
[PROOF STEP]
using Compl_set_less_eq_Compl[of "{}" "- A"]
[PROOF STATE]
proof (prove)
using this:
(- {} \<sqsubseteq> - (- A)) = (- A \<sqsubseteq> {})

goal (1 subgoal):
 1. (UNIV \<sqsubseteq> A) = (A = UNIV)
[PROOF STEP]
by(simp add: Compl_eq_empty_iff)


[STATEMENT]
lemma set_less_UNIV_iff [iff]: "A \<sqsubset> UNIV \<longleftrightarrow> A \<noteq> UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<sqsubset> UNIV) = (A \<noteq> UNIV)
[PROOF STEP]
by(simp add: set_less_def)


[STATEMENT]
lemma not_UNIV_set_less [simp]: "\<not> UNIV \<sqsubset> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> UNIV \<sqsubset> A
[PROOF STEP]
by(simp add: set_less_def)