[STATEMENT]
lemma same_bound:
assumes
  hC: "C \<subseteq> PR" and
  hCk: "np <= card C + khl" and
  hnk: "3 * khl < np"
shows
  "\<exists> i\<in>C. Min (reduce f PR) <= f i \<and> g i <= Max (reduce g PR) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i\<in>C. Min (reduce f PR) \<le> f i \<and> g i \<le> Max (reduce g PR)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i\<in>C. Min (reduce f PR) \<le> f i \<and> g i \<le> Max (reduce g PR)
[PROOF STEP]
have b1: "khl + 1 <= card (C \<inter> (PR - kmin f PR))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. khl + 1 \<le> card (C \<inter> (PR - kmin f PR))
[PROOF STEP]
proof(rule pigeonhole)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. finite ?A
 2. C \<subseteq> ?A
 3. PR - kmin f PR \<subseteq> ?A
 4. card ?A + (khl + 1) \<le> card C + card (PR - kmin f PR)
[PROOF STEP]
show "finite PR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite PR
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite PR

goal (3 subgoals):
 1. C \<subseteq> PR
 2. PR - kmin f PR \<subseteq> PR
 3. card PR + (khl + 1) \<le> card C + card (PR - kmin f PR)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. C \<subseteq> PR
 2. PR - kmin f PR \<subseteq> PR
 3. card PR + (khl + 1) \<le> card C + card (PR - kmin f PR)
[PROOF STEP]
show "C \<subseteq> PR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<subseteq> PR
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
C \<subseteq> PR

goal (2 subgoals):
 1. PR - kmin f PR \<subseteq> PR
 2. card PR + (khl + 1) \<le> card C + card (PR - kmin f PR)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. PR - kmin f PR \<subseteq> PR
 2. card PR + (khl + 1) \<le> card C + card (PR - kmin f PR)
[PROOF STEP]
show "PR - kmin f PR \<subseteq> PR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PR - kmin f PR \<subseteq> PR
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
PR - kmin f PR \<subseteq> PR

goal (1 subgoal):
 1. card PR + (khl + 1) \<le> card C + card (PR - kmin f PR)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card PR + (khl + 1) \<le> card C + card (PR - kmin f PR)
[PROOF STEP]
show "card PR + (khl + 1) \<le> card C + card (PR - kmin f PR)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card PR + (khl + 1) \<le> card C + card (PR - kmin f PR)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card PR + (khl + 1) \<le> card C + card (PR - kmin f PR)
[PROOF STEP]
from hnk and hCk
[PROOF STATE]
proof (chain)
picking this:
3 * khl < np
np \<le> card C + khl
[PROOF STEP]
have
        "np + khl < np + card C - khl"
[PROOF STATE]
proof (prove)
using this:
3 * khl < np
np \<le> card C + khl

goal (1 subgoal):
 1. np + khl < np + card C - khl
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
np + khl < np + card C - khl

goal (1 subgoal):
 1. card PR + (khl + 1) \<le> card C + card (PR - kmin f PR)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
np + khl < np + card C - khl

goal (1 subgoal):
 1. card PR + (khl + 1) \<le> card C + card (PR - kmin f PR)
[PROOF STEP]
from kmin_prop
[PROOF STATE]
proof (chain)
picking this:
kmin ?f PR \<subseteq> PR \<and> card (kmin ?f PR) = khl \<and> (\<forall>i\<in>kmin ?f PR. \<forall>j\<in>PR - kmin ?f PR. ?f i \<le> ?f j)
[PROOF STEP]
have "... = np + card C - card (kmin f PR)"
[PROOF STATE]
proof (prove)
using this:
kmin ?f PR \<subseteq> PR \<and> card (kmin ?f PR) = khl \<and> (\<forall>i\<in>kmin ?f PR. \<forall>j\<in>PR - kmin ?f PR. ?f i \<le> ?f j)

goal (1 subgoal):
 1. np + card C - khl = np + card C - card (kmin f PR)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
np + card C - khl = np + card C - card (kmin f PR)

goal (1 subgoal):
 1. card PR + (khl + 1) \<le> card C + card (PR - kmin f PR)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
np + card C - khl = np + card C - card (kmin f PR)

goal (1 subgoal):
 1. card PR + (khl + 1) \<le> card C + card (PR - kmin f PR)
[PROOF STEP]
have "... = card C + (card PR - card (kmin f PR))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. np + card C - card (kmin f PR) = card C + (card PR - card (kmin f PR))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. np + card C - card (kmin f PR) = card C + (card PR - card (kmin f PR))
[PROOF STEP]
from kmin_prop
[PROOF STATE]
proof (chain)
picking this:
kmin ?f PR \<subseteq> PR \<and> card (kmin ?f PR) = khl \<and> (\<forall>i\<in>kmin ?f PR. \<forall>j\<in>PR - kmin ?f PR. ?f i \<le> ?f j)
[PROOF STEP]
have
          "card (kmin f PR) <= card PR"
[PROOF STATE]
proof (prove)
using this:
kmin ?f PR \<subseteq> PR \<and> card (kmin ?f PR) = khl \<and> (\<forall>i\<in>kmin ?f PR. \<forall>j\<in>PR - kmin ?f PR. ?f i \<le> ?f j)

goal (1 subgoal):
 1. card (kmin f PR) \<le> card PR
[PROOF STEP]
by (intro card_mono, auto)
[PROOF STATE]
proof (state)
this:
card (kmin f PR) \<le> card PR

goal (1 subgoal):
 1. np + card C - card (kmin f PR) = card C + (card PR - card (kmin f PR))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
card (kmin f PR) \<le> card PR

goal (1 subgoal):
 1. np + card C - card (kmin f PR) = card C + (card PR - card (kmin f PR))
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
np + card C - card (kmin f PR) = card C + (card PR - card (kmin f PR))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
np + card C - card (kmin f PR) = card C + (card PR - card (kmin f PR))

goal (1 subgoal):
 1. card PR + (khl + 1) \<le> card C + card (PR - kmin f PR)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
np + card C - card (kmin f PR) = card C + (card PR - card (kmin f PR))

goal (1 subgoal):
 1. card PR + (khl + 1) \<le> card C + card (PR - kmin f PR)
[PROOF STEP]
from kmin_prop
[PROOF STATE]
proof (chain)
picking this:
kmin ?f PR \<subseteq> PR \<and> card (kmin ?f PR) = khl \<and> (\<forall>i\<in>kmin ?f PR. \<forall>j\<in>PR - kmin ?f PR. ?f i \<le> ?f j)
[PROOF STEP]
have "... = card C +  card (PR - kmin f PR)"
[PROOF STATE]
proof (prove)
using this:
kmin ?f PR \<subseteq> PR \<and> card (kmin ?f PR) = khl \<and> (\<forall>i\<in>kmin ?f PR. \<forall>j\<in>PR - kmin ?f PR. ?f i \<le> ?f j)

goal (1 subgoal):
 1. card C + (card PR - card (kmin f PR)) = card C + card (PR - kmin f PR)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>f. kmin f PR \<subseteq> PR \<and> card (kmin f PR) = khl \<and> (\<forall>i\<in>kmin f PR. \<forall>j\<in>PR - kmin f PR. f i \<le> f j)) \<Longrightarrow> card C + (card PR - card (kmin f PR)) = card C + card (PR - kmin f PR)
[PROOF STEP]
from kmin_prop and finite_kmin
[PROOF STATE]
proof (chain)
picking this:
kmin ?f PR \<subseteq> PR \<and> card (kmin ?f PR) = khl \<and> (\<forall>i\<in>kmin ?f PR. \<forall>j\<in>PR - kmin ?f PR. ?f i \<le> ?f j)
finite (kmin ?f PR)
[PROOF STEP]
have
          "card PR - card (kmin f PR) =  card (PR - kmin f PR)"
[PROOF STATE]
proof (prove)
using this:
kmin ?f PR \<subseteq> PR \<and> card (kmin ?f PR) = khl \<and> (\<forall>i\<in>kmin ?f PR. \<forall>j\<in>PR - kmin ?f PR. ?f i \<le> ?f j)
finite (kmin ?f PR)

goal (1 subgoal):
 1. card PR - card (kmin f PR) = card (PR - kmin f PR)
[PROOF STEP]
by (intro card_Diff_subset[THEN sym])(auto)
[PROOF STATE]
proof (state)
this:
card PR - card (kmin f PR) = card (PR - kmin f PR)

goal (1 subgoal):
 1. (\<And>f. kmin f PR \<subseteq> PR \<and> card (kmin f PR) = khl \<and> (\<forall>i\<in>kmin f PR. \<forall>j\<in>PR - kmin f PR. f i \<le> f j)) \<Longrightarrow> card C + (card PR - card (kmin f PR)) = card C + card (PR - kmin f PR)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
card PR - card (kmin f PR) = card (PR - kmin f PR)

goal (1 subgoal):
 1. card C + (card PR - card (kmin f PR)) = card C + card (PR - kmin f PR)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card C + (card PR - card (kmin f PR)) = card C + card (PR - kmin f PR)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card C + (card PR - card (kmin f PR)) = card C + card (PR - kmin f PR)

goal (1 subgoal):
 1. card PR + (khl + 1) \<le> card C + card (PR - kmin f PR)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
np + khl < card C + card (PR - kmin f PR)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
np + khl < card C + card (PR - kmin f PR)

goal (1 subgoal):
 1. card PR + (khl + 1) \<le> card C + card (PR - kmin f PR)
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
card PR + (khl + 1) \<le> card C + card (PR - kmin f PR)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card PR + (khl + 1) \<le> card C + card (PR - kmin f PR)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
khl + 1 \<le> card (C \<inter> (PR - kmin f PR))

goal (1 subgoal):
 1. \<exists>i\<in>C. Min (reduce f PR) \<le> f i \<and> g i \<le> Max (reduce g PR)
[PROOF STEP]
have "C \<inter> (PR - kmin f PR) \<inter> (PR - kmax g PR) \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<inter> (PR - kmin f PR) \<inter> (PR - kmax g PR) \<noteq> {}
[PROOF STEP]
proof(intro subsets_int)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. finite ?A
 2. C \<inter> (PR - kmin f PR) \<subseteq> ?A
 3. PR - kmax g PR \<subseteq> ?A
 4. card ?A < card (C \<inter> (PR - kmin f PR)) + card (PR - kmax g PR)
[PROOF STEP]
show "finite PR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite PR
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite PR

goal (3 subgoals):
 1. C \<inter> (PR - kmin f PR) \<subseteq> PR
 2. PR - kmax g PR \<subseteq> PR
 3. card PR < card (C \<inter> (PR - kmin f PR)) + card (PR - kmax g PR)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. C \<inter> (PR - kmin f PR) \<subseteq> PR
 2. PR - kmax g PR \<subseteq> PR
 3. card PR < card (C \<inter> (PR - kmin f PR)) + card (PR - kmax g PR)
