[STATEMENT]
theorem I_qe_dlo\<^sub>1:
assumes less: "\<forall>a \<in> set as. is_Less a" and dep: "\<forall>a \<in> set as. depends\<^sub>d\<^sub>l\<^sub>o a"
shows "DLO.I (qe_dlo\<^sub>1 as) xs = (\<exists>x. \<forall>a \<in> set as. I\<^sub>d\<^sub>l\<^sub>o a (x#xs))"
  (is "?L = ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DLO.I (qe_dlo\<^sub>1 as) xs = (\<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
let ?lbs = "[i. Less (Suc i) 0 \<leftarrow> as]"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
let ?ubs = "[j. Less 0 (Suc j) \<leftarrow> as]"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
let ?Ls = "set ?lbs"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
let ?Us = "set ?ubs"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
let ?lb = "Max (\<Union>x\<in>?Ls. {xs!x})"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
let ?ub = "Min (\<Union>x\<in>?Us. {xs!x})"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
have 2: "Less 0 0 \<notin> set as \<Longrightarrow> \<forall>a \<in> set as.
      (\<exists>i \<in> ?Ls. a = Less (Suc i) 0) \<or> (\<exists>i \<in> ?Us. a = Less 0 (Suc i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Less 0 0 \<notin> set as \<Longrightarrow> \<forall>a\<in>set as. (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less (Suc i) 0) \<or> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less 0 (Suc i))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>Less 0 0 \<notin> set as; a \<in> set as\<rbrakk> \<Longrightarrow> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less (Suc i) 0) \<or> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less 0 (Suc i))
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>Less 0 0 \<notin> set as; a \<in> set as\<rbrakk> \<Longrightarrow> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less (Suc i) 0) \<or> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less 0 (Suc i))
[PROOF STEP]
assume "Less 0 0 \<notin> set as" "a \<in> set as"
[PROOF STATE]
proof (state)
this:
Less 0 0 \<notin> set as
a \<in> set as

goal (1 subgoal):
 1. \<And>a. \<lbrakk>Less 0 0 \<notin> set as; a \<in> set as\<rbrakk> \<Longrightarrow> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less (Suc i) 0) \<or> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less 0 (Suc i))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Less 0 0 \<notin> set as
a \<in> set as
[PROOF STEP]
obtain i j where [simp]: "a = Less i j"
[PROOF STATE]
proof (prove)
using this:
Less 0 0 \<notin> set as
a \<in> set as

goal (1 subgoal):
 1. (\<And>i j. a = Less i j \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using less
[PROOF STATE]
proof (prove)
using this:
Less 0 0 \<notin> set as
a \<in> set as
\<forall>a\<in>set as. is_Less a

goal (1 subgoal):
 1. (\<And>i j. a = Less i j \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (force simp:is_Less_iff)
[PROOF STATE]
proof (state)
this:
a = Less i j

goal (1 subgoal):
 1. \<And>a. \<lbrakk>Less 0 0 \<notin> set as; a \<in> set as\<rbrakk> \<Longrightarrow> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less (Suc i) 0) \<or> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less 0 (Suc i))
[PROOF STEP]
with dep
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>set as. depends\<^sub>d\<^sub>l\<^sub>o a
a = Less i j
[PROOF STEP]
obtain k where "i = 0 \<and> j = Suc k \<or> i = Suc k \<and> j = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set as. depends\<^sub>d\<^sub>l\<^sub>o a
a = Less i j

goal (1 subgoal):
 1. (\<And>k. i = 0 \<and> j = Suc k \<or> i = Suc k \<and> j = 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>Less 0 0 \<notin> set as\<close> \<open>a \<in> set as\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set as. depends\<^sub>d\<^sub>l\<^sub>o a
a = Less i j
Less 0 0 \<notin> set as
a \<in> set as

goal (1 subgoal):
 1. (\<And>k. i = 0 \<and> j = Suc k \<or> i = Suc k \<and> j = 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto (metis Nat.nat.nchotomy depends\<^sub>d\<^sub>l\<^sub>o.simps(2))
[PROOF STATE]
proof (state)
this:
i = 0 \<and> j = Suc k \<or> i = Suc k \<and> j = 0

goal (1 subgoal):
 1. \<And>a. \<lbrakk>Less 0 0 \<notin> set as; a \<in> set as\<rbrakk> \<Longrightarrow> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less (Suc i) 0) \<or> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less 0 (Suc i))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i = 0 \<and> j = Suc k \<or> i = Suc k \<and> j = 0

goal (1 subgoal):
 1. \<And>a. \<lbrakk>Less 0 0 \<notin> set as; a \<in> set as\<rbrakk> \<Longrightarrow> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less (Suc i) 0) \<or> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less 0 (Suc i))
[PROOF STEP]
hence "i=0 \<and> k \<in> ?Us \<or> j=0 \<and> k \<in> ?Ls"
[PROOF STATE]
proof (prove)
using this:
i = 0 \<and> j = Suc k \<or> i = Suc k \<and> j = 0

goal (1 subgoal):
 1. i = 0 \<and> k \<in> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<or> j = 0 \<and> k \<in> set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as))
[PROOF STEP]
using \<open>a \<in> set as\<close>
[PROOF STATE]
proof (prove)
using this:
i = 0 \<and> j = Suc k \<or> i = Suc k \<and> j = 0
a \<in> set as

