spatial-patterns-equal: handles case of multiple seps on RHS

kframework · Apr 23, 2020 · b8bc773 · b8bc773
1 parent ea25556
commit b8bc773
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md
@@ -645,12 +645,17 @@ Instantiate the axiom: `\forall { L, D } (pto L D) -> L != nil
       => \equals(S1(ARGs1), S2(ARGs2)), #destructEquality(Ps1, Ps2)
       requires S1 =/=K S2 orBool notBool isConstructor(S1)
 
+    rule <claim> \implies(LHS, \exists { Vs } RHS)
+         </claim>
+         <strategy> spatial-patterns-equal => noop ... </strategy>
+      requires isPredicatePattern(RHS)
+
     rule <claim> \implies(               \and(sep(LSPATIAL), LHS)
                          , \exists{ Vs } \and(sep(RSPATIAL), RHS)
                          )
               => \implies(\and(LHS), \exists { Vs } \and(RHS))
          </claim>
-         <strategy> spatial-patterns-equal => noop ... </strategy>
+         <strategy> spatial-patterns-equal ... </strategy>
       requires LSPATIAL -Patterns RSPATIAL ==K .Patterns
        andBool RSPATIAL -Patterns LSPATIAL ==K .Patterns