[PROOF STEP]
show "C \<inter> (PR - kmin f PR) \<subseteq> PR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<inter> (PR - kmin f PR) \<subseteq> PR
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C \<inter> (PR - kmin f PR) \<subseteq> PR

goal (2 subgoals):
 1. PR - kmax g PR \<subseteq> PR
 2. card PR < card (C \<inter> (PR - kmin f PR)) + card (PR - kmax g PR)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. PR - kmax g PR \<subseteq> PR
 2. card PR < card (C \<inter> (PR - kmin f PR)) + card (PR - kmax g PR)
[PROOF STEP]
show "PR - kmax g PR \<subseteq> PR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PR - kmax g PR \<subseteq> PR
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
PR - kmax g PR \<subseteq> PR

goal (1 subgoal):
 1. card PR < card (C \<inter> (PR - kmin f PR)) + card (PR - kmax g PR)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card PR < card (C \<inter> (PR - kmin f PR)) + card (PR - kmax g PR)
[PROOF STEP]
show "card PR <
      card (C \<inter> (PR - kmin f PR)) + card (PR - kmax g PR)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card PR < card (C \<inter> (PR - kmin f PR)) + card (PR - kmax g PR)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card PR < card (C \<inter> (PR - kmin f PR)) + card (PR - kmax g PR)
[PROOF STEP]
from kmax_prop and finite_kmax
[PROOF STATE]
proof (chain)
picking this:
kmax ?f PR \<subseteq> PR \<and> card (kmax ?f PR) = khl \<and> (\<forall>i\<in>kmax ?f PR. \<forall>j\<in>PR - kmax ?f PR. ?f j \<le> ?f i)
finite (kmax ?f PR)
[PROOF STEP]
have "card (PR - kmax g PR)= card PR - card (kmax g PR) "
[PROOF STATE]
proof (prove)
using this:
kmax ?f PR \<subseteq> PR \<and> card (kmax ?f PR) = khl \<and> (\<forall>i\<in>kmax ?f PR. \<forall>j\<in>PR - kmax ?f PR. ?f j \<le> ?f i)
finite (kmax ?f PR)

goal (1 subgoal):
 1. card (PR - kmax g PR) = card PR - card (kmax g PR)
[PROOF STEP]
by  (intro card_Diff_subset, auto)
[PROOF STATE]
proof (state)
this:
card (PR - kmax g PR) = card PR - card (kmax g PR)

goal (1 subgoal):
 1. card PR < card (C \<inter> (PR - kmin f PR)) + card (PR - kmax g PR)
[PROOF STEP]
with kmax_prop
[PROOF STATE]
proof (chain)
picking this:
kmax ?f PR \<subseteq> PR \<and> card (kmax ?f PR) = khl \<and> (\<forall>i\<in>kmax ?f PR. \<forall>j\<in>PR - kmax ?f PR. ?f j \<le> ?f i)
card (PR - kmax g PR) = card PR - card (kmax g PR)
[PROOF STEP]
have
        "card (PR - kmax g PR) = card PR - khl"
[PROOF STATE]
proof (prove)
using this:
kmax ?f PR \<subseteq> PR \<and> card (kmax ?f PR) = khl \<and> (\<forall>i\<in>kmax ?f PR. \<forall>j\<in>PR - kmax ?f PR. ?f j \<le> ?f i)
card (PR - kmax g PR) = card PR - card (kmax g PR)

goal (1 subgoal):
 1. card (PR - kmax g PR) = card PR - khl
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (PR - kmax g PR) = card PR - khl

goal (1 subgoal):
 1. card PR < card (C \<inter> (PR - kmin f PR)) + card (PR - kmax g PR)
[PROOF STEP]
with b1
[PROOF STATE]
proof (chain)
picking this:
khl + 1 \<le> card (C \<inter> (PR - kmin f PR))
card (PR - kmax g PR) = card PR - khl
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
khl + 1 \<le> card (C \<inter> (PR - kmin f PR))
card (PR - kmax g PR) = card PR - khl

goal (1 subgoal):
 1. card PR < card (C \<inter> (PR - kmin f PR)) + card (PR - kmax g PR)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
card PR < card (C \<inter> (PR - kmin f PR)) + card (PR - kmax g PR)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card PR < card (C \<inter> (PR - kmin f PR)) + card (PR - kmax g PR)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
C \<inter> (PR - kmin f PR) \<inter> (PR - kmax g PR) \<noteq> {}

goal (1 subgoal):
 1. \<exists>i\<in>C. Min (reduce f PR) \<le> f i \<and> g i \<le> Max (reduce g PR)
[PROOF STEP]
hence
    "\<exists> i. i \<in> C \<and> i \<in> (PR - kmin f PR) \<and> i \<in> (PR - kmax g PR)"
[PROOF STATE]
proof (prove)
using this:
C \<inter> (PR - kmin f PR) \<inter> (PR - kmax g PR) \<noteq> {}

goal (1 subgoal):
 1. \<exists>i. i \<in> C \<and> i \<in> PR - kmin f PR \<and> i \<in> PR - kmax g PR
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>i. i \<in> C \<and> i \<in> PR - kmin f PR \<and> i \<in> PR - kmax g PR

goal (1 subgoal):
 1. \<exists>i\<in>C. Min (reduce f PR) \<le> f i \<and> g i \<le> Max (reduce g PR)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. i \<in> C \<and> i \<in> PR - kmin f PR \<and> i \<in> PR - kmax g PR
[PROOF STEP]
obtain i where
    in_C: "i \<in> C" and
    not_in_kmin: "i \<in> (PR - kmin f PR)" and
    not_in_kmax: "i \<in> (PR - kmax g PR)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. i \<in> C \<and> i \<in> PR - kmin f PR \<and> i \<in> PR - kmax g PR

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i \<in> C; i \<in> PR - kmin f PR; i \<in> PR - kmax g PR\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i \<in> C
i \<in> PR - kmin f PR
i \<in> PR - kmax g PR

goal (1 subgoal):
 1. \<exists>i\<in>C. Min (reduce f PR) \<le> f i \<and> g i \<le> Max (reduce g PR)
[PROOF STEP]
have "Min (reduce f PR) <= f i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (reduce f PR) \<le> f i
[PROOF STEP]
proof(cases "i \<in> kmax f PR")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i \<in> kmax f PR \<Longrightarrow> Min (reduce f PR) \<le> f i
 2. i \<notin> kmax f PR \<Longrightarrow> Min (reduce f PR) \<le> f i
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i \<in> kmax f PR

goal (2 subgoals):
 1. i \<in> kmax f PR \<Longrightarrow> Min (reduce f PR) \<le> f i
 2. i \<notin> kmax f PR \<Longrightarrow> Min (reduce f PR) \<le> f i
[PROOF STEP]
from reduce_not_empty and finite_reduce
[PROOF STATE]
proof (chain)
picking this:
reduce ?f PR \<noteq> {}
finite (reduce ?f PR)
[PROOF STEP]
have
      " Min (reduce f PR) \<in> reduce f PR"
[PROOF STATE]
proof (prove)
using this:
reduce ?f PR \<noteq> {}
finite (reduce ?f PR)

goal (1 subgoal):
 1. Min (reduce f PR) \<in> reduce f PR
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Min (reduce f PR) \<in> reduce f PR

goal (2 subgoals):
 1. i \<in> kmax f PR \<Longrightarrow> Min (reduce f PR) \<le> f i
 2. i \<notin> kmax f PR \<Longrightarrow> Min (reduce f PR) \<le> f i
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
i \<in> kmax f PR
Min (reduce f PR) \<in> reduce f PR
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<in> kmax f PR
Min (reduce f PR) \<in> reduce f PR

goal (1 subgoal):
 1. Min (reduce f PR) \<le> f i
[PROOF STEP]
using kmax_ge
[PROOF STATE]
proof (prove)
using this:
i \<in> kmax f PR
Min (reduce f PR) \<in> reduce f PR
\<forall>i\<in>kmax ?f PR. \<forall>r\<in>reduce ?f PR. r \<le> ?f i

goal (1 subgoal):
 1. Min (reduce f PR) \<le> f i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Min (reduce f PR) \<le> f i

goal (1 subgoal):
 1. i \<notin> kmax f PR \<Longrightarrow> Min (reduce f PR) \<le> f i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<notin> kmax f PR \<Longrightarrow> Min (reduce f PR) \<le> f i
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<notin> kmax f PR

goal (1 subgoal):
 1. i \<notin> kmax f PR \<Longrightarrow> Min (reduce f PR) \<le> f i
[PROOF STEP]
with not_in_kmin
[PROOF STATE]
proof (chain)
picking this:
i \<in> PR - kmin f PR
i \<notin> kmax f PR
[PROOF STEP]
have "i \<in> PR - (kmax f PR \<union> kmin f PR)"
[PROOF STATE]
proof (prove)
using this:
i \<in> PR - kmin f PR
i \<notin> kmax f PR

goal (1 subgoal):
 1. i \<in> PR - (kmax f PR \<union> kmin f PR)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i \<in> PR - (kmax f PR \<union> kmin f PR)

goal (1 subgoal):
 1. i \<notin> kmax f PR \<Longrightarrow> Min (reduce f PR) \<le> f i
[PROOF STEP]
with reduce_def
[PROOF STATE]
proof (chain)
picking this:
reduce ?f ?P = ?f ` (?P - (kmax ?f ?P \<union> kmin ?f ?P))
i \<in> PR - (kmax f PR \<union> kmin f PR)
[PROOF STEP]
have "f i \<in> reduce f PR"
[PROOF STATE]
proof (prove)
using this:
reduce ?f ?P = ?f ` (?P - (kmax ?f ?P \<union> kmin ?f ?P))
i \<in> PR - (kmax f PR \<union> kmin f PR)

goal (1 subgoal):
 1. f i \<in> reduce f PR
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f i \<in> reduce f PR

goal (1 subgoal):
 1. i \<notin> kmax f PR \<Longrightarrow> Min (reduce f PR) \<le> f i
[PROOF STEP]
with reduce_not_empty and finite_reduce
[PROOF STATE]
proof (chain)
picking this:
reduce ?f PR \<noteq> {}
finite (reduce ?f PR)
f i \<in> reduce f PR
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
reduce ?f PR \<noteq> {}
finite (reduce ?f PR)
f i \<in> reduce f PR

goal (1 subgoal):
 1. Min (reduce f PR) \<le> f i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Min (reduce f PR) \<le> f i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Min (reduce f PR) \<le> f i

