diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index f49d3f68138a9dbdec03862f464741218e3cc198..993249cd06b27009458572a83563de0a4985a496 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -65,6 +65,16 @@ Definition is_constrained (elt : instr_kind) trace sbState :=
   | _, _ => false
   end.
 
+Definition cycle_on_more_advanced (t : trace_kind) (instr : instr_kind) sbState :=
+  let (_, state) := instr in
+  let isSuUsed := List.existsb is_in_su t in
+  List.map (fun (elt : instr_kind) =>
+              let (_, state') := elt in
+              if state_leb state state' && negb (state_leb state' state) then
+                cycle_elt isSuUsed sbState t elt
+              else
+                elt) t.
+
 Section can_advance.
   Variable isSuUsed : bool.
   Variable sbState : sbStateT.