theory PageTableDuplicates

lemma valid_duplicates'_diffI:
  defines "heap_diff m m' \<equiv> {(x::word32). (m x \<noteq> m' x)}"
  shows "\<lbrakk>vs_valid_duplicates' m;
          vs_valid_duplicates' (\<lambda>x. if x \<in> (heap_diff m m') then m' x else None);
          vs_valid_duplicates' (\<lambda>x. if x \<in> (heap_diff m m') then None else m' x)\<rbrakk>
         \<Longrightarrow> vs_valid_duplicates' m'" apply (subst vs_valid_duplicates'_def) apply (clarsimp simp: heap_diff_def split: option.splits) apply (case_tac "m x = m' x") apply simp apply (case_tac "m y = m' y") apply (drule(2) valid_duplicates'_D) apply simp+ apply (drule(2) valid_duplicates'_D) apply (thin_tac "vs_valid_duplicates' m" for m) apply (drule_tac p = x and ko = "the (m' x)" in valid_duplicates'_D) apply (clarsimp split:if_splits) apply assumption apply (clarsimp split:if_splits)+ apply (case_tac "m y = m' y") apply clarsimp apply (thin_tac "vs_valid_duplicates' m" for m) apply (drule_tac p = x and ko = "the (m' x)" in valid_duplicates'_D) apply (clarsimp split:if_splits) apply assumption apply (simp split:if_splits)+ apply (thin_tac "vs_valid_duplicates' m" for m) apply (drule_tac p = x and ko = "the (m' x)" in valid_duplicates'_D) apply (clarsimp split:if_splits) apply assumption apply (clarsimp split:if_splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if x \<in> heap_diff m m' then m' x else None); vs_valid_duplicates' (\<lambda>x. if x \<in> heap_diff m m' then None else m' x)\<rbrakk> \<Longrightarrow> vs_valid_duplicates' m' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if x \<in> heap_diff m m' then m' x else None); vs_valid_duplicates' (\<lambda>x. if x \<in> heap_diff m m' then None else m' x)\<rbrakk> \<Longrightarrow> \<forall>x y. case m' x of None \<Rightarrow> True | Some ko \<Rightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align ko) = y && ~~ mask (vs_ptr_align ko) \<longrightarrow> m' x = m' y proof (prove)
