theory ArchVSpaceEntries_AI

lemma neg_mask_pd_6_4:
  "(ptr && mask pd_bits >> 2) && ~~ mask 4 =
   (ptr::word32) && ~~ mask 6 && mask pd_bits >> 2" apply (simp add:pd_bits_def pageBits_def) apply word_bitwise apply (simp add:word_size mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ptr && mask pd_bits >> 2) && ~~ mask 4 = ptr && ~~ mask 6 && mask pd_bits >> 2 proof (prove)
goal (1 subgoal):
 1. (ptr && mask 14 >> 2) && ~~ mask 4 = ptr && ~~ mask 6 && mask 14 >> 2 proof (prove)
goal (1 subgoal):
 1. (ptr !! 2 \<and> mask 14 !! 2 \<and> \<not> mask 4 !! 0) = (ptr !! 2 \<and> \<not> mask 6 !! 2 \<and> mask 14 !! 2) \<and> (ptr !! 3 \<and> mask 14 !! 3 \<and> \<not> mask 4 !! 1) = (ptr !! 3 \<and> \<not> mask 6 !! 3 \<and> mask 14 !! 3) \<and> (ptr !! 4 \<and> mask 14 !! 4 \<and> \<not> mask 4 !! 2) = (ptr !! 4 \<and> \<not> mask 6 !! 4 \<and> mask 14 !! 4) \<and> (ptr !! 5 \<and> mask 14 !! 5 \<and> \<not> mask 4 !! 3) = (ptr !! 5 \<and> \<not> mask 6 !! 5 \<and> mask 14 !! 5) \<and> (ptr !! 6 \<and> mask 14 !! 6 \<and> \<not> mask 4 !! 4) = (ptr !! 6 \<and> \<not> mask 6 !! 6 \<and> mask 14 !! 6) \<and> (ptr !! 7 \<and> mask 14 !! 7 \<and> \<not> mask 4 !! 5) = (ptr !! 7 \<and> \<not> mask 6 !! 7 \<and> mask 14 !! 7) \<and> (ptr !! 8 \<and> mask 14 !! 8 \<and> \<not> mask 4 !! 6) = (ptr !! 8 \<and> \<not> mask 6 !! 8 \<and> mask 14 !! 8) \<and> (ptr !! 9 \<and> mask 14 !! 9 \<and> \<not> mask 4 !! 7) = (ptr !! 9 \<and> \<not> mask 6 !! 9 \<and> mask 14 !! 9) \<and> (ptr !! 10 \<and> mask 14 !! 10 \<and> \<not> mask 4 !! 8) = (ptr !! 10 \<and> \<not> mask 6 !! 10 \<and> mask 14 !! 10) \<and> (ptr !! 11 \<and> mask 14 !! 11 \<and> \<not> mask 4 !! 9) = (ptr !! 11 \<and> \<not> mask 6 !! 11 \<and> mask 14 !! 11) \<and> (ptr !! 12 \<and> mask 14 !! 12 \<and> \<not> mask 4 !! 10) = (ptr !! 12 \<and> \<not> mask 6 !! 12 \<and> mask 14 !! 12) \<and> (ptr !! 13 \<and> mask 14 !! 13 \<and> \<not> mask 4 !! 11) = (ptr !! 13 \<and> \<not> mask 6 !! 13 \<and> mask 14 !! 13) \<and> (ptr !! 14 \<and> mask 14 !! 14 \<and> \<not> mask 4 !! 12) = (ptr !! 14 \<and> \<not> mask 6 !! 14 \<and> mask 14 !! 14) \<and> (ptr !! 15 \<and> mask 14 !! 15 \<and> \<not> mask 4 !! 13) = (ptr !! 15 \<and> \<not> mask 6 !! 15 \<and> mask 14 !! 15) \<and> (ptr !! 16 \<and> mask 14 !! 16 \<and> \<not> mask 4 !! 14) = (ptr !! 16 \<and> \<not> mask 6 !! 16 \<and> mask 14 !! 16) \<and> (ptr !! 17 \<and> mask 14 !! 17 \<and> \<not> mask 4 !! 15) = (ptr !! 17 \<and> \<not> mask 6 !! 17 \<and> mask 14 !! 17) \<and> (ptr !! 18 \<and> mask 14 !! 18 \<and> \<not> mask 4 !! 16) = (ptr !! 18 \<and> \<not> mask 6 !! 18 \<and> mask 14 !! 18) \<and> (ptr !! 19 \<and> mask 14 !! 19 \<and> \<not> mask 4 !! 17) = (ptr !! 19 \<and> \<not> mask 6 !! 19 \<and> mask 14 !! 19) \<and> (ptr !! 20 \<and> mask 14 !! 20 \<and> \<not> mask 4 !! 18) = (ptr !! 20 \<and> \<not> mask 6 !! 20 \<and> mask 14 !! 20) \<and> (ptr !! 21 \<and> mask 14 !! 21 \<and> \<not> mask 4 !! 19) = (ptr !! 21 \<and> \<not> mask 6 !! 21 \<and> mask 14 !! 21) \<and> (ptr !! 22 \<and> mask 14 !! 22 \<and> \<not> mask 4 !! 20) = (ptr !! 22 \<and> \<not> mask 6 !! 22 \<and> mask 14 !! 22) \<and> (ptr !! 23 \<and> mask 14 !! 23 \<and> \<not> mask 4 !! 21) = (ptr !! 23 \<and> \<not> mask 6 !! 23 \<and> mask 14 !! 23) \<and> (ptr !! 24 \<and> mask 14 !! 24 \<and> \<not> mask 4 !! 22) = (ptr !! 24 \<and> \<not> mask 6 !! 24 \<and> mask 14 !! 24) \<and> (ptr !! 25 \<and> mask 14 !! 25 \<and> \<not> mask 4 !! 23) = (ptr !! 25 \<and> \<not> mask 6 !! 25 \<and> mask 14 !! 25) \<and> (ptr !! 26 \<and> mask 14 !! 26 \<and> \<not> mask 4 !! 24) = (ptr !! 26 \<and> \<not> mask 6 !! 26 \<and> mask 14 !! 26) \<and> (ptr !! 27 \<and> mask 14 !! 27 \<and> \<not> mask 4 !! 25) = (ptr !! 27 \<and> \<not> mask 6 !! 27 \<and> mask 14 !! 27) \<and> (ptr !! 28 \<and> mask 14 !! 28 \<and> \<not> mask 4 !! 26) = (ptr !! 28 \<and> \<not> mask 6 !! 28 \<and> mask 14 !! 28) \<and> (ptr !! 29 \<and> mask 14 !! 29 \<and> \<not> mask 4 !! 27) = (ptr !! 29 \<and> \<not> mask 6 !! 29 \<and> mask 14 !! 29) \<and> (ptr !! 30 \<and> mask 14 !! 30 \<and> \<not> mask 4 !! 28) = (ptr !! 30 \<and> \<not> mask 6 !! 30 \<and> mask 14 !! 30) \<and> (ptr !! 31 \<and> mask 14 !! 31 \<and> \<not> mask 4 !! 29) = (ptr !! 31 \<and> \<not> mask 6 !! 31 \<and> mask 14 !! 31) proof (prove)
goal:
No subgoals!