diff --git a/LeanCats.lean b/LeanCats.lean
index 5e3c11b..f23d9cb 100644
--- a/LeanCats.lean
+++ b/LeanCats.lean
@@ -9,6 +9,7 @@ import LeanCats.CatPreprocessor
 import LeanCats.Macro
 import LeanCats.Theorems
 import LeanCats.TsoWeakerThanSc
+import LeanCats.mipsWeakerThanTSO
 import LeanCats.ModelReader
 import LeanCats.Litmus
 import LeanCats.LitmusParser
@@ -16,3 +17,4 @@ import LeanCats.LitmusGraph
 import LeanCats.LitmusGraphBridge
 import LeanCats.LitmusReader
 import LeanCats.Linux.CoRR_poonceonce_Once
+import LeanCats.Linux.X86_SB_rfi_pos
diff --git a/LeanCats/Basic.lean b/LeanCats/Basic.lean
index c50666a..4406cf2 100644
--- a/LeanCats/Basic.lean
+++ b/LeanCats/Basic.lean
@@ -24,6 +24,10 @@ structure CandidateExecution (evts : Events) where
   ctrl' : SetRel Event Event := ∅
   fence' : SetRel Event Event := ∅
   mb' : SetRel Event Event := ∅
+  SYNC' : Set Event := ∅
+  -- Specific fence event sets depend on the test architecture,
+  -- their name is always uppercase and derives from the mnemonic of the instruction that generates them.
+  syncInF : ∀ (e : Event), e ∈ SYNC' → e ∈ evts.F
   uniqueId : ∀ (e₁ e₂ : Event),
     e₁ ∈ evts.all → e₂ ∈ evts.all
     -> e₁ ≠ e₂
@@ -34,11 +38,6 @@ structure CandidateExecution (evts : Events) where
     (w, r) ∈ rf'
     → w.t_id = r.t_id
     → (w, r) ∈ evts.po
