theory Machine_C

lemma cachRangeOp_corres_helper:
  "\<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk>
   \<Longrightarrow> unat (lineStart w2 - lineStart w1) div 32 =
           unat (lineStart (w3 + (w2 - w1)) - lineStart w3) div 32" apply (subst dvd_div_div_eq_mult, simp) apply (clarsimp simp: and_mask_dvd_nat[where n=5, simplified]) apply (clarsimp simp: lineStart_def cacheLineBits_def shiftr_shiftl1) apply (subst mask_eqs(8)[symmetric]) apply (clarsimp simp: mask_AND_NOT_mask) apply (clarsimp simp: and_mask_dvd_nat[where n=5, simplified]) apply (subst mask_eqs(8)[symmetric]) apply (clarsimp simp: lineStart_mask) apply (subgoal_tac "w3 + (w2 - w1) && mask 5 = w2 && mask 5") apply clarsimp apply (rule_tac x=w1 and y=w3 in linorder_le_cases) apply (subgoal_tac "lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1") apply (rule word_unat.Rep_eqD) apply (subst unat_sub, clarsimp simp: lineStart_le_mono)+ apply (rule minus_minus_swap) apply (clarsimp simp: word_le_nat_alt[symmetric] intro!: lineStart_le_mono) apply (clarsimp simp: word_le_nat_alt unat_plus_simple[THEN iffD1] unat_sub) apply arith apply (clarsimp simp: word_le_nat_alt[symmetric] lineStart_le_mono) apply (clarsimp simp: word_le_nat_alt[symmetric] lineStart_le_mono) apply (clarsimp simp: word_le_nat_alt[symmetric] lineStart_le_mono) apply (subst unat_sub[symmetric], clarsimp simp: intro!: lineStart_le_mono)+ apply (clarsimp simp: word_le_nat_alt unat_plus_simple[THEN iffD1] unat_sub) apply arith apply clarsimp apply (clarsimp simp: lineStart_sub[symmetric] field_simps) apply (subgoal_tac "lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3") apply (rule word_unat.Rep_eqD) apply (subst unat_sub, clarsimp simp: lineStart_le_mono)+ apply (rule minus_minus_swap') apply (clarsimp simp: word_le_nat_alt[symmetric] intro!: lineStart_le_mono) apply (clarsimp simp: word_le_nat_alt unat_plus_simple[THEN iffD1] unat_sub) apply arith apply (clarsimp simp: word_le_nat_alt[symmetric] lineStart_le_mono) apply (clarsimp simp: word_le_nat_alt[symmetric] lineStart_le_mono) apply (clarsimp simp: word_le_nat_alt[symmetric] lineStart_le_mono) apply (subst unat_sub[symmetric], clarsimp simp: intro!: lineStart_le_mono)+ apply (clarsimp simp: word_le_nat_alt unat_plus_simple[THEN iffD1] unat_sub) apply arith apply clarsimp apply (clarsimp simp: lineStart_sub[symmetric] field_simps) apply (subst mask_eqs(7)[symmetric]) apply (subst mask_eqs(8)[symmetric]) apply (clarsimp simp: mask_eqs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineStart w2 - lineStart w1) div 32 = unat (lineStart (w3 + (w2 - w1)) - lineStart w3) div 32 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> 32 dvd unat (lineStart w2 - lineStart w1)
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> 32 dvd unat (lineStart (w3 + (w2 - w1)) - lineStart w3)
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineStart w2 - lineStart w1) * 32 = 32 * unat (lineStart (w3 + (w2 - w1)) - lineStart w3) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 && mask 5 = 0
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> 32 dvd unat (lineStart (w3 + (w2 - w1)) - lineStart w3)
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineStart w2 - lineStart w1) * 32 = 32 * unat (lineStart (w3 + (w2 - w1)) - lineStart w3) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> (w2 && ~~ mask 5) - (w1 && ~~ mask 5) && mask 5 = 0
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> 32 dvd unat (lineStart (w3 + (w2 - w1)) - lineStart w3)
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineStart w2 - lineStart w1) * 32 = 32 * unat (lineStart (w3 + (w2 - w1)) - lineStart w3) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> ((w2 && ~~ mask 5) && mask 5) - ((w1 && ~~ mask 5) && mask 5) && mask 5 = 0
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> 32 dvd unat (lineStart (w3 + (w2 - w1)) - lineStart w3)
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineStart w2 - lineStart w1) * 32 = 32 * unat (lineStart (w3 + (w2 - w1)) - lineStart w3) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> 32 dvd unat (lineStart (w3 + (w2 - w1)) - lineStart w3)
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineStart w2 - lineStart w1) * 32 = 32 * unat (lineStart (w3 + (w2 - w1)) - lineStart w3) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> lineStart (w3 + (w2 - w1)) - lineStart w3 && mask 5 = 0
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineStart w2 - lineStart w1) * 32 = 32 * unat (lineStart (w3 + (w2 - w1)) - lineStart w3) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> (lineStart (w3 + (w2 - w1)) && mask 5) - (lineStart w3 && mask 5) && mask 5 = 0
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineStart w2 - lineStart w1) * 32 = 32 * unat (lineStart (w3 + (w2 - w1)) - lineStart w3) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineStart w2 - lineStart w1) * 32 = 32 * unat (lineStart (w3 + (w2 - w1)) - lineStart w3) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5\<rbrakk> \<Longrightarrow> unat (lineStart w2 - lineStart w1) * 32 = 32 * unat (lineStart (w3 + (w2 - w1)) - lineStart w3)
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 = lineStart (w3 + (w2 - w1)) - lineStart w3
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 = lineStart (w3 + (w2 - w1)) - lineStart w3
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 = lineStart (w3 + (w2 - w1)) - lineStart w3
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 = lineStart (w3 + (w2 - w1)) - lineStart w3
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3\<rbrakk> \<Longrightarrow> lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 = lineStart (w3 + (w2 - w1)) - lineStart w3
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w2 - lineStart w1) = unat (lineStart (w3 + (w2 - w1)) - lineStart w3)
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3\<rbrakk> \<Longrightarrow> lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 = lineStart (w3 + (w2 - w1)) - lineStart w3
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w2) - unat (lineStart w1) = unat (lineStart (w3 + (w2 - w1))) - unat (lineStart w3)
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3\<rbrakk> \<Longrightarrow> lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 = lineStart (w3 + (w2 - w1)) - lineStart w3
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (8 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w2) \<le> unat (lineStart (w3 + (w2 - w1)))
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w1) \<le> unat (lineStart w3)
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w1) \<le> unat (lineStart w2)
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w3) \<le> unat (lineStart (w3 + (w2 - w1)))
 5. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w3) - unat (lineStart w1) = unat (lineStart (w3 + (w2 - w1))) - unat (lineStart w2)
 6. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3\<rbrakk> \<Longrightarrow> lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1
 7. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 = lineStart (w3 + (w2 - w1)) - lineStart w3
 8. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (8 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> w2 \<le> w3 + (w2 - w1)
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w1) \<le> unat (lineStart w3)
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w1) \<le> unat (lineStart w2)
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w3) \<le> unat (lineStart (w3 + (w2 - w1)))
 5. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w3) - unat (lineStart w1) = unat (lineStart (w3 + (w2 - w1))) - unat (lineStart w2)
 6. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3\<rbrakk> \<Longrightarrow> lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1
 7. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 = lineStart (w3 + (w2 - w1)) - lineStart w3
 8. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (8 subgoals):
 1. \<lbrakk>unat w1 \<le> unat w2; unat w3 \<le> unat (w3 + (w2 - w1)); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; unat w1 \<le> unat w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat w2 \<le> unat w3 + unat w2 - unat w1
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w1) \<le> unat (lineStart w3)
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w1) \<le> unat (lineStart w2)
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w3) \<le> unat (lineStart (w3 + (w2 - w1)))
 5. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w3) - unat (lineStart w1) = unat (lineStart (w3 + (w2 - w1))) - unat (lineStart w2)
 6. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3\<rbrakk> \<Longrightarrow> lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1
 7. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 = lineStart (w3 + (w2 - w1)) - lineStart w3
 8. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (7 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w1) \<le> unat (lineStart w3)
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w1) \<le> unat (lineStart w2)
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w3) \<le> unat (lineStart (w3 + (w2 - w1)))
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w3) - unat (lineStart w1) = unat (lineStart (w3 + (w2 - w1))) - unat (lineStart w2)
 5. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3\<rbrakk> \<Longrightarrow> lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1
 6. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 = lineStart (w3 + (w2 - w1)) - lineStart w3
 7. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (6 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w1) \<le> unat (lineStart w2)
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w3) \<le> unat (lineStart (w3 + (w2 - w1)))
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w3) - unat (lineStart w1) = unat (lineStart (w3 + (w2 - w1))) - unat (lineStart w2)
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3\<rbrakk> \<Longrightarrow> lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1
 5. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 = lineStart (w3 + (w2 - w1)) - lineStart w3
 6. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (5 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w3) \<le> unat (lineStart (w3 + (w2 - w1)))
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w3) - unat (lineStart w1) = unat (lineStart (w3 + (w2 - w1))) - unat (lineStart w2)
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3\<rbrakk> \<Longrightarrow> lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 = lineStart (w3 + (w2 - w1)) - lineStart w3
 5. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w3) - unat (lineStart w1) = unat (lineStart (w3 + (w2 - w1))) - unat (lineStart w2)
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3\<rbrakk> \<Longrightarrow> lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 = lineStart (w3 + (w2 - w1)) - lineStart w3
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (5 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> w2 \<le> w3 + (w2 - w1)
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w3 - lineStart w1) = unat (lineStart (w3 + (w2 - w1)) - lineStart w2)
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3\<rbrakk> \<Longrightarrow> lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 = lineStart (w3 + (w2 - w1)) - lineStart w3
 5. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (5 subgoals):
 1. \<lbrakk>unat w1 \<le> unat w2; unat w3 \<le> unat (w3 + (w2 - w1)); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; unat w1 \<le> unat w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat w2 \<le> unat w3 + unat w2 - unat w1
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w3 - lineStart w1) = unat (lineStart (w3 + (w2 - w1)) - lineStart w2)
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3\<rbrakk> \<Longrightarrow> lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 = lineStart (w3 + (w2 - w1)) - lineStart w3
 5. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3; lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1\<rbrakk> \<Longrightarrow> unat (lineStart w3 - lineStart w1) = unat (lineStart (w3 + (w2 - w1)) - lineStart w2)
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3\<rbrakk> \<Longrightarrow> lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 = lineStart (w3 + (w2 - w1)) - lineStart w3
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w1 \<le> w3\<rbrakk> \<Longrightarrow> lineStart (w3 + (w2 - w1)) - lineStart w2 = lineStart w3 - lineStart w1
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 = lineStart (w3 + (w2 - w1)) - lineStart w3
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 = lineStart (w3 + (w2 - w1)) - lineStart w3
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart w1 = lineStart (w3 + (w2 - w1)) - lineStart w3
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w2 - lineStart w1) = unat (lineStart (w3 + (w2 - w1)) - lineStart w3)
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w2) - unat (lineStart w1) = unat (lineStart (w3 + (w2 - w1))) - unat (lineStart w3)
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (7 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart (w3 + (w2 - w1))) \<le> unat (lineStart w2)
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w3) \<le> unat (lineStart w1)
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w1) \<le> unat (lineStart w2)
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w3) \<le> unat (lineStart (w3 + (w2 - w1)))
 5. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w1) - unat (lineStart w3) = unat (lineStart w2) - unat (lineStart (w3 + (w2 - w1)))
 6. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3
 7. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (7 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) \<le> w2
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w3) \<le> unat (lineStart w1)
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w1) \<le> unat (lineStart w2)
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w3) \<le> unat (lineStart (w3 + (w2 - w1)))
 5. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w1) - unat (lineStart w3) = unat (lineStart w2) - unat (lineStart (w3 + (w2 - w1)))
 6. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3
 7. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (7 subgoals):
 1. \<lbrakk>unat w1 \<le> unat w2; unat w3 \<le> unat (w3 + (w2 - w1)); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; unat w3 \<le> unat w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat w3 + unat w2 - unat w1 \<le> unat w2
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w3) \<le> unat (lineStart w1)
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w1) \<le> unat (lineStart w2)
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w3) \<le> unat (lineStart (w3 + (w2 - w1)))
 5. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w1) - unat (lineStart w3) = unat (lineStart w2) - unat (lineStart (w3 + (w2 - w1)))
 6. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3
 7. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (6 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w3) \<le> unat (lineStart w1)
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w1) \<le> unat (lineStart w2)
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w3) \<le> unat (lineStart (w3 + (w2 - w1)))
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w1) - unat (lineStart w3) = unat (lineStart w2) - unat (lineStart (w3 + (w2 - w1)))
 5. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3
 6. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (5 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w1) \<le> unat (lineStart w2)
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w3) \<le> unat (lineStart (w3 + (w2 - w1)))
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w1) - unat (lineStart w3) = unat (lineStart w2) - unat (lineStart (w3 + (w2 - w1)))
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3
 5. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w3) \<le> unat (lineStart (w3 + (w2 - w1)))
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w1) - unat (lineStart w3) = unat (lineStart w2) - unat (lineStart (w3 + (w2 - w1)))
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w1) - unat (lineStart w3) = unat (lineStart w2) - unat (lineStart (w3 + (w2 - w1)))
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) \<le> w2
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w1 - lineStart w3) = unat (lineStart w2 - lineStart (w3 + (w2 - w1)))
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>unat w1 \<le> unat w2; unat w3 \<le> unat (w3 + (w2 - w1)); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; unat w3 \<le> unat w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat w3 + unat w2 - unat w1 \<le> unat w2
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w1 - lineStart w3) = unat (lineStart w2 - lineStart (w3 + (w2 - w1)))
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3
 4. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1; lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3\<rbrakk> \<Longrightarrow> unat (lineStart w1 - lineStart w3) = unat (lineStart w2 - lineStart (w3 + (w2 - w1)))
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3
 3. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; w3 + (w2 - w1) && mask 5 = w2 && mask 5; w3 \<le> w1\<rbrakk> \<Longrightarrow> lineStart w2 - lineStart (w3 + (w2 - w1)) = lineStart w1 - lineStart w3
 2. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w3 + (w2 - w1) && mask 5 = w2 && mask 5 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> (w3 && mask 5) + (w2 - w1 && mask 5) && mask 5 = w2 && mask 5 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> (w3 && mask 5) + ((w2 && mask 5) - (w1 && mask 5) && mask 5) && mask 5 = w2 && mask 5 proof (prove)
goal:
No subgoals!