theory Aligned

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 - 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 - fix m :: nat and  s assume m: "m < 2 ^ (LENGTH('a) - s)" and s: "s < LENGTH('a)" then have "unat ((of_nat m) :: 'a word) = m" apply (subst unat_of_nat) apply (subst mod_less) apply (erule order_less_le_trans) apply (rule power_increasing) apply simp_all done then show "?thesis m s" using s m apply (subst iffD1 [OF unat_mult_lem]) apply (simp add: nat_less_power_trans)+ done qed have s1wb: "s1 < LENGTH('a)" using s2wb s1s2 by simp from alm obtain mq where mmq: "m = 2 ^ s1 * of_nat mq" and mq: "mq < 2 ^ (LENGTH('a) - s1)" by (auto elim: is_alignedE simp: field_simps) from aln obtain nq where nnq: "n = 2 ^ s2 * of_nat nq" and nq: "nq < 2 ^ (LENGTH('a) - s2)" by (auto elim: is_alignedE simp: field_simps) from s1s2 obtain sq where sq: "s2 = s1 + sq" by (auto simp: le_iff_add) note us1 = rl [OF mq s1wb] note us2 = rl [OF nq s2wb] from nm have "n \<le> m" by clarsimp then have "(2::'a word) ^ s2 * of_nat nq \<le> 2 ^ s1 * of_nat mq" using nnq mmq by simp then have "2 ^ s2 * nq \<le> 2 ^ s1 * mq" using s1wb s2wb by (simp add: word_le_nat_alt us1 us2) then have nqmq: "2 ^ sq * nq \<le> mq" using sq by (simp add: power_add) have "m - n = 2 ^ s1 * of_nat mq - 2 ^ s2 * of_nat nq" using mmq nnq by simp also have "\<dots> = 2 ^ s1 * of_nat mq - 2 ^ s1 * 2 ^ sq * of_nat nq" using sq by (simp add: power_add) also have "\<dots> = 2 ^ s1 * (of_nat mq - 2 ^ sq * of_nat nq)" by (simp add: field_simps) also have "\<dots> = 2 ^ s1 * of_nat (mq - 2 ^ sq * nq)" using s1wb s2wb us1 us2 nqmq by (simp add: of_nat_diff) finally have mn: "m - n = of_nat (mq - 2 ^ sq * nq) * 2 ^ s1" by simp moreover from nm have "m - n \<le> 2 ^ s2 - 1" by - (rule word_diff_ls', (simp add: field_simps)+) then have "(2::'a word) ^ s1 * of_nat (mq - 2 ^ sq * nq) < 2 ^ s2" using mn s2wb by (simp add: field_simps) then have "of_nat (mq - 2 ^ sq * nq) < (2::'a word) ^ (s2 - s1)" proof (rule word_power_less_diff) have mm: "mq - 2 ^ sq * nq < 2 ^ (LENGTH('a) - s1)" using mq by simp moreover from s10 have "LENGTH('a) - s1 < LENGTH('a)" by (rule diff_less, simp) ultimately show "of_nat (mq - 2 ^ sq * nq) < (2::'a word) ^ (LENGTH('a) - s1)" using take_bit_nat_less_self_iff [of \<open>LENGTH('a)\<close> \<open>mq - 2 ^ sq * nq\<close>] apply (auto simp add: word_less_nat_alt not_le not_less unsigned_of_nat) apply (metis take_bit_nat_eq_self_iff) done qed then have "mq - 2 ^ sq * nq < 2 ^ (s2 - s1)" using mq s2wb apply (simp add: word_less_nat_alt take_bit_eq_mod unsigned_of_nat) apply (subst (asm) mod_less) apply auto apply (rule order_le_less_trans) apply (rule diff_le_self) apply (erule order_less_le_trans) apply simp done ultimately show ?thesis by auto qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1) proof (state)
goal (1 subgoal):
 1. \<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1) 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 (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 (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 (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 (chain)
picking this:
m < 2 ^ (LENGTH('a) - s)
s < LENGTH('a) proof (prove)
using this:
m < 2 ^ (LENGTH('a) - s)
s < LENGTH('a)

goal (1 subgoal):
 1. unat (word_of_nat m) = m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m < 2 ^ (LENGTH('a) - s); s < LENGTH('a)\<rbrakk> \<Longrightarrow> m mod 2 ^ LENGTH('a) = m 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 (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 (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 (prove)
goal:
No subgoals! 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 (chain)
picking this:
unat (word_of_nat m) = m 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 (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 (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 (prove)
goal:
No subgoals! proof (state)
this:
unat (2 ^ s * word_of_nat m) = 2 ^ s * m

goal:
No subgoals! 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 (prove)
goal (1 subgoal):
 1. s1 < LENGTH('a) proof (prove)
using this:
s2 < LENGTH('a)
s1 \<le> s2

goal (1 subgoal):
 1. s1 < LENGTH('a) 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 (chain)
picking this:
is_aligned m s1 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 (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 (chain)
picking this:
is_aligned n s2 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 (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 (chain)
picking this:
s1 \<le> s2 proof (prove)
using this:
s1 \<le> s2

goal (1 subgoal):
 1. (\<And>sq. s2 = s1 + sq \<Longrightarrow> thesis) \<Longrightarrow> thesis 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 (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 (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 (chain)
picking this:
m \<in> {n..n + (2 ^ s2 - 1)} proof (prove)
using this:
m \<in> {n..n + (2 ^ s2 - 1)}

goal (1 subgoal):
 1. n \<le> m 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 (chain)
picking this:
n \<le> m 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 (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 (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 (chain)
picking this:
2 ^ s2 * word_of_nat nq \<le> 2 ^ s1 * word_of_nat mq 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 (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 (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 (chain)
picking this:
2 ^ s2 * nq \<le> 2 ^ s1 * mq proof (prove)
using this:
2 ^ s2 * nq \<le> 2 ^ s1 * mq

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

goal (1 subgoal):
 1. 2 ^ sq * nq \<le> mq 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 (prove)
goal (1 subgoal):
 1. m - n = 2 ^ s1 * word_of_nat mq - 2 ^ s2 * word_of_nat nq 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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (chain)
picking this:
m - n = 2 ^ s1 * word_of_nat (mq - 2 ^ sq * nq) 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 (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 (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 (chain)
picking this:
m \<in> {n..n + (2 ^ s2 - 1)} proof (prove)
using this:
m \<in> {n..n + (2 ^ s2 - 1)}

goal (1 subgoal):
 1. m - n \<le> 2 ^ s2 - 1 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 (chain)
picking this:
m - n \<le> 2 ^ s2 - 1 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 (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 (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 (chain)
picking this:
2 ^ s1 * word_of_nat (mq - 2 ^ sq * nq) < 2 ^ s2 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 (state)
goal (1 subgoal):
 1. word_of_nat (mq - 2 ^ sq * nq) < 2 ^ (LENGTH('a) - s1) proof (prove)
goal (1 subgoal):
 1. mq - 2 ^ sq * nq < 2 ^ (LENGTH('a) - s1) proof (prove)
using this:
mq < 2 ^ (LENGTH('a) - s1)

goal (1 subgoal):
 1. mq - 2 ^ sq * nq < 2 ^ (LENGTH('a) - s1) 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 (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 (chain)
picking this:
0 < s1 proof (prove)
using this:
0 < s1

goal (1 subgoal):
 1. LENGTH('a) - s1 < LENGTH('a) proof (state)
this:
LENGTH('a) - s1 < LENGTH('a)

goal (1 subgoal):
 1. word_of_nat (mq - 2 ^ sq * nq) < 2 ^ (LENGTH('a) - s1) proof (chain)
picking this:
mq - 2 ^ sq * nq < 2 ^ (LENGTH('a) - s1)
LENGTH('a) - s1 < LENGTH('a) 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 (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 (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 (prove)
goal:
No subgoals! proof (state)
this:
word_of_nat (mq - 2 ^ sq * nq) < 2 ^ (LENGTH('a) - s1)

goal:
No subgoals! 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 (chain)
picking this:
word_of_nat (mq - 2 ^ sq * nq) < 2 ^ (s2 - s1) 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 (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 (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 (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 (prove)
goal (1 subgoal):
 1. \<lbrakk>mq < 2 ^ (LENGTH('a) - s1); s2 < LENGTH('a)\<rbrakk> \<Longrightarrow> mq - 2 ^ sq * nq < 2 ^ LENGTH('a) 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 (prove)
goal (1 subgoal):
 1. \<lbrakk>mq < 2 ^ (LENGTH('a) - s1); s2 < LENGTH('a)\<rbrakk> \<Longrightarrow> mq < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. s2 < LENGTH('a) \<Longrightarrow> 2 ^ (LENGTH('a) - s1) \<le> 2 ^ LENGTH('a) proof (prove)
goal:
No subgoals! 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 (chain)
picking this:
m - n = word_of_nat (mq - 2 ^ sq * nq) * 2 ^ s1
mq - 2 ^ sq * nq < 2 ^ (s2 - s1) 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 (state)
this:
\<exists>q. m - n = word_of_nat q * 2 ^ s1 \<and> q < 2 ^ (s2 - s1)

goal:
No subgoals!