[STATEMENT]
theorem ccard_diff_lgth:
    shows "n'\<ge>n \<Longrightarrow> bc n' - bc n \<ge> ccard n n' (\<lambda>n. mining n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> n' \<Longrightarrow> card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n
[PROOF STEP]
proof (induction n' rule: dec_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. card {i. n < i \<and> i \<le> n \<and> mining i} \<le> bc n - bc n
 2. \<And>na. \<lbrakk>n \<le> na; na < n'; card {i. n < i \<and> i \<le> na \<and> mining i} \<le> bc na - bc n\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc na \<and> mining i} \<le> bc (Suc na) - bc n
[PROOF STEP]
case base
[PROOF STATE]
proof (state)
this:


goal (2 subgoals):
 1. card {i. n < i \<and> i \<le> n \<and> mining i} \<le> bc n - bc n
 2. \<And>na. \<lbrakk>n \<le> na; na < n'; card {i. n < i \<and> i \<le> na \<and> mining i} \<le> bc na - bc n\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc na \<and> mining i} \<le> bc (Suc na) - bc n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> n \<and> mining i} \<le> bc n - bc n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> n \<and> mining i} \<le> bc n - bc n

goal (1 subgoal):
 1. \<And>na. \<lbrakk>n \<le> na; na < n'; card {i. n < i \<and> i \<le> na \<and> mining i} \<le> bc na - bc n\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc na \<and> mining i} \<le> bc (Suc na) - bc n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>n \<le> na; na < n'; card {i. n < i \<and> i \<le> na \<and> mining i} \<le> bc na - bc n\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc na \<and> mining i} \<le> bc (Suc na) - bc n
[PROOF STEP]
case (step n')
[PROOF STATE]
proof (state)
this:
n \<le> n'
n' < n'
card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n

goal (1 subgoal):
 1. \<And>na. \<lbrakk>n \<le> na; na < n'; card {i. n < i \<and> i \<le> na \<and> mining i} \<le> bc na - bc n\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc na \<and> mining i} \<le> bc (Suc na) - bc n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<le> n'
n' < n'
card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n \<le> n'
n' < n'
card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
 2. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
assume "mining (Suc n')"
[PROOF STATE]
proof (state)
this:
mining (Suc n')

goal (2 subgoals):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
 2. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
with as2
[PROOF STATE]
proof (chain)
picking this:
mining (Suc ?n) \<Longrightarrow> bc ?n < bc (Suc ?n)
mining (Suc n')
[PROOF STEP]
have "bc (Suc n') > bc n'"
[PROOF STATE]
proof (prove)
using this:
mining (Suc ?n) \<Longrightarrow> bc ?n < bc (Suc ?n)
mining (Suc n')

goal (1 subgoal):
 1. bc n' < bc (Suc n')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bc n' < bc (Suc n')

goal (2 subgoals):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
 2. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bc n' < bc (Suc n')

goal (2 subgoals):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
 2. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
from step.hyps
[PROOF STATE]
proof (chain)
picking this:
n \<le> n'
n' < n'
[PROOF STEP]
have "bc n'\<ge>bc n"
[PROOF STATE]
proof (prove)
using this:
n \<le> n'
n' < n'

goal (1 subgoal):
 1. bc n \<le> bc n'
[PROOF STEP]
using grow_mono
[PROOF STATE]
proof (prove)
using this:
n \<le> n'
n' < n'
?n \<le> ?n' \<Longrightarrow> bc ?n \<le> bc ?n'

goal (1 subgoal):
 1. bc n \<le> bc n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bc n \<le> bc n'

goal (2 subgoals):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
 2. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bc n' < bc (Suc n')
bc n \<le> bc n'
[PROOF STEP]
have "bc (Suc n') - bc n > bc n' - bc n"
[PROOF STATE]
proof (prove)
using this:
bc n' < bc (Suc n')
bc n \<le> bc n'

goal (1 subgoal):
 1. bc n' - bc n < bc (Suc n') - bc n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bc n' - bc n < bc (Suc n') - bc n

goal (2 subgoals):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
 2. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bc n' - bc n < bc (Suc n') - bc n

goal (2 subgoals):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
 2. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
from as1
[PROOF STATE]
proof (chain)
picking this:
bc ?n \<le> bc (Suc ?n)
[PROOF STEP]
have "bc (Suc n') - bc n \<ge> bc n' - bc n"
[PROOF STATE]
proof (prove)
using this:
bc ?n \<le> bc (Suc ?n)

goal (1 subgoal):
 1. bc n' - bc n \<le> bc (Suc n') - bc n
[PROOF STEP]
by (simp add: diff_le_mono)
[PROOF STATE]
proof (state)
this:
bc n' - bc n \<le> bc (Suc n') - bc n