goal (1 subgoal):
 1. \<exists>i\<in>C. Min (reduce f PR) \<le> f i \<and> g i \<le> Max (reduce g PR)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Min (reduce f PR) \<le> f i

goal (1 subgoal):
 1. \<exists>i\<in>C. Min (reduce f PR) \<le> f i \<and> g i \<le> Max (reduce g PR)
[PROOF STEP]
have "g i <= Max (reduce g PR)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g i \<le> Max (reduce g PR)
[PROOF STEP]
proof(cases "i \<in> kmin g PR")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i \<in> kmin g PR \<Longrightarrow> g i \<le> Max (reduce g PR)
 2. i \<notin> kmin g PR \<Longrightarrow> g i \<le> Max (reduce g PR)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i \<in> kmin g PR

goal (2 subgoals):
 1. i \<in> kmin g PR \<Longrightarrow> g i \<le> Max (reduce g PR)
 2. i \<notin> kmin g PR \<Longrightarrow> g i \<le> Max (reduce g PR)
[PROOF STEP]
from reduce_not_empty and finite_reduce
[PROOF STATE]
proof (chain)
picking this:
reduce ?f PR \<noteq> {}
finite (reduce ?f PR)
[PROOF STEP]
have
      " Max (reduce g PR) \<in> reduce g PR"
[PROOF STATE]
proof (prove)
using this:
reduce ?f PR \<noteq> {}
finite (reduce ?f PR)

goal (1 subgoal):
 1. Max (reduce g PR) \<in> reduce g PR
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Max (reduce g PR) \<in> reduce g PR

goal (2 subgoals):
 1. i \<in> kmin g PR \<Longrightarrow> g i \<le> Max (reduce g PR)
 2. i \<notin> kmin g PR \<Longrightarrow> g i \<le> Max (reduce g PR)
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
i \<in> kmin g PR
Max (reduce g PR) \<in> reduce g PR
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<in> kmin g PR
Max (reduce g PR) \<in> reduce g PR

goal (1 subgoal):
 1. g i \<le> Max (reduce g PR)
[PROOF STEP]
using kmin_le
[PROOF STATE]
proof (prove)
using this:
i \<in> kmin g PR
Max (reduce g PR) \<in> reduce g PR
\<forall>i\<in>kmin ?f PR. \<forall>r\<in>reduce ?f PR. ?f i \<le> r

goal (1 subgoal):
 1. g i \<le> Max (reduce g PR)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
g i \<le> Max (reduce g PR)

goal (1 subgoal):
 1. i \<notin> kmin g PR \<Longrightarrow> g i \<le> Max (reduce g PR)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<notin> kmin g PR \<Longrightarrow> g i \<le> Max (reduce g PR)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<notin> kmin g PR

goal (1 subgoal):
 1. i \<notin> kmin g PR \<Longrightarrow> g i \<le> Max (reduce g PR)
[PROOF STEP]
with not_in_kmax
[PROOF STATE]
proof (chain)
picking this:
i \<in> PR - kmax g PR
i \<notin> kmin g PR
[PROOF STEP]
have "i \<in> PR - (kmax g PR \<union> kmin g PR)"
[PROOF STATE]
proof (prove)
using this:
i \<in> PR - kmax g PR
i \<notin> kmin g PR

goal (1 subgoal):
 1. i \<in> PR - (kmax g PR \<union> kmin g PR)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i \<in> PR - (kmax g PR \<union> kmin g PR)

goal (1 subgoal):
 1. i \<notin> kmin g PR \<Longrightarrow> g i \<le> Max (reduce g PR)
[PROOF STEP]
with reduce_def
[PROOF STATE]
proof (chain)
picking this:
reduce ?f ?P = ?f ` (?P - (kmax ?f ?P \<union> kmin ?f ?P))
i \<in> PR - (kmax g PR \<union> kmin g PR)
[PROOF STEP]
have "g i \<in> reduce g PR"
[PROOF STATE]
proof (prove)
using this:
reduce ?f ?P = ?f ` (?P - (kmax ?f ?P \<union> kmin ?f ?P))
i \<in> PR - (kmax g PR \<union> kmin g PR)

goal (1 subgoal):
 1. g i \<in> reduce g PR
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g i \<in> reduce g PR

goal (1 subgoal):
 1. i \<notin> kmin g PR \<Longrightarrow> g i \<le> Max (reduce g PR)
[PROOF STEP]
with reduce_not_empty and finite_reduce
[PROOF STATE]
proof (chain)
picking this:
reduce ?f PR \<noteq> {}
finite (reduce ?f PR)
g i \<in> reduce g PR
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
reduce ?f PR \<noteq> {}
finite (reduce ?f PR)
g i \<in> reduce g PR

goal (1 subgoal):
 1. g i \<le> Max (reduce g PR)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g i \<le> Max (reduce g PR)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g i \<le> Max (reduce g PR)

goal (1 subgoal):
 1. \<exists>i\<in>C. Min (reduce f PR) \<le> f i \<and> g i \<le> Max (reduce g PR)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g i \<le> Max (reduce g PR)

goal (1 subgoal):
 1. \<exists>i\<in>C. Min (reduce f PR) \<le> f i \<and> g i \<le> Max (reduce g PR)
[PROOF STEP]
note in_C
[PROOF STATE]
proof (state)
this:
i \<in> C

goal (1 subgoal):
 1. \<exists>i\<in>C. Min (reduce f PR) \<le> f i \<and> g i \<le> Max (reduce g PR)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Min (reduce f PR) \<le> f i
g i \<le> Max (reduce g PR)
i \<in> C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Min (reduce f PR) \<le> f i
g i \<le> Max (reduce g PR)
i \<in> C

goal (1 subgoal):
 1. \<exists>i\<in>C. Min (reduce f PR) \<le> f i \<and> g i \<le> Max (reduce g PR)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>C. Min (reduce f PR) \<le> f i \<and> g i \<le> Max (reduce g PR)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem prec_enh:
assumes
  hC: "C \<subseteq> PR" and
  hCF: "np - nF <= card C" and
  hFn: "3 * nF < np" and
  hFk: "nF = khl" and
  hbx: "\<forall> l\<in>C. \<bar>f l - g l\<bar> <= x" and
  hby1: "\<forall> l\<in>C. \<forall> m\<in>C. \<bar>f l - f m\<bar> <= y" and
  hby2: "\<forall> l\<in>C. \<forall> m\<in>C. \<bar>g l - g m\<bar> <= y" and
  hpC: "p\<in>C" and
  hqC: "q\<in>C"
shows "\<bar> cfnl p f - cfnl q g \<bar> <= y / 2 + x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>cfnl p f - cfnl q g\<bar> \<le> y / 2 + x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>cfnl p f - cfnl q g\<bar> \<le> y / 2 + x
[PROOF STEP]
from hCF and hFk
[PROOF STATE]
proof (chain)
picking this:
np - nF \<le> card C
nF = khl
[PROOF STEP]
have hCk: "np <= card C + khl"
[PROOF STATE]
proof (prove)
using this:
np - nF \<le> card C
nF = khl

goal (1 subgoal):
 1. np \<le> card C + khl
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
np \<le> card C + khl

goal (1 subgoal):
 1. \<bar>cfnl p f - cfnl q g\<bar> \<le> y / 2 + x
[PROOF STEP]
from hFn and hFk
[PROOF STATE]
proof (chain)
picking this:
3 * nF < np
nF = khl
[PROOF STEP]
have hnk: "3 * khl < np"
[PROOF STATE]
proof (prove)
using this:
3 * nF < np
nF = khl

goal (1 subgoal):
 1. 3 * khl < np
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
3 * khl < np

goal (1 subgoal):
 1. \<bar>cfnl p f - cfnl q g\<bar> \<le> y / 2 + x
[PROOF STEP]
let    ?maxf = "Max (reduce f PR)"
    and  ?minf = "Min (reduce f PR)"
    and  ?maxg = "Max (reduce g PR)"
    and  ?ming = "Min (reduce g PR)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>cfnl p f - cfnl q g\<bar> \<le> y / 2 + x
[PROOF STEP]
from abs_distrib_div
[PROOF STATE]
proof (chain)
picking this:
0 < ?c \<Longrightarrow> \<bar>?a / ?c - ?b / ?c\<bar> = \<bar>?a - ?b\<bar> / ?c
[PROOF STEP]
have "\<bar>cfnl p f - cfnl q g\<bar> =
    \<bar>?maxf + ?minf  +  - ?maxg + - ?ming\<bar> / 2"
[PROOF STATE]
proof (prove)
using this:
0 < ?c \<Longrightarrow> \<bar>?a / ?c - ?b / ?c\<bar> = \<bar>?a - ?b\<bar> / ?c

goal (1 subgoal):
 1. \<bar>cfnl p f - cfnl q g\<bar> = \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> / 2
[PROOF STEP]
by (unfold cfnl_def) simp
[PROOF STATE]
proof (state)
this:
\<bar>cfnl p f - cfnl q g\<bar> = \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> / 2

goal (1 subgoal):
 1. \<bar>cfnl p f - cfnl q g\<bar> \<le> y / 2 + x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<bar>cfnl p f - cfnl q g\<bar> = \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> / 2

goal (1 subgoal):
 1. \<bar>cfnl p f - cfnl q g\<bar> \<le> y / 2 + x
[PROOF STEP]
have "\<bar>?maxf + ?minf  +  - ?maxg + - ?ming\<bar> <= y + 2 * x"
    \<comment> \<open>The rest of the property can be proved by CVC-lite
           (see appendix \ref{sec:bound_prec_enh})\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
proof ( cases "0 <= ?maxf + ?minf  +  - ?maxg + - ?ming")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
 2. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)

goal (2 subgoals):
 1. 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
 2. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
hence
    "\<bar>?maxf + ?minf  +  - ?maxg + - ?ming\<bar> =
      ?maxf + ?minf  +  - ?maxg + - ?ming"
[PROOF STATE]
proof (prove)
using this:
0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)

goal (1 subgoal):
 1. \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> = Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> = Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)

goal (2 subgoals):
 1. 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
 2. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> = Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)

goal (2 subgoals):
 1. 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
 2. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
from uboundmax hC hCk
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?C \<subseteq> PR; np \<le> card ?C + khl\<rbrakk> \<Longrightarrow> \<exists>i\<in>?C. Max (reduce ?f PR) \<le> ?f i
C \<subseteq> PR
np \<le> card C + khl
[PROOF STEP]
obtain mxf
      where mxfinC: "mxf\<in>C" and
            maxf: "?maxf <= f mxf"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?C \<subseteq> PR; np \<le> card ?C + khl\<rbrakk> \<Longrightarrow> \<exists>i\<in>?C. Max (reduce ?f PR) \<le> ?f i
