arm-hyp refine: fix error

Signed-off-by: Michael McInerney <[email protected]>
seL4 · May 3, 2024 · 108d2d6 · 108d2d6
1 parent 8455f0b
commit 108d2d6
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/proof/refine/ARM_HYP/Arch_R.thy b/proof/refine/ARM_HYP/Arch_R.thy
@@ -1769,7 +1769,7 @@ lemma createMappingEntires_valid_slots_duplicated'[wp]:
    apply (intro conjI impI)
             apply ((clarsimp simp: vmsz_aligned_def pageBitsForSize_def
               slots_duplicated_ensured_def
-              split:vmpage_size.splits)+)[13]
+              split:vmpage_size.splits)+)[9]
    apply clarsimp
    apply (drule lookup_pd_slot_aligned_6)
     apply (simp add:pdBits_def pageBits_def pd_bits_def pde_bits_def)