goal (2 subgoals):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
 2. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bc n' - bc n \<le> bc (Suc n') - bc n

goal (2 subgoals):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
 2. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
from \<open>mining (Suc n')\<close> step.hyps
[PROOF STATE]
proof (chain)
picking this:
mining (Suc n')
n \<le> n'
n' < n'
[PROOF STEP]
have "ccard n (Suc n') (\<lambda>n. mining n) \<le> Suc (ccard n n' (\<lambda>n. mining n))"
[PROOF STATE]
proof (prove)
using this:
mining (Suc n')
n \<le> n'
n' < n'

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> Suc (card {i. n < i \<and> i \<le> n' \<and> mining i})
[PROOF STEP]
using ccard_inc
[PROOF STATE]
proof (prove)
using this:
mining (Suc n')
n \<le> n'
n' < n'
\<lbrakk>?p (Suc ?n'); ?n \<le> ?n'\<rbrakk> \<Longrightarrow> card {i. ?n < i \<and> i \<le> Suc ?n' \<and> ?p i} = Suc (card {i. ?n < i \<and> i \<le> ?n' \<and> ?p i})

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> Suc (card {i. n < i \<and> i \<le> n' \<and> mining i})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> Suc (card {i. n < i \<and> i \<le> n' \<and> mining i})

goal (2 subgoals):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
 2. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> ?P3\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bc n' - bc n < bc (Suc n') - bc n
bc n' - bc n \<le> bc (Suc n') - bc n
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> Suc (card {i. n < i \<and> i \<le> n' \<and> mining i})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bc n' - bc n < bc (Suc n') - bc n
bc n' - bc n \<le> bc (Suc n') - bc n
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> Suc (card {i. n < i \<and> i \<le> n' \<and> mining i})

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
using step.IH
[PROOF STATE]
proof (prove)
using this:
bc n' - bc n < bc (Suc n') - bc n
bc n' - bc n \<le> bc (Suc n') - bc n
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> Suc (card {i. n < i \<and> i \<le> n' \<and> mining i})
card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n

goal (1 subgoal):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> mining (Suc n')\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> mining (Suc n')\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
assume "\<not> mining (Suc n')"
[PROOF STATE]
proof (state)
this:
\<not> mining (Suc n')

goal (1 subgoal):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> mining (Suc n')\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
hence "ccard n (Suc n') (\<lambda>n. mining n) \<le> (ccard n n' (\<lambda>n. mining n))"
[PROOF STATE]
proof (prove)
using this:
\<not> mining (Suc n')

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> card {i. n < i \<and> i \<le> n' \<and> mining i}
[PROOF STEP]
using ccard_same
[PROOF STATE]
proof (prove)
using this:
\<not> mining (Suc n')
\<not> ?p (Suc ?n') \<Longrightarrow> card {i. ?n < i \<and> i \<le> ?n' \<and> ?p i} = card {i. ?n < i \<and> i \<le> Suc ?n' \<and> ?p i}

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> card {i. n < i \<and> i \<le> n' \<and> mining i}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> card {i. n < i \<and> i \<le> n' \<and> mining i}

goal (1 subgoal):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> mining (Suc n')\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> card {i. n < i \<and> i \<le> n' \<and> mining i}

goal (1 subgoal):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> mining (Suc n')\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
from as1
[PROOF STATE]
proof (chain)
picking this:
bc ?n \<le> bc (Suc ?n)
[PROOF STEP]
have "bc (Suc n') - bc n \<ge> bc n' - bc n"
[PROOF STATE]
proof (prove)
using this:
bc ?n \<le> bc (Suc ?n)

goal (1 subgoal):
 1. bc n' - bc n \<le> bc (Suc n') - bc n
[PROOF STEP]
by (simp add: diff_le_mono)
[PROOF STATE]
proof (state)
this:
bc n' - bc n \<le> bc (Suc n') - bc n

goal (1 subgoal):
 1. \<lbrakk>n \<le> n'; n' < n'; card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n; \<not> mining (Suc n')\<rbrakk> \<Longrightarrow> card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> card {i. n < i \<and> i \<le> n' \<and> mining i}
bc n' - bc n \<le> bc (Suc n') - bc n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> card {i. n < i \<and> i \<le> n' \<and> mining i}
bc n' - bc n \<le> bc (Suc n') - bc n

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
using step.IH
[PROOF STATE]
proof (prove)
using this:
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> card {i. n < i \<and> i \<le> n' \<and> mining i}
bc n' - bc n \<le> bc (Suc n') - bc n
card {i. n < i \<and> i \<le> n' \<and> mining i} \<le> bc n' - bc n

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> Suc n' \<and> mining i} \<le> bc (Suc n') - bc n

goal:
No subgoals!
[PROOF STEP]
qed