C \<subseteq> PR
np \<le> card C + khl

goal (1 subgoal):
 1. (\<And>mxf. \<lbrakk>mxf \<in> C; Max (reduce f PR) \<le> f mxf\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mxf \<in> C
Max (reduce f PR) \<le> f mxf

goal (2 subgoals):
 1. 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
 2. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mxf \<in> C
Max (reduce f PR) \<le> f mxf

goal (2 subgoals):
 1. 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
 2. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
from lboundmin hC hCk
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?C \<subseteq> PR; np \<le> card ?C + khl\<rbrakk> \<Longrightarrow> \<exists>i\<in>?C. ?f i \<le> Min (reduce ?f PR)
C \<subseteq> PR
np \<le> card C + khl
[PROOF STEP]
obtain mng
      where mnginC: "mng\<in>C" and
            ming: "g mng <= ?ming"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?C \<subseteq> PR; np \<le> card ?C + khl\<rbrakk> \<Longrightarrow> \<exists>i\<in>?C. ?f i \<le> Min (reduce ?f PR)
C \<subseteq> PR
np \<le> card C + khl

goal (1 subgoal):
 1. (\<And>mng. \<lbrakk>mng \<in> C; g mng \<le> Min (reduce g PR)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mng \<in> C
g mng \<le> Min (reduce g PR)

goal (2 subgoals):
 1. 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
 2. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mng \<in> C
g mng \<le> Min (reduce g PR)

goal (2 subgoals):
 1. 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
 2. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
from same_bound hC hCk hnk
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?C \<subseteq> PR; np \<le> card ?C + khl; 3 * khl < np\<rbrakk> \<Longrightarrow> \<exists>i\<in>?C. Min (reduce ?f PR) \<le> ?f i \<and> ?g i \<le> Max (reduce ?g PR)
C \<subseteq> PR
np \<le> card C + khl
3 * khl < np
[PROOF STEP]
obtain mxn
      where mxninC: "mxn\<in>C" and
            mxnf: "?minf  \<le> f mxn" and
            mxng: "g mxn \<le> ?maxg"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?C \<subseteq> PR; np \<le> card ?C + khl; 3 * khl < np\<rbrakk> \<Longrightarrow> \<exists>i\<in>?C. Min (reduce ?f PR) \<le> ?f i \<and> ?g i \<le> Max (reduce ?g PR)
C \<subseteq> PR
np \<le> card C + khl
3 * khl < np

goal (1 subgoal):
 1. (\<And>mxn. \<lbrakk>mxn \<in> C; Min (reduce f PR) \<le> f mxn; g mxn \<le> Max (reduce g PR)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mxn \<in> C
Min (reduce f PR) \<le> f mxn
g mxn \<le> Max (reduce g PR)

goal (2 subgoals):
 1. 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
 2. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> = Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)
mxf \<in> C
Max (reduce f PR) \<le> f mxf
mng \<in> C
g mng \<le> Min (reduce g PR)
mxn \<in> C
Min (reduce f PR) \<le> f mxn
g mxn \<le> Max (reduce g PR)
[PROOF STEP]
have
      "\<bar> ?maxf + ?minf  +  - ?maxg + - ?ming\<bar> <=
      (f mxf + - g mng) + (f mxn  +  - g mxn)"
[PROOF STATE]
proof (prove)
using this:
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> = Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)
mxf \<in> C
Max (reduce f PR) \<le> f mxf
mng \<in> C
g mng \<le> Min (reduce g PR)
mxn \<in> C
Min (reduce f PR) \<le> f mxn
g mxn \<le> Max (reduce g PR)

goal (1 subgoal):
 1. \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> f mxf + - g mng + (f mxn + - g mxn)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> f mxf + - g mng + (f mxn + - g mxn)

goal (2 subgoals):
 1. 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
 2. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> f mxf + - g mng + (f mxn + - g mxn)

goal (2 subgoals):
 1. 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
 2. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
from  mxninC hbx abs_le_D1
[PROOF STATE]
proof (chain)
picking this:
mxn \<in> C
\<forall>l\<in>C. \<bar>f l - g l\<bar> \<le> x
\<bar>?a\<bar> \<le> ?b \<Longrightarrow> ?a \<le> ?b
[PROOF STEP]
have
      "... <= (f mxf + - g mng) + x"
[PROOF STATE]
proof (prove)
using this:
mxn \<in> C
\<forall>l\<in>C. \<bar>f l - g l\<bar> \<le> x
\<bar>?a\<bar> \<le> ?b \<Longrightarrow> ?a \<le> ?b

goal (1 subgoal):
 1. f mxf + - g mng + (f mxn + - g mxn) \<le> f mxf + - g mng + x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f mxf + - g mng + (f mxn + - g mxn) \<le> f mxf + - g mng + x

goal (2 subgoals):
 1. 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
 2. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f mxf + - g mng + (f mxn + - g mxn) \<le> f mxf + - g mng + x

goal (2 subgoals):
 1. 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
 2. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
have
      "... = (f mxf + - f mng ) + ( f mng + - g mng) + x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f mxf + - g mng + x = f mxf + - f mng + (f mng + - g mng) + x
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
f mxf + - g mng + x = f mxf + - f mng + (f mng + - g mng) + x

goal (2 subgoals):
 1. 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
 2. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f mxf + - g mng + x = f mxf + - f mng + (f mng + - g mng) + x

goal (2 subgoals):
 1. 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
 2. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
have "... <= y + ( f mng + - g mng) + x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f mxf + - f mng + (f mng + - g mng) + x \<le> y + (f mng + - g mng) + x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f mxf + - f mng + (f mng + - g mng) + x \<le> y + (f mng + - g mng) + x
[PROOF STEP]
from  mxfinC mnginC hby1 abs_le_D1
[PROOF STATE]
proof (chain)
picking this:
mxf \<in> C
mng \<in> C
\<forall>l\<in>C. \<forall>m\<in>C. \<bar>f l - f m\<bar> \<le> y
\<bar>?a\<bar> \<le> ?b \<Longrightarrow> ?a \<le> ?b
[PROOF STEP]
have "f mxf + - f mng <= y"
[PROOF STATE]
proof (prove)
using this:
mxf \<in> C
mng \<in> C
\<forall>l\<in>C. \<forall>m\<in>C. \<bar>f l - f m\<bar> \<le> y
\<bar>?a\<bar> \<le> ?b \<Longrightarrow> ?a \<le> ?b

goal (1 subgoal):
 1. f mxf + - f mng \<le> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f mxf + - f mng \<le> y

goal (1 subgoal):
 1. f mxf + - f mng + (f mng + - g mng) + x \<le> y + (f mng + - g mng) + x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f mxf + - f mng \<le> y

goal (1 subgoal):
 1. f mxf + - f mng + (f mng + - g mng) + x \<le> y + (f mng + - g mng) + x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f mxf + - f mng + (f mng + - g mng) + x \<le> y + (f mng + - g mng) + x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f mxf + - f mng + (f mng + - g mng) + x \<le> y + (f mng + - g mng) + x

goal (2 subgoals):
 1. 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
 2. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f mxf + - f mng + (f mng + - g mng) + x \<le> y + (f mng + - g mng) + x

goal (2 subgoals):
 1. 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
 2. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
from  mnginC hbx abs_le_D1
[PROOF STATE]
proof (chain)
picking this:
mng \<in> C
\<forall>l\<in>C. \<bar>f l - g l\<bar> \<le> x
\<bar>?a\<bar> \<le> ?b \<Longrightarrow> ?a \<le> ?b
[PROOF STEP]
have "... <= y + 2 * x"
[PROOF STATE]
proof (prove)
using this:
mng \<in> C
\<forall>l\<in>C. \<bar>f l - g l\<bar> \<le> x
\<bar>?a\<bar> \<le> ?b \<Longrightarrow> ?a \<le> ?b

goal (1 subgoal):
 1. y + (f mng + - g mng) + x \<le> y + 2 * x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y + (f mng + - g mng) + x \<le> y + 2 * x

goal (2 subgoals):
 1. 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
 2. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x

goal (1 subgoal):
 1. \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x

goal (1 subgoal):
 1. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)

goal (1 subgoal):
 1. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
hence
    "\<bar>?maxf + ?minf  +  - ?maxg + - ?ming\<bar> =
      ?maxg + ?ming  +  - ?maxf + - ?minf"
[PROOF STATE]
proof (prove)
using this:
\<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)

goal (1 subgoal):
 1. \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> = Max (reduce g PR) + Min (reduce g PR) + - Max (reduce f PR) + - Min (reduce f PR)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> = Max (reduce g PR) + Min (reduce g PR) + - Max (reduce f PR) + - Min (reduce f PR)

goal (1 subgoal):
 1. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> = Max (reduce g PR) + Min (reduce g PR) + - Max (reduce f PR) + - Min (reduce f PR)

goal (1 subgoal):
 1. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
from uboundmax hC hCk
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?C \<subseteq> PR; np \<le> card ?C + khl\<rbrakk> \<Longrightarrow> \<exists>i\<in>?C. Max (reduce ?f PR) \<le> ?f i
C \<subseteq> PR
np \<le> card C + khl
[PROOF STEP]
obtain mxg
      where mxginC: "mxg\<in>C" and
            maxg: "?maxg <= g mxg"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?C \<subseteq> PR; np \<le> card ?C + khl\<rbrakk> \<Longrightarrow> \<exists>i\<in>?C. Max (reduce ?f PR) \<le> ?f i
C \<subseteq> PR
np \<le> card C + khl