-  coWR : ∀ (w r w' : Event),
-    (w, r) ∈ evts.po
-    → w.effect.location = r.effect.location
-    → (w', r) ∈ rf'
-    → (w, w') ∈ co' ∨ w = w'
 
 /-- from-reads: always defined as rf⁻¹ ; co, so it is transparent to the kernel. -/
 @[simp] def CandidateExecution.fr' {evts : Events} (X : CandidateExecution evts) : SetRel Event Event :=
diff --git a/LeanCats/Cats/examples/models/bpf.cat b/LeanCats/Cats/examples/models/bpf.cat
new file mode 100644
index 0000000..75a592e
--- /dev/null
+++ b/LeanCats/Cats/examples/models/bpf.cat
@@ -0,0 +1,81 @@
+(*************)
+(* Utilities *)
+(*************)
+
+(* Single event atomic ops are marked with both R and W.
+ * These events are marked with SC if the op returns a value.
+ *)
+let RMW = [R & W] & [SC]
+
+(* Atomic ops with separate R and W events are related by the amo relation.
+ * both of these R and W events are  marked with SC if the op returns a value.
+ *)
+let SRMW = (SC * SC) & amo
+
+(* Ignore the SRCU part *)
+let po_amo_fetch = ([M];po;RMW) | (RMW;po;[M])
+
+show po_amo_fetch as atomicfetch
+
+(* Release Consistency processor consistent (RCpc) *)
+let load_acquire = ([AQ];po;[M])
+let store_release = ([M];po;[RL])
+let rcpc = load_acquire | store_release
+
+(****************)
+(* Dependencies *)
+(****************)
+
+let addr_dep = [R];addr;[M]
+let data_dep = [R];data;[W]
+let ctrl_dep = [R];ctrl;[W]
+
+show addr_dep as addr
+show data_dep as data
+show ctrl_dep as ctrl
+
+(**********************)
+(* ppo and prop rules *)
+(**********************)
+
+(* Compute coherence relation *)
+include "cos-opt.cat"
+let com = co | rf | fr
+
+let ppo =
+(* Explicit synchronization *)
+ po_amo_fetch | rcpc
+(* Syntactic Dependencies *)
+| addr_dep
+| data_dep
+| ctrl_dep
+(* Pipeline Dependencies *)
+| [M];(addr|data);[W];rfi;[R]
+| [M];addr;[M];po;[W]
+(* Overlapping-address ordering *)
+| (coi | fri)
+
+(* Propagation ordering from SC and release operations *)
+let A-cumul = rfe? ; (po_amo_fetch | store_release)
+let prop = (coe | fre)? ; A-cumul* ; rfe?
+
+(**********)
+(* Axioms *)
+(**********)
+
+(* Sc per location *)
+acyclic com | po-loc as Coherence
+
+(* No-Thin-Air and Observation *)
+let hb = ppo | rfe | ((prop \ id) & int)
+acyclic hb as Happens-before
+
+(* Propagation *)
+let pb = prop ; po_amo_fetch ; hb*
+acyclic pb as Propagation
+
+(* Atomicity *)
+empty rmw & (fre;coe) as Atomic
+
+(* Atomic fetch as a fence *)
+acyclic po_amo_fetch | com
\ No newline at end of file
diff --git a/LeanCats/Cats/examples/models/mips.cat b/LeanCats/Cats/examples/models/mips.cat
new file mode 100644
index 0000000..256eaee
--- /dev/null
+++ b/LeanCats/Cats/examples/models/mips.cat
@@ -0,0 +1,12 @@
+let fencerel(r) = (po & (_ * r)) ;  po
+let com = rf | fr | co
+acyclic po_loc | com as uniproc
+
+let sync = try fencerel(SYNC) with 0
+
+empty rmw & (fre;coe) as atomic
+
+let ppo = po & (R * M) | sync
+
+let ghb = ppo | rfe | fr | co
+acyclic ghb as pso
\ No newline at end of file
diff --git a/LeanCats/Cats/sc.cat b/LeanCats/Cats/examples/models/sc.cat
similarity index 100%
rename from LeanCats/Cats/sc.cat
rename to LeanCats/Cats/examples/models/sc.cat
diff --git a/LeanCats/Cats/tso.cat b/LeanCats/Cats/examples/models/tso.cat
similarity index 88%
rename from LeanCats/Cats/tso.cat
rename to LeanCats/Cats/examples/models/tso.cat
index 2f0b285..73c7c5b 100644
--- a/LeanCats/Cats/tso.cat
+++ b/LeanCats/Cats/examples/models/tso.cat
@@ -1,5 +1,7 @@
 include "cos.cat"
 
+empty rmw & (fre;coe)
+
 let xppo = ((W*W) | (R*W) | (R*R)) & po
 let At = domain(rmw) | range(rmw)
 let implied = po;[At | F] | [At | F];po
diff --git a/LeanCats/Cats/examples/models/tsox.cat b/LeanCats/Cats/examples/models/tsox.cat
new file mode 100644
index 0000000..71f431b
--- /dev/null
+++ b/LeanCats/Cats/examples/models/tsox.cat
@@ -0,0 +1,4 @@
+let xppo = ((W*W) | (R*W) | (R*R)) & po
+let At = domain(rmw) | range(rmw)
+let implied = po;[At | F] | [At | F];po
+acyclic (implied | xppo | rfe | fr | co) as tso
\ No newline at end of file
diff --git a/LeanCats/Cats/examples/models/x86.cat b/LeanCats/Cats/examples/models/x86.cat
new file mode 100644
index 0000000..f9c30c1
--- /dev/null
+++ b/LeanCats/Cats/examples/models/x86.cat
@@ -0,0 +1,5 @@
+let xppo = ((W*W) | (R*W) | (R*R)) & po
+let At = domain(rmw) | range(rmw)
+let implied = po;[At | F] | [At | F];po
+acyclic (implied | xppo | rfe | fr | co) as tso
+acyclic (po_loc | rf | fr | co) as uniproc
diff --git a/LeanCats/Data.lean b/LeanCats/Data.lean
index c43fed3..6d6adab 100644
--- a/LeanCats/Data.lean
+++ b/LeanCats/Data.lean
@@ -72,10 +72,9 @@ structure Events where
   (B : Set Event)
   (F : Set Event)
   (RMW : Set Event)
-  (M : Set Event)
 
 @[simp] def Events.all (evts : Events) :=
-  evts.IW ∪ evts.R ∪ evts.W ∪ evts.B ∪ evts.F ∪ evts.RMW ∪ evts.M
+  evts.IW ∪ evts.R ∪ evts.W ∪ evts.B ∪ evts.F ∪ evts.RMW
 
 instance : Membership Event Events where
   mem := fun es e => e ∈ es.all
diff --git a/LeanCats/Linux/CoRR_poonceonce_Once.lean b/LeanCats/Linux/CoRR_poonceonce_Once.lean
index 6b322ee..f453d13 100644
--- a/LeanCats/Linux/CoRR_poonceonce_Once.lean
+++ b/LeanCats/Linux/CoRR_poonceonce_Once.lean
@@ -29,10 +29,10 @@ abbrev x := 0
 @[simp] abbrev p1r0 : Data.Event :=
   Data.Event.mk 2 1 rOpX1 ⟨lkmm.Accesses, lkmm.Accesses.ONCE'⟩
 @[simp] abbrev p1r1 : Data.Event :=
-  Data.Event.mk 3 2 rOpX0 ⟨lkmm.Accesses, lkmm.Accesses.ONCE'⟩
+  Data.Event.mk 3 1 rOpX0 ⟨lkmm.Accesses, lkmm.Accesses.ONCE'⟩
 
 @[simp] abbrev corr_evts : Data.Events :=
-  Data.Events.mk {initWx} {p1r0, p1r1} {initWx, p0wX} {} {} {} {}
+  Data.Events.mk {initWx} {p1r0, p1r1} {initWx, p0wX} {} {} {}
 
 @[simp] def corr_co : SetRel Event Event := {(initWx, p0wX)}
 @[simp] def corr_po : SetRel Event Event := {(p1r0, p1r1)}
@@ -65,17 +65,20 @@ Chosen rf edges: `p0wX -> p1r0` and `initWx -> p1r1`. -/
 
 def corr_test : CandidateExecution corr_evts :=
   {
+    evts := corr_evts
     po' := corr_po
     prePo := by candidateExecution_wf
     rf' := corr_rf
     rfInst := corr_rfInst
     co' := corr_co
+    rmw' := ∅
     preRMW := instWellformedRmwEmpty corr_evts
+    syncInF := by
+      intro e h
+      contradiction
     uniqueId := uniqueId_by_id corr_evts
     rfiPo := by
       candidateExecution_wf
-    coWR := by
-      candidateExecution_wf
   }
 
 theorem corr_FindCycle : ¬ (lkmm.coherence corr_evts corr_test) := by
diff --git a/LeanCats/Linux/LB.lean b/LeanCats/Linux/LB.lean
new file mode 100644
index 0000000..0b415cd
--- /dev/null
+++ b/LeanCats/Linux/LB.lean
@@ -0,0 +1,233 @@
+import LeanCats.Basic
+import LeanCats.Data
+import LeanCats.Macro
+import LeanCats.ModelReader
+import LeanCats.Data
+import LeanCats.Relations
+import LeanCats.Theorems
+import LeanCats.Basic
+import LeanCats.mipsWeakerThanTSO
+
+-- In this litmus test, we want to show that sometimes the X86 is weaker than mips because of the sc-per-location.
+
+-- init x = 0, y = 0
+--
+-- rX       rY
+-- Wy=1     rX=1
+
+-- exists: rX0 = 1 ∧ rX1 = 1
+
+open Data
+
+namespace Litmus
+
+
+instance instWellformedPo (evts : Data.Events) : wellformed.po evts.po := by
+  intro x y z hxy hyz
+  rcases hxy with ⟨hx, hy, hxyTid, hxyLt⟩
+  rcases hyz with ⟨_, hz, hyzTid, hyzLt⟩
+  exact ⟨hx, hz, Eq.trans hxyTid hyzTid, Nat.lt_trans hxyLt hyzLt⟩
+
+instance instWellformedRmwEmpty (evts : Data.Events) : wellformed.rmw evts (∅ : SetRel Event Event) := by
+  intro e h
+  contradiction
+
+abbrev x := 0
+abbrev y := 1
+
+inductive Normal where
+| none : Normal
+
+@[simp] abbrev initOpX : Data.Effect :=
+  Data.Effect.mk Data.Op.write x (some 0) true false
+@[simp] abbrev initOpY : Data.Effect :=
+  Data.Effect.mk Data.Op.write y (some 0) true false
+@[simp] abbrev wOpX : Data.Effect :=
+  Data.Effect.mk Data.Op.write x (some 1) false false
+@[simp] abbrev wOpY : Data.Effect :=
+  Data.Effect.mk Data.Op.write y (some 1) false false
+@[simp] abbrev rOpX1 : Data.Effect :=
+  Data.Effect.mk Data.Op.read x (some 1) false false
+@[simp] abbrev rOpY1 : Data.Effect :=
+  Data.Effect.mk Data.Op.read y (some 1) false false
+
+@[simp] abbrev initWx : Data.Event :=
+  Data.Event.mk 100 10 initOpX ⟨Normal, Normal.none⟩
+@[simp] abbrev initWy : Data.Event :=
+  Data.Event.mk 101 10 initOpY ⟨Normal, Normal.none⟩
+
+@[simp] abbrev p0wX : Data.Event :=
+  Data.Event.mk 3 0 wOpX ⟨Normal, Normal.none⟩
+@[simp] abbrev p0rY0 : Data.Event :=
+  Data.Event.mk 1 0 rOpY1 ⟨Normal, Normal.none⟩
+
+@[simp] abbrev p1wY : Data.Event :=
+  Data.Event.mk 6 1 wOpY ⟨Normal, Normal.none⟩
+@[simp] abbrev p1rX0 : Data.Event :=
+  Data.Event.mk 4 1 rOpX1 ⟨Normal, Normal.none⟩
+
+/-- X86 SB+rfi-pos
+
+P0: W(x)=1; R(x)=1; R(y)=0
+P1: W(y)=1; R(y)=1; R(x)=0 -/
+@[simp] abbrev sb_evts : Data.Events :=
+  Data.Events.mk
+    {initWx, initWy}
+    {p0rY0, p1rX0}
+    {initWx, initWy, p0wX, p1wY}
+    {}
+    {}
+    {}
+
+@[simp] def sb_co : SetRel Event Event :=
+  {(initWx, p0wX), (initWy, p1wY)}
+
+instance : wellformed.co sb_evts sb_co where
+  irrefl := by aesop
+  trans := by aesop
+  preco := {
+    wellTyped := by aesop
+    total := by candidateExecution_wf
+  }
+
+/-- rf edges encode the expected outcome:
+  - rfi: p0wX -> p0rX1 and p1wY -> p1rY1
+  - reads of 0 from init writes: initWy -> p0rY0 and initWx -> p1rX0 -/
+@[simp] def sb_rf : SetRel Event Event :=
+  {(p1wY, p0rY0), (p0wX, p1rX0)}
+
+@[simp] def sb_rfInst : wellformed.rf sb_evts sb_rf :=
+  Data.wellformed.rf.mk
+    (by
+      candidateExecution_wf
+    )
+    (by
+      candidateExecution_wf
+    )
+
+@[simp] def sb_test : CandidateExecution sb_evts :=
+  {
+    evts := sb_evts
+    po' := sb_evts.po
+    prePo := instWellformedPo sb_evts
+    rf' := sb_rf
+    rfInst := sb_rfInst
+    co' := sb_co
+    rmw' := ∅
+    preRMW := instWellformedRmwEmpty sb_evts
+    uniqueId := uniqueId_by_id sb_evts
+    syncInF := by
+      intro e h
+      contradiction
+    rfiPo := by
+      candidateExecution_wf
+  }
+
+defcat <"mips.cat">
+defcat <"tsox.cat">
+defcat <"sc.cat">
+
+example : ¬ sc.sc sb_evts sb_test :=
+by
+  intro hsc
+  simp [sc.sc, CatRel.CatUnion.union, sb_test, sb_rf, sb_co, CandidateExecution.fr', SetRel.comp, SetRel.inv] at hsc
+  apply hsc p0rY0
+  exact
+    Relation.TransGen.head (a := p0rY0) (b := p0wX)
+      (by
+        left
+        exact ⟨by simp [Data.Events.all], by simp [Data.Events.all], rfl, by decide⟩)
+      (Relation.TransGen.head (a := p0wX) (b := p1rX0)
+        (by
+          right
+          left
+          simp)
+        (Relation.TransGen.head (a := p1rX0) (b := p1wY)
+          (by
+            left
+            exact ⟨by simp [Data.Events.all], by simp [Data.Events.all], rfl, by decide⟩)
+          (Relation.TransGen.single (a := p1wY) (b := p0rY0)
+            (by
+              right
+              left
+              simp))))
+
+theorem sb_tso : ¬ tsox.tso sb_evts sb_test :=
+by
+  intro htso
+  unfold tsox.tso at htso
+  let rtso : SetRel Data.Event Data.Event :=
+    CatRel.CatUnion.union (tsox.implied sb_evts sb_test)
+      (CatRel.CatUnion.union (tsox.xppo sb_evts sb_test)
+        (CatRel.CatUnion.union (rfe sb_evts sb_test)
+          (CatRel.CatUnion.union sb_test.fr' sb_test.co')))
+  have h1xppo : (p0rY0, p0wX) ∈ tsox.xppo sb_evts sb_test := by
+    refine ⟨?_, ?_⟩
+    · exact Or.inr (Or.inl ⟨by simp, by simp⟩)
+    · exact ⟨by simp [Data.Events.all], by simp [Data.Events.all], rfl, by decide⟩
+  have h2rfe : (p0wX, p1rX0) ∈ rfe sb_evts sb_test := by
+    refine ⟨?_, ?_⟩
+    · simp [sb_test, sb_rf]
+    · simp [CatRel.Rel.external]
+  have h3xppo : (p1rX0, p1wY) ∈ tsox.xppo sb_evts sb_test := by
+    refine ⟨?_, ?_⟩
+    · exact Or.inr (Or.inl ⟨by simp, by simp⟩)
+    · exact ⟨by simp [Data.Events.all], by simp [Data.Events.all], rfl, by decide⟩
+  have h4rfe : (p1wY, p0rY0) ∈ rfe sb_evts sb_test := by
+    refine ⟨?_, ?_⟩
+    · simp [sb_test, sb_rf]
+    · simp [CatRel.Rel.external]
+  have h1 : (p0rY0, p0wX) ∈ rtso := by exact Or.inr (Or.inl h1xppo)
+  have h2 : (p0wX, p1rX0) ∈ rtso := by exact Or.inr (Or.inr (Or.inl h2rfe))
+  have h3 : (p1rX0, p1wY) ∈ rtso := by exact Or.inr (Or.inl h3xppo)
+  have h4 : (p1wY, p0rY0) ∈ rtso := by exact Or.inr (Or.inr (Or.inl h4rfe))
+  apply htso p0rY0
+  exact Relation.TransGen.head h1 (Relation.TransGen.head h2 (Relation.TransGen.head h3 (Relation.TransGen.single h4)))
+
+example : ¬ mips.pso sb_evts sb_test :=
+by
+  intro hmips
+  have hacyc : CatRel.SetRel.Acyclic
+      (CatRel.CatUnion.union (mips.ppo sb_evts sb_test)
+        (CatRel.CatUnion.union (rfe sb_evts sb_test)
+          (CatRel.CatUnion.union sb_test.fr' sb_test.co'))) := by
+    simpa [mips.pso, CatRel.CatUnion.union] using hmips
+
+  have h1ppo : (p0rY0, p0wX) ∈ mips.ppo sb_evts sb_test := by
+    refine ⟨?_, ?_⟩
+    · exact ⟨by simp [Data.Events.all], by simp [Data.Events.all], rfl, by decide⟩
+    · left
+      exact ⟨by simp, Or.inr (by simp)⟩
+  have h2rfe : (p0wX, p1rX0) ∈ rfe sb_evts sb_test := by
+    refine ⟨?_, ?_⟩
+    · simp [sb_test, sb_rf]
+    · simp [CatRel.Rel.external]
+  have h3ppo : (p1rX0, p1wY) ∈ mips.ppo sb_evts sb_test := by
+    refine ⟨?_, ?_⟩
+    · exact ⟨by simp [Data.Events.all], by simp [Data.Events.all], rfl, by decide⟩
+    · left
+      exact ⟨by simp, Or.inr (by simp)⟩
+  have h4rfe : (p1wY, p0rY0) ∈ rfe sb_evts sb_test := by
+    refine ⟨?_, ?_⟩
+    · simp [sb_test, sb_rf]
+    · simp [CatRel.Rel.external]
+
+  have h1 : (p0rY0, p0wX) ∈ CatRel.CatUnion.union (mips.ppo sb_evts sb_test)
+      (CatRel.CatUnion.union (rfe sb_evts sb_test)
+        (CatRel.CatUnion.union sb_test.fr' sb_test.co')) := by
+    exact Or.inl h1ppo
+  have h2 : (p0wX, p1rX0) ∈ CatRel.CatUnion.union (mips.ppo sb_evts sb_test)
+      (CatRel.CatUnion.union (rfe sb_evts sb_test)
+        (CatRel.CatUnion.union sb_test.fr' sb_test.co')) := by
+    exact Or.inr (Or.inl h2rfe)
+  have h3 : (p1rX0, p1wY) ∈ CatRel.CatUnion.union (mips.ppo sb_evts sb_test)
+      (CatRel.CatUnion.union (rfe sb_evts sb_test)
+        (CatRel.CatUnion.union sb_test.fr' sb_test.co')) := by
+    exact Or.inl h3ppo
+  have h4 : (p1wY, p0rY0) ∈ CatRel.CatUnion.union (mips.ppo sb_evts sb_test)
+      (CatRel.CatUnion.union (rfe sb_evts sb_test)
+        (CatRel.CatUnion.union sb_test.fr' sb_test.co')) := by
+    exact Or.inr (Or.inl h4rfe)
+
+  apply hacyc p0rY0
+  exact Relation.TransGen.head h1 (Relation.TransGen.head h2 (Relation.TransGen.head h3 (Relation.TransGen.single h4)))
diff --git a/LeanCats/Linux/SB.lean b/LeanCats/Linux/SB.lean
new file mode 100644
index 0000000..19dec88
--- /dev/null
+++ b/LeanCats/Linux/SB.lean
@@ -0,0 +1,220 @@
+import LeanCats.Basic
+import LeanCats.Data
+import LeanCats.Macro
+import LeanCats.ModelReader
+import LeanCats.Data
+import LeanCats.Relations
+import LeanCats.Theorems
+import LeanCats.Basic
+import LeanCats.mipsWeakerThanTSO
+
+-- In this litmus test, we want to show that sometimes the X86 is weaker than mips because of the sc-per-location.
+
+-- init x = 0
+--
+-- t0        t1
+-- Wx = 1   Wx = 2
+-- rX       rX
+
+-- exists: rX0 = 2 ∧ rX1 = 1
+-- The X86 allows this.
+-- But mips doesn't
+
+open Data
+
+namespace Litmus
+
+
+instance instWellformedPo (evts : Data.Events) : wellformed.po evts.po := by
+  intro x y z hxy hyz
+  rcases hxy with ⟨hx, hy, hxyTid, hxyLt⟩
+  rcases hyz with ⟨_, hz, hyzTid, hyzLt⟩
+  exact ⟨hx, hz, Eq.trans hxyTid hyzTid, Nat.lt_trans hxyLt hyzLt⟩
+
+instance instWellformedRmwEmpty (evts : Data.Events) : wellformed.rmw evts (∅ : SetRel Event Event) := by
+  intro e h
+  contradiction
+
+abbrev x := 0
+abbrev y := 1
+
+inductive Normal where
+| none : Normal
+
+@[simp] abbrev initOpX : Data.Effect :=
+  Data.Effect.mk Data.Op.write x (some 0) true false
+@[simp] abbrev initOpY : Data.Effect :=
+  Data.Effect.mk Data.Op.write y (some 0) true false
+@[simp] abbrev wOpX : Data.Effect :=
+  Data.Effect.mk Data.Op.write x (some 1) false false
+@[simp] abbrev wOpY : Data.Effect :=
+  Data.Effect.mk Data.Op.write y (some 1) false false
+@[simp] abbrev rOpX1 : Data.Effect :=
+  Data.Effect.mk Data.Op.read x (some 1) false false
+@[simp] abbrev rOpY1 : Data.Effect :=
+  Data.Effect.mk Data.Op.read y (some 1) false false
+@[simp] abbrev rOpX0 : Data.Effect :=
+  Data.Effect.mk Data.Op.read x (some 0) false false
+@[simp] abbrev rOpY0 : Data.Effect :=
+  Data.Effect.mk Data.Op.read y (some 0) false false
+
+@[simp] abbrev initWx : Data.Event :=
+  Data.Event.mk 100 10 initOpX ⟨Normal, Normal.none⟩
+@[simp] abbrev initWy : Data.Event :=
+  Data.Event.mk 101 10 initOpY ⟨Normal, Normal.none⟩
+
+@[simp] abbrev p0wX : Data.Event :=
+  Data.Event.mk 1 0 wOpX ⟨Normal, Normal.none⟩
+@[simp] abbrev p0rY0 : Data.Event :=
+  Data.Event.mk 3 0 rOpY0 ⟨Normal, Normal.none⟩
+
+@[simp] abbrev p1wY : Data.Event :=
+  Data.Event.mk 4 1 wOpY ⟨Normal, Normal.none⟩
+@[simp] abbrev p1rX0 : Data.Event :=
+  Data.Event.mk 6 1 rOpX0 ⟨Normal, Normal.none⟩
+
+/-- X86 SB+rfi-pos
+
+P0: W(x)=1; R(x)=1; R(y)=0
+P1: W(y)=1; R(y)=1; R(x)=0 -/
+@[simp] abbrev sb_evts : Data.Events :=
+  Data.Events.mk
+    {initWx, initWy}
+    {p0rY0, p1rX0}
+    {initWx, initWy, p0wX, p1wY}
+    {}
+    {}
+    {}
+
+@[simp] def sb_co : SetRel Event Event :=
+  {(initWx, p0wX), (initWy, p1wY)}
+
+instance : wellformed.co sb_evts sb_co where
+  irrefl := by aesop
+  trans := by aesop
+  preco := {
+    wellTyped := by aesop
+    total := by candidateExecution_wf
+  }
+
+/-- rf edges encode the expected outcome:
+  - rfi: p0wX -> p0rX1 and p1wY -> p1rY1
+  - reads of 0 from init writes: initWy -> p0rY0 and initWx -> p1rX0 -/
+@[simp] def sb_rf : SetRel Event Event :=
+  {(initWy, p0rY0), (initWx, p1rX0)}
+
+@[simp] def sb_rfInst : wellformed.rf sb_evts sb_rf :=
+  Data.wellformed.rf.mk
+    (by
+      candidateExecution_wf
+    )
+    (by
+      candidateExecution_wf
+    )
+
+@[simp] def sb_test : CandidateExecution sb_evts :=
+  {
+    evts := sb_evts
+    po' := sb_evts.po
+    prePo := instWellformedPo sb_evts
+    rf' := sb_rf
+    rfInst := sb_rfInst
+    co' := sb_co
+    rmw' := ∅
+    preRMW := instWellformedRmwEmpty sb_evts
+    uniqueId := uniqueId_by_id sb_evts
+    syncInF := by
+      intro e h
+      contradiction
+    rfiPo := by
+      candidateExecution_wf
+  }
+
+defcat <"mips.cat">
+defcat <"tsox.cat">
+defcat <"sc.cat">
+
+example : ¬ sc.sc sb_evts sb_test :=
+by
+  intro hsc
+  simp [sc.sc, CatRel.CatUnion.union, sb_test, sb_rf, sb_co, CandidateExecution.fr', SetRel.comp, SetRel.inv] at hsc
+  apply hsc p0wX
+  exact
+    Relation.TransGen.head (a := p0wX) (b := p0rY0)
+      (by
+        left
+        exact ⟨by simp [Data.Events.all], by simp [Data.Events.all], rfl, by decide⟩)
+      (Relation.TransGen.head (a := p0rY0) (b := p1wY)
+        (by
+          right
+          right
+          left
+          exact ⟨initWy, by simp, by simp⟩)
+        (Relation.TransGen.head (a := p1wY) (b := p1rX0)
+          (by
+            left
+            exact ⟨by simp [Data.Events.all], by simp [Data.Events.all], rfl, by decide⟩)
+          (Relation.TransGen.single (a := p1rX0) (b := p0wX)
+            (by
+              right
+              right
+              left
+              exact ⟨initWx, by simp, by simp⟩))))
+
+theorem sb_tso : tsox.tso sb_evts sb_test :=
+by
+  simp only [tsox.tso]
+  apply acyclic_of_rank (fun e => match e.id with
+    | 100 => 0  -- initWx
+    | 101 => 1  -- initWy
+    | 3   => 2  -- p0rY0
+    | 6   => 3  -- p1rX0
+    | 4   => 4  -- p1wY
+    | 1   => 5  -- p0wX
+    | _   => 6)
+  intro a b hab
+  simp only [CatRel.CatUnion.union, CatRel.SetRel.union, Set.mem_setOf_eq,
+             tsox.implied, tsox.xppo, tsox.At, rfe,
+             CandidateExecution.fr', SetRel.inv, SetRel.comp,
+             sb_test, sb_rf, sb_co, sb_evts,
+             Data.Events.all, Data.Events.po, SetRel.mkId,
+             CatRel.prod, Set.mem_prod, Set.prod,
+             CatRel.W, CatRel.R,
+             CatRel.Rel.external, CatRel.Rel.internal,
+             Set.mem_inter_iff, Set.mem_union, Set.mem_setOf_eq,
+             Set.mem_insert_iff, Set.mem_singleton_iff, Set.mem_empty_iff_false,
+             Set.mem_preimage, Prod.swap,
+             SetRel.dom, SetRel.cod, SetRel.dom_mkId,
+             Prod.mk.injEq, Prod.fst, Prod.snd,
+             and_false, false_and, false_or, or_false,
+             not_true, not_false_eq_true,
+             exists_false, exists_eq_left, exists_eq_left'] at hab
+  -- implied is impossible since rmw = ∅
+  rcases hab with ⟨mid, _, hmid_in | ⟨mid2, hmid2_in, _⟩⟩ | hab'
+  · obtain ⟨_, h⟩ := hmid_in
+    exact absurd h nofun
+  · obtain ⟨_, h⟩ := hmid2_in
+    exact absurd h nofun
+  -- remaining: xppo ∨ rfe ∨ fr ∨ co
+  rcases hab' with hxppo | (hrfe | (hfr | hco))
+  · obtain ⟨hprod, hpo⟩ := hxppo
+    simp only [Set.mem_setOf_eq] at hprod
+    change a ∈ sb_evts.all ∧ b ∈ sb_evts.all ∧ a.t_id = b.t_id ∧ a.id < b.id at hpo
+    obtain ⟨_, _, htid, hlt⟩ := hpo
+    rcases hprod with (⟨ha, hb⟩ | ⟨ha, hb⟩ | ⟨ha, hb⟩) <;>
+      rcases ha with rfl | rfl | rfl | rfl <;>
+        rcases hb with rfl | rfl | rfl | rfl <;>
+          simp_all
+  · obtain ⟨hrf, htid⟩ := hrfe
+    rcases hrf with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
+    · decide
+    · decide
+  · obtain ⟨w, hrf_inv, hco⟩ := hfr
+    rcases hrf_inv with ⟨hw, ha⟩ | ⟨hw, ha⟩ <;>
+      rcases hco with ⟨hw', hb⟩ | ⟨hw', hb⟩ <;>
+        subst ha hb hw <;> simp_all <;> (try decide) <;> (try (subst hw'; decide))
+  · rcases hco with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ <;> decide
+
+example : mips.pso sb_evts sb_test :=
+by
+  exact mipsWeakerThanTso sb_evts sb_test sb_tso
diff --git a/LeanCats/Linux/X86_SB_rfi_pos.lean b/LeanCats/Linux/X86_SB_rfi_pos.lean
new file mode 100644
index 0000000..1982833
--- /dev/null
+++ b/LeanCats/Linux/X86_SB_rfi_pos.lean
@@ -0,0 +1,197 @@
+import LeanCats.Basic
+import LeanCats.Data
+import LeanCats.Macro
+import LeanCats.ModelReader
+import LeanCats.Data
+import LeanCats.Relations
+import LeanCats.Theorems
+import LeanCats.Basic
+
+defcat <"mips.cat">
+defcat <"tsox.cat">
+
+set_option maxHeartbeats 2000000
+
+open Data
+
+namespace Litmus
+
+instance instWellformedPo (evts : Data.Events) : wellformed.po evts.po := by
+  intro x y z hxy hyz
+  rcases hxy with ⟨hx, hy, hxyTid, hxyLt⟩
+  rcases hyz with ⟨_, hz, hyzTid, hyzLt⟩
+  exact ⟨hx, hz, Eq.trans hxyTid hyzTid, Nat.lt_trans hxyLt hyzLt⟩
+
+instance instWellformedRmwEmpty (evts : Data.Events) : wellformed.rmw evts (∅ : SetRel Event Event) := by
+  intro e h
+  contradiction
+
+abbrev x := 0
+abbrev y := 1
+
+inductive Normal where
+| none : Normal
+
+@[simp] abbrev initOpX : Data.Effect :=
+  Data.Effect.mk Data.Op.write x (some 0) true false
+@[simp] abbrev initOpY : Data.Effect :=
+  Data.Effect.mk Data.Op.write y (some 0) true false
+@[simp] abbrev wOpX : Data.Effect :=
+  Data.Effect.mk Data.Op.write x (some 1) false false
+@[simp] abbrev wOpY : Data.Effect :=
+  Data.Effect.mk Data.Op.write y (some 1) false false
+@[simp] abbrev rOpX1 : Data.Effect :=
+  Data.Effect.mk Data.Op.read x (some 1) false false
+@[simp] abbrev rOpY1 : Data.Effect :=
+  Data.Effect.mk Data.Op.read y (some 1) false false
+@[simp] abbrev rOpX0 : Data.Effect :=
+  Data.Effect.mk Data.Op.read x (some 0) false false
+@[simp] abbrev rOpY0 : Data.Effect :=
+  Data.Effect.mk Data.Op.read y (some 0) false false
+
+@[simp] abbrev initWx : Data.Event :=
+  Data.Event.mk 100 10 initOpX ⟨Normal, Normal.none⟩
+@[simp] abbrev initWy : Data.Event :=
+  Data.Event.mk 101 10 initOpY ⟨Normal, Normal.none⟩
+
+@[simp] abbrev p0wX : Data.Event :=
+  Data.Event.mk 1 0 wOpX ⟨Normal, Normal.none⟩
+@[simp] abbrev p0rX1 : Data.Event :=
+  Data.Event.mk 2 0 rOpX1 ⟨Normal, Normal.none⟩
+@[simp] abbrev p0rY0 : Data.Event :=
+  Data.Event.mk 3 0 rOpY0 ⟨Normal, Normal.none⟩
+
+@[simp] abbrev p1wY : Data.Event :=
+  Data.Event.mk 4 1 wOpY ⟨Normal, Normal.none⟩
+@[simp] abbrev p1rY1 : Data.Event :=
+  Data.Event.mk 5 1 rOpY1 ⟨Normal, Normal.none⟩
+@[simp] abbrev p1rX0 : Data.Event :=
+  Data.Event.mk 6 1 rOpX0 ⟨Normal, Normal.none⟩
+
+/-- X86 SB+rfi-pos
+
+P0: W(x)=1; R(x)=1; R(y)=0
+P1: W(y)=1; R(y)=1; R(x)=0 -/
+@[simp] abbrev sbrfi_evts : Data.Events :=
+  Data.Events.mk
+    {initWx, initWy}
+    {p0rX1, p0rY0, p1rY1, p1rX0}
+    {initWx, initWy, p0wX, p1wY}
+    {}
+    {}
+    {}
+
+@[simp] def sbrfi_co : SetRel Event Event :=
+  {(initWx, p0wX), (initWy, p1wY)}
+
+instance : wellformed.co sbrfi_evts sbrfi_co where
+  irrefl := by aesop
+  trans := by aesop
+  preco := {
+    wellTyped := by aesop
+    total := by candidateExecution_wf
+  }
+
+/-- rf edges encode the expected outcome:
+  - rfi: p0wX -> p0rX1 and p1wY -> p1rY1
+  - reads of 0 from init writes: initWy -> p0rY0 and initWx -> p1rX0 -/
+@[simp] def sbrfi_rf : SetRel Event Event :=
+  {(p0wX, p0rX1), (p1wY, p1rY1), (initWy, p0rY0), (initWx, p1rX0)}
+
+@[simp] def sbrfi_rfInst : wellformed.rf sbrfi_evts sbrfi_rf :=
+  Data.wellformed.rf.mk
+    (by
+      candidateExecution_wf
+    )
+    (by
+      candidateExecution_wf
+    )
+
+@[simp] def sbrfi_test : CandidateExecution sbrfi_evts :=
+  {
+    evts := sbrfi_evts
+    po' := sbrfi_evts.po
+    prePo := instWellformedPo sbrfi_evts
+    rf' := sbrfi_rf
+    rfInst := sbrfi_rfInst
+    co' := sbrfi_co
+    rmw' := ∅
+    preRMW := instWellformedRmwEmpty sbrfi_evts
+    uniqueId := uniqueId_by_id sbrfi_evts
+    syncInF := by
+      intro e h
+      contradiction
+    rfiPo := by
+      intro w r hrf htid
+      simp [sbrfi_rf] at hrf
+      rcases hrf with h | h | h | h
+      · rcases h with ⟨rfl, rfl⟩
+        exact ⟨by simp [Data.Events.all], by simp [Data.Events.all], rfl, by decide⟩
+      · rcases h with ⟨rfl, rfl⟩
+        exact ⟨by simp [Data.Events.all], by simp [Data.Events.all], rfl, by decide⟩
+      · rcases h with ⟨rfl, rfl⟩
+        simp at htid
+      · rcases h with ⟨rfl, rfl⟩
+        simp at htid
+  }
+
+example : tsox.tso sbrfi_evts sbrfi_test := by
+  simp only [tsox.tso]
+  apply acyclic_of_rank (fun e => match e.id with
+    | 100 => 0  -- initWx
+    | 101 => 1  -- initWy
+    | 2   => 2  -- p0rX1
+    | 5   => 3  -- p1rY1
+    | 3   => 4  -- p0rY0
+    | 6   => 5  -- p1rX0
+    | 4   => 6  -- p1wY
+    | 1   => 7  -- p0wX
+    | _   => 8)
+  intro a b hab
+  simp only [CatRel.CatUnion.union, CatRel.SetRel.union, Set.mem_setOf_eq,
+             tsox.implied, tsox.xppo, tsox.At, rfe,
+             CandidateExecution.fr', SetRel.inv, SetRel.comp,
+             sbrfi_test, sbrfi_rf, sbrfi_co, sbrfi_evts,
+             Data.Events.all, Data.Events.po, SetRel.mkId,
+             CatRel.prod, Set.mem_prod, Set.prod,
+             CatRel.W, CatRel.R,
+             CatRel.Rel.external, CatRel.Rel.internal,
+             Set.mem_inter_iff, Set.mem_union, Set.mem_setOf_eq,
+             Set.mem_insert_iff, Set.mem_singleton_iff, Set.mem_empty_iff_false,
+             Set.mem_preimage, Prod.swap,
+             SetRel.dom, SetRel.cod, SetRel.dom_mkId,
+             Prod.mk.injEq, Prod.fst, Prod.snd,
+             and_false, false_and, false_or, or_false,
+             not_true, not_false_eq_true,
+             exists_false, exists_eq_left, exists_eq_left'] at hab
+  -- Eliminate implied branch (rmw = ∅ makes At = ∅, so SetRel.mkId of ∅ has no members)
+  rcases hab with ⟨mid, _, hmid_in | ⟨mid2, hmid2_in, _⟩⟩ | hab'
+  · obtain ⟨_, h⟩ := hmid_in; exact absurd h nofun
+  · obtain ⟨_, h⟩ := hmid2_in; exact absurd h nofun
+  -- Now hab' is: xppo ∨ rfe ∨ fr ∨ co
+  rcases hab' with hxppo | (hrfe | (hfr | hco))
+  -- xppo: ((W×W)|(R×W)|(R×R)) ∩ po
+  · obtain ⟨hprod, hpo⟩ := hxppo
+    simp only [Set.mem_setOf_eq] at hprod
+    change a ∈ sbrfi_evts.all ∧ b ∈ sbrfi_evts.all ∧ a.t_id = b.t_id ∧ a.id < b.id at hpo
+    obtain ⟨_, _, htid, hlt⟩ := hpo
+    rcases hprod with (⟨ha, hb⟩ | ⟨ha, hb⟩ | ⟨ha, hb⟩) <;>
+      rcases ha with rfl | rfl | rfl | rfl <;>
+        rcases hb with rfl | rfl | rfl | rfl <;>
+          simp_all
+  -- rfe: rf ∩ external (only external pairs survive)
+  · obtain ⟨hrf, htid⟩ := hrfe
+    rcases hrf with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
+    · exact absurd rfl htid  -- p0wX → p0rX1: same thread, contradiction
+    · exact absurd rfl htid  -- p1wY → p1rY1: same thread, contradiction
+    · decide  -- initWy → p0rY0: 1 < 4 ✓
+    · decide  -- initWx → p1rX0: 0 < 5 ✓
+  -- fr: rf⁻¹ ; co
+  · obtain ⟨w, hrf_inv, hco⟩ := hfr
+    rcases hrf_inv with ⟨hw, ha⟩ | ⟨hw, ha⟩ | ⟨hw, ha⟩ | ⟨hw, ha⟩ <;>
+      rcases hco with ⟨hw', hb⟩ | ⟨hw', hb⟩ <;>
+        subst ha hb hw <;> simp_all <;> (try decide) <;> (try (subst hw'; decide))
+  -- co
+  · rcases hco with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ <;> decide
+
+end Litmus
diff --git a/LeanCats/Linux/X86_mips_rf.lean b/LeanCats/Linux/X86_mips_rf.lean
new file mode 100644
index 0000000..2ca4bcd
--- /dev/null
+++ b/LeanCats/Linux/X86_mips_rf.lean
@@ -0,0 +1,137 @@
+import LeanCats.Basic
+import LeanCats.Data
+import LeanCats.Macro
+import LeanCats.ModelReader
+import LeanCats.Data
+import LeanCats.Relations
+import LeanCats.Theorems
+import LeanCats.Basic
+
+defcat <"mips.cat">
+defcat <"tsox.cat">
+
+-- In this litmus test, we want to show that sometimes the X86 is weaker than mips because of the sc-per-location.
+
+open Data
+
+namespace Litmus
+
+
+instance instWellformedPo (evts : Data.Events) : wellformed.po evts.po := by
+  intro x y z hxy hyz
+  rcases hxy with ⟨hx, hy, hxyTid, hxyLt⟩
+  rcases hyz with ⟨_, hz, hyzTid, hyzLt⟩
+  exact ⟨hx, hz, Eq.trans hxyTid hyzTid, Nat.lt_trans hxyLt hyzLt⟩
+
+instance instWellformedRmwEmpty (evts : Data.Events) : wellformed.rmw evts (∅ : SetRel Event Event) := by
+  intro e h
+  contradiction
+
+abbrev x := 0
+abbrev y := 1
+
+inductive Normal where
+| none : Normal
+
+@[simp] abbrev initOpX : Data.Effect :=
+  Data.Effect.mk Data.Op.write x (some 0) true false
+@[simp] abbrev initOpY : Data.Effect :=
+  Data.Effect.mk Data.Op.write y (some 0) true false
+@[simp] abbrev wOpX : Data.Effect :=
+  Data.Effect.mk Data.Op.write x (some 1) false false
+@[simp] abbrev wOpY : Data.Effect :=
+  Data.Effect.mk Data.Op.write y (some 1) false false
+@[simp] abbrev rOpX1 : Data.Effect :=
+  Data.Effect.mk Data.Op.read x (some 1) false false
+@[simp] abbrev rOpY1 : Data.Effect :=
+  Data.Effect.mk Data.Op.read y (some 1) false false
+@[simp] abbrev rOpX0 : Data.Effect :=
+  Data.Effect.mk Data.Op.read x (some 0) false false
+@[simp] abbrev rOpY0 : Data.Effect :=
+  Data.Effect.mk Data.Op.read y (some 0) false false
+
+@[simp] abbrev initWx : Data.Event :=
+  Data.Event.mk 100 10 initOpX ⟨Normal, Normal.none⟩
+@[simp] abbrev initWy : Data.Event :=
+  Data.Event.mk 101 10 initOpY ⟨Normal, Normal.none⟩
+
+@[simp] abbrev p0wX : Data.Event :=
+  Data.Event.mk 1 0 wOpX ⟨Normal, Normal.none⟩
+@[simp] abbrev p0rX1 : Data.Event :=
+  Data.Event.mk 2 0 rOpX1 ⟨Normal, Normal.none⟩
+@[simp] abbrev p0rY0 : Data.Event :=
+  Data.Event.mk 3 0 rOpY0 ⟨Normal, Normal.none⟩
+
+@[simp] abbrev p1wY : Data.Event :=
+  Data.Event.mk 4 1 wOpY ⟨Normal, Normal.none⟩
+@[simp] abbrev p1rY1 : Data.Event :=
+  Data.Event.mk 5 1 rOpY1 ⟨Normal, Normal.none⟩
+@[simp] abbrev p1rX0 : Data.Event :=
+  Data.Event.mk 6 1 rOpX0 ⟨Normal, Normal.none⟩
+
+/-- X86 SB+rfi-pos
+
+P0: W(x)=1; R(x)=1; R(y)=0
+P1: W(y)=1; R(y)=1; R(x)=0 -/
+@[simp] abbrev sbrfi_evts : Data.Events :=
+  Data.Events.mk
+    {initWx, initWy}
+    {p0rX1, p0rY0, p1rY1, p1rX0}
+    {initWx, initWy, p0wX, p1wY}
+    {}
+    {}
+    {}
+
+@[simp] def sbrfi_co : SetRel Event Event :=
+  {(initWx, p0wX), (initWy, p1wY)}
+
+instance : wellformed.co sbrfi_evts sbrfi_co where
+  irrefl := by aesop
+  trans := by aesop
+  preco := {
+    wellTyped := by aesop
+    total := by candidateExecution_wf
+  }
+
+/-- rf edges encode the expected outcome:
+  - rfi: p0wX -> p0rX1 and p1wY -> p1rY1
+  - reads of 0 from init writes: initWy -> p0rY0 and initWx -> p1rX0 -/
+@[simp] def sbrfi_rf : SetRel Event Event :=
+  {(p0wX, p0rX1), (p1wY, p1rY1), (initWy, p0rY0), (initWx, p1rX0)}
+
+@[simp] def sbrfi_rfInst : wellformed.rf sbrfi_evts sbrfi_rf :=
+  Data.wellformed.rf.mk
+    (by
+      candidateExecution_wf
+    )
+    (by
+      candidateExecution_wf
+    )
+
+@[simp] def sbrfi_test : CandidateExecution sbrfi_evts :=
+  {
+    evts := sbrfi_evts
+    po' := sbrfi_evts.po
+    prePo := instWellformedPo sbrfi_evts
+    rf' := sbrfi_rf
+    rfInst := sbrfi_rfInst
+    co' := sbrfi_co
+    rmw' := ∅
+    preRMW := instWellformedRmwEmpty sbrfi_evts
+    uniqueId := uniqueId_by_id sbrfi_evts
+    syncInF := by
+      intro e h
+      contradiction
+    rfiPo := by
+      intro w r hrf htid
+      simp [sbrfi_rf] at hrf
+      rcases hrf with h | h | h | h
+      · rcases h with ⟨rfl, rfl⟩
+        exact ⟨by simp [Data.Events.all], by simp [Data.Events.all], rfl, by decide⟩
+      · rcases h with ⟨rfl, rfl⟩
+        exact ⟨by simp [Data.Events.all], by simp [Data.Events.all], rfl, by decide⟩
+      · rcases h with ⟨rfl, rfl⟩
+        simp at htid
+      · rcases h with ⟨rfl, rfl⟩
+        simp at htid
+  }
diff --git a/LeanCats/Macro.lean b/LeanCats/Macro.lean
index 3d0cb97..e1bb938 100644
--- a/LeanCats/Macro.lean
+++ b/LeanCats/Macro.lean
@@ -53,6 +53,21 @@ instance : Coe (TSyntax `predefined_relations) (TSyntax `expr) where
 def SetRel.mkId (s : Set Event) : SetRel Event Event :=
   fun (e₁, e₂) => e₁ = e₂ ∧ e₁ ∈ s
 
+@[simp] theorem SetRel.dom_mkId (s : Set Event) : SetRel.dom (SetRel.mkId s) = s := by
+  ext e
+  constructor
+  · intro h
+    rcases h with ⟨e', heq, hs⟩
+    simpa [SetRel.mkId] using hs
+  · intro hs
+    exact ⟨e, rfl, hs⟩
+
+instance : Coe (Set Event) (SetRel Event Event) where
+  coe := SetRel.mkId
+
+instance : Coe (SetRel Event Event) (Set Event) where
+  coe := SetRel.dom
+
 macro_rules
   | `([dsl-term| $i:cat_ident, $evts, $X, $arg]) =>
     -- Apply the arg instead of using the id in the env.
@@ -92,6 +107,9 @@ macro_rules
   | `([expr| $e *, $evts, $X, $arg]) =>
     `(([expr| $e, $evts, $X, $arg]) ∪ {(e₁, e₂) | e₁ = e₂})
 
+  | `([expr| try $e with $_, $evts, $X, $arg]) =>
+    `(([expr| $e, $evts, $X, $arg]))
+
   | `([expr| $e +, $evts, $X, $arg]) =>
     `(([expr| $e, $evts, $X, $arg]))
 
@@ -165,6 +183,10 @@ macro_rules
     let nm := mkIdent "mb'".toName
     `($X.$nm)
 
+  | `([predefined-relations| SYNC , $_, $X]) =>
+    let nm := mkIdent "SYNC'".toName
+    `($X.$nm)
+
 macro_rules
   | `([keyword| and]) => Lean.Macro.throwUnsupported
   | `([keyword| as]) => Lean.Macro.throwUnsupported
@@ -195,6 +217,9 @@ macro_rules
   | `([annotable-events| W, $evts, $X]) =>
     let nm := mkIdent "W".toName
     `(($X.$evts.$nm : Set Event))
+  | `([annotable-events| _, $evts, $X]) =>
+    let nm := mkIdent "all".toName
+    `(($X.$evts.$nm : Set Event))
   | `([annotable-events| R, $evts, $X]) =>
     let nm := mkIdent "R".toName
     `(($X.$evts.$nm : Set Event))
@@ -211,8 +236,9 @@ macro_rules
     let nm := mkIdent "SRCU".toName
     `(($X.$evts.$nm : Set Event))
   | `([annotable-events| M, $evts, $X]) =>
-    let nm := mkIdent "M".toName
-    `(($X.$evts.$nm : Set Event))
+      let reads := mkIdent "R".toName
+      let writes := mkIdent "W".toName
+      `(($X.$evts.$reads ∪ $X.$evts.$writes : Set Event))
 
 macro_rules
   -- | `([predefined-events| ___]) => __ TODO!(figure all the definiations of all the events. (⋃?))
@@ -220,10 +246,6 @@ macro_rules
     let nm := mkIdent "IW".toName
     `($evts.$nm)
 
-  | `([predefined-events| M, $evts, $_]) =>
-    let nm := mkIdent "M".toName
-    `($evts.$nm)
-
   | `([predefined-events| $a:annotable_events, $evts, $X]) =>
     `([annotable-events| $a, $evts, $X])
 
diff --git a/LeanCats/ModelReader.lean b/LeanCats/ModelReader.lean
index fb2d022..5891291 100644
--- a/LeanCats/ModelReader.lean
+++ b/LeanCats/ModelReader.lean
@@ -26,7 +26,7 @@ def evalCat (s : String) : Lean.Elab.Command.CommandElabM Unit := do
 -- we can call IO under the CommandM.
 elab "defcat" "<" filename:str ">" : command => do
     let fn := Filename.mkName filename.getString
-    let path := "LeanCats/Cats/" ++ filename.getString
+    let path := "LeanCats/Cats/examples/models/" ++ filename.getString
     let s <- IO.FS.readFile path
     let model := "[model| " ++ fn.toString ++ " " ++ (removeComments s) ++ "]"
     -- Add the declaration to the environment
diff --git a/LeanCats/Syntax.lean b/LeanCats/Syntax.lean
index 2189679..c9e1cec 100644
--- a/LeanCats/Syntax.lean
+++ b/LeanCats/Syntax.lean
@@ -63,8 +63,8 @@ syntax "RMW" : annotable_events -- read-modify-write events
 syntax "SRCU" : annotable_events -- srcu events
 syntax "IW" : annotable_events -- initial writes
 syntax "M" : annotable_events -- memory events, M = W ∪ R
+syntax "_" : annotable_events -- all events
 
-syntax "___" : predefined_events -- all events
 syntax annotable_events : predefined_events
 
 /- defined_relations: -/
@@ -83,6 +83,7 @@ syntax "addr" : predefined_relations -- address dependencies, starts with a read
 syntax "rmb" : predefined_relations -- read memory barrier, read -> read
 syntax "wmb" : predefined_relations -- write memory barrier, write -> write
 syntax "fence" : predefined_relations -- fence barrier
+syntax "SYNC" : predefined_relations -- SYNC instruction for mips.
 
 syntax keyword : dsl_term
 syntax num : dsl_term
@@ -111,6 +112,8 @@ syntax:71 expr "^-1" : expr
 syntax dsl_term "(" expr,* ")" : expr
 
 syntax "[" expr "]" : expr
+-- Error handling in OCaml, we can just ignore it.
+syntax "try" expr "with" expr : expr
 
 syntax assertion expr ("as" cat_ident)? : inst
 -- The flag is used to witness the assertion, so it doesn't change the states of the execution, we could just ignore it.
diff --git a/LeanCats/Theorems.lean b/LeanCats/Theorems.lean
index 6b30f72..8d9beb4 100644
--- a/LeanCats/Theorems.lean
+++ b/LeanCats/Theorems.lean
@@ -234,3 +234,19 @@ theorem fr_co_subset_fr
   simp only [CandidateExecution.fr'] at *
   obtain ⟨w₀, h_inv, h_co⟩ := hfr
   exact ⟨w₀, h_inv, X.preCo.trans w₀ w w' h_co hco⟩
+
+/-- If a function f : Event → ℕ strictly increases along every edge of r,
+    then r is acyclic.  A transitive path can only increase f, so no cycle exists. -/
+lemma acyclic_of_rank
+    {r : SetRel Event Event}
+    (f : Event → ℕ)
+    (hf : ∀ a b, (a, b) ∈ r → f a < f b) :
+    SetRel.Acyclic r := by
+  intro a ha
+  simp only [SetRel.TransGen, Set.mem_setOf_eq] at ha
+  have key : ∀ x y, Relation.TransGen (fun e₁ e₂ => (e₁, e₂) ∈ r) x y → f x < f y := by
+    intro x y hxy
+    induction hxy with
+    | single h => exact hf _ _ h
+    | tail _ h ih => exact Nat.lt_trans ih (hf _ _ h)
+  exact Nat.lt_irrefl _ (key a a ha)
diff --git a/LeanCats/mipsWeakerThanTSO.lean b/LeanCats/mipsWeakerThanTSO.lean
new file mode 100644
index 0000000..d58d4d2
--- /dev/null
+++ b/LeanCats/mipsWeakerThanTSO.lean
@@ -0,0 +1,72 @@
+import LeanCats.Macro
+import LeanCats.ModelReader
+import LeanCats.Data
+import LeanCats.Relations
+import LeanCats.Theorems
+import LeanCats.Basic
+
+defcat <"mips.cat">
+defcat <"tsox.cat">
+
+-- SC is not sc per-location, thus X86 is not strictly stronger than mips.
+-- The X86 is not strong enough to prove the atomicity
+-- Because the X86 only make sure the execution is acyclic, but it's not.
+theorem mipsWeakerThanTso
+  (evts : Data.Events)
+  (X : CandidateExecution evts)
+  : tsox.tso evts X → mips.pso evts X :=
+by
+  intro htso
+  unfold tsox.tso at htso
+  unfold mips.pso
+  simp
+  . apply ayclicMono_trans htso
+    intro a b h
+    simp [CatRel.CatUnion.union, Set.mem_setOf_eq] at h
+    let rtso : SetRel Data.Event Data.Event :=
+      CatRel.CatUnion.union (tsox.implied evts X)
+        (CatRel.CatUnion.union (tsox.xppo evts X)
+          (CatRel.CatUnion.union (rfe evts X) (CatRel.CatUnion.union X.fr' X.co')))
+    change Relation.TransGen (fun e₁ e₂ => (e₁, e₂) ∈ rtso) a b
+    rcases h with hppo | h
+    · rcases hppo with ⟨hpo, hppo_core⟩
+      rcases hppo_core with hpo_rm | hsync_raw
+      · have hxppo : (a, b) ∈ tsox.xppo evts X := by
+          rcases hpo_rm with ⟨haR, hbM⟩
+          rcases hbM with hbR | hbW
+          · refine ⟨?_, hpo⟩
+            exact Or.inr (Or.inr ⟨haR, hbR⟩)
+          · refine ⟨?_, hpo⟩
+            exact Or.inr (Or.inl ⟨haR, hbW⟩)
+        have hstep : (a, b) ∈ rtso := by
+          exact Or.inr (Or.inl hxppo)
+        exact Relation.TransGen.single hstep
+      · rcases hsync_raw with ⟨mid, hhead, hpo_midb⟩
+        rcases hhead with ⟨hpo_amid, hall_sync⟩
+        rcases hall_sync with ⟨_, hmid_syncdom⟩
+        have hmidSYNC : mid ∈ X.SYNC' := by
+          simpa [SetRel.dom_mkId] using hmid_syncdom
+        have hsyncInF : X.SYNC' ⊆ X.evts.F := by
+          exact X.syncInF
+        have hmidF : mid ∈ X.evts.F := hsyncInF hmidSYNC
+        have himplied_ab : (a, b) ∈ tsox.implied evts X := by
+          unfold tsox.implied
+          simp [CatRel.CatUnion.union]
+          refine ⟨mid, hpo_amid, ?_⟩
+          refine Or.inr ?_
+          refine ⟨mid, ?_, hpo_midb⟩
+          exact ⟨rfl, Or.inr hmidF⟩
+        have hstep : (a, b) ∈ rtso := by
+          exact Or.inl himplied_ab
+        exact Relation.TransGen.single hstep
+    · rcases h with hrfe | h
+      · have hstep : (a, b) ∈ rtso := by
+          exact Or.inr (Or.inr (Or.inl hrfe))
+        exact Relation.TransGen.single hstep
+      · rcases h with hfr | hco
+        · have hstep : (a, b) ∈ rtso := by
+            exact Or.inr (Or.inr (Or.inr (Or.inl hfr)))
+          exact Relation.TransGen.single hstep
+        · have hstep : (a, b) ∈ rtso := by
+            exact Or.inr (Or.inr (Or.inr (Or.inr hco)))
+          exact Relation.TransGen.single hstep