theory Machine_C

lemma cacheRangeOp_ccorres:
  "\<lbrakk>\<And>x y. empty_fail (oper x y);
    \<forall>n. ccorres dc xfdc \<top> (\<lbrace>\<acute>index = lineIndex w1 + of_nat n\<rbrace>) hs
                (doMachineOp (oper (lineStart w1 + of_nat n * 0x20)
                                   (lineStart w3 + of_nat n * 0x20)))
                f;
   \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f ({t. index_' t = index_' s}) \<rbrakk> \<Longrightarrow>
   ccorres dc xfdc (\<lambda>_. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1)
                      \<and> w1 && mask 5 = w3 && mask 5)
                   (\<lbrace>\<acute>index = w1 >> 5\<rbrace>) hs
           (doMachineOp (cacheRangeOp oper w1 w2 w3))
           (While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace>
             (f;; \<acute>index :== \<acute>index + 1))" apply (clarsimp simp: cacheRangeOp_def doMachineOp_mapM_x split_def
                        cacheLine_def cacheLineBits_def) apply (rule ccorres_gen_asm[where G=\<top>, simplified]) apply (rule ccorres_guard_imp) apply (rule ccorres_rel_imp) apply (rule_tac i="unat (lineIndex w1)" and F="\<lambda>_. \<top>"
             in ccorres_mapM_x_while_gen'[OF _ _ _ _ _ index_xf_for_sequence,
                                           where j=1, simplified], simp_all) apply clarsimp apply (clarsimp simp: length_upto_enum_step lineStart_le_mono) apply (clarsimp simp: upto_enum_step_nth lineStart_le_mono) apply (clarsimp simp: length_upto_enum_step lineStart_le_mono unat_div) apply (subst min_absorb1[OF order_eq_refl]) apply (erule (2) cachRangeOp_corres_helper) apply (simp add: lineIndex_lineStart_diff) apply (simp add: lineIndex_def2 cacheLineBits_def) apply unat_arith apply wp apply (clarsimp simp: length_upto_enum_step lineStart_le_mono unat_div) apply (subst min_absorb1[OF order_eq_refl]) apply (erule (2) cachRangeOp_corres_helper) apply (simp add: lineIndex_lineStart_diff unat_sub[OF lineIndex_le_mono]) apply (subst le_add_diff_inverse) apply (simp add: lineIndex_le_mono word_le_nat_alt[symmetric]) apply (simp add: lineIndex_def2 cacheLineBits_def) apply (rule unat_mono[where 'a=32 and b="0xFFFFFFFF", simplified]) apply word_bitwise apply (simp add: lineIndex_def cacheLineBits_def lineStart_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>_. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5) \<lbrace>\<acute>index = w1 >> 5\<rbrace> hs (doMachineOp (cacheRangeOp oper w1 w2 w3)) (While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (f;;
\<acute>index :== \<acute>index + 1)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>_. w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5) \<lbrace>\<acute>index = w1 >> 5\<rbrace> hs (mapM_x (doMachineOp \<circ> (\<lambda>p. oper (fst p) (snd p))) (zip [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))])) (While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (f;;
\<acute>index :== \<acute>index + 1)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = w1 >> 5\<rbrace> hs (mapM_x (doMachineOp \<circ> (\<lambda>p. oper (fst p) (snd p))) (zip [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))])) (While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (f;;
\<acute>index :== \<acute>index + 1)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Q14 ?Q'14 hs (mapM_x (doMachineOp \<circ> (\<lambda>p. oper (fst p) (snd p))) (zip [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))])) (While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (f;;
\<acute>index :== \<acute>index + 1))
 2. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; True\<rbrakk> \<Longrightarrow> ?Q14 s
 3. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; s \<in> \<lbrace>\<acute>index = w1 >> 5\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> ?Q'14 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> ccorres ?r'18 ?xf'18 ?Q14 ?Q'14 hs (mapM_x (doMachineOp \<circ> (\<lambda>p. oper (fst p) (snd p))) (zip [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))])) (While \<lbrace>\<acute>index < (w2 >> 5) + 1\<rbrace> (f;;
\<acute>index :== \<acute>index + 1))
 2. \<And>x y. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; ?r'18 x (?xf'18 y)\<rbrakk> \<Longrightarrow> dc x (xfdc y)
 3. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; True\<rbrakk> \<Longrightarrow> ?Q14 s
 4. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; s \<in> \<lbrace>\<acute>index = w1 >> 5\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> ?Q'14 proof (prove)
