diff --git a/Arm/MemoryProofs.lean b/Arm/MemoryProofs.lean
index 13ca9e86..44eca53c 100644
--- a/Arm/MemoryProofs.lean
+++ b/Arm/MemoryProofs.lean
@@ -7,8 +7,9 @@ import Arm.SeparateProofs
 import Arm.FromMathlib
 -- import Auto
 
--- In this file, we have memory (non-)interference proofs that depend
--- on auto.
+-- In this file, we have memory (non-)interference proofs. Many of
+-- these are skipped right now as we eliminate our dependency on auto
+-- (and SMT solving).
 
 -- set_option auto.smt true
 -- set_option auto.smt.trust true
@@ -33,8 +34,10 @@ theorem mem_separate_preserved_second_start_addr_add_one
   (h2 : mem_separate a b c (c + m#64)) :
   mem_separate a b (c + 1#64) (c + m#64) := by
   rw [mem_separate_for_subset2 h2]
-  unfold mem_subset; simp
-  simp [BitVec.le_of_eq]
+  unfold mem_subset;
+  simp only [Nat.reducePow, Nat.succ_sub_succ_eq_sub, Nat.sub_zero,
+             Bool.or_eq_true, decide_eq_true_eq, Bool.and_eq_true]
+  simp only [BitVec.le_of_eq, true_and]
   rw [BitVec.add_sub_self_left_64 c m#64]
   rw [BitVec.add_sub_self_left_64 c 1#64]
   apply Or.inr
@@ -46,18 +49,19 @@ theorem read_mem_of_write_mem_bytes_different (hn1 : n <= 2^64)
   read_mem addr1 (write_mem_bytes n addr2 v s) = read_mem addr1 s := by
   by_cases hn0 : n = 0
   case pos => -- n = 0
-    subst n; simp [write_mem_bytes]
+    subst n; simp only [write_mem_bytes]
   case neg => -- n ≠ 0
     have hn0' : 0 < n := by omega
     induction n, hn0' using Nat.le_induction generalizing addr2 s
     case base =>
       have h' : addr1 ≠ addr2 := by apply mem_separate_starting_addresses_neq h
-      simp [write_mem_bytes]
+      simp only [write_mem_bytes]
       apply read_mem_of_write_mem_different h'
     case succ =>
       have h' : addr1 ≠ addr2 := by refine mem_separate_starting_addresses_neq h
       rename_i m hn n_ih
-      simp_all [write_mem_bytes]
+      simp_all only [Nat.succ_sub_succ_eq_sub, Nat.sub_zero, Nat.succ_ne_zero,
+                     not_false_eq_true, ne_eq, write_mem_bytes, Nat.add_eq, Nat.add_zero]
       rw [n_ih]
       · rw [read_mem_of_write_mem_different h']
       · omega
@@ -84,30 +88,32 @@ theorem read_mem_bytes_of_write_mem_bytes_same (hn1 : n <= 2^64) :
   case pos =>
     subst n
     unfold read_mem_bytes
-    simp [BitVec.bitvec_zero_is_unique]
+    simp only [of_length_zero]
   case neg => -- n ≠ 0
    have hn0' : 0 < n := by omega
    induction n, hn0' using Nat.le_induction generalizing addr s
    case base =>
-     simp [read_mem_bytes, write_mem_bytes, read_mem_of_write_mem_same]
+     simp only [read_mem_bytes, write_mem_bytes,
+                read_mem_of_write_mem_same, BitVec.cast_eq]
      have l1 := BitVec.extractLsb_eq v
-     simp at l1
+     simp only [Nat.reduceSucc, Nat.one_mul, Nat.succ_sub_succ_eq_sub,
+                Nat.sub_zero, Nat.reduceAdd, BitVec.cast_eq, forall_const] at l1
      rw [l1]
      have l2 := BitVec.empty_bitvector_append_left v
-     simp at l2
+     simp only [Nat.reduceSucc, Nat.one_mul, Nat.zero_add, BitVec.cast_eq, forall_const] at l2
      exact l2
    case succ =>
      rename_i n hn n_ih
-     simp [read_mem_bytes, write_mem_bytes]
+     simp only [read_mem_bytes, Nat.add_eq, Nat.add_zero, write_mem_bytes]
      rw [n_ih]
      rw [read_mem_of_write_mem_bytes_different]
-     · simp [read_mem_of_write_mem_same]
+     · simp only [Nat.add_eq, Nat.add_zero, read_mem_of_write_mem_same]
        rw [append_byte_of_extract_rest_same_cast n v hn]
      · omega
      · have := mem_separate_contiguous_regions addr 0#64 (n - 1)#64
-       simp [BitVec.add_zero, BitVec.sub_zero] at this
+       simp only [Nat.reducePow, Nat.succ_sub_succ_eq_sub, Nat.sub_zero, BitVec.sub_zero, ofNat_lt_ofNat, Nat.reduceMod, BitVec.add_zero] at this
        apply this
-       simp at hn1
+       simp only [Nat.reducePow] at hn1
        omega
      · omega
      · omega
@@ -124,18 +130,19 @@ theorem read_mem_bytes_of_write_mem_bytes_different
   read_mem_bytes n1 addr1 s := by
   by_cases h1 : n1 = 0
   case pos =>
-    subst n1; simp [read_mem_bytes]
+    subst n1; simp only [read_mem_bytes]
   case neg => -- n1 ≠ 0
    have h1' : 0 < n1 := by omega
    induction n1, h1' using Nat.le_induction generalizing addr1 s
    case base =>
-     simp [read_mem_bytes]
+     simp only [read_mem_bytes, BitVec.cast_eq]
      rw [read_mem_of_write_mem_bytes_different hn2]
-     simp at h; exact h
+     simp only [Nat.reduceSucc, Nat.succ_sub_succ_eq_sub, Nat.sub_self, BitVec.add_zero] at h
+     exact h
    case succ =>
      rename_i n1 hn n_ih
-     simp [read_mem_bytes]
-     simp [Nat.add_sub_cancel] at h
+     simp only [read_mem_bytes, Nat.add_eq, Nat.add_zero]
+     simp only [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at h
      rw [read_mem_of_write_mem_bytes_different hn2]
      · rw [n_ih]
        · omega
@@ -156,12 +163,12 @@ theorem write_mem_of_write_mem_commute
   (h : mem_separate addr2 addr2 addr1 addr1) :
   write_mem addr2 val2 (write_mem addr1 val1 s) =
   write_mem addr1 val1 (write_mem addr2 val2 s) := by
-  simp_all [write_mem]
+  simp_all only [write_mem, ArmState.mk.injEq, and_self, and_true, true_and]
   unfold write_store
   have := @mem_separate_starting_addresses_neq addr2 addr2 addr1 addr1
   simp [h] at this
   funext x
-  split <;> simp_all
+  split <;> simp_all only [ite_false]
   done
 
 theorem write_mem_of_write_mem_bytes_commute
@@ -170,21 +177,21 @@ theorem write_mem_of_write_mem_bytes_commute
   write_mem addr2 val2 (write_mem_bytes n addr1 val1 s) =
   write_mem_bytes n addr1 val1 (write_mem addr2 val2 s) := by
   by_cases h : n = 0
-  case pos => subst n; simp [write_mem_bytes]
+  case pos => subst n; simp only [write_mem_bytes]
   case neg => -- n ≠ 0
     have h' : 0 < n := by omega
     induction n, h' using Nat.le_induction generalizing addr1 addr2 val2 s
     case base =>
-      simp_all [write_mem_bytes]
+      simp_all only [Nat.succ_sub_succ_eq_sub, Nat.sub_self, BitVec.add_zero, Nat.succ_ne_zero, not_false_eq_true, write_mem_bytes]
       rw [write_mem_of_write_mem_commute]; assumption
     case succ =>
       rename_i n' h' n_ih
-      simp [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at h1
-      simp [write_mem_bytes]
+      simp only [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at h1
+      simp only [write_mem_bytes, Nat.add_eq, Nat.add_zero]
       rw [n_ih]
       · rw [write_mem_of_write_mem_commute]
         rw [mem_separate_for_subset2 h1]
-        simp [first_address_is_subset_of_region]
+        simp only [first_address_is_subset_of_region]
       · omega
       · rw [@mem_separate_for_subset2 addr2 addr2 addr1 (addr1 + n'#64)]
         · assumption
@@ -201,23 +208,24 @@ theorem write_mem_bytes_of_write_mem_bytes_commute
   write_mem_bytes n1 addr1 val1 (write_mem_bytes n2 addr2 val2 s) := by
   by_cases h_n1 : n1 = 0
   case pos => -- (n1 = 0)
-    subst n1; simp [write_mem_bytes]
+    subst n1; simp only [write_mem_bytes]
   case neg => -- (n1 ≠ 0)
     induction n2 generalizing n1 addr1 addr2 val1 s
-    case zero => simp [write_mem_bytes]
+    case zero => simp only [write_mem_bytes]
     case succ =>
       rename_i n n_ih
       by_cases hn0 : n = 0
-      case pos =>
-        subst n; simp [write_mem_bytes]
+      case pos => -- (n = 0)
+        subst n; simp only [write_mem_bytes]
         rw [write_mem_of_write_mem_bytes_commute h1]
-        simp at h3; exact h3
+        simp only [Nat.reduceSucc, Nat.succ_sub_succ_eq_sub, Nat.sub_self, BitVec.add_zero] at h3
+        exact h3
       case neg => -- (n ≠ 0)
-        simp at h3
-        conv in write_mem_bytes (n + 1) => simp [write_mem_bytes]
+        simp only [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at h3
+        conv in write_mem_bytes (n + 1) => simp only [write_mem_bytes]
         rw [write_mem_of_write_mem_bytes_commute h1]
         · rw [n_ih h1]
-          · conv in write_mem_bytes (n + 1) => simp [write_mem_bytes]
+          · conv in write_mem_bytes (n + 1) => simp only [write_mem_bytes]
           · omega
           · rw [mem_separate_for_subset1 h3]
             have := @mem_subset_same_region_lemma n addr2
@@ -236,10 +244,10 @@ theorem write_mem_bytes_of_write_mem_bytes_shadow_same_region
   write_mem_bytes n addr val2 (write_mem_bytes n addr val1 s) =
   write_mem_bytes n addr val2 s := by
   induction n generalizing addr s
-  case zero => simp [write_mem_bytes]
+  case zero => simp only [write_mem_bytes]
   case succ =>
     rename_i n' n_ih
-    simp [write_mem_bytes]
+    simp only [write_mem_bytes]
     rw [@write_mem_of_write_mem_bytes_commute n' addr]
     · rw [write_mem_of_write_mem_shadow]
       rw [n_ih]; omega
@@ -254,22 +262,22 @@ theorem write_mem_bytes_of_write_mem_bytes_shadow_same_first_address
   write_mem_bytes n2 addr val2 s := by
   by_cases h : n1 = 0
   case pos =>
-    subst n1; simp [write_mem_bytes]
+    subst n1; simp only [write_mem_bytes]
   case neg => -- n1 ≠ 0
     induction n2, h2l using Nat.le_induction generalizing n1 addr val1 s
     case base => -- (n1 ≠ 0) and (n2 = 1)
       -- n1 must also be 1, given h3. So this case reduces to shadowing
       -- of exactly one write.
-      simp at h3
+      simp only [Nat.reduceSucc, Nat.succ_sub_succ_eq_sub, Nat.sub_self, BitVec.add_zero] at h3
       have h1u' : n1 - 1 < 2^64 := by omega
       have h0 := @mem_subset_one_addr_region_lemma_alt (n1 - 1) addr addr h1u'
-      simp [h3] at h0
+      simp only [h3, and_true, forall_const] at h0
       have : n1 = 1 := by omega
       subst_vars
-      simp [write_mem_bytes, write_mem_of_write_mem_shadow]
+      simp only [write_mem_bytes, write_mem_of_write_mem_shadow]
     case succ =>
       rename_i n hnl' n_ih
-      conv in write_mem_bytes (n + 1) => simp [write_mem_bytes]
+      conv in write_mem_bytes (n + 1) => simp only [write_mem_bytes, Nat.add_eq, Nat.add_zero]
       conv in write_mem_bytes n1 addr .. => unfold write_mem_bytes
       split
       · contradiction
@@ -280,11 +288,11 @@ theorem write_mem_bytes_of_write_mem_bytes_shadow_same_first_address
           by_cases hn' : n' = 0
           case pos =>
             subst_vars
-            simp [write_mem_bytes]
+            simp only [write_mem_bytes, Nat.add_eq, Nat.add_zero]
           case neg => -- n' ≠ 0
             rw [n_ih (by omega) (by omega) _ hn']
-            · conv in write_mem_bytes (n + 1) .. => simp [write_mem_bytes]
-            · simp [Nat.succ_eq_add_one] at h3
+            · conv in write_mem_bytes (n + 1) .. => simp only [write_mem_bytes, Nat.add_eq, Nat.add_zero]
+            · simp only [Nat.succ_eq_add_one, Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at h3
               rw [addr_add_one_add_m_sub_one n' addr (by omega) h1u]
               rw [addr_add_one_add_m_sub_one n addr (by omega) h2u]
               rw [first_addresses_add_one_preserves_subset_same_addr
@@ -301,18 +309,18 @@ private theorem mem_subset_neq_first_addr_small_second_region
   (h_addr : ¬addr1 = addr2) :
   mem_subset addr1 (addr1 + (n1 - 1)#64) (addr2 + 1#64) (addr2 + n'#64) := by
   have : 2^64 - 1 = 18446744073709551615 := by decide
-  simp_all [mem_subset, lt_and_bitvec_lt, le_and_bitvec_le]
+  simp_all only [mem_subset, Bool.decide_eq_true, Bool.or_eq_true, decide_eq_true_eq, Bool.and_eq_true]
   cases h2
   · rename_i h
     simp [BitVec.add_sub_self_left_64] at h
     have l1 : n' = 18446744073709551615 := by
       rw [BitVec.toNat_eq n'#64 18446744073709551615#64] at h
-      simp [BitVec.bitvec_to_nat_of_nat] at h
+      simp only [toNat_ofNat, Nat.reducePow, Nat.reduceMod] at h
       omega
     simp [l1] at h1
   · rename_i h
-    apply Or.inr
-    sorry -- auto
+    bv_omega
+    done
 
 private theorem write_mem_bytes_of_write_mem_bytes_shadow_general_n2_lt
   (h1u : n1 <= 2^64) (h2l : 0 < n2) (h2u : n2 < 2^64)
@@ -321,23 +329,24 @@ private theorem write_mem_bytes_of_write_mem_bytes_shadow_general_n2_lt
   write_mem_bytes n2 addr2 val2 s := by
   by_cases h : n1 = 0
   case pos =>
-    subst n1; simp [write_mem_bytes]
+    subst n1; simp only [write_mem_bytes]
   case neg => -- n1 ≠ 0
     induction n2, h2l using Nat.le_induction generalizing addr1 addr2 val1 s
     case base =>
       have h1u' : n1 - 1 < 2^64 := by omega
-      simp_all [write_mem_bytes]
+      simp_all only [Nat.one_lt_two_pow_iff, ne_eq, Nat.succ_ne_zero, not_false_eq_true, Nat.succ_sub_succ_eq_sub,
+  Nat.sub_self, BitVec.add_zero, write_mem_bytes]
       have h0 := @mem_subset_one_addr_region_lemma_alt (n1 - 1) addr1 addr2 h1u'
-      simp [h3] at h0
+      simp only [h3, forall_const] at h0
       have ⟨h₀, h₁⟩ := h0
       have : n1 = 1 := by omega
       subst_vars
-      simp [write_mem_bytes, write_mem_of_write_mem_shadow]
+      simp only [write_mem_bytes, write_mem_of_write_mem_shadow]
     case succ =>
       rename_i n' hn' ihn'
       have h_sep : mem_separate addr2 addr2 (addr2 + 1#64) (addr2 + 1#64 + (n' - 1)#64) := by
           have :=  mem_separate_contiguous_regions addr2 0#64 (n' - 1)#64
-          simp [BitVec.sub_zero, BitVec.add_zero] at this
+          simp only [Nat.reducePow, Nat.succ_sub_succ_eq_sub, Nat.sub_zero, BitVec.sub_zero, ofNat_lt_ofNat, Nat.reduceMod, BitVec.add_zero] at this
           rw [this]
           exact n_minus_1_lt_2_64_1 n' hn' (by omega)
           done
@@ -352,7 +361,7 @@ private theorem write_mem_bytes_of_write_mem_bytes_shadow_general_n2_lt
       case neg => -- addr1 ≠ addr2
        repeat (conv =>
                 pattern write_mem_bytes (n' + 1) ..
-                simp [write_mem_bytes])
+                simp only [write_mem_bytes, Nat.add_eq, Nat.add_zero])
        rw [←write_mem_of_write_mem_bytes_commute (by omega)]
        · rw [ihn' (by omega)]
          · rw [write_mem_of_write_mem_bytes_commute (by omega)]
@@ -371,25 +380,25 @@ theorem write_mem_bytes_of_write_mem
   write_mem_bytes n addr2 val2 s := by
   induction n, h0 using Nat.le_induction generalizing addr1 addr2 val1 s
   case base =>
-    simp [write_mem_bytes]
+    simp only [write_mem_bytes]
     by_cases h₀ : addr1 = addr2
     case pos => -- (addr1 = addr2)
       subst addr2
-      simp [write_mem_of_write_mem_shadow]
+      simp only [write_mem_of_write_mem_shadow]
     case neg => -- (addr1 ≠ addr2)
-      simp at h2
-      simp_all [mem_subset_eq]
+      simp only [Nat.reduceSucc, Nat.succ_sub_succ_eq_sub, Nat.sub_self, BitVec.add_zero] at h2
+      simp_all only [mem_subset_eq]
   case succ =>
     rename_i n' hn' n_ih
-    simp [write_mem_bytes]
+    simp only [write_mem_bytes, Nat.add_eq, Nat.add_zero]
     by_cases h₀ : addr1 = addr2
     case pos => -- (addr1 = addr2)
       subst addr2
-      simp [write_mem_of_write_mem_shadow]
+      simp only [write_mem_of_write_mem_shadow]
     case neg =>
       rw [write_mem_of_write_mem_commute]
       · rw [n_ih (by omega)]
-        simp at h2
+        simp only [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at h2
         rw [addr_add_one_add_m_sub_one n' addr2 hn' h1]
         rw [mem_subset_one_addr_neq h₀]
         assumption
@@ -405,25 +414,25 @@ private theorem write_mem_bytes_of_write_mem_bytes_shadow_general_n2_eq
   by_cases h₀ : n1 = 0
   case pos =>
     subst n1
-    simp [write_mem_bytes]
+    simp only [write_mem_bytes]
   case neg => -- ¬(n1 = 0)
     induction n1 generalizing addr1 val2 s
     case zero =>
-      conv in write_mem_bytes 0 _ _ => simp [write_mem_bytes]
+      conv in write_mem_bytes 0 _ _ => simp only [write_mem_bytes]
     case succ =>
       rename_i n n_ih
-      conv in write_mem_bytes (Nat.succ n) .. => simp [write_mem_bytes]
+      conv in write_mem_bytes (Nat.succ n) .. => simp only [write_mem_bytes]
       have n_ih' := @n_ih (addr1 + 1#64) val2 (zeroExtend (n * 8) (val1 >>> 8))
                    (write_mem addr1 (extractLsb 7 0 val1) s)
                    (by omega)
-      simp at h3
+      simp only [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at h3
       by_cases h₁ : n = 0
       case pos =>
         subst n
-        simp [write_mem_bytes]
+        simp only [write_mem_bytes]
         rw [write_mem_bytes_of_write_mem h2l]
         · omega
-        · simp at h3; assumption
+        · simp only [BitVec.add_zero] at h3; exact h3
       case neg => -- ¬(n = 0)
         rw [n_ih']
         · rw [write_mem_bytes_of_write_mem h2l]
@@ -433,14 +442,14 @@ private theorem write_mem_bytes_of_write_mem_bytes_shadow_general_n2_eq
           · have l0 := @mem_subset_trans
                         (addr1 + 1#64) (addr1 + n#64) addr1 (addr1 + n#64)
                         addr2 (addr2 + (n2 - 1)#64)
-            simp [h3] at l0
+            simp only [h3, forall_const] at l0
             rw [first_addresses_add_one_is_subset_of_region_general] at l0
-            simp at l0
+            simp only [forall_const] at l0
             · assumption
             · omega
             · omega
             · omega
-            · simp [mem_subset_refl]
+            · simp only [mem_subset_refl]
           · omega
           · omega
         · exact h₁
@@ -452,10 +461,10 @@ theorem write_mem_bytes_of_write_mem_bytes_shadow_general
   write_mem_bytes n2 addr2 val2 (write_mem_bytes n1 addr1 val1 s) =
   write_mem_bytes n2 addr2 val2 s := by
   by_cases h : n2 = 2^64
-  case pos => simp_all [write_mem_bytes_of_write_mem_bytes_shadow_general_n2_eq]
+  case pos => simp_all only [write_mem_bytes_of_write_mem_bytes_shadow_general_n2_eq, Nat.le_refl]
   case neg =>
     have h' : n2 < 2^64 := by omega
-    simp_all [write_mem_bytes_of_write_mem_bytes_shadow_general_n2_lt]
+    simp_all only [write_mem_bytes_of_write_mem_bytes_shadow_general_n2_lt]
   done
 
 ----------------------------------------------------------------------
@@ -465,11 +474,11 @@ theorem read_mem_of_write_mem_bytes_same_first_address
   (h0 : 0 < n) (h1 : n <= 2^64) (h : 7 - 0 + 1 = 8) :
   read_mem addr (write_mem_bytes n addr val s) =
   BitVec.cast h (extractLsb 7 0 val) := by
-  unfold write_mem_bytes; simp
+  unfold write_mem_bytes; simp only [Nat.sub_zero, BitVec.cast_eq]
   split
   · contradiction
   · rw [←write_mem_of_write_mem_bytes_commute (by exact Nat.le_of_lt h1)]
-    · simp [read_mem_of_write_mem_same]
+    · simp only [read_mem_of_write_mem_same]
     · rw [mem_separate_contiguous_regions_one_address addr h1]
   done
 
@@ -489,35 +498,36 @@ theorem read_mem_bytes_of_write_mem_bytes_subset_same_first_address
   read_mem_bytes n2 addr (write_mem_bytes n1 addr val s) =
   BitVec.cast h (extractLsb ((n2 * 8) - 1) 0 val) := by
   have rm_lemma := @read_mem_of_write_mem_bytes_same_first_address n1 addr val s h0 h1
-  simp at rm_lemma
+  simp only [Nat.sub_zero, Nat.reduceAdd, BitVec.cast_eq, forall_const] at rm_lemma
   induction n2, h2 using Nat.le_induction generalizing n1 addr val s
   case base =>
-    simp [read_mem_bytes, rm_lemma]
+    simp only [read_mem_bytes, rm_lemma, BitVec.cast_eq, Nat.sub_zero]
     apply BitVec.empty_bitvector_append_left
     decide
   case succ =>
     rename_i n hmn n_ih
-    simp [read_mem_bytes, rm_lemma]
-    unfold write_mem_bytes; simp
+    simp only [read_mem_bytes, Nat.add_eq, Nat.add_zero, rm_lemma, Nat.sub_zero, BitVec.cast_eq]
+    unfold write_mem_bytes; simp only [Nat.add_eq, Nat.add_zero]
     split
     · contradiction
     · rename_i i _ n1_1 v
-      simp at h4
+      simp only [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at h4
       by_cases hn1_1 : n1_1 = 0
       case pos =>
         subst n1_1
-        simp at h4
+        simp only [BitVec.add_zero] at h4
         have := mem_subset_one_addr_region_lemma_alt addr addr h3
-        simp [h4] at this
+        simp only [h4, and_true, forall_const] at this
         subst n
-        simp [write_mem_bytes, read_mem_bytes, read_mem_of_write_mem_same]
-        apply BitVec.empty_bitvector_append_left; simp
+        simp only [Nat.add_eq, Nat.add_zero, read_mem_bytes, BitVec.cast_eq]
+        apply BitVec.empty_bitvector_append_left
+        simp only [Nat.zero_mul, Nat.zero_add]
         done
       case neg =>
         have hn := mem_subset_same_address_different_sizes h4
         have hn' : n <= n1_1 := by
           rw [BitVec.le_iff_val_le_val] at hn
-          simp [BitVec.bitvec_to_nat_of_nat] at hn
+          simp only [toNat_ofNat, Nat.reducePow] at hn
           -- TODO `erw` should not be needed here after the 2^64 simproc is disabled.
           erw [Nat.mod_eq_of_lt h3] at hn
           erw [Nat.mod_eq_of_lt h1] at hn
@@ -525,7 +535,7 @@ theorem read_mem_bytes_of_write_mem_bytes_subset_same_first_address
         rw [n_ih (by omega) (by omega) (by omega) _ (by omega)]
         · rw [BitVec.extract_lsb_of_zeroExtend (v >>> 8)]
           · have l1 := @BitVec.append_of_extract_general ((n1_1 + 1) * 8) 8 (n*8-1+1) (n*8) v
-            simp (config := {decide := true}) at l1
+            simp (config := { decide := true }) only [Nat.zero_lt_succ, Nat.mul_pos_iff_of_pos_left, Nat.succ_sub_succ_eq_sub, Nat.sub_zero, Nat.reduceAdd, Nat.succ.injEq, forall_const] at l1
             rw [l1 (by omega) (by omega)]
             · simp only [Nat.add_eq, Nat.sub_zero, BitVec.cast_cast]
               apply @cast_of_extract_eq ((n1_1 + 1) * 8) (n * 8 - 1 + 1 + 7) ((n + 1) * 8 - 1) 0 0 <;>
@@ -535,8 +545,8 @@ theorem read_mem_bytes_of_write_mem_bytes_subset_same_first_address
                               n1_1 (addr + 1#64)
                               (zeroExtend (n1_1 * 8) (v >>> 8))
                               (write_mem addr (extractLsb 7 0 v) s)
-          simp at rw_lemma2
-          rw [rw_lemma2 (by omega) (by simp at h1; omega)]
+          simp only [Nat.reducePow, Nat.sub_zero, Nat.reduceAdd, BitVec.cast_eq, forall_const] at rw_lemma2
+          rw [rw_lemma2 (by omega) (by simp only [Nat.reducePow] at h1; omega)]
         · rw [addr_add_one_add_m_sub_one n addr hmn h3]
           rw [addr_add_one_add_m_sub_one n1_1 addr (by omega) (by omega)]
           rw [first_addresses_add_one_preserves_subset_same_addr hmn h3 _ h1]
@@ -566,46 +576,45 @@ private theorem read_mem_of_write_mem_bytes_subset_helper_3 (a : Nat) (h1 : 0 <
  done
 
 private theorem read_mem_of_write_mem_bytes_subset_helper_4
-  (v a : Nat) (h_v_size : v < 2 ^ ((n' + 1) * 8)) (h_a_base : a ≠ 0) (h_a_size : a < 2 ^ 64) :
-  (v >>> 8 % 2 ^ ((n' + 1) * 8) % 2 ^ (n' * 8)) >>> ((a + (2 ^ 64 - 1)) % 2 ^ 64 * 8) % 2 ^ 8 = v >>> (a * 8) % 2 ^ 8 := by
-  apply Nat.eq_of_testBit_eq
-  intro i
+  (v a n' : Nat) (h_v_size : v < 2 ^ ((n' + 1) * 8)) (h_a_base : a ≠ 0) (h_a_size : a < 2 ^ 64) :
+  (v >>> 8 % 2 ^ (n' * 8)) >>> ((a + (2 ^ 64 - 1)) % 2 ^ 64 * 8) % 2 ^ 8 = v >>> (a * 8) % 2 ^ 8 := by
+  apply Nat.eq_of_testBit_eq; intro i
   simp only [Nat.testBit_mod_two_pow]
-  by_cases h₂ : i < 8
-  case pos => -- (i < 8)
-    simp only [h₂, Nat.testBit_shiftRight, Nat.testBit_mod_two_pow]
-    by_cases h₃ : ((a + (2 ^ 64 - 1)) % 2 ^ 64 * 8 + i < n' * 8)
+  by_cases h₀ : i < 8
+  case pos => -- i < 8
+    simp only [h₀, Nat.testBit_shiftRight, Nat.testBit_mod_two_pow, decide_True, Bool.and_true, Bool.true_and]
+    by_cases h₁ : ((a + (2 ^ 64 - 1)) % 2 ^ 64 * 8 + i < n' * 8)
     case pos => -- (i < 8) and ((a + (2 ^ 64 - 1)) % 2 ^ 64 * 8 + i < n' * 8)
-      simp only [h₃]
+      simp only [h₁, decide_True, Bool.and_true, Bool.true_and]
       rw [read_mem_of_write_mem_bytes_subset_helper_1]
-      · have := read_mem_of_write_mem_bytes_subset_helper_2
-                 ((a + (2 ^ 64 - 1)) % 2 ^ 64 * 8 + i) n' h₃
-        simp only [this]
-        simp
       · exact Nat.pos_of_ne_zero h_a_base
       · exact h_a_size
-    case neg => -- (i < 8) and (not ((a + (2 ^ 64 - 1)) % 2 ^ 64 * 8 + i < n' * 8))
-      simp only [h₃]
-      rw [read_mem_of_write_mem_bytes_subset_helper_3 a (Nat.pos_of_ne_zero h_a_base) h_a_size] at h₃
-      simp at h₃
+    case neg => -- (i < 8) and ¬((a + (2 ^ 64 - 1)) % 2 ^ 64 * 8 + i < n' * 8)
+      simp only [h₁, decide_False, Bool.false_and]
+      rw [read_mem_of_write_mem_bytes_subset_helper_3 a (Nat.pos_of_ne_zero h_a_base) h_a_size] at h₁
+      simp only [Nat.not_lt] at h₁
       have : (n' + 1) * 8 ≤ a * 8 + i := by omega
-      simp
       rw [Nat.testBit_lt_two_pow]
       exact calc
         _ < 2 ^ ((n' + 1) * 8) := by exact h_v_size
         _ <= 2 ^ (a * 8 + i) := by apply Nat.pow_le_pow_right; decide; exact this
       done
-  case neg => simp [h₂]
+  case neg => -- ¬(i < 8)
+    simp only [h₀, decide_False, Bool.false_and]
   done
 
--- (FIXME) Prove without omega and for general bitvectors.
+theorem read_mem_of_write_mem_bytes_subset_helper_5 (a x y : Nat) :
+  (((a + x) % y + 1) * 8 - 1 - (a + x) % y * 8 + 1) = 8 := by
+  omega
+
+-- (FIXME) Prove for general bitvectors.
 theorem BitVec.to_nat_zero_lt_sub_64 (x y : BitVec 64) (h : ¬x = y) :
   (x - y).toNat ≠ 0 := by
   simp only [BitVec.toNat_sub]
   simp only [toNat_eq] at h
   have := x.toNat_lt
   have := y.toNat_lt
-  simp_all
+  simp_all only [ne_eq]
   omega
 
 theorem read_mem_of_write_mem_bytes_subset
@@ -621,52 +630,52 @@ theorem read_mem_of_write_mem_bytes_subset
       val) := by
   induction n generalizing addr1 addr2 s
   case zero => contradiction
-  -- case succ =>
-  -- -- FIXME
-  --   rename_i n' n_ih
-  --   simp_all [write_mem_bytes]
-  --   have cast_lemma := @cast_of_extract_eq
-  --   by_cases h₀ : n' = 0
-  --   case pos =>
-  --     simp_all [mem_subset_eq]
-  --     subst_vars
-  --     simp [write_mem_bytes, read_mem_of_write_mem_same]
-  --     rw [←cast_lemma] <;> simp
-  --   case neg => -- (n' ≠ 0)
-  --     by_cases h₁ : addr2 = addr1
-  --     case pos => -- (n' ≠ 0) and (addr2 = addr1)
-  --       subst_vars
-  --       rw [read_mem_of_write_mem_bytes_different (by omega)]
-  --       · simp [read_mem_of_write_mem_same]
-  --         rw [←cast_lemma] <;> simp
-  --       · rw [mem_separate_contiguous_regions_one_address _ (by omega)]
-  --     case neg => -- (addr2 ≠ addr1)
-  --       rw [n_ih]
-  --       · ext
-  --         simp [toNat_cast, extractLsb, extractLsb']
-  --         simp [BitVec.bitvec_to_nat_of_nat, toNat_zeroExtend]
-  --         simp [HShiftRight.hShiftRight, ushiftRight, ShiftRight.shiftRight,
-  --               BitVec.bitvec_to_nat_of_nat]
-  --         simp [BitVec.sub_of_add_is_sub_sub]
-  --         have h_sub := BitVec.nat_bitvec_sub (addr2 - addr1) 1#64
-  --         simp [BitVec.bitvec_to_nat_of_nat, Nat.mod_eq_of_lt] at h_sub
-  --         simp [h_sub]
-  --         have h_a_size := (addr2 - addr1).isLt
-  --         have h_v_size := val.isLt
-  --         have h_a_base := BitVec.to_nat_zero_lt_sub_64 addr2 addr1 h₁
-  --         generalize BitVec.toNat val = v at h_v_size
-  --         generalize BitVec.toNat (addr2 - addr1) = a at h_a_size h_a_base
-  --         rw [read_mem_of_write_mem_bytes_subset_helper_4]
-  --         exact h_v_size
-  --         exact h_a_base
-  --         exact h_a_size
-  --       · omega
-  --       · omega
-  --       · rw [addr_add_one_add_m_sub_one _ _ (by omega) (by omega)]
-  --         rw [mem_subset_one_addr_neq h₁ h2]
-  --       · omega
-  --   done
-  sorry
+  case succ =>
+    rename_i n' n_ih
+    simp_all only [write_mem_bytes, Nat.succ.injEq, Nat.zero_lt_succ, Nat.succ_sub_succ_eq_sub, Nat.sub_zero]
+    have cast_lemma := @cast_of_extract_eq
+    by_cases h₀ : n' = 0
+    case pos =>
+      simp_all only [Nat.lt_irrefl, Nat.zero_le, Nat.zero_sub, BitVec.add_zero, mem_subset_eq, forall_const, false_implies, implies_true]
+      subst_vars
+      simp only [write_mem_bytes, read_mem_of_write_mem_same]
+      rw [←cast_lemma] <;> bv_omega
+    case neg => -- (n' ≠ 0)
+      by_cases h₁ : addr2 = addr1
+      case pos => -- (n' ≠ 0) and (addr2 = addr1)
+        subst_vars
+        rw [read_mem_of_write_mem_bytes_different (by omega)]
+        · simp only [read_mem_of_write_mem_same]
+          rw [←cast_lemma] <;> bv_omega
+        · rw [mem_separate_contiguous_regions_one_address _ (by omega)]
+      case neg => -- (addr2 ≠ addr1)
+        rw [n_ih]
+        · ext
+          -- simp only [bv_toNat]
+          simp only [toNat_cast, extractLsb, extractLsb', toNat_zeroExtend]
+          simp only [toNat_ushiftRight]
+          simp_all only [toNat_ofNat, toNat_ofNatLt]
+          simp only [BitVec.sub_of_add_is_sub_sub, Nat.succ_sub_succ_eq_sub, Nat.mod_eq_of_lt, Nat.reduceLT, Nat.mod_add_mod, Nat.sub_zero]
+          have h_sub := BitVec.toNat_sub (addr2 - addr1) 1#64
+          simp only [toNat_ofNat] at h_sub
+          simp only [h_sub]
+          have h_a_size := (addr2 - addr1).isLt
+          have h_v_size := val.isLt
+          have h_a_base := BitVec.to_nat_zero_lt_sub_64 addr2 addr1 h₁
+          generalize BitVec.toNat val = v at h_v_size
+          generalize BitVec.toNat (addr2 - addr1) = a at h_a_size h_a_base
+          have mod_lt_conc : (2 ^ 64 - 1 % 2 ^ 64) = 2 ^ 64 - 1 := by decide
+          -- (FIXME) We won't need
+          -- read_mem_of_write_mem_bytes_subset_helper_5 once we can
+          -- disable simproc for 2^64.
+          simp only [mod_lt_conc, read_mem_of_write_mem_bytes_subset_helper_5]
+          apply read_mem_of_write_mem_bytes_subset_helper_4 v a n' h_v_size h_a_base h_a_size
+        · omega
+        · omega
+        · rw [addr_add_one_add_m_sub_one _ _ (by omega) (by omega)]
+          rw [mem_subset_one_addr_neq h₁ h2]
+        · omega
+    done
 
 theorem read_mem_bytes_of_write_mem_bytes_subset_helper1 (a i : Nat)
   (h1 : a < 2^64 - 1) (h2 : 8 <= i):
@@ -679,61 +688,49 @@ theorem read_mem_bytes_of_write_mem_bytes_subset_helper2
   (addr2 addr1 : BitVec 64) (val : BitVec (n1 * 8))
   (h0 : 0 < n1) (h1 : n1 <= 2 ^ 64) (h2 : 0 < n)
   (h4 : addr1 ≠ addr2) (h5 : addr2 - addr1 < (2 ^ 64 - 1)#64) :
-  BitVec.toNat
-    ((BitVec.toNat val >>>
-      ((BitVec.toNat (addr2 - addr1) + BitVec.toNat 1#64) % 2 ^ 64 * 8))#(n * 8)
-     ++
-     (BitVec.toNat val >>> (BitVec.toNat (addr2 - addr1) * 8))#8) =
-  BitVec.toNat val >>>
-    (BitVec.toNat (addr2 - addr1) * 8) %
-      2 ^ ((BitVec.toNat (addr2 - addr1) + (n + 1)) * 8 - 1
-        - BitVec.toNat (addr2 - addr1) * 8 + 1) := by
+  (BitVec.toNat val >>> ((BitVec.toNat (addr2 - addr1) + 1) % 2 ^ 64 * 8) % 2 ^ (n * 8)) <<< 8 |||
+      BitVec.toNat val >>> (BitVec.toNat (addr2 - addr1) * 8) % 2 ^ 8 =
+    BitVec.toNat val >>> (BitVec.toNat (addr2 - addr1) * 8) %
+      2 ^ ((BitVec.toNat (addr2 - addr1) + (n + 1)) * 8 - 1 - BitVec.toNat (addr2 - addr1) * 8 + 1) := by
   have h_a_size := (addr2 - addr1).isLt
   have h_v_size := val.isLt
   -- (FIXME) whnf timeout?
   -- generalize hv : BitVec.toNat val = v at h_v_size
   -- generalize ha :  BitVec.toNat (addr2 - addr1) = a
-  apply Nat.eq_of_testBit_eq
-  intro i
+  apply Nat.eq_of_testBit_eq; intro i
   simp only [Nat.testBit_mod_two_pow, Nat.testBit_shiftRight]
-  sorry
-  -- by_cases h₀ : (i < (BitVec.toNat (addr2 - addr1) + (n + 1))
-  --                      * 8 - 1 - BitVec.toNat (addr2 - addr1) * 8 + 1)
-  -- case pos =>
-  --   simp only [h₀, BitVec.bitvec_to_nat_of_nat, BitVec.toNat_append, Nat.testBit_or]
-  --   simp only [Nat.testBit_shiftRight, Nat.testBit_mod_two_pow]
-  --   by_cases h₁ : (i < 8)
-  --   case pos => -- (i < 8)
-  --     simp [Nat.testBit_shiftLeft, Nat.testBit_mod_two_pow]
-  --     have : ¬(8 <= i) := by simp_all
-  --     simp [h₁, this]
-  --   case neg => -- ¬(i < 8)
-  --     simp [h₁]
-  --     simp [Nat.testBit_shiftLeft, Nat.testBit_mod_two_pow]
-  --     simp_all
-  --     have l1 : (i - 8 < n * 8) := by omega
-  --     simp [l1]
-  --     simp [Nat.testBit_shiftRight, Nat.testBit_mod_two_pow]
-  --     rw [read_mem_bytes_of_write_mem_bytes_subset_helper1] <;> assumption
-  -- case neg => -- ¬(i < (n + 1) * 8)
-  --   -- FIXME
-  --   simp [h₀, BitVec.bitvec_to_nat_of_nat, BitVec.toNat_append, Nat.testBit_or]
-  --   simp [Nat.testBit_shiftLeft, Nat.testBit_mod_two_pow]
-  --   by_cases h₁ : (i < 8)
-  --   case pos =>
-  --     simp at h₀
-  --     simp [h₁]
-  --     have h₁' : ¬(8 <= i) := by omega
-  --     simp [h₀, h₁']
-  --     have h₀' : (n + 1) * 8 ≤ i := by omega
-  --     rw [Nat.testBit_lt_two_pow]
-  --     omega
-  --   case neg => -- (8 <= i)
-  --     simp at h₀ h₁
-  --     simp [h₀, h₁]
-  --     have :  n * 8 ≤ i - 8 := by omega
-  --     simp [this]
-  -- done
+  by_cases h₀ : (i < (BitVec.toNat (addr2 - addr1) + (n + 1)) * 8 - 1 - BitVec.toNat (addr2 - addr1) * 8 + 1)
+  case pos =>
+    simp only [h₀, decide_True, Bool.true_and, BitVec.toNat_ofNat, BitVec.toNat_append, Nat.testBit_or]
+    simp only [Nat.testBit_shiftRight, Nat.testBit_mod_two_pow]
+    by_cases h₁ : (i < 8)
+    case pos => -- (i < 8)
+      have : ¬(8 <= i) := by omega
+      simp only [this, h₁, Nat.testBit_shiftLeft, Nat.testBit_mod_two_pow]
+      simp only [decide_False, Bool.false_and, decide_True, Bool.true_and, Bool.false_or]
+    case neg => -- ¬(i < 8)
+      simp only [h₁, decide_False, Bool.false_and, Bool.or_false]
+      simp only [Nat.testBit_shiftLeft, Nat.testBit_mod_two_pow, Nat.testBit_shiftRight]
+      simp_all only [ne_eq, Nat.not_lt, ge_iff_le, decide_True, Bool.true_and]
+      have l1 : (i - 8 < n * 8) := by omega
+      simp_all only [l1, decide_True, Bool.true_and, Nat.add_mod_mod]
+      rw [read_mem_bytes_of_write_mem_bytes_subset_helper1] <;> assumption
+  case neg =>
+    simp only [h₀, BitVec.bitvec_to_nat_of_nat, BitVec.toNat_append, Nat.testBit_or]
+    simp only [Nat.testBit_shiftLeft, Nat.testBit_mod_two_pow]
+    by_cases h₁ : (i < 8)
+    case pos => -- (i < 8)
+      have h₀' : i - 8 < n * 8 := by omega
+      have h₁' : ¬(8 <= i) := by omega
+      simp only [Nat.not_lt] at h₀
+      simp only [h₀', h₁, h₁', decide_True, decide_False, Bool.false_and, Bool.true_and, Bool.false_or]
+      rw [Nat.testBit_lt_two_pow]
+      omega
+    case neg => -- (8 <= i)
+      have :  ¬ (i - 8 < n * 8) := by omega
+      simp [h₁, this]
+  done
+
 
 -- set_option auto.smt.savepath "/tmp/mem_legal_lemma.smt2" in
 private theorem mem_legal_lemma (h0 : 0 < n) (h1 : n < 2^64)
@@ -767,76 +764,67 @@ private theorem read_mem_bytes_of_write_mem_bytes_subset_n2_lt
   read_mem_bytes n2 addr2 (write_mem_bytes n1 addr1 val s) =
    BitVec.cast h
     (extractLsb ((((addr2 - addr1).toNat + n2) * 8) - 1) ((addr2 - addr1).toNat * 8) val) := by
-  -- -- FIXME
-  -- induction n2, h2 using Nat.le_induction generalizing addr1 addr2 val s
-  -- case base =>
-  --   simp_all [read_mem_bytes]
-  --   have h' : (BitVec.toNat (addr2 - addr1) + 1) * 8 - 1 - BitVec.toNat (addr2 - addr1) * 8 + 1 = 8 := by
-  --     omega
-  --   rw [read_mem_of_write_mem_bytes_subset h0 h1 h4 h']
-  --   apply BitVec.empty_bitvector_append_left
-  --   decide
-  -- case succ =>
-  --   rename_i n h2' n_ih
-  --   by_cases h_addr : addr1 = addr2
-  --   case pos => -- (addr1 = addr2)
-  --     subst addr2
-  --     have h' : (n + 1) * 8 - 1 - 0 + 1 = (n + 1) * 8 := by omega
-  --     have := @read_mem_bytes_of_write_mem_bytes_subset_same_first_address n1 (n + 1) addr1 val s
-  --              h0 h1 (by omega) (by omega) h4 h'
-  --     rw [this]
-  --     ext; simp
-  --     -- (FIXME) painful!
-  --     conv =>
-  --       rhs
-  --       rw [BitVec.sub_self]
-  --       simp [BitVec.bitvec_to_nat_of_nat]
-  --     rw [Nat.zero_add]
-  --   case neg => -- (addr1 ≠ addr2)
-  --     simp [read_mem_bytes]
-  --     simp at h4
-  --     have h_sub : mem_subset (addr2 + 1#64) (addr2 + 1#64 + (n - 1)#64) addr1 (addr1 + (n1 - 1)#64) := by
-  --       rw [addr_add_one_add_m_sub_one]
-  --       · have l0 := @mem_subset_trans (addr2 + 1#64) (addr2 + n#64) addr2 (addr2 + n#64)
-  --                  addr1 (addr1 + (n1 - 1)#64)
-  --         simp [h4] at l0
-  --         rw [first_addresses_add_one_is_subset_of_region_general (by omega) (by omega) (by omega)] at l0
-  --         · simp_all
-  --         · simp [mem_subset_refl]
-  --       · omega
-  --       · omega
-  --     have l1 := @read_mem_of_write_mem_bytes_subset n1 addr2 addr1 val s (by omega) (by omega)
-  --     have l2 := @first_address_is_subset_of_region addr2 n#64
-  --     have l3 := mem_subset_trans l2 h4
-  --     simp [l3] at l1
-  --     rw [l1]
-  --     · simp at h5
-  --       have n_ih' := @n_ih (addr2 + 1#64) addr1 val s (by omega)
-  --       simp [h_sub] at n_ih'
-  --       rw [mem_legal_lemma h2'] at n_ih'
-  --       · simp at n_ih'
-  --         have h' : (BitVec.toNat (addr2 + 1#64 - addr1) + n) * 8 - 1 - BitVec.toNat (addr2 + 1#64 - addr1) * 8 + 1 = n * 8 := by omega
-  --         FIXME
-  --         have n_ih'' := n_ih' h6 h'
-  --         rw [n_ih'']
-  --         · ext; simp
-  --           simp [toNat_cast, extractLsb, extractLsb']
-  --           simp [BitVec.bitvec_to_nat_of_nat, toNat_zeroExtend, BitVec.add_of_sub_sub_of_add]
-  --           simp [BitVec.nat_bitvec_add (addr2 - addr1) 1#64]
-  --           have := @addr_diff_upper_bound_lemma
-  --                     n1 n addr1 addr2 h0 h1 (by omega) (by omega) h6 h5 h4
-  --           rw [read_mem_bytes_of_write_mem_bytes_subset_helper2]
-  --           · omega
-  --           · omega
-  --           · omega
-  --           · exact h_addr
-  --           · assumption
-  --         · omega
-  --       · omega
-  --       · assumption
-  -- done
-  sorry
-
+  induction n2, h2 using Nat.le_induction generalizing addr1 addr2 val s
+  case base =>
+    simp only [Nat.reduceSucc, Nat.succ_sub_succ_eq_sub, Nat.sub_self, BitVec.add_zero] at h4
+    simp_all only [read_mem_bytes, BitVec.cast_eq]
+    have h' : (BitVec.toNat (addr2 - addr1) + 1) * 8 - 1 - BitVec.toNat (addr2 - addr1) * 8 + 1 = 8 := by
+      omega
+    rw [read_mem_of_write_mem_bytes_subset h0 h1 h4 h']
+    apply BitVec.empty_bitvector_append_left
+    decide
+  case succ =>
+    rename_i n h2' n_ih
+    by_cases h_addr : addr1 = addr2
+    case pos => -- (addr1 = addr2)
+      subst addr2
+      have h' : (n + 1) * 8 - 1 - 0 + 1 = (n + 1) * 8 := by omega
+      have := @read_mem_bytes_of_write_mem_bytes_subset_same_first_address n1 (n + 1) addr1 val s
+               h0 h1 (by omega) (by omega) h4 h'
+      rw [this]
+      ext
+      simp only [Nat.sub_zero, BitVec.cast_eq, extractLsb_toNat,
+                 Nat.shiftRight_zero, toNat_cast, BitVec.sub_self,
+                 toNat_ofNat, Nat.zero_mod, Nat.zero_mul, Nat.zero_add]
+    case neg => -- (addr1 ≠ addr2)
+      simp only [read_mem_bytes, Nat.add_eq, Nat.add_zero]
+      simp only [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at h4
+      have h_sub : mem_subset (addr2 + 1#64) (addr2 + 1#64 + (n - 1)#64) addr1 (addr1 + (n1 - 1)#64) := by
+        rw [addr_add_one_add_m_sub_one]
+        · have l0 := @mem_subset_trans (addr2 + 1#64) (addr2 + n#64) addr2 (addr2 + n#64)
+                   addr1 (addr1 + (n1 - 1)#64)
+          simp only [h4] at l0
+          rw [first_addresses_add_one_is_subset_of_region_general (by omega) (by omega) (by omega)] at l0
+          · simp_all only [Nat.succ_sub_succ_eq_sub, Nat.sub_zero, forall_const]
+          · simp only [mem_subset_refl]
+        · omega
+        · omega
+      have l1 := @read_mem_of_write_mem_bytes_subset n1 addr2 addr1 val s (by omega) (by omega)
+      have l2 := @first_address_is_subset_of_region addr2 n#64
+      have l3 := mem_subset_trans l2 h4
+      simp only [l3, forall_const] at l1
+      rw [l1 (by omega)]
+      simp only [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at h5
+      have n_ih' := @n_ih (addr2 + 1#64) addr1 val s (by omega)
+      simp only [h_sub, forall_const] at n_ih'
+      rw [mem_legal_lemma h2'] at n_ih'
+      · simp only [forall_const] at n_ih'
+        have h' : (BitVec.toNat (addr2 + 1#64 - addr1) + n) * 8 - 1 -
+                  BitVec.toNat (addr2 + 1#64 - addr1) * 8 + 1 =
+                  n * 8 := by
+             omega
+        rw [n_ih' h6 h']
+        ext
+        simp only [extractLsb, extractLsb', toNat_ofNat, toNat_cast,
+                   BitVec.add_of_sub_sub_of_add]
+        simp only [toNat_add (addr2 - addr1) 1#64, Nat.add_eq, Nat.add_zero,
+                   toNat_ofNat, Nat.add_mod_mod, cast_ofNat, toNat_append]
+        have := @addr_diff_upper_bound_lemma n1 n addr1 addr2 h0 h1
+                 (by omega) (by omega) h6 h5 h4
+        rw [read_mem_bytes_of_write_mem_bytes_subset_helper2] <;> assumption
+      · omega
+      · assumption
+  done
 
 -- (FIXME) I found myself needing to hide "^" inside this irreducible
 -- definition because whenever I ran into a large term like 2^64 * 8,
@@ -881,15 +869,16 @@ private theorem read_mem_bytes_of_write_mem_bytes_subset_n2_eq_alt_helper (val :
     BitVec.cast h
       (extractLsb ((BitVec.toNat (addr2 - addr2) + x) * 8 - 1)
         (BitVec.toNat (addr2 - addr2) * 8) val) := by
-  -- FIXME
-  -- ext; simp
-  -- simp [toNat_cast, extractLsb, extractLsb']
-  -- rw [Nat.mod_eq_of_lt]
-  -- rw [Nat.sub_add_cancel]
-  -- · exact val.isLt
-  -- · omega
-  -- done
-  sorry
+  ext
+  simp only [extractLsb, extractLsb', BitVec.sub_self, toNat_ofNat,
+             Nat.zero_mod, Nat.zero_mul, Nat.shiftRight_zero,
+             ofNat_toNat, toNat_cast, toNat_truncate, Nat.zero_add,
+             Nat.sub_zero]
+  rw [Nat.mod_eq_of_lt]
+  rw [Nat.sub_add_cancel]
+  · exact val.isLt
+  · omega
+  done
 
 private theorem read_mem_bytes_of_write_mem_bytes_subset_n2_eq_alt
   (h0 : 0 < n1) (h1 : n1 <= my_pow 2 64) (h2 : 0 < n2) (h3 : n2 = my_pow 2 64)
@@ -943,67 +932,62 @@ theorem read_mem_bytes_of_write_mem_bytes_subset
 ----------------------------------------------------------------------
 -- Key theorem : write_mem_bytes_irrelevant
 
-theorem leftshift_n_or_rightshift_n (x y : Nat) (h : y < 2^n) :
+theorem leftshift_n_or_rightshift_n (n x y : Nat) (h : y < 2^n) :
   (x <<< n ||| y) >>> n = x := by
-  -- FIXME
-  -- apply Nat.eq_of_testBit_eq; intro i
-  -- simp [Nat.testBit_shiftRight, Nat.testBit_or]
-  -- have l0 : y < 2^(n + i) :=
-  --   calc
-  --     _ < 2^n := by assumption
-  --     _ <= 2^(n + i) := Nat.pow_le_pow_right (by omega) (by omega)
-  -- rw [Nat.testBit_lt_two_pow l0]
-  -- simp [Nat.testBit_shiftLeft, Nat.add_sub_cancel_left, Nat.le_add_right]
-  sorry
+  apply Nat.eq_of_testBit_eq; intro i
+  simp only [Nat.testBit_shiftRight, Nat.testBit_or]
+  have l0 : y < 2^(n + i) :=
+    calc
+      _ < 2^n := by assumption
+      _ <= 2^(n + i) := Nat.pow_le_pow_right (by omega) (by omega)
+  rw [Nat.testBit_lt_two_pow l0]
+  simp only [Nat.testBit_shiftLeft, decide_True, Nat.add_sub_cancel_left,
+             Nat.le_add_right, Bool.true_and, Bool.or_false]
 
 private theorem write_mem_bytes_irrelevant_helper (h : n * 8 + 8 = (n + 1) * 8) :
   (zeroExtend (n * 8)
     ((BitVec.cast h (read_mem_bytes n (addr + 1#64) s ++ read_mem addr s)) >>> 8)) =
   read_mem_bytes n (addr + 1#64) s := by
-  sorry
-  -- ext
-  -- simp [zeroExtend]
-  -- simp [HShiftRight.hShiftRight, ushiftRight, ShiftRight.shiftRight,
-  --               BitVec.bitvec_to_nat_of_nat]
-  -- have h_x_size := (read_mem_bytes n (addr + 1#64) s).isLt
-  -- have h_y_size := (read_mem addr s).isLt
-  -- generalize h_x : (BitVec.toNat (read_mem_bytes n (addr + 1#64) s)) = x
-  -- generalize h_y : (BitVec.toNat (read_mem addr s)) = y
-  -- simp [h_x] at h_x_size
-  -- simp [h_y] at h_y_size
-  -- rw [leftshift_n_or_rightshift_n _ _ h_y_size]
-  -- have l0 : 1 < 2 := by decide
-  -- have l1 : n * 8 < (n + 1) * 8 := by omega
-  -- have l2 := pow_lt_pow_right l0 l1
-  -- rw [Nat.mod_eq_of_lt]
-  -- · rw [Nat.mod_eq_of_lt]
-  --   omega
-  -- · rw [Nat.mod_eq_of_lt]
-  --   · exact h_x_size
-  --   · omega
-  -- done
+  ext
+  simp [ushiftRight, ShiftRight.shiftRight, BitVec.bitvec_to_nat_of_nat]
+  have h_x_size := (read_mem_bytes n (addr + 1#64) s).isLt
+  have h_y_size := (read_mem addr s).isLt
+  generalize h_x : (BitVec.toNat (read_mem_bytes n (addr + 1#64) s)) = x
+  generalize h_y : (BitVec.toNat (read_mem addr s)) = y
+  simp only [h_x] at h_x_size
+  simp only [h_y] at h_y_size
+  rw [leftshift_n_or_rightshift_n 8 x y h_y_size]
+  rw [Nat.mod_eq_of_lt h_x_size]
+  done
+
+private theorem extract_byte_of_read_mem_bytes_succ (n : Nat) :
+  extractLsb 7 0 (read_mem_bytes (n + 1) addr s) = read_mem addr s := by
+  simp only [read_mem_bytes, Nat.add_eq, Nat.add_zero, toNat_eq, extractLsb_toNat, 
+             toNat_cast, toNat_append, Nat.shiftRight_zero, Nat.reduceAdd]
+  generalize read_mem addr s = y
+  generalize (read_mem_bytes n (addr + 1#64) s) = x
+  have l0 := @leftshift_n_or_mod_2n x.toNat 8 y.toNat
+  rw [l0, Nat.mod_eq_of_lt y.isLt]
+  done
 
 @[simp]
 theorem write_mem_bytes_irrelevant :
   write_mem_bytes n addr (read_mem_bytes n addr s) s = s := by
-  sorry
-  -- FIXME
-  -- induction n generalizing addr s
-  -- case zero => simp [write_mem_bytes]
-  -- case succ =>
-  --   rename_i n n_ih
-  --   simp [write_mem_bytes, read_mem_bytes]
-  --   conv =>
-  --     pattern write_mem ..
-  --     arg 2
-  --     simp [toNat_cast, extractLsb, extractLsb']
-  --     simp [BitVec.bitvec_to_nat_of_nat, toNat_zeroExtend]
-  --     simp [BitVec.truncate_to_lsb_of_append]
-  --   simp [write_mem_irrelevant]
-  --   have n_ih' := @n_ih (addr + 1#64) s
-  --   rw [write_mem_bytes_irrelevant_helper]
-  --   exact n_ih'
-  --   done
+  induction n generalizing addr s
+  case zero => simp only [write_mem_bytes]
+  case succ =>
+    rename_i n n_ih
+    simp only [write_mem_bytes]
+    conv =>
+      pattern write_mem ..
+      arg 2
+      simp only [extract_byte_of_read_mem_bytes_succ]
+    simp only [write_mem_irrelevant]
+    have n_ih' := @n_ih (addr + 1#64) s
+    simp only [read_mem_bytes]
+    rw [write_mem_bytes_irrelevant_helper]
+    exact n_ih'
+    done
 
 ----------------------------------------------------------------------
 
diff --git a/Arm/SeparateProofs.lean b/Arm/SeparateProofs.lean
index 964785e9..39cbb52f 100644
--- a/Arm/SeparateProofs.lean
+++ b/Arm/SeparateProofs.lean
@@ -6,7 +6,9 @@ Author(s): Shilpi Goel
 import Arm.Memory
 -- import Auto
 
--- In this file, we have memory-related proofs that depend on auto.
+-- In this file, we have proofs pertaining to separateness of memory
+-- regions. Many of these are skipped right now as we eliminate our
+-- dependency on auto (and SMT solving).
 
 -- set_option auto.smt true
 -- set_option auto.smt.trust true
@@ -35,90 +37,48 @@ theorem n_minus_1_lt_2_64_1 (n : Nat)
   simp_all [Nat.mod_eq_of_lt]
   exact Nat.sub_lt_left_of_lt_add h1 h2
 
--- (FIXME) Prove for all bitvector widths, without using auto.
--- set_option auto.smt.savepath "/tmp/BitVec.add_sub_self_left_64.smt2" in
+-- (FIXME) Prove for all bitvector widths.
 theorem BitVec.add_sub_self_left_64 (a m : BitVec 64) :
   a + m - a = m := by
-  sorry -- auto
+  bv_omega
 
--- (FIXME) Prove for all bitvector widths, without using auto.
--- set_option auto.smt.savepath "/tmp/BitVec.add_sub_self_right_64.smt2" in
+-- (FIXME) Prove for all bitvector widths.
 theorem BitVec.add_sub_self_right_64 (a m : BitVec 64) :
   a + m - m = a := by
-  sorry -- auto
+  bv_omega
 
--- (FIXME) Prove for all bitvector widths, without using auto.
--- set_option auto.smt.savepath "/tmp/BitVec.add_sub_add_left.smt2" in
+-- (FIXME) Prove for all bitvector widths.
 theorem BitVec.add_sub_add_left (a m n : BitVec 64) :
   a + m - (a + n) = m - n := by
-  sorry -- auto
+  bv_omega
 
--- (FIXME) Prove without auto using general assoc/comm BitVec lemmas.
--- set_option auto.smt.savepath "/tmp/BitVec.sub_of_add_is_sub_sub.smt2" in
+-- (FIXME) Prove for all bitvector widths, using general assoc/comm
+-- BitVec lemmas.
 theorem BitVec.sub_of_add_is_sub_sub (a b c : BitVec 64) :
   (a - (b + c)) = a - b - c := by
-  sorry -- auto
+  bv_omega
 
--- (FIXME) Prove without auto using general assoc/comm BitVec lemmas.
--- set_option auto.smt.savepath "/tmp/BitVec.add_of_sub_sub_of_add.smt2" in
+-- (FIXME) Prove for all bitvector widths, using general assoc/comm
+-- BitVec lemmas.
 theorem BitVec.add_of_sub_sub_of_add (a b c : BitVec 64) :
   (a + b - c) = a - c + b := by
-  sorry -- auto
+  bv_omega
 
 -- set_option auto.smt.savepath "/tmp/nat_bitvec_sub1.smt2" in
 theorem nat_bitvec_sub1 (x y : BitVec 64)
   (_h : y.toNat <= x.toNat) :
   (x - y).toNat = (x.toNat - y.toNat) % 2^64 := by
-  rw [BitVec.nat_bitvec_sub]
-  generalize hx1 : BitVec.toNat x = x1
-  generalize hy1 : BitVec.toNat y = y1
-  have : x1 < 2^64 := by subst x1; exact x.isLt
-  have : y1 < 2^64 := by subst y1; exact y.isLt
-  -- Let's reduce 2^64 to a constant for SMT solvers.
-  simp (config := {ground := true}) only
-  rw [Nat.mod_eq_sub_mod]
-  sorry; sorry -- auto; auto
+  bv_omega
 
 theorem nat_bitvec_sub2 (x y : Nat)
   (h : y <= x) (xub : x < 2^64) :
   (x - y)#64 = x#64 - y#64 := by
-  have yub : y < 2^64 := calc
-    _ ≤ x := h
-    _ < _ := xub
-  ext
-  rw [nat_bitvec_sub1]
-  simp only [BitVec.bitvec_to_nat_of_nat]
-  have xmyub : x - y < 2^64 := calc
-    x - y ≤ x := Nat.sub_le x y
-    _ < _ := xub
-  simp at xmyub
-  -- rw [Nat.mod_eq_of_lt xmyub]
-  -- simp at xub yub
-  -- conv =>
-  --   pattern (x % 18446744073709551616 - y % 18446744073709551616)
-  --   rw [Nat.mod_eq_of_lt xub, Nat.mod_eq_of_lt yub]
-  -- rw [Nat.mod_eq_of_lt xmyub]
-  -- simp only [BitVec.bitvec_to_nat_of_nat]
-  -- simp at xub yub
-  -- rw [Nat.mod_eq_of_lt xub, Nat.mod_eq_of_lt yub]
-  -- exact h
-  repeat sorry
+  bv_omega
 
 theorem addr_add_one_add_m_sub_one  (n : Nat) (addr : BitVec 64)
   (h_lb : Nat.succ 0 ≤ n) (h_ub : n + 1 ≤ 2 ^ 64) :
   (addr + 1#64 + (n - 1)#64) = addr + n#64 := by
-  sorry
-/-
-  have h_ub' : n < 2^64 := by exact h_ub
-  rw [nat_bitvec_sub2 n 1 h_lb h_ub']
-  ext
-  rw [BitVec.toNat_add]
-  rw [←nat_bitvec_sub2 n 1 h_lb h_ub]
-  simp [BitVec.bitvec_to_nat_of_nat]
-  rw [←Nat.add_sub_assoc h_lb]
-  omega
--/
-
+  bv_omega
 
 ----------------------------------------------------------------------
 ---- mem_subset ----
@@ -311,8 +271,7 @@ theorem mem_subset_trans
   mem_subset a1 a2 c1 c2 := by
   revert h1 h2
   simp [mem_subset_and_mem_subset_for_auto]
-  -- auto d[mem_subset_for_auto]
-  sorry
+  sorry -- auto d[mem_subset_for_auto]
 
 ----------------------------------------------------------------------
 ---- mem_separate ----