goal (1 subgoal):
 1. i = 0 \<and> k \<in> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<or> j = 0 \<and> k \<in> set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
i = 0 \<and> k \<in> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<or> j = 0 \<and> k \<in> set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as))

goal (1 subgoal):
 1. \<And>a. \<lbrakk>Less 0 0 \<notin> set as; a \<in> set as\<rbrakk> \<Longrightarrow> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less (Suc i) 0) \<or> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less 0 (Suc i))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i = 0 \<and> j = Suc k \<or> i = Suc k \<and> j = 0
i = 0 \<and> k \<in> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<or> j = 0 \<and> k \<in> set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as))
[PROOF STEP]
show "(\<exists>i\<in>?Ls. a=Less (Suc i) 0) \<or> (\<exists>i\<in>?Us. a=Less 0 (Suc i))"
[PROOF STATE]
proof (prove)
using this:
i = 0 \<and> j = Suc k \<or> i = Suc k \<and> j = 0
i = 0 \<and> k \<in> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<or> j = 0 \<and> k \<in> set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as))

goal (1 subgoal):
 1. (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less (Suc i) 0) \<or> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less 0 (Suc i))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less (Suc i) 0) \<or> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less 0 (Suc i))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Less 0 0 \<notin> set as \<Longrightarrow> \<forall>a\<in>set as. (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less (Suc i) 0) \<or> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less 0 (Suc i))

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
assume qe1: ?L
[PROOF STATE]
proof (state)
this:
DLO.I (qe_dlo\<^sub>1 as) xs

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
hence 0: "Less 0 0 \<notin> set as"
[PROOF STATE]
proof (prove)
using this:
DLO.I (qe_dlo\<^sub>1 as) xs

goal (1 subgoal):
 1. Less 0 0 \<notin> set as
[PROOF STEP]
by (auto simp:qe_dlo\<^sub>1_def)
[PROOF STATE]
proof (state)
this:
Less 0 0 \<notin> set as

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
with qe1
[PROOF STATE]
proof (chain)
picking this:
DLO.I (qe_dlo\<^sub>1 as) xs
Less 0 0 \<notin> set as
[PROOF STEP]
have 1: "\<forall>x\<in>?Ls. \<forall>y\<in>?Us. xs ! x < xs ! y"
[PROOF STATE]
proof (prove)
using this:
DLO.I (qe_dlo\<^sub>1 as) xs
Less 0 0 \<notin> set as

goal (1 subgoal):
 1. \<forall>x\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). \<forall>y\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). xs ! x < xs ! y
[PROOF STEP]
by (fastforce simp:qe_dlo\<^sub>1_def)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). \<forall>y\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). xs ! x < xs ! y

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
have finite: "finite ?Ls" "finite ?Us"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as))) &&& finite (set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)))
[PROOF STEP]
by (rule finite_set)+
[PROOF STATE]
proof (state)
this:
finite (set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)))
finite (set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)))

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
finite (set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)))
finite (set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)))

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
fix i x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
assume "Less i 0 \<in> set as | Less 0 i \<in> set as"
[PROOF STATE]
proof (state)
this:
Less i 0 \<in> set as \<or> Less 0 i \<in> set as

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Less i 0 \<in> set as \<or> Less 0 i \<in> set as

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
hence "i \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
Less i 0 \<in> set as \<or> Less 0 i \<in> set as

goal (1 subgoal):
 1. i \<noteq> 0
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
Less i 0 \<in> set as \<or> Less 0 i \<in> set as
Less 0 0 \<notin> set as

goal (1 subgoal):
 1. i \<noteq> 0
[PROOF STEP]
by iprover
[PROOF STATE]
proof (state)
this:
i \<noteq> 0

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Less i 0 \<in> set as \<or> Less 0 i \<in> set as
i \<noteq> 0
[PROOF STEP]
have "(x#xs) ! i = xs!(i - 1)"
[PROOF STATE]
proof (prove)
using this:
Less i 0 \<in> set as \<or> Less 0 i \<in> set as
i \<noteq> 0

goal (1 subgoal):
 1. (x # xs) ! i = xs ! (i - 1)
[PROOF STEP]
by (simp add: nth_Cons')
[PROOF STATE]
proof (state)
this:
(x # xs) ! i = xs ! (i - 1)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Less ?i2 0 \<in> set as \<or> Less 0 ?i2 \<in> set as \<Longrightarrow> (?x2 # xs) ! ?i2 = xs ! (?i2 - 1)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
note this[simp]
[PROOF STATE]
proof (state)
this:
Less ?i2 0 \<in> set as \<or> Less 0 ?i2 \<in> set as \<Longrightarrow> (?x2 # xs) ! ?i2 = xs ! (?i2 - 1)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Less ?i2 0 \<in> set as \<or> Less 0 ?i2 \<in> set as \<Longrightarrow> (?x2 # xs) ! ?i2 = xs ! (?i2 - 1)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
assume nonempty: "?Ls \<noteq> {} \<and> ?Us \<noteq> {}"
[PROOF STATE]
proof (state)
this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {}

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
hence "Max (\<Union>x\<in>?Ls. {xs!x}) < Min (\<Union>x\<in>?Us. {xs!x})"
[PROOF STATE]
proof (prove)
using this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {}

goal (1 subgoal):
 1. Max (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x}) < Min (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x})
[PROOF STEP]
using 1 finite
[PROOF STATE]
proof (prove)
using this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {}
\<forall>x\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). \<forall>y\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). xs ! x < xs ! y
finite (set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)))
finite (set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)))

