diff --git a/proof/crefine/ARM/CSpace_RAB_C.thy b/proof/crefine/ARM/CSpace_RAB_C.thy
index 9fdb2a75d..ca62f330c 100644
--- a/proof/crefine/ARM/CSpace_RAB_C.thy
+++ b/proof/crefine/ARM/CSpace_RAB_C.thy
@@ -324,8 +324,8 @@ next
       unat guardBits = capCNodeGuardSize cap;
       \<not> guard < capCNodeBits cap + capCNodeGuardSize cap \<rbrakk> \<Longrightarrow>
       \<forall>s s'. (s, s') \<in> rf_sr \<and> True \<and> True \<longrightarrow>
-                (guard = capCNodeBits cap + capCNodeGuardSize cap) = (s' \<in> \<lbrace>nb \<le> radixBits + guardBits\<rbrace>)"
-      by (simp add: Collect_const_mem word_le_nat_alt unat_word_ariths)
+                (guard = capCNodeBits cap + capCNodeGuardSize cap) = (s' \<in> \<lbrace>nb = radixBits + guardBits\<rbrace>)"
+      by clarsimp unat_arith
 
     have cond4:
       "\<And>rva nodeCapb ret__unsigned_long.
diff --git a/proof/crefine/ARM_HYP/CSpace_RAB_C.thy b/proof/crefine/ARM_HYP/CSpace_RAB_C.thy
index 65a01fbcb..3869ed4ac 100644
--- a/proof/crefine/ARM_HYP/CSpace_RAB_C.thy
+++ b/proof/crefine/ARM_HYP/CSpace_RAB_C.thy
@@ -360,8 +360,8 @@ next
       unat guardBits = capCNodeGuardSize cap;
       \<not> guard < capCNodeBits cap + capCNodeGuardSize cap \<rbrakk> \<Longrightarrow>
       \<forall>s s'. (s, s') \<in> rf_sr \<and> True \<and> True \<longrightarrow>
-                (guard = capCNodeBits cap + capCNodeGuardSize cap) = (s' \<in> \<lbrace>nb \<le> radixBits + guardBits\<rbrace>)"
-      by (simp add: Collect_const_mem word_le_nat_alt unat_word_ariths)
+                (guard = capCNodeBits cap + capCNodeGuardSize cap) = (s' \<in> \<lbrace>nb = radixBits + guardBits\<rbrace>)"
+      by clarsimp unat_arith
 
     have cond4:
       "\<And>rva nodeCapb ret__unsigned_long.
diff --git a/proof/crefine/RISCV64/CSpace_RAB_C.thy b/proof/crefine/RISCV64/CSpace_RAB_C.thy
index 159e18855..573d7a568 100644
--- a/proof/crefine/RISCV64/CSpace_RAB_C.thy
+++ b/proof/crefine/RISCV64/CSpace_RAB_C.thy
@@ -362,8 +362,8 @@ next
       unat guardBits = capCNodeGuardSize cap;
       \<not> guard < capCNodeBits cap + capCNodeGuardSize cap \<rbrakk> \<Longrightarrow>
       \<forall>s s'. (s, s') \<in> rf_sr \<and> True \<and> True \<longrightarrow>
-                (guard = capCNodeBits cap + capCNodeGuardSize cap) = (s' \<in> \<lbrace>nb \<le> radixBits + guardBits\<rbrace>)"
-      by (simp add: Collect_const_mem word_le_nat_alt unat_word_ariths)
+                (guard = capCNodeBits cap + capCNodeGuardSize cap) = (s' \<in> \<lbrace>nb = radixBits + guardBits\<rbrace>)"
+      by clarsimp unat_arith
 
     have cond4:
       "\<And>rva nodeCapb ret__unsigned_long.
diff --git a/proof/crefine/X64/CSpace_RAB_C.thy b/proof/crefine/X64/CSpace_RAB_C.thy
index acba84fb1..5dce367d2 100644
--- a/proof/crefine/X64/CSpace_RAB_C.thy
+++ b/proof/crefine/X64/CSpace_RAB_C.thy
@@ -362,8 +362,8 @@ next
       unat guardBits = capCNodeGuardSize cap;
       \<not> guard < capCNodeBits cap + capCNodeGuardSize cap \<rbrakk> \<Longrightarrow>
       \<forall>s s'. (s, s') \<in> rf_sr \<and> True \<and> True \<longrightarrow>
-                (guard = capCNodeBits cap + capCNodeGuardSize cap) = (s' \<in> \<lbrace>nb \<le> radixBits + guardBits\<rbrace>)"
-      by (simp add: Collect_const_mem word_le_nat_alt unat_word_ariths)
+                (guard = capCNodeBits cap + capCNodeGuardSize cap) = (s' \<in> \<lbrace>nb = radixBits + guardBits\<rbrace>)"
+      by clarsimp unat_arith
 
     have cond4:
       "\<And>rva nodeCapb ret__unsigned_long.