goal (5 subgoals):
 1. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> \<forall>n. n < length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] \<and> n < length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))] \<longrightarrow> ccorres dc xfdc (\<lambda>a. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper ([lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] ! n) ([lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))] ! n))) f
 2. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> (n < (w2 >> 5) + 1) = (n < lineIndex w1 + word_of_nat (min (length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2]) (length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))])))
 3. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; Suc n < length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] \<and> Suc n < length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (oper ([lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] ! n) ([lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))] ! n)) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineIndex w1) + min (length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2]) (length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]) < 4294967296
 5. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; index_' s = w1 >> 5\<rbrakk> \<Longrightarrow> w1 >> 5 = lineIndex w1 proof (prove)
goal (5 subgoals):
 1. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; n < length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2]; n < length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>a. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper ([lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] ! n) ([lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))] ! n))) f
 2. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> (n < (w2 >> 5) + 1) = (n < lineIndex w1 + word_of_nat (min (length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2]) (length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))])))
 3. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; Suc n < length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] \<and> Suc n < length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (oper ([lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] ! n) ([lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))] ! n)) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineIndex w1) + min (length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2]) (length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]) < 4294967296
 5. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; index_' s = w1 >> 5\<rbrakk> \<Longrightarrow> w1 >> 5 = lineIndex w1 proof (prove)
goal (5 subgoals):
 1. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5; n < Suc (unat ((lineStart w2 - lineStart w1) div 0x20)); n < Suc (unat ((lineStart (w3 + (w2 - w1)) - lineStart w3) div 0x20))\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>a. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper ([lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] ! n) ([lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))] ! n))) f
 2. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> (n < (w2 >> 5) + 1) = (n < lineIndex w1 + word_of_nat (min (length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2]) (length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))])))
 3. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; Suc n < length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] \<and> Suc n < length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (oper ([lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] ! n) ([lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))] ! n)) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineIndex w1) + min (length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2]) (length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]) < 4294967296
 5. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; index_' s = w1 >> 5\<rbrakk> \<Longrightarrow> w1 >> 5 = lineIndex w1 proof (prove)
goal (4 subgoals):
 1. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> (n < (w2 >> 5) + 1) = (n < lineIndex w1 + word_of_nat (min (length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2]) (length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))])))
 2. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; Suc n < length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] \<and> Suc n < length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (oper ([lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] ! n) ([lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))] ! n)) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineIndex w1) + min (length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2]) (length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]) < 4294967296
 4. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; index_' s = w1 >> 5\<rbrakk> \<Longrightarrow> w1 >> 5 = lineIndex w1 proof (prove)
goal (4 subgoals):
 1. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> (n < (w2 >> 5) + 1) = (n < lineIndex w1 + (1 + word_of_nat (min (unat (lineStart w2 - lineStart w1) div 32) (unat (lineStart (w3 + (w2 - w1)) - lineStart w3) div 32))))
 2. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; Suc n < length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] \<and> Suc n < length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (oper ([lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] ! n) ([lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))] ! n)) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineIndex w1) + min (length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2]) (length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]) < 4294967296
 4. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; index_' s = w1 >> 5\<rbrakk> \<Longrightarrow> w1 >> 5 = lineIndex w1 proof (prove)
goal (5 subgoals):
 1. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; 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
 2. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> (n < (w2 >> 5) + 1) = (n < lineIndex w1 + (1 + word_of_nat (unat (lineStart w2 - lineStart w1) div 32)))
 3. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; Suc n < length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] \<and> Suc n < length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (oper ([lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] ! n) ([lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))] ! n)) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineIndex w1) + min (length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2]) (length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]) < 4294967296
 5. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; index_' s = w1 >> 5\<rbrakk> \<Longrightarrow> w1 >> 5 = lineIndex w1 proof (prove)
goal (4 subgoals):
 1. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> (n < (w2 >> 5) + 1) = (n < lineIndex w1 + (1 + word_of_nat (unat (lineStart w2 - lineStart w1) div 32)))
 2. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; Suc n < length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] \<and> Suc n < length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (oper ([lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] ! n) ([lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))] ! n)) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineIndex w1) + min (length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2]) (length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]) < 4294967296
 4. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; index_' s = w1 >> 5\<rbrakk> \<Longrightarrow> w1 >> 5 = lineIndex w1 proof (prove)