goal (1 subgoal):
 1. Max (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x}) < Min (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Max (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x}) < Min (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x})

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Max (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x}) < Min (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x})
[PROOF STEP]
obtain m where "?lb < m \<and> m < ?ub"
[PROOF STATE]
proof (prove)
using this:
Max (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x}) < Min (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x})

goal (1 subgoal):
 1. (\<And>m. Max (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x}) < m \<and> m < Min (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x}) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using dense
[PROOF STATE]
proof (prove)
using this:
Max (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x}) < Min (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x})
?x < ?z \<Longrightarrow> \<exists>y>?x. y < ?z

goal (1 subgoal):
 1. (\<And>m. Max (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x}) < m \<and> m < Min (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x}) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Max (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x}) < m \<and> m < Min (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x})

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
hence "\<forall>i\<in>?Ls. xs!i < m" and "\<forall>j\<in>?Us. m < xs!j"
[PROOF STATE]
proof (prove)
using this:
Max (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x}) < m \<and> m < Min (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x})

goal (1 subgoal):
 1. \<forall>i\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). xs ! i < m &&& \<forall>j\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). m < xs ! j
[PROOF STEP]
using nonempty finite
[PROOF STATE]
proof (prove)
using this:
Max (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x}) < m \<and> m < Min (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x})
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {}
finite (set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)))
finite (set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)))

goal (1 subgoal):
 1. \<forall>i\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). xs ! i < m &&& \<forall>j\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). m < xs ! j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). xs ! i < m
\<forall>j\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). m < xs ! j

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
hence "\<forall>a \<in> set as. I\<^sub>d\<^sub>l\<^sub>o a (m # xs)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). xs ! i < m
\<forall>j\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). m < xs ! j

goal (1 subgoal):
 1. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (m # xs)
[PROOF STEP]
using 2[OF 0]
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). xs ! i < m
\<forall>j\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). m < xs ! j
\<forall>a\<in>set as. (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less (Suc i) 0) \<or> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less 0 (Suc i))

goal (1 subgoal):
 1. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (m # xs)
[PROOF STEP]
by(auto simp:less)
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (m # xs)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
hence ?R
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (m # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
assume asm: "?Ls \<noteq> {} \<and> ?Us = {}"
[PROOF STATE]
proof (state)
this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {}

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {}
[PROOF STEP]
obtain m where "?lb < m"
[PROOF STATE]
proof (prove)
using this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {}

goal (1 subgoal):
 1. (\<And>m. Max (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x}) < m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using no_ub
[PROOF STATE]
proof (prove)
using this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {}
\<exists>u. ?x < u

goal (1 subgoal):
 1. (\<And>m. Max (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x}) < m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Max (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x}) < m

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
hence "\<forall>a\<in> set as. I\<^sub>d\<^sub>l\<^sub>o a (m # xs)"
[PROOF STATE]
proof (prove)
using this:
Max (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x}) < m

goal (1 subgoal):
 1. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (m # xs)
[PROOF STEP]
using 2[OF 0] asm finite
[PROOF STATE]
proof (prove)
using this:
Max (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x}) < m
\<forall>a\<in>set as. (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less (Suc i) 0) \<or> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less 0 (Suc i))
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {}
finite (set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)))
finite (set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)))

goal (1 subgoal):
 1. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (m # xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (m # xs)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
hence ?R
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (m # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
assume asm: "?Ls = {} \<and> ?Us \<noteq> {}"
[PROOF STATE]
proof (state)
this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {}

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {}
[PROOF STEP]
obtain m where "m < ?ub"
[PROOF STATE]
proof (prove)
using this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {}

goal (1 subgoal):
 1. (\<And>m. m < Min (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x}) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using no_lb
[PROOF STATE]
proof (prove)
using this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {}
\<exists>l. l < ?x

goal (1 subgoal):
 1. (\<And>m. m < Min (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x}) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
m < Min (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x})

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
hence "\<forall>a\<in> set as. I\<^sub>d\<^sub>l\<^sub>o a (m # xs)"
[PROOF STATE]
proof (prove)
using this:
m < Min (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x})

goal (1 subgoal):
 1. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (m # xs)
[PROOF STEP]
using 2[OF 0] asm finite
[PROOF STATE]
proof (prove)
using this:
m < Min (\<Union>x\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). {xs ! x})
\<forall>a\<in>set as. (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less (Suc i) 0) \<or> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less 0 (Suc i))
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {}
finite (set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)))
finite (set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)))

goal (1 subgoal):
 1. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (m # xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (m # xs)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
hence ?R
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (m # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
assume "?Ls = {} \<and> ?Us = {}"
[PROOF STATE]
proof (state)
this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {}

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
hence ?R
[PROOF STATE]
proof (prove)
using this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {}

goal (1 subgoal):
 1. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
[PROOF STEP]
using 2[OF 0]
[PROOF STATE]
proof (prove)
using this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {}
\<forall>a\<in>set as. (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less (Suc i) 0) \<or> (\<exists>i\<in>set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)). a = Less 0 (Suc i))

goal (1 subgoal):
 1. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
[PROOF STEP]
by (auto simp add:less)
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

goal (2 subgoals):
 1. DLO.I (qe_dlo\<^sub>1 as) xs \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
 2. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
