fix loadL and loadR rule

m4lvin · Jul 7, 2024 · 3b86ccf · 3b86ccf
1 parent 75644ea
commit 3b86ccf
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Pdl/Tableau.lean b/Pdl/Tableau.lean
@@ -57,9 +57,9 @@ theorem LoadedPathRepeat_isLoaded (lpr : LoadedPathRepeat Hist X) : X.isLoaded :
 inductive PdlRule : (Γ : TNode) → (Δ : TNode) → Type
   -- The (L+) rule:
   | loadL : (~⌈⌈δ⌉⌉⌈α⌉φ) ∈ L → PdlRule (L, R, none)
-                                       (L.erase (~⌈⌈δ⌉⌉φ), R, some (Sum.inl (~'(⌊⌊δ⌋⌋⌊α⌋φ))))
+                                       (L.erase (~⌈⌈δ⌉⌉⌈α⌉φ), R, some (Sum.inl (~'(⌊⌊δ⌋⌋⌊α⌋φ))))
   | loadR : (~⌈⌈δ⌉⌉⌈α⌉φ) ∈ R → PdlRule (L, R, none)
-                                       (L, R.erase (~⌈⌈δ⌉⌉φ), some (Sum.inr (~'(⌊⌊δ⌋⌋⌊α⌋φ))))
+                                       (L, R.erase (~⌈⌈δ⌉⌉⌈α⌉φ), some (Sum.inr (~'(⌊⌊δ⌋⌋⌊α⌋φ))))
   -- The (L-) rule:
   | freeL : PdlRule (L, R, some (Sum.inl (~'(⌊⌊δ⌋⌋⌊α⌋(φ : Formula)))))
                     (L.insert (~⌈⌈δ⌉⌉⌈α⌉φ), R, none)