goal (1 subgoal):
 1. (\<And>mxg. \<lbrakk>mxg \<in> C; Max (reduce g PR) \<le> g mxg\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mxg \<in> C
Max (reduce g PR) \<le> g mxg

goal (1 subgoal):
 1. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mxg \<in> C
Max (reduce g PR) \<le> g mxg

goal (1 subgoal):
 1. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
from lboundmin hC hCk
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?C \<subseteq> PR; np \<le> card ?C + khl\<rbrakk> \<Longrightarrow> \<exists>i\<in>?C. ?f i \<le> Min (reduce ?f PR)
C \<subseteq> PR
np \<le> card C + khl
[PROOF STEP]
obtain mnf
      where mnfinC: "mnf\<in>C" and
            minf: "f mnf <= ?minf"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?C \<subseteq> PR; np \<le> card ?C + khl\<rbrakk> \<Longrightarrow> \<exists>i\<in>?C. ?f i \<le> Min (reduce ?f PR)
C \<subseteq> PR
np \<le> card C + khl

goal (1 subgoal):
 1. (\<And>mnf. \<lbrakk>mnf \<in> C; f mnf \<le> Min (reduce f PR)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mnf \<in> C
f mnf \<le> Min (reduce f PR)

goal (1 subgoal):
 1. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mnf \<in> C
f mnf \<le> Min (reduce f PR)

goal (1 subgoal):
 1. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
from same_bound hC hCk hnk
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?C \<subseteq> PR; np \<le> card ?C + khl; 3 * khl < np\<rbrakk> \<Longrightarrow> \<exists>i\<in>?C. Min (reduce ?f PR) \<le> ?f i \<and> ?g i \<le> Max (reduce ?g PR)
C \<subseteq> PR
np \<le> card C + khl
3 * khl < np
[PROOF STEP]
obtain mxn
      where mxninC: "mxn\<in>C" and
            mxnf: "?ming  \<le> g mxn" and
            mxng: "f mxn \<le> ?maxf"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?C \<subseteq> PR; np \<le> card ?C + khl; 3 * khl < np\<rbrakk> \<Longrightarrow> \<exists>i\<in>?C. Min (reduce ?f PR) \<le> ?f i \<and> ?g i \<le> Max (reduce ?g PR)
C \<subseteq> PR
np \<le> card C + khl
3 * khl < np

goal (1 subgoal):
 1. (\<And>mxn. \<lbrakk>mxn \<in> C; Min (reduce g PR) \<le> g mxn; f mxn \<le> Max (reduce f PR)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mxn \<in> C
Min (reduce g PR) \<le> g mxn
f mxn \<le> Max (reduce f PR)

goal (1 subgoal):
 1. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> = Max (reduce g PR) + Min (reduce g PR) + - Max (reduce f PR) + - Min (reduce f PR)
mxg \<in> C
Max (reduce g PR) \<le> g mxg
mnf \<in> C
f mnf \<le> Min (reduce f PR)
mxn \<in> C
Min (reduce g PR) \<le> g mxn
f mxn \<le> Max (reduce f PR)
[PROOF STEP]
have
      "\<bar> ?maxf + ?minf  +  - ?maxg + - ?ming\<bar> <=
      (g mxg + - f mnf) + (g mxn  +  - f mxn)"
[PROOF STATE]
proof (prove)
using this:
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> = Max (reduce g PR) + Min (reduce g PR) + - Max (reduce f PR) + - Min (reduce f PR)
mxg \<in> C
Max (reduce g PR) \<le> g mxg
mnf \<in> C
f mnf \<le> Min (reduce f PR)
mxn \<in> C
Min (reduce g PR) \<le> g mxn
f mxn \<le> Max (reduce f PR)

goal (1 subgoal):
 1. \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> g mxg + - f mnf + (g mxn + - f mxn)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> g mxg + - f mnf + (g mxn + - f mxn)

goal (1 subgoal):
 1. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> g mxg + - f mnf + (g mxn + - f mxn)

goal (1 subgoal):
 1. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
from  mxninC hbx
[PROOF STATE]
proof (chain)
picking this:
mxn \<in> C
\<forall>l\<in>C. \<bar>f l - g l\<bar> \<le> x
[PROOF STEP]
have "... <= (g mxg + - f mnf) + x"
[PROOF STATE]
proof (prove)
using this:
mxn \<in> C
\<forall>l\<in>C. \<bar>f l - g l\<bar> \<le> x

goal (1 subgoal):
 1. g mxg + - f mnf + (g mxn + - f mxn) \<le> g mxg + - f mnf + x
[PROOF STEP]
by (auto dest!: abs_le_D2)
[PROOF STATE]
proof (state)
this:
g mxg + - f mnf + (g mxn + - f mxn) \<le> g mxg + - f mnf + x

goal (1 subgoal):
 1. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
g mxg + - f mnf + (g mxn + - f mxn) \<le> g mxg + - f mnf + x

goal (1 subgoal):
 1. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
have
      "... = (g mxg + - g mnf ) + ( g mnf + - f mnf) + x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g mxg + - f mnf + x = g mxg + - g mnf + (g mnf + - f mnf) + x
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
g mxg + - f mnf + x = g mxg + - g mnf + (g mnf + - f mnf) + x

goal (1 subgoal):
 1. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
g mxg + - f mnf + x = g mxg + - g mnf + (g mnf + - f mnf) + x

goal (1 subgoal):
 1. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
have "... <= y + ( g mnf + - f mnf) + x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g mxg + - g mnf + (g mnf + - f mnf) + x \<le> y + (g mnf + - f mnf) + x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g mxg + - g mnf + (g mnf + - f mnf) + x \<le> y + (g mnf + - f mnf) + x
[PROOF STEP]
from  mxginC mnfinC hby2 abs_le_D1
[PROOF STATE]
proof (chain)
picking this:
mxg \<in> C
mnf \<in> C
\<forall>l\<in>C. \<forall>m\<in>C. \<bar>g l - g m\<bar> \<le> y
\<bar>?a\<bar> \<le> ?b \<Longrightarrow> ?a \<le> ?b
[PROOF STEP]
have "g mxg + - g mnf <= y"
[PROOF STATE]
proof (prove)
using this:
mxg \<in> C
mnf \<in> C
\<forall>l\<in>C. \<forall>m\<in>C. \<bar>g l - g m\<bar> \<le> y
\<bar>?a\<bar> \<le> ?b \<Longrightarrow> ?a \<le> ?b

goal (1 subgoal):
 1. g mxg + - g mnf \<le> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g mxg + - g mnf \<le> y

goal (1 subgoal):
 1. g mxg + - g mnf + (g mnf + - f mnf) + x \<le> y + (g mnf + - f mnf) + x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
g mxg + - g mnf \<le> y

goal (1 subgoal):
 1. g mxg + - g mnf + (g mnf + - f mnf) + x \<le> y + (g mnf + - f mnf) + x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g mxg + - g mnf + (g mnf + - f mnf) + x \<le> y + (g mnf + - f mnf) + x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g mxg + - g mnf + (g mnf + - f mnf) + x \<le> y + (g mnf + - f mnf) + x

goal (1 subgoal):
 1. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
g mxg + - g mnf + (g mnf + - f mnf) + x \<le> y + (g mnf + - f mnf) + x

goal (1 subgoal):
 1. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
from  mnfinC hbx
[PROOF STATE]
proof (chain)
picking this:
mnf \<in> C
\<forall>l\<in>C. \<bar>f l - g l\<bar> \<le> x
[PROOF STEP]
have "... <= y + 2 * x"
[PROOF STATE]
proof (prove)
using this:
mnf \<in> C
\<forall>l\<in>C. \<bar>f l - g l\<bar> \<le> x

goal (1 subgoal):
 1. y + (g mnf + - f mnf) + x \<le> y + 2 * x
[PROOF STEP]
by (auto dest!: abs_le_D2)
[PROOF STATE]
proof (state)
this:
y + (g mnf + - f mnf) + x \<le> y + 2 * x

goal (1 subgoal):
 1. \<not> 0 \<le> Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR) \<Longrightarrow> \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x

goal (1 subgoal):
 1. \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x

goal (1 subgoal):
 1. \<bar>cfnl p f - cfnl q g\<bar> \<le> y / 2 + x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>cfnl p f - cfnl q g\<bar> = \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> / 2
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>cfnl p f - cfnl q g\<bar> = \<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> / 2
\<bar>Max (reduce f PR) + Min (reduce f PR) + - Max (reduce g PR) + - Min (reduce g PR)\<bar> \<le> y + 2 * x

goal (1 subgoal):
 1. \<bar>cfnl p f - cfnl q g\<bar> \<le> y / 2 + x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>cfnl p f - cfnl q g\<bar> \<le> y / 2 + x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem accur_pres:
assumes
  hC: "C \<subseteq> PR" and
  hCF: "np - nF <= card C" and
  hFk: "nF = khl" and
  hby: "\<forall> l\<in>C. \<forall> m\<in>C. \<bar>f l - f m\<bar> <= y" and
  hqC: "q\<in>C"
shows "\<bar> cfnl p f - f q \<bar> <= y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
from hCF and hFk
[PROOF STATE]
proof (chain)
picking this:
np - nF \<le> card C
nF = khl
[PROOF STEP]
have npleCk: "np <= card C + khl"
[PROOF STATE]
proof (prove)
using this:
np - nF \<le> card C
nF = khl

goal (1 subgoal):
 1. np \<le> card C + khl
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
np \<le> card C + khl

goal (1 subgoal):
 1. \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
proof(cases "f q <= cfnl p f")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
 2. \<not> f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
f q \<le> cfnl p f

goal (2 subgoals):
 1. f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
 2. \<not> f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
from npleCk hC and  uboundmax
[PROOF STATE]
proof (chain)
picking this:
np \<le> card C + khl
C \<subseteq> PR
\<lbrakk>?C \<subseteq> PR; np \<le> card ?C + khl\<rbrakk> \<Longrightarrow> \<exists>i\<in>?C. Max (reduce ?f PR) \<le> ?f i
[PROOF STEP]
have "\<exists> i\<in>C. Max (reduce f PR) <= f i"
[PROOF STATE]
proof (prove)
using this:
np \<le> card C + khl
C \<subseteq> PR
\<lbrakk>?C \<subseteq> PR; np \<le> card ?C + khl\<rbrakk> \<Longrightarrow> \<exists>i\<in>?C. Max (reduce ?f PR) \<le> ?f i

goal (1 subgoal):
 1. \<exists>i\<in>C. Max (reduce f PR) \<le> f i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>C. Max (reduce f PR) \<le> f i

goal (2 subgoals):
 1. f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
 2. \<not> f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<in>C. Max (reduce f PR) \<le> f i
[PROOF STEP]
obtain pi where
      hpiC: "pi \<in> C" and
      fpiGeMax: "Max (reduce f PR) <= f pi"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<in>C. Max (reduce f PR) \<le> f i

goal (1 subgoal):
 1. (\<And>pi. \<lbrakk>pi \<in> C; Max (reduce f PR) \<le> f pi\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pi \<in> C
Max (reduce f PR) \<le> f pi

goal (2 subgoals):
 1. f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
 2. \<not> f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
from reduce_not_empty
[PROOF STATE]
proof (chain)
picking this:
reduce ?f PR \<noteq> {}
[PROOF STEP]
have "Min (reduce f PR) <= Max (reduce f PR)"
[PROOF STATE]
proof (prove)
using this:
reduce ?f PR \<noteq> {}

goal (1 subgoal):
 1. Min (reduce f PR) \<le> Max (reduce f PR)
[PROOF STEP]
by (auto simp add: reduce_def)
[PROOF STATE]
proof (state)
this:
Min (reduce f PR) \<le> Max (reduce f PR)

goal (2 subgoals):
 1. f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
 2. \<not> f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
with fpiGeMax
[PROOF STATE]
proof (chain)
picking this:
Max (reduce f PR) \<le> f pi
Min (reduce f PR) \<le> Max (reduce f PR)
[PROOF STEP]
have
      cfnlLefpi: "cfnl p f <= f pi"
[PROOF STATE]
proof (prove)
using this:
Max (reduce f PR) \<le> f pi
Min (reduce f PR) \<le> Max (reduce f PR)

goal (1 subgoal):
 1. cfnl p f \<le> f pi
[PROOF STEP]
by (auto simp add: cfnl_def)
[PROOF STATE]
proof (state)
this:
cfnl p f \<le> f pi

goal (2 subgoals):
 1. f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
 2. \<not> f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
f q \<le> cfnl p f
cfnl p f \<le> f pi
[PROOF STEP]
have
      "\<bar> cfnl p f - f q \<bar> <= \<bar> f pi - f q \<bar>"
[PROOF STATE]
proof (prove)
using this:
f q \<le> cfnl p f
cfnl p f \<le> f pi

goal (1 subgoal):
 1. \<bar>cfnl p f - f q\<bar> \<le> \<bar>f pi - f q\<bar>
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<bar>cfnl p f - f q\<bar> \<le> \<bar>f pi - f q\<bar>

goal (2 subgoals):
 1. f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
 2. \<not> f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
with hpiC and hqC and hby
[PROOF STATE]
proof (chain)
picking this:
pi \<in> C
q \<in> C
\<forall>l\<in>C. \<forall>m\<in>C. \<bar>f l - f m\<bar> \<le> y
\<bar>cfnl p f - f q\<bar> \<le> \<bar>f pi - f q\<bar>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pi \<in> C
q \<in> C
\<forall>l\<in>C. \<forall>m\<in>C. \<bar>f l - f m\<bar> \<le> y
\<bar>cfnl p f - f q\<bar> \<le> \<bar>f pi - f q\<bar>

goal (1 subgoal):
 1. \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<bar>cfnl p f - f q\<bar> \<le> y

goal (1 subgoal):
 1. \<not> f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> f q \<le> cfnl p f

goal (1 subgoal):
 1. \<not> f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
from npleCk hC and lboundmin
[PROOF STATE]
proof (chain)
picking this:
np \<le> card C + khl
C \<subseteq> PR
\<lbrakk>?C \<subseteq> PR; np \<le> card ?C + khl\<rbrakk> \<Longrightarrow> \<exists>i\<in>?C. ?f i \<le> Min (reduce ?f PR)
[PROOF STEP]
have "\<exists> i\<in>C. f i <= Min (reduce f PR)"
[PROOF STATE]
proof (prove)
using this:
np \<le> card C + khl
C \<subseteq> PR
\<lbrakk>?C \<subseteq> PR; np \<le> card ?C + khl\<rbrakk> \<Longrightarrow> \<exists>i\<in>?C. ?f i \<le> Min (reduce ?f PR)

goal (1 subgoal):
 1. \<exists>i\<in>C. f i \<le> Min (reduce f PR)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>C. f i \<le> Min (reduce f PR)

goal (1 subgoal):
 1. \<not> f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i\<in>C. f i \<le> Min (reduce f PR)
[PROOF STEP]
obtain qi where
      hqiC: "qi \<in> C" and
      fqiLeMax: "f qi <= Min (reduce f PR)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i\<in>C. f i \<le> Min (reduce f PR)

goal (1 subgoal):
 1. (\<And>qi. \<lbrakk>qi \<in> C; f qi \<le> Min (reduce f PR)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
qi \<in> C
f qi \<le> Min (reduce f PR)

goal (1 subgoal):
 1. \<not> f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
from reduce_not_empty
[PROOF STATE]
proof (chain)
picking this:
reduce ?f PR \<noteq> {}
[PROOF STEP]
have "Min (reduce f PR) <= Max (reduce f PR)"
[PROOF STATE]
proof (prove)
using this:
reduce ?f PR \<noteq> {}

goal (1 subgoal):
 1. Min (reduce f PR) \<le> Max (reduce f PR)
[PROOF STEP]
by (auto simp add: reduce_def)
[PROOF STATE]
proof (state)
this:
Min (reduce f PR) \<le> Max (reduce f PR)

goal (1 subgoal):
 1. \<not> f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
with fqiLeMax
[PROOF STATE]
proof (chain)
picking this:
f qi \<le> Min (reduce f PR)
Min (reduce f PR) \<le> Max (reduce f PR)
[PROOF STEP]
have "f qi <= cfnl p f"
[PROOF STATE]
proof (prove)
using this:
f qi \<le> Min (reduce f PR)
Min (reduce f PR) \<le> Max (reduce f PR)

goal (1 subgoal):
 1. f qi \<le> cfnl p f
[PROOF STEP]
by (auto simp add: cfnl_def)
[PROOF STATE]
proof (state)
this:
f qi \<le> cfnl p f

goal (1 subgoal):
 1. \<not> f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
\<not> f q \<le> cfnl p f
f qi \<le> cfnl p f
[PROOF STEP]
have
      "\<bar> cfnl p f - f q \<bar> <= \<bar> f qi - f q \<bar>"
[PROOF STATE]
proof (prove)
using this:
\<not> f q \<le> cfnl p f
f qi \<le> cfnl p f

goal (1 subgoal):
 1. \<bar>cfnl p f - f q\<bar> \<le> \<bar>f qi - f q\<bar>
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<bar>cfnl p f - f q\<bar> \<le> \<bar>f qi - f q\<bar>

goal (1 subgoal):
 1. \<not> f q \<le> cfnl p f \<Longrightarrow> \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
with hqiC and hqC and hby
[PROOF STATE]
proof (chain)
picking this:
qi \<in> C
q \<in> C
\<forall>l\<in>C. \<forall>m\<in>C. \<bar>f l - f m\<bar> \<le> y
\<bar>cfnl p f - f q\<bar> \<le> \<bar>f qi - f q\<bar>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
qi \<in> C
q \<in> C
\<forall>l\<in>C. \<forall>m\<in>C. \<bar>f l - f m\<bar> \<le> y
\<bar>cfnl p f - f q\<bar> \<le> \<bar>f qi - f q\<bar>

goal (1 subgoal):
 1. \<bar>cfnl p f - f q\<bar> \<le> y
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<bar>cfnl p f - f q\<bar> \<le> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>cfnl p f - f q\<bar> \<le> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in normal_set) less_next: "x < (LEAST z. z \<in> A \<and> x < z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < (LEAST z. z \<in> A \<and> x < z)
[PROOF STEP]
apply (rule LeastI2_ex)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>a. a \<in> A \<and> x < a
 2. \<And>xa. xa \<in> A \<and> x < xa \<Longrightarrow> x < xa
[PROOF STEP]
apply (fold Bex_def, rule unbounded)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> A \<and> x < xa \<Longrightarrow> x < xa
[PROOF STEP]
apply (erule conjunct2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in normal_set) mem_next: "(LEAST z. z \<in> A \<and> x < z) \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST z. z \<in> A \<and> x < z) \<in> A
[PROOF STEP]
apply (rule LeastI2_ex)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>a. a \<in> A \<and> x < a
 2. \<And>xa. xa \<in> A \<and> x < xa \<Longrightarrow> xa \<in> A
[PROOF STEP]
apply (fold Bex_def, rule unbounded)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> A \<and> x < xa \<Longrightarrow> xa \<in> A
[PROOF STEP]
apply (erule conjunct1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in normal) normal_set_range: "normal_set (range F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal_set (range F)
[PROOF STEP]
apply (rule normal_set.intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>g. \<forall>n. g n \<in> range F \<Longrightarrow> oLimit g \<in> range F
 2. \<And>x. \<exists>y\<in>range F. x < y
[PROOF STEP]
apply (simp add: image_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>g. \<forall>n. \<exists>x. g n = F x \<Longrightarrow> \<exists>x. oLimit g = F x
 2. \<And>x. \<exists>y\<in>range F. x < y
[PROOF STEP]
apply (rule_tac x="oLimit (\<lambda>n. LEAST x. g n = F x)" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>g. \<forall>n. \<exists>x. g n = F x \<Longrightarrow> oLimit g = F (oLimit (\<lambda>n. LEAST x. g n = F x))
 2. \<And>x. \<exists>y\<in>range F. x < y
[PROOF STEP]
apply (simp only: oLimit)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>g. \<forall>n. \<exists>x. g n = F x \<Longrightarrow> oLimit g = oLimit (\<lambda>n. F (LEAST x. g n = F x))
 2. \<And>x. \<exists>y\<in>range F. x < y
[PROOF STEP]
apply (rule_tac f=oLimit in arg_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>g. \<forall>n. \<exists>x. g n = F x \<Longrightarrow> g = (\<lambda>n. F (LEAST x. g n = F x))
 2. \<And>x. \<exists>y\<in>range F. x < y
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>g n. \<forall>n. \<exists>x. g n = F x \<Longrightarrow> g n = F (LEAST x. g n = F x)
 2. \<And>x. \<exists>y\<in>range F. x < y
[PROOF STEP]
apply (rule LeastI_ex)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>g n. \<forall>n. \<exists>x. g n = F x \<Longrightarrow> \<exists>x. g n = F x
 2. \<And>x. \<exists>y\<in>range F. x < y
[PROOF STEP]
apply (erule spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<exists>y\<in>range F. x < y
[PROOF STEP]
apply (rule_tac x="F (oSuc x)" in bexI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x < F (oSuc x)
 2. \<And>x. F (oSuc x) \<in> range F
[PROOF STEP]
apply (rule order_le_less_trans [OF increasing])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. F x < F (oSuc x)
 2. \<And>x. F (oSuc x) \<in> range F
[PROOF STEP]
apply (simp add: cancel_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. F (oSuc x) \<in> range F
[PROOF STEP]
apply (rule rangeI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma oLimit_mem_INTER:
"\<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n;
  \<forall>n. f n \<in> A n; mono f\<rbrakk>
  \<Longrightarrow> oLimit f \<in> (\<Inter>n. A n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; \<forall>n. f n \<in> A n; mono f\<rbrakk> \<Longrightarrow> oLimit f \<in> \<Inter> (range A)
[PROOF STEP]
apply (clarsimp, rename_tac k)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; \<forall>n. f n \<in> A n; mono f\<rbrakk> \<Longrightarrow> oLimit f \<in> A k
[PROOF STEP]
apply (subgoal_tac "oLimit (\<lambda>n. f (n + k)) \<in> A k")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; \<forall>n. f n \<in> A n; mono f; oLimit (\<lambda>n. f (n + k)) \<in> A k\<rbrakk> \<Longrightarrow> oLimit f \<in> A k
 2. \<And>k. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; \<forall>n. f n \<in> A n; mono f\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. f (n + k)) \<in> A k
[PROOF STEP]
apply (simp add: oLimit_shift_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; \<forall>n. f n \<in> A n; mono f\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. f (n + k)) \<in> A k
[PROOF STEP]
apply (rule normal_set.closed [rule_format], erule spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k n. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; \<forall>n. f n \<in> A n; mono f\<rbrakk> \<Longrightarrow> f (n + k) \<in> A k
[PROOF STEP]
apply (rule_tac A="A (n + k)" in subsetD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k n. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; \<forall>n. f n \<in> A n; mono f\<rbrakk> \<Longrightarrow> A (n + k) \<subseteq> A k
 2. \<And>k n. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; \<forall>n. f n \<in> A n; mono f\<rbrakk> \<Longrightarrow> f (n + k) \<in> A (n + k)
[PROOF STEP]
apply (induct_tac n, simp, rename_tac m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k n m. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; \<forall>n. f n \<in> A n; mono f; A (m + k) \<subseteq> A k\<rbrakk> \<Longrightarrow> A (Suc m + k) \<subseteq> A k
 2. \<And>k n. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; \<forall>n. f n \<in> A n; mono f\<rbrakk> \<Longrightarrow> f (n + k) \<in> A (n + k)
[PROOF STEP]
apply (rule_tac B="A (m + k)" in subset_trans, simp, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k n. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; \<forall>n. f n \<in> A n; mono f\<rbrakk> \<Longrightarrow> f (n + k) \<in> A (n + k)
[PROOF STEP]
apply (erule spec)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma normal_set_INTER:
"\<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> normal_set (\<Inter>n. A n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> normal_set (\<Inter> (range A))
[PROOF STEP]
apply (rule normal_set.intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>g. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n; \<forall>n. g n \<in> \<Inter> (range A)\<rbrakk> \<Longrightarrow> oLimit g \<in> \<Inter> (range A)
 2. \<And>x. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> \<exists>y\<in>\<Inter> (range A). x < y
[PROOF STEP]
apply (clarsimp simp add: normal_set.closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> \<exists>y\<in>\<Inter> (range A). x < y
[PROOF STEP]
apply (rule_tac x="oLimit (\<lambda>n. LEAST y. y \<in> A n \<and> x < y)" in bexI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> x < oLimit (\<lambda>n. LEAST y. y \<in> A n \<and> x < y)
 2. \<And>x. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. LEAST y. y \<in> A n \<and> x < y) \<in> \<Inter> (range A)
[PROOF STEP]
apply (rule_tac y="LEAST y. y \<in> A n \<and> x < y" in order_less_le_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> x < (LEAST y. y \<in> A n \<and> x < y)
 2. \<And>x. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> (LEAST y. y \<in> A n \<and> x < y) \<le> oLimit (\<lambda>n. LEAST y. y \<in> A n \<and> x < y)
 3. \<And>x. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. LEAST y. y \<in> A n \<and> x < y) \<in> \<Inter> (range A)
[PROOF STEP]
apply (simp only: normal_set.less_next)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> (LEAST y. y \<in> A n \<and> x < y) \<le> oLimit (\<lambda>n. LEAST y. y \<in> A n \<and> x < y)
 2. \<And>x. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. LEAST y. y \<in> A n \<and> x < y) \<in> \<Inter> (range A)
[PROOF STEP]
apply (rule le_oLimit)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. LEAST y. y \<in> A n \<and> x < y) \<in> \<Inter> (range A)
[PROOF STEP]
apply (rule oLimit_mem_INTER, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> \<forall>n. (LEAST y. y \<in> A n \<and> x < y) \<in> A n
 2. \<And>x. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> mono (\<lambda>n. LEAST y. y \<in> A n \<and> x < y)
[PROOF STEP]
apply (simp add: normal_set.mem_next)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> mono (\<lambda>n. LEAST y. y \<in> A n \<and> x < y)
[PROOF STEP]
apply (rule mono_natI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> (LEAST y. y \<in> A n \<and> x < y) \<le> (LEAST y. y \<in> A (Suc n) \<and> x < y)
[PROOF STEP]
apply (rule Least_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> (LEAST y. y \<in> A (Suc n) \<and> x < y) \<in> A n \<and> x < (LEAST y. y \<in> A (Suc n) \<and> x < y)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x n. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> (LEAST y. y \<in> A (Suc n) \<and> x < y) \<in> A n
 2. \<And>x n. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> x < (LEAST y. y \<in> A (Suc n) \<and> x < y)
[PROOF STEP]
apply (rule subsetD, erule spec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x n. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> (LEAST y. y \<in> A (Suc n) \<and> x < y) \<in> A (Suc n)
 2. \<And>x n. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> x < (LEAST y. y \<in> A (Suc n) \<and> x < y)
[PROOF STEP]
apply (simp only: normal_set.mem_next)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>\<forall>n. normal_set (A n); \<forall>n. A (Suc n) \<subseteq> A n\<rbrakk> \<Longrightarrow> x < (LEAST y. y \<in> A (Suc n) \<and> x < y)
[PROOF STEP]
apply (simp only: normal_set.less_next)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ordering_0:
"ordering A 0 = (LEAST z. z \<in> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdinalVeblen.ordering A 0 = (LEAST z. z \<in> A)
[PROOF STEP]
by (simp add: ordering_def)


[STATEMENT]
lemma ordering_oSuc:
"ordering A (oSuc x) = (LEAST z. z \<in> A \<and> ordering A x < z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdinalVeblen.ordering A (oSuc x) = (LEAST z. z \<in> A \<and> OrdinalVeblen.ordering A x < z)
[PROOF STEP]
by (simp add: ordering_def)


[STATEMENT]
lemma (in normal_set) normal_ordering: "normal (ordering A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal (OrdinalVeblen.ordering A)
[PROOF STEP]
apply (unfold ordering_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal (ordinal_rec (LEAST z. z \<in> A) (\<lambda>p x. LEAST z. z \<in> A \<and> x < z))
[PROOF STEP]
apply (rule normal_ordinal_rec [rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p x. x < (LEAST z. z \<in> A \<and> x < z)
[PROOF STEP]
apply (rule less_next)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in normal_set) ordering_oLimit:
"ordering A (oLimit f) = oLimit (\<lambda>n. ordering A (f n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdinalVeblen.ordering A (oLimit f) = oLimit (\<lambda>n. OrdinalVeblen.ordering A (f n))
[PROOF STEP]
apply (rule normal.oLimit)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal (OrdinalVeblen.ordering A)
[PROOF STEP]
apply (rule normal_ordering)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in normal) ordering_range: "ordering (range F) = F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdinalVeblen.ordering (range F) = F
[PROOF STEP]
apply (rule ext, rule_tac a=x in oLimit_induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. OrdinalVeblen.ordering (range F) 0 = F 0
 2. \<And>x xa. OrdinalVeblen.ordering (range F) xa = F xa \<Longrightarrow> OrdinalVeblen.ordering (range F) (oSuc xa) = F (oSuc xa)
 3. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. OrdinalVeblen.ordering (range F) (f n) = F (f n)\<rbrakk> \<Longrightarrow> OrdinalVeblen.ordering (range F) (oLimit f) = F (oLimit f)
[PROOF STEP]
apply (simp add: ordering_0)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (LEAST z. z \<in> range F) = F 0
 2. \<And>x xa. OrdinalVeblen.ordering (range F) xa = F xa \<Longrightarrow> OrdinalVeblen.ordering (range F) (oSuc xa) = F (oSuc xa)
 3. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. OrdinalVeblen.ordering (range F) (f n) = F (f n)\<rbrakk> \<Longrightarrow> OrdinalVeblen.ordering (range F) (oLimit f) = F (oLimit f)
[PROOF STEP]
apply (rule Least_equality)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. F 0 \<in> range F
 2. \<And>y. y \<in> range F \<Longrightarrow> F 0 \<le> y
 3. \<And>x xa. OrdinalVeblen.ordering (range F) xa = F xa \<Longrightarrow> OrdinalVeblen.ordering (range F) (oSuc xa) = F (oSuc xa)
 4. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. OrdinalVeblen.ordering (range F) (f n) = F (f n)\<rbrakk> \<Longrightarrow> OrdinalVeblen.ordering (range F) (oLimit f) = F (oLimit f)
[PROOF STEP]
apply (rule rangeI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>y. y \<in> range F \<Longrightarrow> F 0 \<le> y
 2. \<And>x xa. OrdinalVeblen.ordering (range F) xa = F xa \<Longrightarrow> OrdinalVeblen.ordering (range F) (oSuc xa) = F (oSuc xa)
 3. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. OrdinalVeblen.ordering (range F) (f n) = F (f n)\<rbrakk> \<Longrightarrow> OrdinalVeblen.ordering (range F) (oLimit f) = F (oLimit f)
[PROOF STEP]
apply (clarsimp simp add: cancel_le)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. OrdinalVeblen.ordering (range F) xa = F xa \<Longrightarrow> OrdinalVeblen.ordering (range F) (oSuc xa) = F (oSuc xa)
 2. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. OrdinalVeblen.ordering (range F) (f n) = F (f n)\<rbrakk> \<Longrightarrow> OrdinalVeblen.ordering (range F) (oLimit f) = F (oLimit f)
[PROOF STEP]
apply (simp add: ordering_oSuc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. OrdinalVeblen.ordering (range F) xa = F xa \<Longrightarrow> (LEAST z. z \<in> range F \<and> F xa < z) = F (oSuc xa)
 2. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. OrdinalVeblen.ordering (range F) (f n) = F (f n)\<rbrakk> \<Longrightarrow> OrdinalVeblen.ordering (range F) (oLimit f) = F (oLimit f)
[PROOF STEP]
apply (rule Least_equality)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa. OrdinalVeblen.ordering (range F) xa = F xa \<Longrightarrow> F (oSuc xa) \<in> range F \<and> F xa < F (oSuc xa)
 2. \<And>xa y. \<lbrakk>OrdinalVeblen.ordering (range F) xa = F xa; y \<in> range F \<and> F xa < y\<rbrakk> \<Longrightarrow> F (oSuc xa) \<le> y
 3. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. OrdinalVeblen.ordering (range F) (f n) = F (f n)\<rbrakk> \<Longrightarrow> OrdinalVeblen.ordering (range F) (oLimit f) = F (oLimit f)
[PROOF STEP]
apply (simp add: cancel_less)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>OrdinalVeblen.ordering (range F) xa = F xa; y \<in> range F \<and> F xa < y\<rbrakk> \<Longrightarrow> F (oSuc xa) \<le> y
 2. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. OrdinalVeblen.ordering (range F) (f n) = F (f n)\<rbrakk> \<Longrightarrow> OrdinalVeblen.ordering (range F) (oLimit f) = F (oLimit f)
[PROOF STEP]
apply (clarsimp simp add: cancel_le cancel_less oSuc_leI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. OrdinalVeblen.ordering (range F) (f n) = F (f n)\<rbrakk> \<Longrightarrow> OrdinalVeblen.ordering (range F) (oLimit f) = F (oLimit f)
[PROOF STEP]
apply (subst normal_set.ordering_oLimit)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. OrdinalVeblen.ordering (range F) (f n) = F (f n)\<rbrakk> \<Longrightarrow> normal_set (range F)
 2. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. OrdinalVeblen.ordering (range F) (f n) = F (f n)\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. OrdinalVeblen.ordering (range F) (f n)) = F (oLimit f)
[PROOF STEP]
apply (rule normal_set_range)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. OrdinalVeblen.ordering (range F) (f n) = F (f n)\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. OrdinalVeblen.ordering (range F) (f n)) = F (oLimit f)
[PROOF STEP]
apply (simp add: oLimit)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in normal_set) ordering_mem: "ordering A x \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdinalVeblen.ordering A x \<in> A
[PROOF STEP]
apply (rule_tac a=x in oLimit_induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. OrdinalVeblen.ordering A 0 \<in> A
 2. \<And>x. OrdinalVeblen.ordering A x \<in> A \<Longrightarrow> OrdinalVeblen.ordering A (oSuc x) \<in> A
 3. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. OrdinalVeblen.ordering A (f n) \<in> A\<rbrakk> \<Longrightarrow> OrdinalVeblen.ordering A (oLimit f) \<in> A
[PROOF STEP]
apply (subst ordering_0)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (LEAST z. z \<in> A) \<in> A
 2. \<And>x. OrdinalVeblen.ordering A x \<in> A \<Longrightarrow> OrdinalVeblen.ordering A (oSuc x) \<in> A
 3. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. OrdinalVeblen.ordering A (f n) \<in> A\<rbrakk> \<Longrightarrow> OrdinalVeblen.ordering A (oLimit f) \<in> A
[PROOF STEP]
apply (rule LeastI_ex)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<exists>x. x \<in> A
 2. \<And>x. OrdinalVeblen.ordering A x \<in> A \<Longrightarrow> OrdinalVeblen.ordering A (oSuc x) \<in> A
 3. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. OrdinalVeblen.ordering A (f n) \<in> A\<rbrakk> \<Longrightarrow> OrdinalVeblen.ordering A (oLimit f) \<in> A
[PROOF STEP]
apply (cut_tac unbounded, force)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. OrdinalVeblen.ordering A x \<in> A \<Longrightarrow> OrdinalVeblen.ordering A (oSuc x) \<in> A
 2. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. OrdinalVeblen.ordering A (f n) \<in> A\<rbrakk> \<Longrightarrow> OrdinalVeblen.ordering A (oLimit f) \<in> A
[PROOF STEP]
apply (subst ordering_oSuc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. OrdinalVeblen.ordering A x \<in> A \<Longrightarrow> (LEAST z. z \<in> A \<and> OrdinalVeblen.ordering A x < z) \<in> A
 2. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. OrdinalVeblen.ordering A (f n) \<in> A\<rbrakk> \<Longrightarrow> OrdinalVeblen.ordering A (oLimit f) \<in> A
[PROOF STEP]
apply (rule mem_next)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. OrdinalVeblen.ordering A (f n) \<in> A\<rbrakk> \<Longrightarrow> OrdinalVeblen.ordering A (oLimit f) \<in> A
[PROOF STEP]
apply (subst ordering_oLimit)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n. OrdinalVeblen.ordering A (f n) \<in> A\<rbrakk> \<Longrightarrow> oLimit (\<lambda>n. OrdinalVeblen.ordering A (f n)) \<in> A
[PROOF STEP]
apply (erule closed)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in normal_set) range_ordering_lemma:
"\<forall>y. y \<in> A \<longrightarrow> y < ordering A x \<longrightarrow> y \<in> range (ordering A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y. y \<in> A \<longrightarrow> y < OrdinalVeblen.ordering A x \<longrightarrow> y \<in> range (OrdinalVeblen.ordering A)
[PROOF STEP]
apply (simp add: image_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y. y \<in> A \<longrightarrow> y < OrdinalVeblen.ordering A x \<longrightarrow> (\<exists>x. y = OrdinalVeblen.ordering A x)
[PROOF STEP]
apply (rule_tac a=x in oLimit_induct, safe)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>y \<in> A; y < OrdinalVeblen.ordering A 0\<rbrakk> \<Longrightarrow> \<exists>x. y = OrdinalVeblen.ordering A x
 2. \<And>x y. \<lbrakk>\<forall>y. y \<in> A \<longrightarrow> y < OrdinalVeblen.ordering A x \<longrightarrow> (\<exists>x. y = OrdinalVeblen.ordering A x); y \<in> A; y < OrdinalVeblen.ordering A (oSuc x)\<rbrakk> \<Longrightarrow> \<exists>x. y = OrdinalVeblen.ordering A x
 3. \<And>f y. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<in> A \<longrightarrow> y < OrdinalVeblen.ordering A (f n) \<longrightarrow> (\<exists>x. y = OrdinalVeblen.ordering A x); y \<in> A; y < OrdinalVeblen.ordering A (oLimit f)\<rbrakk> \<Longrightarrow> \<exists>x. y = OrdinalVeblen.ordering A x
[PROOF STEP]
apply (simp add: ordering_0)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>y \<in> A; y < (LEAST z. z \<in> A)\<rbrakk> \<Longrightarrow> \<exists>x. y = OrdinalVeblen.ordering A x
 2. \<And>x y. \<lbrakk>\<forall>y. y \<in> A \<longrightarrow> y < OrdinalVeblen.ordering A x \<longrightarrow> (\<exists>x. y = OrdinalVeblen.ordering A x); y \<in> A; y < OrdinalVeblen.ordering A (oSuc x)\<rbrakk> \<Longrightarrow> \<exists>x. y = OrdinalVeblen.ordering A x
 3. \<And>f y. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<in> A \<longrightarrow> y < OrdinalVeblen.ordering A (f n) \<longrightarrow> (\<exists>x. y = OrdinalVeblen.ordering A x); y \<in> A; y < OrdinalVeblen.ordering A (oLimit f)\<rbrakk> \<Longrightarrow> \<exists>x. y = OrdinalVeblen.ordering A x
[PROOF STEP]
apply (drule not_less_Least, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>y. y \<in> A \<longrightarrow> y < OrdinalVeblen.ordering A x \<longrightarrow> (\<exists>x. y = OrdinalVeblen.ordering A x); y \<in> A; y < OrdinalVeblen.ordering A (oSuc x)\<rbrakk> \<Longrightarrow> \<exists>x. y = OrdinalVeblen.ordering A x
 2. \<And>f y. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<in> A \<longrightarrow> y < OrdinalVeblen.ordering A (f n) \<longrightarrow> (\<exists>x. y = OrdinalVeblen.ordering A x); y \<in> A; y < OrdinalVeblen.ordering A (oLimit f)\<rbrakk> \<Longrightarrow> \<exists>x. y = OrdinalVeblen.ordering A x
[PROOF STEP]
apply (simp add: ordering_oSuc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>y. y \<in> A \<longrightarrow> y < OrdinalVeblen.ordering A x \<longrightarrow> (\<exists>x. y = OrdinalVeblen.ordering A x); y \<in> A; y < (LEAST z. z \<in> A \<and> OrdinalVeblen.ordering A x < z)\<rbrakk> \<Longrightarrow> \<exists>x. y = OrdinalVeblen.ordering A x
 2. \<And>f y. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<in> A \<longrightarrow> y < OrdinalVeblen.ordering A (f n) \<longrightarrow> (\<exists>x. y = OrdinalVeblen.ordering A x); y \<in> A; y < OrdinalVeblen.ordering A (oLimit f)\<rbrakk> \<Longrightarrow> \<exists>x. y = OrdinalVeblen.ordering A x
[PROOF STEP]
apply (drule not_less_Least, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>\<forall>y. y \<in> A \<longrightarrow> y < OrdinalVeblen.ordering A x \<longrightarrow> (\<exists>x. y = OrdinalVeblen.ordering A x); y \<in> A; \<not> OrdinalVeblen.ordering A x < y\<rbrakk> \<Longrightarrow> \<exists>x. y = OrdinalVeblen.ordering A x
 2. \<And>f y. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<in> A \<longrightarrow> y < OrdinalVeblen.ordering A (f n) \<longrightarrow> (\<exists>x. y = OrdinalVeblen.ordering A x); y \<in> A; y < OrdinalVeblen.ordering A (oLimit f)\<rbrakk> \<Longrightarrow> \<exists>x. y = OrdinalVeblen.ordering A x
[PROOF STEP]
apply (force simp add: linorder_not_less order_le_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f y. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<in> A \<longrightarrow> y < OrdinalVeblen.ordering A (f n) \<longrightarrow> (\<exists>x. y = OrdinalVeblen.ordering A x); y \<in> A; y < OrdinalVeblen.ordering A (oLimit f)\<rbrakk> \<Longrightarrow> \<exists>x. y = OrdinalVeblen.ordering A x
[PROOF STEP]
apply (simp add: ordering_oLimit)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f y. \<lbrakk>OrdinalInduct.strict_mono f; \<forall>n y. y \<in> A \<longrightarrow> y < OrdinalVeblen.ordering A (f n) \<longrightarrow> (\<exists>x. y = OrdinalVeblen.ordering A x); y \<in> A; y < oLimit (\<lambda>n. OrdinalVeblen.ordering A (f n))\<rbrakk> \<Longrightarrow> \<exists>x. y = OrdinalVeblen.ordering A x
[PROOF STEP]
apply (drule less_oLimitD, clarsimp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in normal_set) range_ordering: "range (ordering A) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range (OrdinalVeblen.ordering A) = A
[PROOF STEP]
apply (safe intro!: ordering_mem)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> range (OrdinalVeblen.ordering A)
[PROOF STEP]
apply (erule_tac x="oSuc x" in range_ordering_lemma[rule_format])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x < OrdinalVeblen.ordering A (oSuc x)
[PROOF STEP]
apply (rule order_less_le_trans[OF less_oSuc])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. oSuc x \<le> OrdinalVeblen.ordering A (oSuc x)
[PROOF STEP]
apply (rule normal.increasing[OF normal_ordering])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done