[PROOF STEP]
show ?R
[PROOF STATE]
proof (prove)
using this:
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) \<noteq> {} \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
set (concat (map (\<lambda>x. case x of Less 0 nat2 \<Rightarrow> [] | Less (Suc i) 0 \<Rightarrow> [i] | Less (Suc i) (Suc nata) \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<and> set (concat (map (\<lambda>x. case x of Less 0 0 \<Rightarrow> [] | Less 0 (Suc j) \<Rightarrow> [j] | Less (Suc nat) nat2 \<Rightarrow> [] | Eq nat1 nat2 \<Rightarrow> []) as)) = {} \<Longrightarrow> \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
assume ?R
[PROOF STATE]
proof (state)
this:
\<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)
[PROOF STEP]
obtain x where 1: "\<forall>a\<in> set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

goal (1 subgoal):
 1. (\<And>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

goal (1 subgoal):
 1. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
hence 0: "Less 0 0 \<notin> set as"
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

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

goal (1 subgoal):
 1. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Less 0 0 \<notin> set as

goal (1 subgoal):
 1. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
assume asm: "Less i 0 \<in> set as" "Less 0 j \<in> set as"
[PROOF STATE]
proof (state)
this:
Less i 0 \<in> set as
Less 0 j \<in> set as

goal (1 subgoal):
 1. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
hence "(x#xs)!i < x" "x < (x#xs)!j"
[PROOF STATE]
proof (prove)
using this:
Less i 0 \<in> set as
Less 0 j \<in> set as

goal (1 subgoal):
 1. (x # xs) ! i < x &&& x < (x # xs) ! j
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
Less i 0 \<in> set as
Less 0 j \<in> set as
\<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs)

goal (1 subgoal):
 1. (x # xs) ! i < x &&& x < (x # xs) ! j
[PROOF STEP]
by auto+
[PROOF STATE]
proof (state)
this:
(x # xs) ! i < x
x < (x # xs) ! j

goal (1 subgoal):
 1. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
hence "(x#xs)!i < (x#xs)!j"
[PROOF STATE]
proof (prove)
using this:
(x # xs) ! i < x
x < (x # xs) ! j

goal (1 subgoal):
 1. (x # xs) ! i < (x # xs) ! j
[PROOF STEP]
by(rule order_less_trans)
[PROOF STATE]
proof (state)
this:
(x # xs) ! i < (x # xs) ! j

goal (1 subgoal):
 1. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x # xs) ! i < (x # xs) ! j

goal (1 subgoal):
 1. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
have "\<not>(i = 0 | j = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (i = 0 \<or> j = 0)
[PROOF STEP]
using 0 asm
[PROOF STATE]
proof (prove)
using this:
Less 0 0 \<notin> set as
Less i 0 \<in> set as
Less 0 j \<in> set as

goal (1 subgoal):
 1. \<not> (i = 0 \<or> j = 0)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> (i = 0 \<or> j = 0)

goal (1 subgoal):
 1. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(x # xs) ! i < (x # xs) ! j
\<not> (i = 0 \<or> j = 0)
[PROOF STEP]
have "xs ! (i - 1) < xs ! (j - 1)"
[PROOF STATE]
proof (prove)
using this:
(x # xs) ! i < (x # xs) ! j
\<not> (i = 0 \<or> j = 0)

goal (1 subgoal):
 1. xs ! (i - 1) < xs ! (j - 1)
[PROOF STEP]
by (simp add: nth_Cons')
[PROOF STATE]
proof (state)
this:
xs ! (i - 1) < xs ! (j - 1)

goal (1 subgoal):
 1. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>Less ?i2 0 \<in> set as; Less 0 ?j2 \<in> set as\<rbrakk> \<Longrightarrow> xs ! (?i2 - 1) < xs ! (?j2 - 1)

goal (1 subgoal):
 1. \<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs) \<Longrightarrow> DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
thus ?L
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Less ?i2 0 \<in> set as; Less 0 ?j2 \<in> set as\<rbrakk> \<Longrightarrow> xs ! (?i2 - 1) < xs ! (?j2 - 1)

goal (1 subgoal):
 1. DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
using 0 less
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Less ?i2 0 \<in> set as; Less 0 ?j2 \<in> set as\<rbrakk> \<Longrightarrow> xs ! (?i2 - 1) < xs ! (?j2 - 1)
Less 0 0 \<notin> set as
\<forall>a\<in>set as. is_Less a

goal (1 subgoal):
 1. DLO.I (qe_dlo\<^sub>1 as) xs
[PROOF STEP]
by (fastforce simp: qe_dlo\<^sub>1_def is_Less_iff split:atom.splits nat.splits)
[PROOF STATE]
proof (state)
this:
DLO.I (qe_dlo\<^sub>1 as) xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma I_qe_dlo\<^sub>1_pretty:
  "\<forall>a \<in> set as. is_Less a \<and> depends\<^sub>d\<^sub>l\<^sub>o a \<Longrightarrow> DLO.is_dnf_qe _ qe_dlo\<^sub>1 as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>set as. is_Less a \<and> depends\<^sub>d\<^sub>l\<^sub>o a \<Longrightarrow> \<forall>xs. DLO.I (qe_dlo\<^sub>1 as) xs = (\<exists>x. \<forall>a\<in>set as. I\<^sub>d\<^sub>l\<^sub>o a (x # xs))
[PROOF STEP]
by(metis I_qe_dlo\<^sub>1)


[STATEMENT]
lemma subst\<^sub>0_pretty:
  "subst\<^sub>0 (Eq i j) (Less m n) = Less (subst i j m) (subst i j n)"
  "subst\<^sub>0 (Eq i j) (Eq m n) = Eq (subst i j m) (subst i j n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst\<^sub>0 (Eq i j) (Less m n) = Less (QEdlo.subst i j m) (QEdlo.subst i j n) &&& subst\<^sub>0 (Eq i j) (Eq m n) = Eq (QEdlo.subst i j m) (QEdlo.subst i j n)
[PROOF STEP]
by auto


[STATEMENT]
lemma qfree_qe_dlo\<^sub>1: "qfree (qe_dlo\<^sub>1 as)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qfree (qe_dlo\<^sub>1 as)
[PROOF STEP]
by(auto simp:qe_dlo\<^sub>1_def intro!:qfree_list_conj)


[STATEMENT]
theorem I_qe_dlo: "DLO.I (qe_dlo \<phi>) xs = DLO.I \<phi> xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DLO.I (qe_dlo \<phi>) xs = DLO.I \<phi> xs
[PROOF STEP]
unfolding qe_dlo_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DLO.I (DLO\<^sub>e.lift_dnfeq_qe qe_dlo\<^sub>1 \<phi>) xs = DLO.I \<phi> xs
[PROOF STEP]
by(fastforce intro!: I_qe_dlo\<^sub>1 qfree_qe_dlo\<^sub>1 DLO\<^sub>e.I_lift_dnfeq_qe
        simp: is_Less_iff not_is_Eq_iff split:atom.splits cong:conj_cong)


[STATEMENT]
theorem qfree_qe_dlo: "qfree (qe_dlo \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qfree (qe_dlo \<phi>)
[PROOF STEP]
by(simp add:qe_dlo_def DLO\<^sub>e.qfree_lift_dnfeq_qe qfree_qe_dlo\<^sub>1)


[STATEMENT]
lemma distance_mono:
assumes "C\<^sub>1 \<subseteq> C\<^sub>2" and "C\<^sub>1 \<noteq> {}" and "finite C\<^sub>2"
shows "distance C\<^sub>1 s \<ge> distance C\<^sub>2 s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distance C\<^sub>2 s \<le> distance C\<^sub>1 s
[PROOF STEP]
by (simp add: Min.subset_imp assms distance_def image_mono)


[STATEMENT]
lemma finite_distances: "finite (distance C ` S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (distance C ` S)
[PROOF STEP]
using finite_sites
[PROOF STATE]
proof (prove)
using this:
finite S

goal (1 subgoal):
 1. finite (distance C ` S)
[PROOF STEP]
by simp


[STATEMENT]
lemma non_empty_distances: "distance C ` S \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distance C ` S \<noteq> {}
[PROOF STEP]
using non_empty_sites
[PROOF STATE]
proof (prove)
using this:
S \<noteq> {}

goal (1 subgoal):
 1. distance C ` S \<noteq> {}
[PROOF STEP]
by simp


[STATEMENT]
lemma radius_contained: "radius C \<in> distance C ` S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. radius C \<in> distance C ` S
[PROOF STEP]
using finite_distances non_empty_distances Max_in radius_def
[PROOF STATE]
proof (prove)
using this:
finite (distance ?C ` S)
distance ?C ` S \<noteq> {}
\<lbrakk>finite ?A; ?A \<noteq> {}\<rbrakk> \<Longrightarrow> Max ?A \<in> ?A
radius ?C = Max (distance ?C ` S)

goal (1 subgoal):
 1. radius C \<in> distance C ` S
[PROOF STEP]
by simp


[STATEMENT]
lemma radius_def2: "\<exists>s \<in> S. distance C s = radius C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s\<in>S. distance C s = radius C
[PROOF STEP]
using radius_contained image_iff
[PROOF STATE]
proof (prove)
using this:
radius ?C \<in> distance ?C ` S
(?z \<in> ?f ` ?A) = (\<exists>x\<in>?A. ?z = ?f x)

goal (1 subgoal):
 1. \<exists>s\<in>S. distance C s = radius C
[PROOF STEP]
by metis


[STATEMENT]
lemma dist_lemmas_aux:
  assumes  "finite C"
      and  "C \<noteq> {}"
  shows  "finite (dist s ` C)"
    and "finite (dist s ` C) \<Longrightarrow> distance C s \<in> dist s ` C"
    and "distance C s \<in> dist s ` C \<Longrightarrow> \<exists>c \<in> C. dist s c = distance C s"
and "\<exists>c \<in> C. dist s c = distance C s \<Longrightarrow> distance C s \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (finite (dist s ` C) &&& (finite (dist s ` C) \<Longrightarrow> distance C s \<in> dist s ` C)) &&& (distance C s \<in> dist s ` C \<Longrightarrow> \<exists>c\<in>C. dist s c = distance C s) &&& (\<exists>c\<in>C. dist s c = distance C s \<Longrightarrow> 0 \<le> distance C s)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. finite C
 2. finite (dist s ` C) \<Longrightarrow> distance C s \<in> dist s ` C
 3. distance C s \<in> dist s ` C \<Longrightarrow> \<exists>c\<in>C. dist s c = distance C s
 4. \<exists>c\<in>C. dist s c = distance C s \<Longrightarrow> 0 \<le> distance C s
[PROOF STEP]
show "finite C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite C
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
finite C

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

goal (3 subgoals):
 1. finite (dist s ` C) \<Longrightarrow> distance C s \<in> dist s ` C
 2. distance C s \<in> dist s ` C \<Longrightarrow> \<exists>c\<in>C. dist s c = distance C s
 3. \<exists>c\<in>C. dist s c = distance C s \<Longrightarrow> 0 \<le> distance C s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. finite (dist s ` C) \<Longrightarrow> distance C s \<in> dist s ` C
 2. distance C s \<in> dist s ` C \<Longrightarrow> \<exists>c\<in>C. dist s c = distance C s
 3. \<exists>c\<in>C. dist s c = distance C s \<Longrightarrow> 0 \<le> distance C s
[PROOF STEP]
assume "finite (dist s ` C)"
[PROOF STATE]
proof (state)
this:
finite (dist s ` C)

goal (3 subgoals):
 1. finite (dist s ` C) \<Longrightarrow> distance C s \<in> dist s ` C
 2. distance C s \<in> dist s ` C \<Longrightarrow> \<exists>c\<in>C. dist s c = distance C s
 3. \<exists>c\<in>C. dist s c = distance C s \<Longrightarrow> 0 \<le> distance C s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (dist s ` C)
[PROOF STEP]
show "distance C s \<in> dist s ` C"
[PROOF STATE]
proof (prove)
using this:
finite (dist s ` C)

goal (1 subgoal):
 1. distance C s \<in> dist s ` C
[PROOF STEP]
using distance_def eq_Min_iff assms(2)
[PROOF STATE]
proof (prove)
using this:
finite (dist s ` C)
distance ?C ?s = Min (dist ?s ` ?C)
\<lbrakk>finite ?A; ?A \<noteq> {}\<rbrakk> \<Longrightarrow> (?m = Min ?A) = (?m \<in> ?A \<and> (\<forall>a\<in>?A. ?m \<le> a))
C \<noteq> {}

goal (1 subgoal):
 1. distance C s \<in> dist s ` C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distance C s \<in> dist s ` C

goal (2 subgoals):
 1. distance C s \<in> dist s ` C \<Longrightarrow> \<exists>c\<in>C. dist s c = distance C s
 2. \<exists>c\<in>C. dist s c = distance C s \<Longrightarrow> 0 \<le> distance C s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. distance C s \<in> dist s ` C \<Longrightarrow> \<exists>c\<in>C. dist s c = distance C s
 2. \<exists>c\<in>C. dist s c = distance C s \<Longrightarrow> 0 \<le> distance C s
[PROOF STEP]
assume "distance C s \<in> dist s ` C"
[PROOF STATE]
proof (state)
this:
distance C s \<in> dist s ` C

goal (2 subgoals):
 1. distance C s \<in> dist s ` C \<Longrightarrow> \<exists>c\<in>C. dist s c = distance C s
 2. \<exists>c\<in>C. dist s c = distance C s \<Longrightarrow> 0 \<le> distance C s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distance C s \<in> dist s ` C
[PROOF STEP]
show "\<exists>c \<in> C. dist s c = distance C s"
[PROOF STATE]
proof (prove)
using this:
distance C s \<in> dist s ` C

goal (1 subgoal):
 1. \<exists>c\<in>C. dist s c = distance C s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>c\<in>C. dist s c = distance C s

goal (1 subgoal):
 1. \<exists>c\<in>C. dist s c = distance C s \<Longrightarrow> 0 \<le> distance C s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>c\<in>C. dist s c = distance C s \<Longrightarrow> 0 \<le> distance C s
[PROOF STEP]
assume "\<exists>c \<in> C. dist s c = distance C s"
[PROOF STATE]
proof (state)
this:
\<exists>c\<in>C. dist s c = distance C s

goal (1 subgoal):
 1. \<exists>c\<in>C. dist s c = distance C s \<Longrightarrow> 0 \<le> distance C s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>c\<in>C. dist s c = distance C s
[PROOF STEP]
show "distance C s \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>c\<in>C. dist s c = distance C s

goal (1 subgoal):
 1. 0 \<le> distance C s
[PROOF STEP]
by (metis zero_le_dist)
[PROOF STATE]
proof (state)
this:
0 \<le> distance C s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dist_lemmas:
  assumes "finite C"
      and "C \<noteq> {}"
  shows "finite (dist s ` C)"
    and "distance C s \<in> dist s ` C"
    and "\<exists>c \<in> C. dist s c = distance C s"
    and "distance C s \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (finite (dist s ` C) &&& distance C s \<in> dist s ` C) &&& \<exists>c\<in>C. dist s c = distance C s &&& 0 \<le> distance C s
[PROOF STEP]
using dist_lemmas_aux assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?C; ?C \<noteq> {}\<rbrakk> \<Longrightarrow> finite (dist ?s ` ?C)
\<lbrakk>finite ?C; ?C \<noteq> {}; finite (dist ?s ` ?C)\<rbrakk> \<Longrightarrow> distance ?C ?s \<in> dist ?s ` ?C
\<lbrakk>finite ?C; ?C \<noteq> {}; distance ?C ?s \<in> dist ?s ` ?C\<rbrakk> \<Longrightarrow> \<exists>c\<in>?C. dist ?s c = distance ?C ?s
\<lbrakk>finite ?C; ?C \<noteq> {}; \<exists>c\<in>?C. dist ?s c = distance ?C ?s\<rbrakk> \<Longrightarrow> 0 \<le> distance ?C ?s
finite C
C \<noteq> {}

goal (1 subgoal):
 1. (finite (dist s ` C) &&& distance C s \<in> dist s ` C) &&& \<exists>c\<in>C. dist s c = distance C s &&& 0 \<le> distance C s
[PROOF STEP]
by auto


[STATEMENT]
lemma radius_max_prop: "(\<forall>s \<in> S. distance C s \<le> r) \<Longrightarrow> (radius C \<le> r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s\<in>S. distance C s \<le> r \<Longrightarrow> radius C \<le> r
[PROOF STEP]
by (metis image_iff radius_contained)


[STATEMENT]
lemma dist_ins:
assumes "\<forall>c\<^sub>1 \<in> C. \<forall>c\<^sub>2 \<in> C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> x < dist c\<^sub>1 c\<^sub>2"
and "distance C s > x"
and "finite C"
and "C \<noteq> {}"
shows "\<forall>c\<^sub>1 \<in> (C \<union> {s}). \<forall>c\<^sub>2 \<in> (C \<union> {s}). c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> x < dist c\<^sub>1 c\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c\<^sub>1\<in>C \<union> {s}. \<forall>c\<^sub>2\<in>C \<union> {s}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
proof (rule+)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c\<^sub>1 c\<^sub>2. \<lbrakk>c\<^sub>1 \<in> C \<union> {s}; c\<^sub>2 \<in> C \<union> {s}; c\<^sub>1 \<noteq> c\<^sub>2\<rbrakk> \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
fix c\<^sub>1 c\<^sub>2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c\<^sub>1 c\<^sub>2. \<lbrakk>c\<^sub>1 \<in> C \<union> {s}; c\<^sub>2 \<in> C \<union> {s}; c\<^sub>1 \<noteq> c\<^sub>2\<rbrakk> \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
assume local_assms: "c\<^sub>1\<in>C \<union> {s}" "c\<^sub>2\<in>C \<union> {s}" "c\<^sub>1 \<noteq> c\<^sub>2"
[PROOF STATE]
proof (state)
this:
c\<^sub>1 \<in> C \<union> {s}
c\<^sub>2 \<in> C \<union> {s}
c\<^sub>1 \<noteq> c\<^sub>2

goal (1 subgoal):
 1. \<And>c\<^sub>1 c\<^sub>2. \<lbrakk>c\<^sub>1 \<in> C \<union> {s}; c\<^sub>2 \<in> C \<union> {s}; c\<^sub>1 \<noteq> c\<^sub>2\<rbrakk> \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c\<^sub>1 \<in> C \<union> {s}
c\<^sub>2 \<in> C \<union> {s}
c\<^sub>1 \<noteq> c\<^sub>2
[PROOF STEP]
have "c\<^sub>1 \<in> C  \<and> c\<^sub>2 \<in> C  \<or> c\<^sub>1 \<in>C  \<and> c\<^sub>2\<in> {s} \<or> c\<^sub>2\<in>C  \<and> c\<^sub>1 \<in> {s} \<or> c\<^sub>1 \<in> {s} \<and> c\<^sub>2\<in> {s}"
[PROOF STATE]
proof (prove)
using this:
c\<^sub>1 \<in> C \<union> {s}
c\<^sub>2 \<in> C \<union> {s}
c\<^sub>1 \<noteq> c\<^sub>2

goal (1 subgoal):
 1. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C \<or> c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> {s} \<or> c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s} \<or> c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C \<or> c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> {s} \<or> c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s} \<or> c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s}

goal (1 subgoal):
 1. \<And>c\<^sub>1 c\<^sub>2. \<lbrakk>c\<^sub>1 \<in> C \<union> {s}; c\<^sub>2 \<in> C \<union> {s}; c\<^sub>1 \<noteq> c\<^sub>2\<rbrakk> \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C \<or> c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> {s} \<or> c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s} \<or> c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s}
[PROOF STEP]
show "x < dist c\<^sub>1 c\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C \<or> c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> {s} \<or> c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s} \<or> c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s}

goal (1 subgoal):
 1. x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 3. c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 4. c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
assume "c\<^sub>1 \<in>C  \<and> c\<^sub>2\<in>C"
[PROOF STATE]
proof (state)
this:
c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C

goal (4 subgoals):
 1. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 3. c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 4. c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C

goal (1 subgoal):
 1. x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
using assms(1) local_assms(3)
[PROOF STATE]
proof (prove)
using this:
c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> C
\<forall>c\<^sub>1\<in>C. \<forall>c\<^sub>2\<in>C. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> x < dist c\<^sub>1 c\<^sub>2
c\<^sub>1 \<noteq> c\<^sub>2

goal (1 subgoal):
 1. x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x < dist c\<^sub>1 c\<^sub>2

goal (3 subgoals):
 1. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 3. c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 3. c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
assume case_assm: "c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> {s}"
[PROOF STATE]
proof (state)
this:
c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> {s}

goal (3 subgoals):
 1. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 3. c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
have "x < distance C c\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < distance C c\<^sub>2
[PROOF STEP]
using assms(2) case_assm
[PROOF STATE]
proof (prove)
using this:
x < distance C s
c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> {s}

goal (1 subgoal):
 1. x < distance C c\<^sub>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x < distance C c\<^sub>2

goal (3 subgoals):
 1. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 3. c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x < distance C c\<^sub>2

goal (3 subgoals):
 1. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 3. c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
have " ... \<le> dist c\<^sub>2 c\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distance C c\<^sub>2 \<le> dist c\<^sub>2 c\<^sub>1
[PROOF STEP]
using Min.coboundedI distance_def assms(3,4) dist_lemmas(1, 2) case_assm
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; ?a \<in> ?A\<rbrakk> \<Longrightarrow> Min ?A \<le> ?a
distance ?C ?s = Min (dist ?s ` ?C)
finite C
C \<noteq> {}
\<lbrakk>finite ?C; ?C \<noteq> {}\<rbrakk> \<Longrightarrow> finite (dist ?s ` ?C)
\<lbrakk>finite ?C; ?C \<noteq> {}\<rbrakk> \<Longrightarrow> distance ?C ?s \<in> dist ?s ` ?C
c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> {s}

goal (1 subgoal):
 1. distance C c\<^sub>2 \<le> dist c\<^sub>2 c\<^sub>1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distance C c\<^sub>2 \<le> dist c\<^sub>2 c\<^sub>1

goal (3 subgoals):
 1. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 3. c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
distance C c\<^sub>2 \<le> dist c\<^sub>2 c\<^sub>1

goal (3 subgoals):
 1. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 3. c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
have " ... = dist c\<^sub>1 c\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist c\<^sub>2 c\<^sub>1 = dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
using dist_commute
[PROOF STATE]
proof (prove)
using this:
dist ?x ?y = dist ?y ?x

goal (1 subgoal):
 1. dist c\<^sub>2 c\<^sub>1 = dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
dist c\<^sub>2 c\<^sub>1 = dist c\<^sub>1 c\<^sub>2

goal (3 subgoals):
 1. c\<^sub>1 \<in> C \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 3. c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x < dist c\<^sub>1 c\<^sub>2

goal (1 subgoal):
 1. x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x < dist c\<^sub>1 c\<^sub>2

goal (2 subgoals):
 1. c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
assume case_assm: "c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s}"
[PROOF STATE]
proof (state)
this:
c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s}

goal (2 subgoals):
 1. c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
have "x < distance C c\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < distance C c\<^sub>1
[PROOF STEP]
using assms(2) case_assm
[PROOF STATE]
proof (prove)
using this:
x < distance C s
c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s}

goal (1 subgoal):
 1. x < distance C c\<^sub>1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x < distance C c\<^sub>1

goal (2 subgoals):
 1. c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x < distance C c\<^sub>1

goal (2 subgoals):
 1. c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
have " ... \<le> dist c\<^sub>1 c\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distance C c\<^sub>1 \<le> dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
using Min.coboundedI distance_def assms(3,4) dist_lemmas(1, 2) case_assm
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; ?a \<in> ?A\<rbrakk> \<Longrightarrow> Min ?A \<le> ?a
distance ?C ?s = Min (dist ?s ` ?C)
finite C
C \<noteq> {}
\<lbrakk>finite ?C; ?C \<noteq> {}\<rbrakk> \<Longrightarrow> finite (dist ?s ` ?C)
\<lbrakk>finite ?C; ?C \<noteq> {}\<rbrakk> \<Longrightarrow> distance ?C ?s \<in> dist ?s ` ?C
c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s}

goal (1 subgoal):
 1. distance C c\<^sub>1 \<le> dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distance C c\<^sub>1 \<le> dist c\<^sub>1 c\<^sub>2

goal (2 subgoals):
 1. c\<^sub>2 \<in> C \<and> c\<^sub>1 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
 2. c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x < dist c\<^sub>1 c\<^sub>2

goal (1 subgoal):
 1. x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x < dist c\<^sub>1 c\<^sub>2

goal (1 subgoal):
 1. c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
assume "c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s}"
[PROOF STATE]
proof (state)
this:
c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s}

goal (1 subgoal):
 1. c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s}
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s}

goal (1 subgoal):
 1. False
[PROOF STEP]
using local_assms
[PROOF STATE]
proof (prove)
using this:
c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s}
c\<^sub>1 \<in> C \<union> {s}
c\<^sub>2 \<in> C \<union> {s}
c\<^sub>1 \<noteq> c\<^sub>2

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

goal (1 subgoal):
 1. c\<^sub>1 \<in> {s} \<and> c\<^sub>2 \<in> {s} \<Longrightarrow> x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. x < dist c\<^sub>1 c\<^sub>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x < dist c\<^sub>1 c\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x < dist c\<^sub>1 c\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv_init: "inv S {} r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.inv S {} r
[PROOF STEP]
unfolding inv_def non_empty_sites
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>s\<in>S - S. distance {} s \<le> 2 * r) \<and> S \<subseteq> S \<and> {} \<subseteq> S \<and> (\<forall>c\<in>{}. \<forall>s\<in>S. S \<noteq> {} \<longrightarrow> 2 * r < dist c s) \<and> (S = S \<or> {} \<noteq> {}) \<and> (\<forall>c\<^sub>1\<in>{}. \<forall>c\<^sub>2\<in>{}. c\<^sub>1 \<noteq> c\<^sub>2 \<longrightarrow> 2 * r < dist c\<^sub>1 c\<^sub>2)
[PROOF STEP]
by simp