spatial-patterns-match: works with multiple seps anywhere on lhs

kframework · Apr 22, 2020 · 98e7f3b · 98e7f3b
1 parent 8d0b0a6
commit 98e7f3b
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md
@@ -702,10 +702,11 @@ Instantiate the axiom: `\forall { L, D } (pto L D) -> L != nil
     //      </strategy>
     //   requires RSPATIAL -Patterns REST ==K .Patterns
 
-    rule <claim> \implies(LHS, RHS) </claim>
+    rule <claim> \implies(\and(LHS), RHS)
+              => \implies(\and(LHS -Patterns getSpatialPatterns(LHS)), RHS)
+         </claim>
          <strategy> spatial-patterns-match => noop ... </strategy>
-       requires isPredicatePattern(LHS)
-        andBool isPredicatePattern(RHS)
+       requires isPredicatePattern(RHS)
 ```
 
 ### Footprint Analysis