goal (4 subgoals):
 1. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> (n < (w2 >> 5) + 1) = (n < 1 + lineIndex w2)
 2. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; Suc n < length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] \<and> Suc n < length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (oper ([lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] ! n) ([lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))] ! n)) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineIndex w1) + min (length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2]) (length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]) < 4294967296
 4. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; index_' s = w1 >> 5\<rbrakk> \<Longrightarrow> w1 >> 5 = lineIndex w1 proof (prove)
goal (4 subgoals):
 1. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = (w1 >> 5) + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> (n < (w2 >> 5) + 1) = (n < 1 + (w2 >> 5))
 2. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; Suc n < length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] \<and> Suc n < length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (oper ([lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] ! n) ([lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))] ! n)) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineIndex w1) + min (length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2]) (length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]) < 4294967296
 4. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; index_' s = w1 >> 5\<rbrakk> \<Longrightarrow> w1 >> 5 = lineIndex w1 proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; Suc n < length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] \<and> Suc n < length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (oper ([lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2] ! n) ([lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))] ! n)) \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineIndex w1) + min (length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2]) (length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]) < 4294967296
 3. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; index_' s = w1 >> 5\<rbrakk> \<Longrightarrow> w1 >> 5 = lineIndex w1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineIndex w1) + min (length [lineStart w1 , lineStart w1 + 0x20 .e. lineStart w2]) (length [lineStart w3 , lineStart w3 + 0x20 .e. lineStart (w3 + (w2 - w1))]) < 4294967296
 2. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; index_' s = w1 >> 5\<rbrakk> \<Longrightarrow> w1 >> 5 = lineIndex w1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineIndex w1) + min (unat (lineStart w2 - lineStart w1) div 32) (unat (lineStart (w3 + (w2 - w1)) - lineStart w3) div 32) < 4294967295
 2. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; index_' s = w1 >> 5\<rbrakk> \<Longrightarrow> w1 >> 5 = lineIndex w1 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; 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
 2. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineIndex w1) + unat (lineStart w2 - lineStart w1) div 32 < 4294967295
 3. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; index_' s = w1 >> 5\<rbrakk> \<Longrightarrow> w1 >> 5 = lineIndex w1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineIndex w1) + unat (lineStart w2 - lineStart w1) div 32 < 4294967295
 2. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; index_' s = w1 >> 5\<rbrakk> \<Longrightarrow> w1 >> 5 = lineIndex w1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineIndex w1) + (unat (lineIndex w2) - unat (lineIndex w1)) < 4294967295
 2. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; index_' s = w1 >> 5\<rbrakk> \<Longrightarrow> w1 >> 5 = lineIndex w1 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineIndex w1) \<le> unat (lineIndex w2)
 2. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineIndex w2) < 4294967295
 3. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; index_' s = w1 >> 5\<rbrakk> \<Longrightarrow> w1 >> 5 = lineIndex w1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (lineIndex w2) < 4294967295
 2. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; index_' s = w1 >> 5\<rbrakk> \<Longrightarrow> w1 >> 5 = lineIndex w1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = (w1 >> 5) + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> unat (w2 >> 5) < 4294967295
 2. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; index_' s = w1 >> 5\<rbrakk> \<Longrightarrow> w1 >> 5 = lineIndex w1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = (w1 >> 5) + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2; w3 \<le> w3 + (w2 - w1); w1 && mask 5 = w3 && mask 5\<rbrakk> \<Longrightarrow> w2 >> 5 < 0xFFFFFFFF
 2. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; index_' s = w1 >> 5\<rbrakk> \<Longrightarrow> w1 >> 5 = lineIndex w1 proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>x y. empty_fail (oper x y); \<forall>n. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>index = lineIndex w1 + word_of_nat n\<rbrace> hs (doMachineOp (oper (lineStart w1 + word_of_nat n * 0x20) (lineStart w3 + word_of_nat n * 0x20))) f; \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f \<lbrace>\<acute>index = \<^bsup>s\<^esup>index\<rbrace>; w1 \<le> w2 \<and> w3 \<le> w3 + (w2 - w1) \<and> w1 && mask 5 = w3 && mask 5; index_' s = w1 >> 5\<rbrakk> \<Longrightarrow> w1 >> 5 = lineIndex w1 proof (prove)
goal:
No subgoals!