goal (1 subgoal):
 1. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (2 subgoals):
 1. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = m' x\<rbrakk> \<Longrightarrow> Some x2 = m' y
 2. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> m' x\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (2 subgoals):
 1. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2\<rbrakk> \<Longrightarrow> Some x2 = m' y
 2. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> m' x\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (3 subgoals):
 1. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y = m' y\<rbrakk> \<Longrightarrow> Some x2 = m' y
 2. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y \<noteq> m' y\<rbrakk> \<Longrightarrow> Some x2 = m' y
 3. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> m' x\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (4 subgoals):
 1. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y = m' y\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)
 2. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y = m' y; m y = Some x2\<rbrakk> \<Longrightarrow> Some x2 = m' y
 3. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y \<noteq> m' y\<rbrakk> \<Longrightarrow> Some x2 = m' y
 4. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> m' x\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (2 subgoals):
 1. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y \<noteq> m' y\<rbrakk> \<Longrightarrow> Some x2 = m' y
 2. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> m' x\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (3 subgoals):
 1. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y \<noteq> m' y\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)
 2. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y \<noteq> m' y; m y = Some x2\<rbrakk> \<Longrightarrow> Some x2 = m' y
 3. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> m' x\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (3 subgoals):
 1. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y \<noteq> m' y\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)
 2. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y \<noteq> m' y; m y = Some x2\<rbrakk> \<Longrightarrow> Some x2 = m' y
 3. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> m' x\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (6 subgoals):
 1. \<And>x y x2. \<lbrakk>m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y \<noteq> m' y\<rbrakk> \<Longrightarrow> (if m x \<noteq> m' x then None else m' x) = Some (the (m' x))
 2. \<And>x y x2. \<lbrakk>m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y \<noteq> m' y\<rbrakk> \<Longrightarrow> is_aligned (?p'40 x y x2) 2
 3. \<And>x y x2. \<lbrakk>m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y \<noteq> m' y\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (the (m' x))) = ?p'40 x y x2 && ~~ mask (vs_ptr_align (the (m' x)))
 4. \<And>x y x2. \<lbrakk>m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y \<noteq> m' y; (if m (?p'40 x y x2) \<noteq> m' (?p'40 x y x2) then None else m' (?p'40 x y x2)) = Some (the (m' x))\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)
 5. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y \<noteq> m' y; m y = Some x2\<rbrakk> \<Longrightarrow> Some x2 = m' y
 6. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> m' x\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (5 subgoals):
 1. \<And>x y x2. \<lbrakk>m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y \<noteq> m' y\<rbrakk> \<Longrightarrow> is_aligned (?p'40 x y x2) 2
 2. \<And>x y x2. \<lbrakk>m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y \<noteq> m' y\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (the (m' x))) = ?p'40 x y x2 && ~~ mask (vs_ptr_align (the (m' x)))
 3. \<And>x y x2. \<lbrakk>m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y \<noteq> m' y; (if m (?p'40 x y x2) \<noteq> m' (?p'40 x y x2) then None else m' (?p'40 x y x2)) = Some (the (m' x))\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)
 4. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y \<noteq> m' y; m y = Some x2\<rbrakk> \<Longrightarrow> Some x2 = m' y
 5. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> m' x\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (4 subgoals):
 1. \<And>x y x2. \<lbrakk>m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y \<noteq> m' y\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (the (m' x))) = y && ~~ mask (vs_ptr_align (the (m' x)))
 2. \<And>x y x2. \<lbrakk>m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y \<noteq> m' y; (if m y \<noteq> m' y then None else m' y) = Some (the (m' x))\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)
 3. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; m y \<noteq> m' y; m y = Some x2\<rbrakk> \<Longrightarrow> Some x2 = m' y
 4. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> m' x\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (2 subgoals):
 1. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; Some x2 \<noteq> m' y; m y = Some x2\<rbrakk> \<Longrightarrow> False
 2. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> m' x\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (3 subgoals):
 1. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; Some x2 \<noteq> m' y; m y = Some x2; m y = m' y\<rbrakk> \<Longrightarrow> False
 2. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; Some x2 \<noteq> m' y; m y = Some x2; m y \<noteq> m' y\<rbrakk> \<Longrightarrow> False
 3. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> m' x\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (2 subgoals):
 1. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; Some x2 \<noteq> m' y; m y = Some x2; m y \<noteq> m' y\<rbrakk> \<Longrightarrow> False
 2. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> m' x\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (2 subgoals):
 1. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; Some x2 \<noteq> m' y; m y = Some x2; m y \<noteq> m' y\<rbrakk> \<Longrightarrow> False
 2. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> m' x\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (5 subgoals):
 1. \<And>x y x2. \<lbrakk>m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; Some x2 \<noteq> m' y; m y = Some x2; m y \<noteq> m' y\<rbrakk> \<Longrightarrow> (if m x \<noteq> m' x then None else m' x) = Some (the (m' x))
 2. \<And>x y x2. \<lbrakk>m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; Some x2 \<noteq> m' y; m y = Some x2; m y \<noteq> m' y\<rbrakk> \<Longrightarrow> is_aligned (?p'50 x y x2) 2
 3. \<And>x y x2. \<lbrakk>m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; Some x2 \<noteq> m' y; m y = Some x2; m y \<noteq> m' y\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (the (m' x))) = ?p'50 x y x2 && ~~ mask (vs_ptr_align (the (m' x)))
 4. \<And>x y x2. \<lbrakk>m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; Some x2 \<noteq> m' y; m y = Some x2; m y \<noteq> m' y; (if m (?p'50 x y x2) \<noteq> m' (?p'50 x y x2) then None else m' (?p'50 x y x2)) = Some (the (m' x))\<rbrakk> \<Longrightarrow> False
 5. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> m' x\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (4 subgoals):
 1. \<And>x y x2. \<lbrakk>m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; Some x2 \<noteq> m' y; m y = Some x2; m y \<noteq> m' y\<rbrakk> \<Longrightarrow> is_aligned (?p'50 x y x2) 2
 2. \<And>x y x2. \<lbrakk>m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; Some x2 \<noteq> m' y; m y = Some x2; m y \<noteq> m' y\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (the (m' x))) = ?p'50 x y x2 && ~~ mask (vs_ptr_align (the (m' x)))
 3. \<And>x y x2. \<lbrakk>m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; Some x2 \<noteq> m' y; m y = Some x2; m y \<noteq> m' y; (if m (?p'50 x y x2) \<noteq> m' (?p'50 x y x2) then None else m' (?p'50 x y x2)) = Some (the (m' x))\<rbrakk> \<Longrightarrow> False
 4. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> m' x\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (3 subgoals):
 1. \<And>x y x2. \<lbrakk>m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; Some x2 \<noteq> m' y; m y = Some x2; m y \<noteq> m' y\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (the (m' x))) = y && ~~ mask (vs_ptr_align (the (m' x)))
 2. \<And>x y x2. \<lbrakk>m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x = Some x2; Some x2 \<noteq> m' y; m y = Some x2; m y \<noteq> m' y; (if m y \<noteq> m' y then None else m' y) = Some (the (m' x))\<rbrakk> \<Longrightarrow> False
 3. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> m' x\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (1 subgoal):
 1. \<And>x y x2. \<lbrakk>vs_valid_duplicates' m; vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> Some x2\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (1 subgoal):
 1. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then m' x else None); vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> Some x2\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (4 subgoals):
 1. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> Some x2\<rbrakk> \<Longrightarrow> (if m x \<noteq> m' x then m' x else None) = Some (the (m' x))
 2. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> Some x2\<rbrakk> \<Longrightarrow> is_aligned (?p'57 x y x2) 2
 3. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> Some x2\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (the (m' x))) = ?p'57 x y x2 && ~~ mask (vs_ptr_align (the (m' x)))
 4. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> Some x2; (if m (?p'57 x y x2) \<noteq> m' (?p'57 x y x2) then m' (?p'57 x y x2) else None) = Some (the (m' x))\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (3 subgoals):
 1. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> Some x2\<rbrakk> \<Longrightarrow> is_aligned (?p'57 x y x2) 2
 2. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> Some x2\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (the (m' x))) = ?p'57 x y x2 && ~~ mask (vs_ptr_align (the (m' x)))
 3. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> Some x2; (if m (?p'57 x y x2) \<noteq> m' (?p'57 x y x2) then m' (?p'57 x y x2) else None) = Some (the (m' x))\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal (2 subgoals):
 1. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> Some x2\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (the (m' x))) = y && ~~ mask (vs_ptr_align (the (m' x)))
 2. \<And>x y x2. \<lbrakk>vs_valid_duplicates' (\<lambda>x. if m x \<noteq> m' x then None else m' x); m' x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); m x \<noteq> Some x2; (if m y \<noteq> m' y then m' y else None) = Some (the (m' x))\<rbrakk> \<Longrightarrow> Some x2 = m' y proof (prove)
goal:
No subgoals!