[STATEMENT]
lemma is_aligned_diff:
  fixes m :: "'a::len word"
  assumes alm: "is_aligned m s1"
  and     aln: "is_aligned n s2"
  and    s2wb: "s2 < LENGTH('a)"
  and      nm: "m \<in> {n .. n + (2 ^ s2 - 1)}"
  and    s1s2: "s1 \<le> s2"
  and     s10: "0 < s1" (* Probably can be folded into the proof \<dots> *)
shows  "\<exists>q. m - n = of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
have rl: "\<And>m s. \<lbrakk> m < 2 ^ (LENGTH('a) - s); s < LENGTH('a) \<rbrakk> \<Longrightarrow> unat ((2::'a word) ^ s * of_nat m) = 2 ^ s * m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m s. \<lbrakk>m < 2 ^ (LENGTH('a) - s); s < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ s * word_of_nat m) = 2 ^ s * m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m s. \<lbrakk>m < 2 ^ (LENGTH('a) - s); s < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ s * word_of_nat m) = 2 ^ s * m
[PROOF STEP]
fix m :: nat and  s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m s. \<lbrakk>m < 2 ^ (LENGTH('a) - s); s < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ s * word_of_nat m) = 2 ^ s * m
[PROOF STEP]
assume m: "m < 2 ^ (LENGTH('a) - s)" and s: "s < LENGTH('a)"
[PROOF STATE]
proof (state)
this:
m < 2 ^ (LENGTH('a) - s)
s < LENGTH('a)

goal (1 subgoal):
 1. \<And>m s. \<lbrakk>m < 2 ^ (LENGTH('a) - s); s < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ s * word_of_nat m) = 2 ^ s * m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m < 2 ^ (LENGTH('a) - s)
s < LENGTH('a)
[PROOF STEP]
have "unat ((of_nat m) :: 'a word) = m"
[PROOF STATE]
proof (prove)
using this:
m < 2 ^ (LENGTH('a) - s)
s < LENGTH('a)

goal (1 subgoal):
 1. unat (word_of_nat m) = m
[PROOF STEP]
apply (subst unat_of_nat)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m < 2 ^ (LENGTH('a) - s); s < LENGTH('a)\<rbrakk> \<Longrightarrow> m mod 2 ^ LENGTH('a) = m
[PROOF STEP]
apply (subst mod_less)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m < 2 ^ (LENGTH('a) - s); s < LENGTH('a)\<rbrakk> \<Longrightarrow> m < 2 ^ LENGTH('a)
 2. \<lbrakk>m < 2 ^ (LENGTH('a) - s); s < LENGTH('a)\<rbrakk> \<Longrightarrow> m = m
[PROOF STEP]
apply (erule order_less_le_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. s < LENGTH('a) \<Longrightarrow> 2 ^ (LENGTH('a) - s) \<le> 2 ^ LENGTH('a)
 2. \<lbrakk>m < 2 ^ (LENGTH('a) - s); s < LENGTH('a)\<rbrakk> \<Longrightarrow> m = m
[PROOF STEP]
apply (rule power_increasing)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. s < LENGTH('a) \<Longrightarrow> LENGTH('a) - s \<le> LENGTH('a)
 2. s < LENGTH('a) \<Longrightarrow> 1 \<le> 2
 3. \<lbrakk>m < 2 ^ (LENGTH('a) - s); s < LENGTH('a)\<rbrakk> \<Longrightarrow> m = m
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
unat (word_of_nat m) = m

goal (1 subgoal):
 1. \<And>m s. \<lbrakk>m < 2 ^ (LENGTH('a) - s); s < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ s * word_of_nat m) = 2 ^ s * m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
unat (word_of_nat m) = m
[PROOF STEP]
show "?thesis m s"
[PROOF STATE]
proof (prove)
using this:
unat (word_of_nat m) = m

goal (1 subgoal):
 1. unat (2 ^ s * word_of_nat m) = 2 ^ s * m
[PROOF STEP]
using s m
[PROOF STATE]
proof (prove)
using this:
unat (word_of_nat m) = m
s < LENGTH('a)
m < 2 ^ (LENGTH('a) - s)

goal (1 subgoal):
 1. unat (2 ^ s * word_of_nat m) = 2 ^ s * m
[PROOF STEP]
apply (subst iffD1 [OF unat_mult_lem])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>unat (word_of_nat m) = m; s < LENGTH('a); m < 2 ^ (LENGTH('a) - s)\<rbrakk> \<Longrightarrow> unat (2 ^ s) * unat (word_of_nat m) < 2 ^ LENGTH('a)
 2. \<lbrakk>unat (word_of_nat m) = m; s < LENGTH('a); m < 2 ^ (LENGTH('a) - s)\<rbrakk> \<Longrightarrow> unat (2 ^ s) * unat (word_of_nat m) = 2 ^ s * m
[PROOF STEP]
apply (simp add: nat_less_power_trans)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
unat (2 ^ s * word_of_nat m) = 2 ^ s * m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?m < 2 ^ (LENGTH('a) - ?s); ?s < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (2 ^ ?s * word_of_nat ?m) = 2 ^ ?s * ?m

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
have s1wb: "s1 < LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s1 < LENGTH('a)
[PROOF STEP]
using s2wb s1s2
[PROOF STATE]
proof (prove)
using this:
s2 < LENGTH('a)
s1 \<le> s2

goal (1 subgoal):
 1. s1 < LENGTH('a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s1 < LENGTH('a)

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
from alm
[PROOF STATE]
proof (chain)
picking this:
is_aligned m s1
[PROOF STEP]
obtain mq where mmq: "m = 2 ^ s1 * of_nat mq" and mq: "mq < 2 ^ (LENGTH('a) - s1)"
[PROOF STATE]
proof (prove)
using this:
is_aligned m s1

goal (1 subgoal):
 1. (\<And>mq. \<lbrakk>m = 2 ^ s1 * word_of_nat mq; mq < 2 ^ (LENGTH('a) - s1)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: is_alignedE simp: field_simps)
[PROOF STATE]
proof (state)
this:
m = 2 ^ s1 * word_of_nat mq
mq < 2 ^ (LENGTH('a) - s1)

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
from aln
[PROOF STATE]
proof (chain)
picking this:
is_aligned n s2
[PROOF STEP]
obtain nq where nnq: "n = 2 ^ s2 * of_nat nq" and nq: "nq < 2 ^ (LENGTH('a) - s2)"
[PROOF STATE]
proof (prove)
using this:
is_aligned n s2

goal (1 subgoal):
 1. (\<And>nq. \<lbrakk>n = 2 ^ s2 * word_of_nat nq; nq < 2 ^ (LENGTH('a) - s2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: is_alignedE simp: field_simps)
[PROOF STATE]
proof (state)
this:
n = 2 ^ s2 * word_of_nat nq
nq < 2 ^ (LENGTH('a) - s2)

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
from s1s2
[PROOF STATE]
proof (chain)
picking this:
s1 \<le> s2
[PROOF STEP]
obtain sq where sq: "s2 = s1 + sq"
[PROOF STATE]
proof (prove)
using this:
s1 \<le> s2

goal (1 subgoal):
 1. (\<And>sq. s2 = s1 + sq \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: le_iff_add)
[PROOF STATE]
proof (state)
this:
s2 = s1 + sq

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
note us1 = rl [OF mq s1wb]
[PROOF STATE]
proof (state)
this:
unat (2 ^ s1 * word_of_nat mq) = 2 ^ s1 * mq

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
note us2 = rl [OF nq s2wb]
[PROOF STATE]
proof (state)
this:
unat (2 ^ s2 * word_of_nat nq) = 2 ^ s2 * nq

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
from nm
[PROOF STATE]
proof (chain)
picking this:
m \<in> {n..n + (2 ^ s2 - 1)}
[PROOF STEP]
have "n \<le> m"
[PROOF STATE]
proof (prove)
using this:
m \<in> {n..n + (2 ^ s2 - 1)}

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

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<le> m
[PROOF STEP]
have "(2::'a word) ^ s2 * of_nat nq \<le> 2 ^ s1 * of_nat mq"
[PROOF STATE]
proof (prove)
using this:
n \<le> m

goal (1 subgoal):
 1. 2 ^ s2 * word_of_nat nq \<le> 2 ^ s1 * word_of_nat mq
[PROOF STEP]
using nnq mmq
[PROOF STATE]
proof (prove)
using this:
n \<le> m
n = 2 ^ s2 * word_of_nat nq
m = 2 ^ s1 * word_of_nat mq

goal (1 subgoal):
 1. 2 ^ s2 * word_of_nat nq \<le> 2 ^ s1 * word_of_nat mq
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ s2 * word_of_nat nq \<le> 2 ^ s1 * word_of_nat mq

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 ^ s2 * word_of_nat nq \<le> 2 ^ s1 * word_of_nat mq
[PROOF STEP]
have "2 ^ s2 * nq \<le> 2 ^ s1 * mq"
[PROOF STATE]
proof (prove)
using this:
2 ^ s2 * word_of_nat nq \<le> 2 ^ s1 * word_of_nat mq

goal (1 subgoal):
 1. 2 ^ s2 * nq \<le> 2 ^ s1 * mq
[PROOF STEP]
using s1wb s2wb
[PROOF STATE]
proof (prove)
using this:
2 ^ s2 * word_of_nat nq \<le> 2 ^ s1 * word_of_nat mq
s1 < LENGTH('a)
s2 < LENGTH('a)

goal (1 subgoal):
 1. 2 ^ s2 * nq \<le> 2 ^ s1 * mq
[PROOF STEP]
by (simp add: word_le_nat_alt us1 us2)
[PROOF STATE]
proof (state)
this:
2 ^ s2 * nq \<le> 2 ^ s1 * mq

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 ^ s2 * nq \<le> 2 ^ s1 * mq
[PROOF STEP]
have nqmq: "2 ^ sq * nq \<le> mq"
[PROOF STATE]
proof (prove)
using this:
2 ^ s2 * nq \<le> 2 ^ s1 * mq

goal (1 subgoal):
 1. 2 ^ sq * nq \<le> mq
[PROOF STEP]
using sq
[PROOF STATE]
proof (prove)
using this:
2 ^ s2 * nq \<le> 2 ^ s1 * mq
s2 = s1 + sq

goal (1 subgoal):
 1. 2 ^ sq * nq \<le> mq
[PROOF STEP]
by (simp add: power_add)
[PROOF STATE]
proof (state)
this:
2 ^ sq * nq \<le> mq

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
have "m - n = 2 ^ s1 * of_nat mq - 2 ^ s2 * of_nat nq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m - n = 2 ^ s1 * word_of_nat mq - 2 ^ s2 * word_of_nat nq
[PROOF STEP]
using mmq nnq
[PROOF STATE]
proof (prove)
using this:
m = 2 ^ s1 * word_of_nat mq
n = 2 ^ s2 * word_of_nat nq

goal (1 subgoal):
 1. m - n = 2 ^ s1 * word_of_nat mq - 2 ^ s2 * word_of_nat nq
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m - n = 2 ^ s1 * word_of_nat mq - 2 ^ s2 * word_of_nat nq

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
m - n = 2 ^ s1 * word_of_nat mq - 2 ^ s2 * word_of_nat nq

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
have "\<dots> = 2 ^ s1 * of_nat mq - 2 ^ s1 * 2 ^ sq * of_nat nq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ s1 * word_of_nat mq - 2 ^ s2 * word_of_nat nq = 2 ^ s1 * word_of_nat mq - 2 ^ s1 * 2 ^ sq * word_of_nat nq
[PROOF STEP]
using sq
[PROOF STATE]
proof (prove)
using this:
s2 = s1 + sq

goal (1 subgoal):
 1. 2 ^ s1 * word_of_nat mq - 2 ^ s2 * word_of_nat nq = 2 ^ s1 * word_of_nat mq - 2 ^ s1 * 2 ^ sq * word_of_nat nq
[PROOF STEP]
by (simp add: power_add)
[PROOF STATE]
proof (state)
this:
2 ^ s1 * word_of_nat mq - 2 ^ s2 * word_of_nat nq = 2 ^ s1 * word_of_nat mq - 2 ^ s1 * 2 ^ sq * word_of_nat nq

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 ^ s1 * word_of_nat mq - 2 ^ s2 * word_of_nat nq = 2 ^ s1 * word_of_nat mq - 2 ^ s1 * 2 ^ sq * word_of_nat nq

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
have "\<dots> = 2 ^ s1 * (of_nat mq - 2 ^ sq * of_nat nq)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ s1 * word_of_nat mq - 2 ^ s1 * 2 ^ sq * word_of_nat nq = 2 ^ s1 * (word_of_nat mq - 2 ^ sq * word_of_nat nq)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
2 ^ s1 * word_of_nat mq - 2 ^ s1 * 2 ^ sq * word_of_nat nq = 2 ^ s1 * (word_of_nat mq - 2 ^ sq * word_of_nat nq)

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 ^ s1 * word_of_nat mq - 2 ^ s1 * 2 ^ sq * word_of_nat nq = 2 ^ s1 * (word_of_nat mq - 2 ^ sq * word_of_nat nq)

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
have "\<dots> = 2 ^ s1 * of_nat (mq - 2 ^ sq * nq)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ s1 * (word_of_nat mq - 2 ^ sq * word_of_nat nq) = 2 ^ s1 * word_of_nat (mq - 2 ^ sq * nq)
[PROOF STEP]
using s1wb s2wb us1 us2 nqmq
[PROOF STATE]
proof (prove)
using this:
s1 < LENGTH('a)
s2 < LENGTH('a)
unat (2 ^ s1 * word_of_nat mq) = 2 ^ s1 * mq
unat (2 ^ s2 * word_of_nat nq) = 2 ^ s2 * nq
2 ^ sq * nq \<le> mq

goal (1 subgoal):
 1. 2 ^ s1 * (word_of_nat mq - 2 ^ sq * word_of_nat nq) = 2 ^ s1 * word_of_nat (mq - 2 ^ sq * nq)
[PROOF STEP]
by (simp add: of_nat_diff)
[PROOF STATE]
proof (state)
this:
2 ^ s1 * (word_of_nat mq - 2 ^ sq * word_of_nat nq) = 2 ^ s1 * word_of_nat (mq - 2 ^ sq * nq)

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
m - n = 2 ^ s1 * word_of_nat (mq - 2 ^ sq * nq)
[PROOF STEP]
have mn: "m - n = of_nat (mq - 2 ^ sq * nq) * 2 ^ s1"
[PROOF STATE]
proof (prove)
using this:
m - n = 2 ^ s1 * word_of_nat (mq - 2 ^ sq * nq)

goal (1 subgoal):
 1. m - n = word_of_nat (mq - 2 ^ sq * nq) * 2 ^ s1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m - n = word_of_nat (mq - 2 ^ sq * nq) * 2 ^ s1

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
m - n = word_of_nat (mq - 2 ^ sq * nq) * 2 ^ s1

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
from nm
[PROOF STATE]
proof (chain)
picking this:
m \<in> {n..n + (2 ^ s2 - 1)}
[PROOF STEP]
have "m - n \<le> 2 ^ s2 - 1"
[PROOF STATE]
proof (prove)
using this:
m \<in> {n..n + (2 ^ s2 - 1)}

goal (1 subgoal):
 1. m - n \<le> 2 ^ s2 - 1
[PROOF STEP]
by - (rule word_diff_ls', (simp add: field_simps)+)
[PROOF STATE]
proof (state)
this:
m - n \<le> 2 ^ s2 - 1

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m - n \<le> 2 ^ s2 - 1
[PROOF STEP]
have "(2::'a word) ^ s1 * of_nat (mq - 2 ^ sq * nq) < 2 ^ s2"
[PROOF STATE]
proof (prove)
using this:
m - n \<le> 2 ^ s2 - 1

goal (1 subgoal):
 1. 2 ^ s1 * word_of_nat (mq - 2 ^ sq * nq) < 2 ^ s2
[PROOF STEP]
using mn s2wb
[PROOF STATE]
proof (prove)
using this:
m - n \<le> 2 ^ s2 - 1
m - n = word_of_nat (mq - 2 ^ sq * nq) * 2 ^ s1
s2 < LENGTH('a)

goal (1 subgoal):
 1. 2 ^ s1 * word_of_nat (mq - 2 ^ sq * nq) < 2 ^ s2
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
2 ^ s1 * word_of_nat (mq - 2 ^ sq * nq) < 2 ^ s2

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 ^ s1 * word_of_nat (mq - 2 ^ sq * nq) < 2 ^ s2
[PROOF STEP]
have "of_nat (mq - 2 ^ sq * nq) < (2::'a word) ^ (s2 - s1)"
[PROOF STATE]
proof (prove)
using this:
2 ^ s1 * word_of_nat (mq - 2 ^ sq * nq) < 2 ^ s2

goal (1 subgoal):
 1. word_of_nat (mq - 2 ^ sq * nq) < 2 ^ (s2 - s1)
[PROOF STEP]
proof (rule word_power_less_diff)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. word_of_nat (mq - 2 ^ sq * nq) < 2 ^ (LENGTH('a) - s1)
[PROOF STEP]
have mm: "mq - 2 ^ sq * nq < 2 ^ (LENGTH('a) - s1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mq - 2 ^ sq * nq < 2 ^ (LENGTH('a) - s1)
[PROOF STEP]
using mq
[PROOF STATE]
proof (prove)
using this:
mq < 2 ^ (LENGTH('a) - s1)

goal (1 subgoal):
 1. mq - 2 ^ sq * nq < 2 ^ (LENGTH('a) - s1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mq - 2 ^ sq * nq < 2 ^ (LENGTH('a) - s1)

goal (1 subgoal):
 1. word_of_nat (mq - 2 ^ sq * nq) < 2 ^ (LENGTH('a) - s1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mq - 2 ^ sq * nq < 2 ^ (LENGTH('a) - s1)

goal (1 subgoal):
 1. word_of_nat (mq - 2 ^ sq * nq) < 2 ^ (LENGTH('a) - s1)
[PROOF STEP]
from s10
[PROOF STATE]
proof (chain)
picking this:
0 < s1
[PROOF STEP]
have "LENGTH('a) - s1 < LENGTH('a)"
[PROOF STATE]
proof (prove)
using this:
0 < s1

goal (1 subgoal):
 1. LENGTH('a) - s1 < LENGTH('a)
[PROOF STEP]
by (rule diff_less, simp)
[PROOF STATE]
proof (state)
this:
LENGTH('a) - s1 < LENGTH('a)

goal (1 subgoal):
 1. word_of_nat (mq - 2 ^ sq * nq) < 2 ^ (LENGTH('a) - s1)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mq - 2 ^ sq * nq < 2 ^ (LENGTH('a) - s1)
LENGTH('a) - s1 < LENGTH('a)
[PROOF STEP]
show "of_nat (mq - 2 ^ sq * nq) < (2::'a word) ^ (LENGTH('a) - s1)"
[PROOF STATE]
proof (prove)
using this:
mq - 2 ^ sq * nq < 2 ^ (LENGTH('a) - s1)
LENGTH('a) - s1 < LENGTH('a)

goal (1 subgoal):
 1. word_of_nat (mq - 2 ^ sq * nq) < 2 ^ (LENGTH('a) - s1)
[PROOF STEP]
using take_bit_nat_less_self_iff [of \<open>LENGTH('a)\<close> \<open>mq - 2 ^ sq * nq\<close>]
[PROOF STATE]
proof (prove)
using this:
mq - 2 ^ sq * nq < 2 ^ (LENGTH('a) - s1)
LENGTH('a) - s1 < LENGTH('a)
(take_bit LENGTH('a) (mq - 2 ^ sq * nq) < mq - 2 ^ sq * nq) = (2 ^ LENGTH('a) \<le> mq - 2 ^ sq * nq)

goal (1 subgoal):
 1. word_of_nat (mq - 2 ^ sq * nq) < 2 ^ (LENGTH('a) - s1)
[PROOF STEP]
apply (auto simp add: word_less_nat_alt not_le not_less unsigned_of_nat)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mq - 2 ^ sq * nq < 2 ^ (LENGTH('a) - s1); LENGTH('a) - s1 < LENGTH('a); mq - 2 ^ sq * nq \<le> take_bit LENGTH('a) (mq - 2 ^ sq * nq); mq - 2 ^ sq * nq < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> take_bit LENGTH('a) (mq - 2 ^ sq * nq) < 2 ^ (LENGTH('a) - s1)
[PROOF STEP]
apply (metis take_bit_nat_eq_self_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
word_of_nat (mq - 2 ^ sq * nq) < 2 ^ (LENGTH('a) - s1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
word_of_nat (mq - 2 ^ sq * nq) < 2 ^ (s2 - s1)

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
word_of_nat (mq - 2 ^ sq * nq) < 2 ^ (s2 - s1)
[PROOF STEP]
have "mq - 2 ^ sq * nq < 2 ^ (s2 - s1)"
[PROOF STATE]
proof (prove)
using this:
word_of_nat (mq - 2 ^ sq * nq) < 2 ^ (s2 - s1)

goal (1 subgoal):
 1. mq - 2 ^ sq * nq < 2 ^ (s2 - s1)
[PROOF STEP]
using mq s2wb
[PROOF STATE]
proof (prove)
using this:
word_of_nat (mq - 2 ^ sq * nq) < 2 ^ (s2 - s1)
mq < 2 ^ (LENGTH('a) - s1)
s2 < LENGTH('a)

goal (1 subgoal):
 1. mq - 2 ^ sq * nq < 2 ^ (s2 - s1)
[PROOF STEP]
apply (simp add: word_less_nat_alt take_bit_eq_mod unsigned_of_nat)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(mq - 2 ^ sq * nq) mod 2 ^ LENGTH('a) < 2 ^ (s2 - s1); mq < 2 ^ (LENGTH('a) - s1); s2 < LENGTH('a)\<rbrakk> \<Longrightarrow> mq - 2 ^ sq * nq < 2 ^ (s2 - s1)
[PROOF STEP]
apply (subst (asm) mod_less)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mq < 2 ^ (LENGTH('a) - s1); s2 < LENGTH('a)\<rbrakk> \<Longrightarrow> mq - 2 ^ sq * nq < 2 ^ LENGTH('a)
 2. \<lbrakk>mq - 2 ^ sq * nq < 2 ^ (s2 - s1); mq < 2 ^ (LENGTH('a) - s1); s2 < LENGTH('a)\<rbrakk> \<Longrightarrow> mq - 2 ^ sq * nq < 2 ^ (s2 - s1)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mq < 2 ^ (LENGTH('a) - s1); s2 < LENGTH('a)\<rbrakk> \<Longrightarrow> mq - 2 ^ sq * nq < 2 ^ LENGTH('a)
[PROOF STEP]
apply (rule order_le_less_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mq < 2 ^ (LENGTH('a) - s1); s2 < LENGTH('a)\<rbrakk> \<Longrightarrow> mq - 2 ^ sq * nq \<le> ?y71
 2. \<lbrakk>mq < 2 ^ (LENGTH('a) - s1); s2 < LENGTH('a)\<rbrakk> \<Longrightarrow> ?y71 < 2 ^ LENGTH('a)
[PROOF STEP]
apply (rule diff_le_self)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mq < 2 ^ (LENGTH('a) - s1); s2 < LENGTH('a)\<rbrakk> \<Longrightarrow> mq < 2 ^ LENGTH('a)
[PROOF STEP]
apply (erule order_less_le_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s2 < LENGTH('a) \<Longrightarrow> 2 ^ (LENGTH('a) - s1) \<le> 2 ^ LENGTH('a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
mq - 2 ^ sq * nq < 2 ^ (s2 - s1)

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
m - n = word_of_nat (mq - 2 ^ sq * nq) * 2 ^ s1
mq - 2 ^ sq * nq < 2 ^ (s2 - s1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m - n = word_of_nat (mq - 2 ^ sq * nq) * 2 ^ s1
mq - 2 ^ sq * nq < 2 ^ (s2 - s1)

goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_aligned_addD1:
  assumes al1: "is_aligned (x + y) n"
  and     al2: "is_aligned (x::'a::len word) n"
  shows "is_aligned y n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned y n
[PROOF STEP]
using al2
[PROOF STATE]
proof (prove)
using this:
is_aligned x n

goal (1 subgoal):
 1. is_aligned y n
[PROOF STEP]
proof (rule is_aligned_get_word_bits)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned y n
 2. \<lbrakk>x = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> is_aligned y n
[PROOF STEP]
assume "x = 0"
[PROOF STATE]
proof (state)
this:
x = 0

goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned y n
 2. \<lbrakk>x = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> is_aligned y n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0

goal (1 subgoal):
 1. is_aligned y n
[PROOF STEP]
using al1
[PROOF STATE]
proof (prove)
using this:
x = 0
is_aligned (x + y) n

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

goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned y n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned y n
[PROOF STEP]
assume nv: "n < LENGTH('a)"
[PROOF STATE]
proof (state)
this:
n < LENGTH('a)

goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned y n
[PROOF STEP]
from al1
[PROOF STATE]
proof (chain)
picking this:
is_aligned (x + y) n
[PROOF STEP]
obtain q1
    where xy: "x + y = 2 ^ n * of_nat q1" and "q1 < 2 ^ (LENGTH('a) - n)"
[PROOF STATE]
proof (prove)
using this:
is_aligned (x + y) n

goal (1 subgoal):
 1. (\<And>q1. \<lbrakk>x + y = 2 ^ n * word_of_nat q1; q1 < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule is_alignedE)
[PROOF STATE]
proof (state)
this:
x + y = 2 ^ n * word_of_nat q1
q1 < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned y n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x + y = 2 ^ n * word_of_nat q1
q1 < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned y n
[PROOF STEP]
from al2
[PROOF STATE]
proof (chain)
picking this:
is_aligned x n
[PROOF STEP]
obtain q2
    where x: "x = 2 ^ n * of_nat q2" and "q2 < 2 ^ (LENGTH('a) - n)"
[PROOF STATE]
proof (prove)
using this:
is_aligned x n

goal (1 subgoal):
 1. (\<And>q2. \<lbrakk>x = 2 ^ n * word_of_nat q2; q2 < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule is_alignedE)
[PROOF STATE]
proof (state)
this:
x = 2 ^ n * word_of_nat q2
q2 < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned y n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x + y = 2 ^ n * word_of_nat q1
q1 < 2 ^ (LENGTH('a) - n)
x = 2 ^ n * word_of_nat q2
q2 < 2 ^ (LENGTH('a) - n)
[PROOF STEP]
have "y = 2 ^ n * (of_nat q1 - of_nat q2)"
[PROOF STATE]
proof (prove)
using this:
x + y = 2 ^ n * word_of_nat q1
q1 < 2 ^ (LENGTH('a) - n)
x = 2 ^ n * word_of_nat q2
q2 < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. y = 2 ^ n * (word_of_nat q1 - word_of_nat q2)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
y = 2 ^ n * (word_of_nat q1 - word_of_nat q2)

goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned y n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y = 2 ^ n * (word_of_nat q1 - word_of_nat q2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y = 2 ^ n * (word_of_nat q1 - word_of_nat q2)

goal (1 subgoal):
 1. is_aligned y n
[PROOF STEP]
using nv
[PROOF STATE]
proof (prove)
using this:
y = 2 ^ n * (word_of_nat q1 - word_of_nat q2)
n < LENGTH('a)

goal (1 subgoal):
 1. is_aligned y n
[PROOF STEP]
by (simp add: is_aligned_mult_triv1)
[PROOF STATE]
proof (state)
this:
is_aligned y n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_aligned_add:
  "\<lbrakk>is_aligned p n; is_aligned q n\<rbrakk> \<Longrightarrow> is_aligned (p + q) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned q n\<rbrakk> \<Longrightarrow> is_aligned (p + q) n
[PROOF STEP]
by (simp add: is_aligned_mask mask_add_aligned)


[STATEMENT]
lemma aligned_shift:
  "\<lbrakk>x < 2 ^ n; is_aligned (y :: 'a :: len word) n;n \<le> LENGTH('a)\<rbrakk>
   \<Longrightarrow> (x + y) >> n = y >> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ n; is_aligned y n; n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> x + y >> n = y >> n
[PROOF STEP]
apply (subst word_plus_and_or_coroll; rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>x < 2 ^ n; is_aligned y n; n \<le> LENGTH('a); na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (x AND y) na = bit 0 na
 2. \<And>na. \<lbrakk>x < 2 ^ n; is_aligned y n; n \<le> LENGTH('a); na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (x OR y >> n) na = bit (y >> n) na
[PROOF STEP]
apply (auto simp add: bit_simps is_aligned_nth)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>x < 2 ^ n; \<forall>na<n. \<not> bit y na; n \<le> LENGTH('a); na < LENGTH('a); bit x na; bit y na\<rbrakk> \<Longrightarrow> False
 2. \<And>na. \<lbrakk>x < 2 ^ n; \<forall>na<n. \<not> bit y na; n \<le> LENGTH('a); na < LENGTH('a); bit x (n + na)\<rbrakk> \<Longrightarrow> bit y (n + na)
[PROOF STEP]
apply (metis less_2p_is_upper_bits_unset not_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>x < 2 ^ n; \<forall>na<n. \<not> bit y na; n \<le> LENGTH('a); na < LENGTH('a); bit x (n + na)\<rbrakk> \<Longrightarrow> bit y (n + na)
[PROOF STEP]
apply (metis le_add1 less_2p_is_upper_bits_unset test_bit_bin)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma aligned_shift':
  "\<lbrakk>x < 2 ^ n; is_aligned (y :: 'a :: len word) n;n \<le> LENGTH('a)\<rbrakk>
   \<Longrightarrow> (y + x) >> n = y >> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ n; is_aligned y n; n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> y + x >> n = y >> n
[PROOF STEP]
apply (subst word_plus_and_or_coroll; rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>x < 2 ^ n; is_aligned y n; n \<le> LENGTH('a); na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (y AND x) na = bit 0 na
 2. \<And>na. \<lbrakk>x < 2 ^ n; is_aligned y n; n \<le> LENGTH('a); na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (y OR x >> n) na = bit (y >> n) na
[PROOF STEP]
apply (auto simp add: bit_simps is_aligned_nth)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>x < 2 ^ n; \<forall>na<n. \<not> bit y na; n \<le> LENGTH('a); na < LENGTH('a); bit y na; bit x na\<rbrakk> \<Longrightarrow> False
 2. \<And>na. \<lbrakk>x < 2 ^ n; \<forall>na<n. \<not> bit y na; n \<le> LENGTH('a); na < LENGTH('a); bit x (n + na)\<rbrakk> \<Longrightarrow> bit y (n + na)
[PROOF STEP]
apply (metis less_2p_is_upper_bits_unset not_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>x < 2 ^ n; \<forall>na<n. \<not> bit y na; n \<le> LENGTH('a); na < LENGTH('a); bit x (n + na)\<rbrakk> \<Longrightarrow> bit y (n + na)
[PROOF STEP]
apply (metis bit_imp_le_length le_add1 less_2p_is_upper_bits_unset)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma and_neg_mask_plus_mask_mono: "(p AND NOT (mask n)) + mask n \<ge> p"
  for p :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le> (p AND NOT (mask n)) + mask n
[PROOF STEP]
apply (rule word_le_minus_cancel[where x = "p AND NOT (mask n)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. p - (p AND NOT (mask n)) \<le> (p AND NOT (mask n)) + mask n - (p AND NOT (mask n))
 2. p AND NOT (mask n) \<le> (p AND NOT (mask n)) + mask n
[PROOF STEP]
apply (clarsimp simp: subtract_mask)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. p AND mask n \<le> mask n
 2. p AND NOT (mask n) \<le> (p AND NOT (mask n)) + mask n
[PROOF STEP]
using word_and_le1[where a = "mask n" and y = p]
[PROOF STATE]
proof (prove)
using this:
p AND mask n \<le> mask n

goal (2 subgoals):
 1. p AND mask n \<le> mask n
 2. p AND NOT (mask n) \<le> (p AND NOT (mask n)) + mask n
[PROOF STEP]
apply (clarsimp simp: mask_eq_decr_exp word_le_less_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p AND NOT (mask n) \<le> (p AND NOT (mask n)) + mask n
[PROOF STEP]
apply (rule is_aligned_no_overflow'[folded mask_2pm1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned (p AND NOT (mask n)) n
[PROOF STEP]
apply (clarsimp simp: is_aligned_neg_mask)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma word_neg_and_le:
  "ptr \<le> (ptr AND NOT (mask n)) + (2 ^ n - 1)"
  for ptr :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ptr \<le> (ptr AND NOT (mask n)) + (2 ^ n - 1)
[PROOF STEP]
by (simp add: and_neg_mask_plus_mask_mono mask_2pm1[symmetric])


[STATEMENT]
lemma is_aligned_sub_helper:
  "\<lbrakk> is_aligned (p - d) n; d < 2 ^ n \<rbrakk>
     \<Longrightarrow> (p AND mask n = d) \<and> (p AND (NOT (mask n)) = p - d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned (p - d) n; d < 2 ^ n\<rbrakk> \<Longrightarrow> p AND mask n = d \<and> p AND NOT (mask n) = p - d
[PROOF STEP]
by (drule(1) is_aligned_add_helper, simp)


[STATEMENT]
lemma is_aligned_after_mask:
  "\<lbrakk>is_aligned k m;m\<le> n\<rbrakk> \<Longrightarrow> is_aligned (k AND mask n) m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned k m; m \<le> n\<rbrakk> \<Longrightarrow> is_aligned (k AND mask n) m
[PROOF STEP]
by (rule is_aligned_andI1)


[STATEMENT]
lemma and_mask_plus:
  "\<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk>
   \<Longrightarrow> ptr + a AND mask n = (ptr AND mask n) + a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> ptr + a AND mask n = (ptr AND mask n) + a
[PROOF STEP]
apply (rule mask_eqI[where n = m])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND mask m = (ptr AND mask n) + a AND mask m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr AND mask n) + a AND NOT (mask m)
[PROOF STEP]
apply (simp add:mask_twice min_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> ptr + a AND mask m = (ptr AND mask n) + a AND mask m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr AND mask n) + a AND NOT (mask m)
[PROOF STEP]
apply (simp add:is_aligned_add_helper)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> a = (ptr AND mask n) + a AND mask m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr AND mask n) + a AND NOT (mask m)
[PROOF STEP]
apply (subst is_aligned_add_helper[THEN conjunct1])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> is_aligned (ptr AND mask n) m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> a < 2 ^ m
 3. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> a = a
 4. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr AND mask n) + a AND NOT (mask m)
[PROOF STEP]
apply (erule is_aligned_after_mask)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> m \<le> n
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> a < 2 ^ m
 3. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> a = a
 4. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr AND mask n) + a AND NOT (mask m)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> a < 2 ^ m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> a = a
 3. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr AND mask n) + a AND NOT (mask m)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> a = a
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr AND mask n) + a AND NOT (mask m)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr AND mask n) + a AND NOT (mask m)
[PROOF STEP]
apply (subgoal_tac "(ptr + a AND mask n) AND NOT (mask m)
     = (ptr + a AND NOT (mask m) ) AND mask n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m; (ptr + a AND mask n) AND NOT (mask m) = (ptr + a AND NOT (mask m)) AND mask n\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr AND mask n) + a AND NOT (mask m)
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr + a AND NOT (mask m)) AND mask n
[PROOF STEP]
apply (simp add:is_aligned_add_helper)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m; (ptr + a AND mask n) AND NOT (mask m) = ptr AND mask n\<rbrakk> \<Longrightarrow> ptr AND mask n = (ptr AND mask n) + a AND NOT (mask m)
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr + a AND NOT (mask m)) AND mask n
[PROOF STEP]
apply (subst is_aligned_add_helper[THEN conjunct2])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m; (ptr + a AND mask n) AND NOT (mask m) = ptr AND mask n\<rbrakk> \<Longrightarrow> is_aligned (ptr AND mask n) m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m; (ptr + a AND mask n) AND NOT (mask m) = ptr AND mask n\<rbrakk> \<Longrightarrow> a < 2 ^ m
 3. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m; (ptr + a AND mask n) AND NOT (mask m) = ptr AND mask n\<rbrakk> \<Longrightarrow> ptr AND mask n = ptr AND mask n
 4. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr + a AND NOT (mask m)) AND mask n
[PROOF STEP]
apply (simp add:is_aligned_after_mask)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m; (ptr + a AND mask n) AND NOT (mask m) = ptr AND mask n\<rbrakk> \<Longrightarrow> a < 2 ^ m
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m; (ptr + a AND mask n) AND NOT (mask m) = ptr AND mask n\<rbrakk> \<Longrightarrow> ptr AND mask n = ptr AND mask n
 3. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr + a AND NOT (mask m)) AND mask n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m; (ptr + a AND mask n) AND NOT (mask m) = ptr AND mask n\<rbrakk> \<Longrightarrow> ptr AND mask n = ptr AND mask n
 2. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr + a AND NOT (mask m)) AND mask n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr m; m \<le> n; a < 2 ^ m\<rbrakk> \<Longrightarrow> (ptr + a AND mask n) AND NOT (mask m) = (ptr + a AND NOT (mask m)) AND mask n
[PROOF STEP]
apply (simp add:word_bw_comms word_bw_lcs)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_aligned_add_not_aligned:
  "\<lbrakk>is_aligned (p::'a::len word) n; \<not> is_aligned (q::'a::len word) n\<rbrakk> \<Longrightarrow> \<not> is_aligned (p + q) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; \<not> is_aligned q n\<rbrakk> \<Longrightarrow> \<not> is_aligned (p + q) n
[PROOF STEP]
by (metis is_aligned_addD1)


[STATEMENT]
lemma neg_mask_add_aligned:
  "\<lbrakk> is_aligned p n; q < 2 ^ n \<rbrakk> \<Longrightarrow> (p + q) AND NOT (mask n) = p AND NOT (mask n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; q < 2 ^ n\<rbrakk> \<Longrightarrow> p + q AND NOT (mask n) = p AND NOT (mask n)
[PROOF STEP]
by (metis is_aligned_add_helper is_aligned_neg_mask_eq)


[STATEMENT]
lemma word_add_power_off:
  fixes a :: "'a :: len word"
  assumes ak: "a < k"
  and kw: "k < 2 ^ (LENGTH('a) - m)"
  and mw: "m < LENGTH('a)"
  and off: "off < 2 ^ m"
shows "(a * 2 ^ m) + off < k * 2 ^ m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * 2 ^ m + off < k * 2 ^ m
[PROOF STEP]
proof (cases "m = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. m = 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m
 2. m \<noteq> 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
m = 0

goal (2 subgoals):
 1. m = 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m
 2. m \<noteq> 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m = 0

goal (1 subgoal):
 1. a * 2 ^ m + off < k * 2 ^ m
[PROOF STEP]
using off ak
[PROOF STATE]
proof (prove)
using this:
m = 0
off < 2 ^ m
a < k

goal (1 subgoal):
 1. a * 2 ^ m + off < k * 2 ^ m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a * 2 ^ m + off < k * 2 ^ m

goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
m \<noteq> 0

goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m
[PROOF STEP]
from ak
[PROOF STATE]
proof (chain)
picking this:
a < k
[PROOF STEP]
have ak1: "a + 1 \<le> k"
[PROOF STATE]
proof (prove)
using this:
a < k

goal (1 subgoal):
 1. a + 1 \<le> k
[PROOF STEP]
by (rule inc_le)
[PROOF STATE]
proof (state)
this:
a + 1 \<le> k

goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a + 1 \<le> k
[PROOF STEP]
have "(a + 1) * 2 ^ m \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
a + 1 \<le> k

goal (1 subgoal):
 1. (a + 1) * 2 ^ m \<noteq> 0
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + 1 \<le> k \<Longrightarrow> (a + 1) * 2 ^ m \<noteq> 0
[PROOF STEP]
apply (rule word_power_nonzero)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a + 1 \<le> k \<Longrightarrow> a + 1 < 2 ^ (LENGTH('a) - m)
 2. a + 1 \<le> k \<Longrightarrow> m < LENGTH('a)
 3. a + 1 \<le> k \<Longrightarrow> a + 1 \<noteq> 0
[PROOF STEP]
apply (erule order_le_less_trans  [OF _ kw])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a + 1 \<le> k \<Longrightarrow> m < LENGTH('a)
 2. a + 1 \<le> k \<Longrightarrow> a + 1 \<noteq> 0
[PROOF STEP]
apply (rule mw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + 1 \<le> k \<Longrightarrow> a + 1 \<noteq> 0
[PROOF STEP]
apply (rule less_is_non_zero_p1 [OF ak])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(a + 1) * 2 ^ m \<noteq> 0

goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(a + 1) * 2 ^ m \<noteq> 0
[PROOF STEP]
have "(a * 2 ^ m) + off < ((a + 1) * 2 ^ m)"
[PROOF STATE]
proof (prove)
using this:
(a + 1) * 2 ^ m \<noteq> 0

goal (1 subgoal):
 1. a * 2 ^ m + off < (a + 1) * 2 ^ m
[PROOF STEP]
using kw mw
[PROOF STATE]
proof (prove)
using this:
(a + 1) * 2 ^ m \<noteq> 0
k < 2 ^ (LENGTH('a) - m)
m < LENGTH('a)

goal (1 subgoal):
 1. a * 2 ^ m + off < (a + 1) * 2 ^ m
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a + 1) * 2 ^ m \<noteq> 0; k < 2 ^ (LENGTH('a) - m); m < LENGTH('a)\<rbrakk> \<Longrightarrow> a * 2 ^ m + off < (a + 1) * 2 ^ m
[PROOF STEP]
apply (simp add: distrib_right)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a * 2 ^ m + 2 ^ m \<noteq> 0; k < 2 ^ (LENGTH('a) - m); m < LENGTH('a)\<rbrakk> \<Longrightarrow> a * 2 ^ m + off < a * 2 ^ m + 2 ^ m
[PROOF STEP]
apply (rule word_plus_strict_mono_right [OF off])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a * 2 ^ m + 2 ^ m \<noteq> 0; k < 2 ^ (LENGTH('a) - m); m < LENGTH('a)\<rbrakk> \<Longrightarrow> a * 2 ^ m \<le> a * 2 ^ m + 2 ^ m
[PROOF STEP]
apply (rule is_aligned_no_overflow'')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a * 2 ^ m + 2 ^ m \<noteq> 0; k < 2 ^ (LENGTH('a) - m); m < LENGTH('a)\<rbrakk> \<Longrightarrow> is_aligned (a * 2 ^ m) m
 2. \<lbrakk>a * 2 ^ m + 2 ^ m \<noteq> 0; k < 2 ^ (LENGTH('a) - m); m < LENGTH('a)\<rbrakk> \<Longrightarrow> a * 2 ^ m + 2 ^ m \<noteq> 0
[PROOF STEP]
apply (rule is_aligned_mult_triv2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a * 2 ^ m + 2 ^ m \<noteq> 0; k < 2 ^ (LENGTH('a) - m); m < LENGTH('a)\<rbrakk> \<Longrightarrow> a * 2 ^ m + 2 ^ m \<noteq> 0
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
a * 2 ^ m + off < (a + 1) * 2 ^ m

goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a * 2 ^ m + off < (a + 1) * 2 ^ m

goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m
[PROOF STEP]
have "\<dots> \<le> k * 2 ^ m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a + 1) * 2 ^ m \<le> k * 2 ^ m
[PROOF STEP]
using ak1 mw kw False
[PROOF STATE]
proof (prove)
using this:
a + 1 \<le> k
m < LENGTH('a)
k < 2 ^ (LENGTH('a) - m)
m \<noteq> 0

goal (1 subgoal):
 1. (a + 1) * 2 ^ m \<le> k * 2 ^ m
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a + 1 \<le> k; m < LENGTH('a); k < 2 ^ (LENGTH('a) - m); m \<noteq> 0\<rbrakk> \<Longrightarrow> (a + 1) * 2 ^ m \<le> k * 2 ^ m
[PROOF STEP]
apply (erule word_mult_le_mono1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m < LENGTH('a); k < 2 ^ (LENGTH('a) - m); m \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < 2 ^ m
 2. \<lbrakk>m < LENGTH('a); k < 2 ^ (LENGTH('a) - m); m \<noteq> 0\<rbrakk> \<Longrightarrow> unat k * unat (2 ^ m) < 2 ^ LENGTH('a)
[PROOF STEP]
apply (simp add: p2_gt_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m < LENGTH('a); k < 2 ^ (LENGTH('a) - m); m \<noteq> 0\<rbrakk> \<Longrightarrow> unat k * unat (2 ^ m) < 2 ^ LENGTH('a)
[PROOF STEP]
apply (simp add: word_less_nat_alt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m < LENGTH('a); unat k < 2 ^ (LENGTH('a) - m); 0 < m\<rbrakk> \<Longrightarrow> unat k * 2 ^ m < 2 ^ LENGTH('a)
[PROOF STEP]
apply (meson nat_mult_power_less_eq zero_less_numeral)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(a + 1) * 2 ^ m \<le> k * 2 ^ m

goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> a * 2 ^ m + off < k * 2 ^ m
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
a * 2 ^ m + off < k * 2 ^ m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a * 2 ^ m + off < k * 2 ^ m

goal (1 subgoal):
 1. a * 2 ^ m + off < k * 2 ^ m
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
a * 2 ^ m + off < k * 2 ^ m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma offset_not_aligned:
  "\<lbrakk> is_aligned (p::'a::len word) n; i > 0; i < 2 ^ n; n < LENGTH('a)\<rbrakk> \<Longrightarrow>
   \<not> is_aligned (p + of_nat i) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; 0 < i; i < 2 ^ n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> \<not> is_aligned (p + word_of_nat i) n
[PROOF STEP]
apply (erule is_aligned_add_not_aligned)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < i; i < 2 ^ n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> \<not> is_aligned (word_of_nat i) n
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i n. \<lbrakk>0 < i; i < 2 ^ n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> \<not> 2 ^ n dvd take_bit LENGTH('a) (int i)
[PROOF STEP]
apply (auto simp add: is_aligned_iff_udvd)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i n. \<lbrakk>0 < i; i < 2 ^ n; n < LENGTH('a); 2 ^ n dvd take_bit LENGTH('a) (int i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis (no_types, lifting) le_less_trans less_not_refl2 less_or_eq_imp_le of_nat_eq_0_iff take_bit_eq_0_iff take_bit_nat_eq_self_iff take_bit_of_nat unat_lt2p unat_power_lower)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma le_or_mask:
  "w \<le> w' \<Longrightarrow> w OR mask x \<le> w' OR mask x"
  for w w' :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<le> w' \<Longrightarrow> w OR mask x \<le> w' OR mask x
[PROOF STEP]
by (metis neg_mask_add_mask add.commute le_word_or1 mask_2pm1 neg_mask_mono_le word_plus_mono_left)


[STATEMENT]
lemma delt_out_of_range:
  assumes "x < mi \<or> x > ma" and "deg \<ge> 2"
  shows
  "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =(Node (Some (mi, ma)) deg treeList summary)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = Node (Some (mi, ma)) deg treeList summary
[PROOF STEP]
using vebt_delete.simps(7)[of mi ma "deg-2" treeList summary x]
[PROOF STATE]
proof (prove)
using this:
vebt_delete (Node (Some (mi, ma)) (Suc (Suc (deg - 2))) treeList summary) x = (if x < mi \<or> ma < x then Node (Some (mi, ma)) (Suc (Suc (deg - 2))) treeList summary else if x = mi \<and> x = ma then Node None (Suc (Suc (deg - 2))) treeList summary else let xn = if x = mi then the (vebt_mint summary) * 2 ^ (Suc (Suc (deg - 2)) div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x; minn = if x = mi then xn else mi; l = low xn (Suc (Suc (deg - 2)) div 2); h = high xn (Suc (Suc (deg - 2)) div 2) in if h < length treeList then let newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode] in if minNull newnode then let sn = vebt_delete summary h in Node (Some (minn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then minn else 2 ^ (Suc (Suc (deg - 2)) div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) (Suc (Suc (deg - 2))) newlist sn else Node (Some (minn, if xn = ma then h * 2 ^ (Suc (Suc (deg - 2)) div 2) + the (vebt_maxt (newlist ! h)) else ma)) (Suc (Suc (deg - 2))) newlist summary else Node (Some (mi, ma)) (Suc (Suc (deg - 2))) treeList summary)

goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = Node (Some (mi, ma)) deg treeList summary
[PROOF STEP]
by (metis add_2_eq_Suc assms(1) assms(2) le_add_diff_inverse)


[STATEMENT]
lemma del_single_cont:
  assumes "x = mi \<and> x = ma" and "deg \<ge> 2"
  shows  "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (Node None deg treeList summary)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = Node None deg treeList summary
[PROOF STEP]
using vebt_delete.simps(7)[of mi ma "deg-2" treeList summary x]
[PROOF STATE]
proof (prove)
using this:
vebt_delete (Node (Some (mi, ma)) (Suc (Suc (deg - 2))) treeList summary) x = (if x < mi \<or> ma < x then Node (Some (mi, ma)) (Suc (Suc (deg - 2))) treeList summary else if x = mi \<and> x = ma then Node None (Suc (Suc (deg - 2))) treeList summary else let xn = if x = mi then the (vebt_mint summary) * 2 ^ (Suc (Suc (deg - 2)) div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x; minn = if x = mi then xn else mi; l = low xn (Suc (Suc (deg - 2)) div 2); h = high xn (Suc (Suc (deg - 2)) div 2) in if h < length treeList then let newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode] in if minNull newnode then let sn = vebt_delete summary h in Node (Some (minn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then minn else 2 ^ (Suc (Suc (deg - 2)) div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) (Suc (Suc (deg - 2))) newlist sn else Node (Some (minn, if xn = ma then h * 2 ^ (Suc (Suc (deg - 2)) div 2) + the (vebt_maxt (newlist ! h)) else ma)) (Suc (Suc (deg - 2))) newlist summary else Node (Some (mi, ma)) (Suc (Suc (deg - 2))) treeList summary)

goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = Node None deg treeList summary
[PROOF STEP]
by (metis add_2_eq_Suc assms(1) assms(2) le_add_diff_inverse nat_less_le)


[STATEMENT]
lemma del_in_range:
  assumes "x \<ge> mi \<and> x \<le> ma" and "mi \<noteq> ma" and "deg \<ge> 2"
  shows
  " vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = ( let xn = (if x = mi
                             then the (vebt_mint summary) * 2^(deg div 2)
                                      + the (vebt_mint (treeList ! the (vebt_mint summary)))
                             else x);
                   minn = (if x = mi then xn else mi);
                   l = low xn (deg div 2);
                   h = high xn (deg div 2) in
                    if h < length treeList
                       then(
                          let newnode = vebt_delete (treeList ! h) l;
                              newlist = treeList[h:= newnode] in
                             if minNull newnode
                             then(
                                let sn = vebt_delete summary h in
                               (Node (Some (minn, if xn  = ma then (let maxs = vebt_maxt sn in
                                                                      (if maxs = None
                                                                         then minn
                                                                         else 2^(deg div 2) * the maxs
                                                                               + the (vebt_maxt (newlist ! the maxs))
                                                                       )
                                                                   )
                                                              else ma))
                                      deg newlist sn)
                             )else
                               (Node (Some (minn, (if xn = ma then
                                                    h * 2^(deg div 2) + the( vebt_maxt (newlist ! h))
                                                            else ma)))
                                 deg newlist summary )
                       )else
                        (Node (Some (mi, ma)) deg treeList summary))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (let xn = if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x; minn = if x = mi then xn else mi; l = low xn (deg div 2); h = high xn (deg div 2) in if h < length treeList then let newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode] in if minNull newnode then let sn = vebt_delete summary h in Node (Some (minn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then minn else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (minn, if xn = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary else Node (Some (mi, ma)) deg treeList summary)
[PROOF STEP]
using vebt_delete.simps(7)[of mi ma "deg-2" treeList summary x]
[PROOF STATE]
proof (prove)
using this:
vebt_delete (Node (Some (mi, ma)) (Suc (Suc (deg - 2))) treeList summary) x = (if x < mi \<or> ma < x then Node (Some (mi, ma)) (Suc (Suc (deg - 2))) treeList summary else if x = mi \<and> x = ma then Node None (Suc (Suc (deg - 2))) treeList summary else let xn = if x = mi then the (vebt_mint summary) * 2 ^ (Suc (Suc (deg - 2)) div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x; minn = if x = mi then xn else mi; l = low xn (Suc (Suc (deg - 2)) div 2); h = high xn (Suc (Suc (deg - 2)) div 2) in if h < length treeList then let newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode] in if minNull newnode then let sn = vebt_delete summary h in Node (Some (minn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then minn else 2 ^ (Suc (Suc (deg - 2)) div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) (Suc (Suc (deg - 2))) newlist sn else Node (Some (minn, if xn = ma then h * 2 ^ (Suc (Suc (deg - 2)) div 2) + the (vebt_maxt (newlist ! h)) else ma)) (Suc (Suc (deg - 2))) newlist summary else Node (Some (mi, ma)) (Suc (Suc (deg - 2))) treeList summary)

goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (let xn = if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x; minn = if x = mi then xn else mi; l = low xn (deg div 2); h = high xn (deg div 2) in if h < length treeList then let newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode] in if minNull newnode then let sn = vebt_delete summary h in Node (Some (minn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then minn else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (minn, if xn = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary else Node (Some (mi, ma)) deg treeList summary)
[PROOF STEP]
by (smt (z3) add_2_eq_Suc assms(1) assms(2) assms(3) leD le_add_diff_inverse)


[STATEMENT]
lemma del_x_not_mia:
  assumes "x > mi \<and> x \<le> ma" and "mi \<noteq> ma"  and "deg \<ge> 2"  and "high x (deg div 2) = h" and
  "low x (deg div 2) = l"and  "high x (deg div 2) < length treeList"
  shows
  " vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (
                  let  newnode = vebt_delete (treeList ! h) l;
                              newlist = treeList[h:= newnode] in
                             if minNull newnode
                             then(
                                let sn = vebt_delete summary h in
                               (Node (Some (mi, if x  = ma then (let maxs = vebt_maxt sn in
                                                                      (if maxs = None
                                                                         then mi
                                                                         else 2^(deg div 2) * the maxs
                                                                               + the (vebt_maxt (newlist ! the maxs))
                                                                       )
                                                                   )
                                                              else ma))
                                      deg newlist sn)
                             )else
                               (Node (Some (mi, (if x = ma then
                                                    h * 2^(deg div 2) + the( vebt_maxt (newlist ! h))
                                                            else ma)))
                                 deg newlist summary )
)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (let newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode] in if minNull newnode then let sn = vebt_delete summary h in Node (Some (mi, if x = ma then let maxs = vebt_maxt sn in if maxs = None then mi else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (mi, if x = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary)
[PROOF STEP]
using del_in_range[of mi x ma deg treeList summary]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mi \<le> x \<and> x \<le> ma; mi \<noteq> ma; 2 \<le> deg\<rbrakk> \<Longrightarrow> vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (let xn = if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x; minn = if x = mi then xn else mi; l = low xn (deg div 2); h = high xn (deg div 2) in if h < length treeList then let newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode] in if minNull newnode then let sn = vebt_delete summary h in Node (Some (minn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then minn else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (minn, if xn = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary else Node (Some (mi, ma)) deg treeList summary)

goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (let newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode] in if minNull newnode then let sn = vebt_delete summary h in Node (Some (mi, if x = ma then let maxs = vebt_maxt sn in if maxs = None then mi else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (mi, if x = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary)
[PROOF STEP]
unfolding Let_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mi \<le> x \<and> x \<le> ma; mi \<noteq> ma; 2 \<le> deg\<rbrakk> \<Longrightarrow> vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (if high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2) < length treeList then if minNull (vebt_delete (treeList ! high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2)) (low (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2))) then Node (Some (if x = mi then if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x else mi, if (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) = ma then if vebt_maxt (vebt_delete summary (high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2))) = None then if x = mi then if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x else mi else 2 ^ (deg div 2) * the (vebt_maxt (vebt_delete summary (high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2)))) + the (vebt_maxt (treeList[high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2) := vebt_delete (treeList ! high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2)) (low (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2))] ! the (vebt_maxt (vebt_delete summary (high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2)))))) else ma)) deg (treeList[high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2) := vebt_delete (treeList ! high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2)) (low (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2))]) (vebt_delete summary (high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2))) else Node (Some (if x = mi then if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x else mi, if (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) = ma then high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2) * 2 ^ (deg div 2) + the (vebt_maxt (treeList[high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2) := vebt_delete (treeList ! high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2)) (low (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2))] ! high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2))) else ma)) deg (treeList[high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2) := vebt_delete (treeList ! high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2)) (low (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2))]) summary else Node (Some (mi, ma)) deg treeList summary)

goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (if minNull (vebt_delete (treeList ! h) l) then Node (Some (mi, if x = ma then if vebt_maxt (vebt_delete summary h) = None then mi else 2 ^ (deg div 2) * the (vebt_maxt (vebt_delete summary h)) + the (vebt_maxt (treeList[h := vebt_delete (treeList ! h) l] ! the (vebt_maxt (vebt_delete summary h)))) else ma)) deg (treeList[h := vebt_delete (treeList ! h) l]) (vebt_delete summary h) else Node (Some (mi, if x = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (treeList[h := vebt_delete (treeList ! h) l] ! h)) else ma)) deg (treeList[h := vebt_delete (treeList ! h) l]) summary)
[PROOF STEP]
using assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) nat_less_le
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mi \<le> x \<and> x \<le> ma; mi \<noteq> ma; 2 \<le> deg\<rbrakk> \<Longrightarrow> vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (if high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2) < length treeList then if minNull (vebt_delete (treeList ! high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2)) (low (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2))) then Node (Some (if x = mi then if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x else mi, if (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) = ma then if vebt_maxt (vebt_delete summary (high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2))) = None then if x = mi then if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x else mi else 2 ^ (deg div 2) * the (vebt_maxt (vebt_delete summary (high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2)))) + the (vebt_maxt (treeList[high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2) := vebt_delete (treeList ! high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2)) (low (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2))] ! the (vebt_maxt (vebt_delete summary (high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2)))))) else ma)) deg (treeList[high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2) := vebt_delete (treeList ! high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2)) (low (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2))]) (vebt_delete summary (high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2))) else Node (Some (if x = mi then if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x else mi, if (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) = ma then high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2) * 2 ^ (deg div 2) + the (vebt_maxt (treeList[high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2) := vebt_delete (treeList ! high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2)) (low (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2))] ! high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2))) else ma)) deg (treeList[high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2) := vebt_delete (treeList ! high (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2)) (low (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x) (deg div 2))]) summary else Node (Some (mi, ma)) deg treeList summary)
mi < x \<and> x \<le> ma
mi \<noteq> ma
2 \<le> deg
high x (deg div 2) = h
low x (deg div 2) = l
high x (deg div 2) < length treeList
(?m < ?n) = (?m \<le> ?n \<and> ?m \<noteq> ?n)

goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (if minNull (vebt_delete (treeList ! h) l) then Node (Some (mi, if x = ma then if vebt_maxt (vebt_delete summary h) = None then mi else 2 ^ (deg div 2) * the (vebt_maxt (vebt_delete summary h)) + the (vebt_maxt (treeList[h := vebt_delete (treeList ! h) l] ! the (vebt_maxt (vebt_delete summary h)))) else ma)) deg (treeList[h := vebt_delete (treeList ! h) l]) (vebt_delete summary h) else Node (Some (mi, if x = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (treeList[h := vebt_delete (treeList ! h) l] ! h)) else ma)) deg (treeList[h := vebt_delete (treeList ! h) l]) summary)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma del_x_not_mi:
  assumes "x > mi \<and> x \<le> ma" and "mi \<noteq> ma"  and "deg \<ge> 2"  and "high x (deg div 2) = h" and
  "low x (deg div 2) = l"and " newnode = vebt_delete (treeList ! h) l"
  and "newlist = treeList[h:= newnode]" and "high x (deg div 2) < length treeList"
  shows
  " vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (
                  if minNull newnode
                             then(
                                let sn = vebt_delete summary h in
                               (Node (Some (mi, if x  = ma then (let maxs = vebt_maxt sn in
                                                                      (if maxs = None
                                                                         then mi
                                                                         else 2^(deg div 2) * the maxs
                                                                               + the (vebt_maxt (newlist ! the maxs))
                                                                       )
                                                                   )
                                                              else ma))
                                      deg newlist sn)
                             )else
                               (Node (Some (mi, (if x = ma then
                                                    h * 2^(deg div 2) + the( vebt_maxt (newlist ! h))
                                                            else ma)))
                                 deg newlist summary )
)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (if minNull newnode then let sn = vebt_delete summary h in Node (Some (mi, if x = ma then let maxs = vebt_maxt sn in if maxs = None then mi else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (mi, if x = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary)
[PROOF STEP]
using del_x_not_mia[of mi x ma deg h l treeList summary]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mi < x \<and> x \<le> ma; mi \<noteq> ma; 2 \<le> deg; high x (deg div 2) = h; low x (deg div 2) = l; high x (deg div 2) < length treeList\<rbrakk> \<Longrightarrow> vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (let newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode] in if minNull newnode then let sn = vebt_delete summary h in Node (Some (mi, if x = ma then let maxs = vebt_maxt sn in if maxs = None then mi else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (mi, if x = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary)

goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (if minNull newnode then let sn = vebt_delete summary h in Node (Some (mi, if x = ma then let maxs = vebt_maxt sn in if maxs = None then mi else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (mi, if x = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary)
[PROOF STEP]
by (smt (z3) assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) assms(7) assms(8))


[STATEMENT]
lemma del_x_not_mi_new_node_nil:
  assumes "x > mi \<and> x \<le> ma" and "mi \<noteq> ma"  and "deg \<ge> 2"  and "high x (deg div 2) = h" and
    "low x (deg div 2) = l"and " newnode = vebt_delete (treeList ! h) l" and "minNull newnode " and
    "sn = vebt_delete summary h"  and "newlist =treeList[h:= newnode]" and  "high x (deg div 2) < length treeList"
  shows
  " vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =  (Node (Some (mi, if x  = ma then (let maxs = vebt_maxt sn in
                                                                      (if maxs = None
                                                                         then mi
                                                                         else 2^(deg div 2) * the maxs
                                                                               + the (vebt_maxt (newlist ! the maxs))
                                                                       )
                                                                   )
                                                              else ma))  deg newlist sn)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = Node (Some (mi, if x = ma then let maxs = vebt_maxt sn in if maxs = None then mi else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn
[PROOF STEP]
using del_x_not_mi[of mi x ma deg h l newnode treeList]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mi < x \<and> x \<le> ma; mi \<noteq> ma; 2 \<le> deg; high x (deg div 2) = h; low x (deg div 2) = l; newnode = vebt_delete (treeList ! h) l; ?newlist = treeList[h := newnode]; high x (deg div 2) < length treeList\<rbrakk> \<Longrightarrow> vebt_delete (Node (Some (mi, ma)) deg treeList ?summary) x = (if minNull newnode then let sn = vebt_delete ?summary h in Node (Some (mi, if x = ma then let maxs = vebt_maxt sn in if maxs = None then mi else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (?newlist ! the maxs)) else ma)) deg ?newlist sn else Node (Some (mi, if x = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (?newlist ! h)) else ma)) deg ?newlist ?summary)

goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = Node (Some (mi, if x = ma then let maxs = vebt_maxt sn in if maxs = None then mi else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn
[PROOF STEP]
by (metis assms(1) assms(10) assms(2) assms(3) assms(4) assms(5) assms(6) assms(7) assms(8) assms(9))


[STATEMENT]
lemma del_x_not_mi_newnode_not_nil:
  assumes "x > mi \<and> x \<le> ma" and "mi \<noteq> ma"  and "deg \<ge> 2"  and "high x (deg div 2) = h" and
    "low x (deg div 2) = l"and " newnode = vebt_delete (treeList ! h) l" and "\<not>  minNull newnode " and
     "newlist = treeList[h:= newnode]" and"high x (deg div 2) < length treeList"
  shows
  " vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =
                               (Node (Some (mi, (if x = ma then
                                                    h * 2^(deg div 2) + the( vebt_maxt (newlist ! h))
                                                            else ma)))
                                 deg newlist summary )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = Node (Some (mi, if x = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary
[PROOF STEP]
using del_x_not_mi[of mi x ma deg h l newnode treeList newlist summary]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mi < x \<and> x \<le> ma; mi \<noteq> ma; 2 \<le> deg; high x (deg div 2) = h; low x (deg div 2) = l; newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode]; high x (deg div 2) < length treeList\<rbrakk> \<Longrightarrow> vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (if minNull newnode then let sn = vebt_delete summary h in Node (Some (mi, if x = ma then let maxs = vebt_maxt sn in if maxs = None then mi else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (mi, if x = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary)

goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = Node (Some (mi, if x = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary
[PROOF STEP]
using assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) assms(7) assms(8) assms(9)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mi < x \<and> x \<le> ma; mi \<noteq> ma; 2 \<le> deg; high x (deg div 2) = h; low x (deg div 2) = l; newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode]; high x (deg div 2) < length treeList\<rbrakk> \<Longrightarrow> vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (if minNull newnode then let sn = vebt_delete summary h in Node (Some (mi, if x = ma then let maxs = vebt_maxt sn in if maxs = None then mi else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (mi, if x = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary)
mi < x \<and> x \<le> ma
mi \<noteq> ma
2 \<le> deg
high x (deg div 2) = h
low x (deg div 2) = l
newnode = vebt_delete (treeList ! h) l
\<not> minNull newnode
newlist = treeList[h := newnode]
high x (deg div 2) < length treeList

goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = Node (Some (mi, if x = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary
[PROOF STEP]
by auto


[STATEMENT]
lemma del_x_mia: assumes "x = mi \<and> x < ma" and "mi \<noteq> ma"  and "deg \<ge> 2"
  shows "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =(
              let xn = the (vebt_mint summary) * 2^(deg div 2)
                                      + the (vebt_mint (treeList ! the (vebt_mint summary)));
                                             minn = xn;
                   l = low xn (deg div 2);
                   h = high xn (deg div 2) in
                    if h < length treeList
                       then(
                          let newnode = vebt_delete (treeList ! h) l;
                              newlist = treeList[h:= newnode]in
                             if minNull newnode
                             then(
                                let sn = vebt_delete summary h in
                               (Node (Some (minn, if xn  = ma then (let maxs = vebt_maxt sn in
                                                                      (if maxs = None
                                                                         then minn
                                                                         else 2^(deg div 2) * the maxs
                                                                               + the (vebt_maxt (newlist ! the maxs))
                                                                       )
                                                                   )
                                                              else ma))
                                      deg newlist sn)
                             )else
                               (Node (Some (minn, (if xn = ma then
                                                    h * 2^(deg div 2) + the( vebt_maxt (newlist ! h))
                                                            else ma)))
                                 deg newlist summary )
                       )else
                        (Node (Some (mi, ma)) deg treeList summary)
           )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (let xn = the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))); minn = xn; l = low xn (deg div 2); h = high xn (deg div 2) in if h < length treeList then let newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode] in if minNull newnode then let sn = vebt_delete summary h in Node (Some (minn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then minn else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (minn, if xn = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary else Node (Some (mi, ma)) deg treeList summary)
[PROOF STEP]
using del_in_range[of mi x ma deg treeList summary]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mi \<le> x \<and> x \<le> ma; mi \<noteq> ma; 2 \<le> deg\<rbrakk> \<Longrightarrow> vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (let xn = if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x; minn = if x = mi then xn else mi; l = low xn (deg div 2); h = high xn (deg div 2) in if h < length treeList then let newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode] in if minNull newnode then let sn = vebt_delete summary h in Node (Some (minn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then minn else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (minn, if xn = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary else Node (Some (mi, ma)) deg treeList summary)

goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (let xn = the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))); minn = xn; l = low xn (deg div 2); h = high xn (deg div 2) in if h < length treeList then let newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode] in if minNull newnode then let sn = vebt_delete summary h in Node (Some (minn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then minn else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (minn, if xn = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary else Node (Some (mi, ma)) deg treeList summary)
[PROOF STEP]
using assms(1) assms(3) nat_less_le order_refl
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>mi \<le> x \<and> x \<le> ma; mi \<noteq> ma; 2 \<le> deg\<rbrakk> \<Longrightarrow> vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (let xn = if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x; minn = if x = mi then xn else mi; l = low xn (deg div 2); h = high xn (deg div 2) in if h < length treeList then let newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode] in if minNull newnode then let sn = vebt_delete summary h in Node (Some (minn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then minn else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (minn, if xn = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary else Node (Some (mi, ma)) deg treeList summary)
x = mi \<and> x < ma
2 \<le> deg
(?m < ?n) = (?m \<le> ?n \<and> ?m \<noteq> ?n)
?x \<le> ?x

goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (let xn = the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))); minn = xn; l = low xn (deg div 2); h = high xn (deg div 2) in if h < length treeList then let newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode] in if minNull newnode then let sn = vebt_delete summary h in Node (Some (minn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then minn else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (minn, if xn = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary else Node (Some (mi, ma)) deg treeList summary)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma del_x_mi:
  assumes "x = mi \<and> x < ma" and "mi \<noteq> ma"  and "deg \<ge> 2"  and "high xn (deg div 2) = h" and
    "xn =  the (vebt_mint summary) * 2^(deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) "
    "low xn (deg div 2) = l"and  "high xn (deg div 2) < length treeList"
  shows
  "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =(
                          let newnode = vebt_delete (treeList ! h) l;
                              newlist = treeList[h:= newnode]in
                             if minNull newnode
                             then(
                                let sn = vebt_delete summary h in
                               (Node (Some (xn, if xn  = ma then (let maxs = vebt_maxt sn in
                                                                      (if maxs = None
                                                                         then xn
                                                                         else 2^(deg div 2) * the maxs
                                                                               + the (vebt_maxt (newlist ! the maxs))
                                                                       )
                                                                   )
                                                              else ma))
                                      deg newlist sn)
                             )else
                               (Node (Some (xn, (if xn = ma then
                                                    h * 2^(deg div 2) + the( vebt_maxt (newlist ! h))
                                                            else ma)))
                                 deg newlist summary ))
          "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (let newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode] in if minNull newnode then let sn = vebt_delete summary h in Node (Some (xn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then xn else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (xn, if xn = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary)
[PROOF STEP]
using del_x_mia[of x mi ma deg treeList summary]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = mi \<and> x < ma; mi \<noteq> ma; 2 \<le> deg\<rbrakk> \<Longrightarrow> vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (let xn = the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))); minn = xn; l = low xn (deg div 2); h = high xn (deg div 2) in if h < length treeList then let newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode] in if minNull newnode then let sn = vebt_delete summary h in Node (Some (minn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then minn else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (minn, if xn = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary else Node (Some (mi, ma)) deg treeList summary)

goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (let newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode] in if minNull newnode then let sn = vebt_delete summary h in Node (Some (xn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then xn else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (xn, if xn = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary)
[PROOF STEP]
by (smt (z3) assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) assms(7))


[STATEMENT]
lemma del_x_mi_lets_in:
  assumes "x = mi \<and> x < ma" and "mi \<noteq> ma"  and "deg \<ge> 2"  and "high xn (deg div 2) = h" and
    "xn =  the (vebt_mint summary) * 2^(deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) "
    "low xn (deg div 2) = l"and  "high xn (deg div 2) < length treeList" and
    " newnode = vebt_delete (treeList ! h) l" and " newlist = treeList[h:= newnode]"
  shows  "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =(      if minNull newnode
                             then(
                                let sn = vebt_delete summary h in
                               (Node (Some (xn, if xn  = ma then (let maxs = vebt_maxt sn in
                                                                      (if maxs = None
                                                                         then xn
                                                                         else 2^(deg div 2) * the maxs
                                                                               + the (vebt_maxt (newlist ! the maxs))
                                                                       )
                                                                   )
                                                              else ma))
                                      deg newlist sn)
                             )else
                               (Node (Some (xn, (if xn = ma then
                                                    h * 2^(deg div 2) + the( vebt_maxt (newlist ! h))
                                                            else ma)))
                                 deg newlist summary ))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (if minNull newnode then let sn = vebt_delete summary h in Node (Some (xn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then xn else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (xn, if xn = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary)
[PROOF STEP]
using del_x_mi[of x mi ma deg xn h summary treeList l]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = mi \<and> x < ma; mi \<noteq> ma; 2 \<le> deg; high xn (deg div 2) = h; xn = the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))); low xn (deg div 2) = l; high xn (deg div 2) < length treeList\<rbrakk> \<Longrightarrow> vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (let newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode] in if minNull newnode then let sn = vebt_delete summary h in Node (Some (xn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then xn else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (xn, if xn = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary)

goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (if minNull newnode then let sn = vebt_delete summary h in Node (Some (xn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then xn else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (xn, if xn = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary)
[PROOF STEP]
by (smt (z3) assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) assms(7) assms(8) assms(9))


[STATEMENT]
lemma del_x_mi_lets_in_minNull:
  assumes "x = mi \<and> x < ma" and "mi \<noteq> ma"  and "deg \<ge> 2"  and "high xn (deg div 2) = h" and
    "xn =  the (vebt_mint summary) * 2^(deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) "
    "low xn (deg div 2) = l"and  "high xn (deg div 2) < length treeList" and
    "newnode = vebt_delete (treeList ! h) l" and " newlist =treeList[h:= newnode]" and
    "minNull newnode " and " sn = vebt_delete summary h"
  shows
  "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =
                               (Node (Some (xn, if xn  = ma then (let maxs = vebt_maxt sn in
                                                                      (if maxs = None
                                                                         then xn
                                                                         else 2^(deg div 2) * the maxs
                                                                               + the (vebt_maxt (newlist ! the maxs))
                                                                       )
                                                                   )
                                                              else ma))   deg newlist sn)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = Node (Some (xn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then xn else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn
[PROOF STEP]
using del_x_mi_lets_in[of x mi ma deg xn h summary treeList l newnode newlist]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = mi \<and> x < ma; mi \<noteq> ma; 2 \<le> deg; high xn (deg div 2) = h; xn = the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))); low xn (deg div 2) = l; high xn (deg div 2) < length treeList; newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode]\<rbrakk> \<Longrightarrow> vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (if minNull newnode then let sn = vebt_delete summary h in Node (Some (xn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then xn else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (xn, if xn = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary)

goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = Node (Some (xn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then xn else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn
[PROOF STEP]
by (metis assms(1) assms(10) assms(11) assms(2) assms(3) assms(4) assms(5) assms(6) assms(7) assms(8) assms(9))


[STATEMENT]
lemma del_x_mi_lets_in_not_minNull:
  assumes "x = mi \<and> x < ma" and "mi \<noteq> ma"  and "deg \<ge> 2"  and "high xn (deg div 2) = h" and
    "xn =  the (vebt_mint summary) * 2^(deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) "
    "low xn (deg div 2) = l"and  "high xn (deg div 2) < length treeList" and
    " newnode = vebt_delete (treeList ! h) l" and " newlist = treeList[h:= newnode]" and
    "\<not>minNull newnode "
  shows
  "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =
                               (Node (Some (xn, (if xn = ma then
                                                    h * 2^(deg div 2) + the( vebt_maxt (newlist ! h))
                                                            else ma)))
                                 deg newlist summary )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = Node (Some (xn, if xn = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary
[PROOF STEP]
using del_x_mi_lets_in[of x mi ma deg xn h summary treeList l newnode newlist]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = mi \<and> x < ma; mi \<noteq> ma; 2 \<le> deg; high xn (deg div 2) = h; xn = the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))); low xn (deg div 2) = l; high xn (deg div 2) < length treeList; newnode = vebt_delete (treeList ! h) l; newlist = treeList[h := newnode]\<rbrakk> \<Longrightarrow> vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (if minNull newnode then let sn = vebt_delete summary h in Node (Some (xn, if xn = ma then let maxs = vebt_maxt sn in if maxs = None then xn else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (newlist ! the maxs)) else ma)) deg newlist sn else Node (Some (xn, if xn = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary)

goal (1 subgoal):
 1. vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = Node (Some (xn, if xn = ma then h * 2 ^ (deg div 2) + the (vebt_maxt (newlist ! h)) else ma)) deg newlist summary
[PROOF STEP]
by (meson assms(1) assms(10) assms(2) assms(3) assms(4) assms(5) assms(6) assms(7) assms(8) assms(9))