From b8bc77300c60d15ec520ad8acf63f547512b06a6 Mon Sep 17 00:00:00 2001
From: Lucas Pena <lpena7@illinois.edu>
Date: Thu, 23 Apr 2020 16:29:23 -0500
Subject: [PATCH] spatial-patterns-equal: handles case of multiple seps on RHS

---
 prover/strategies/matching.md | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md
index c8caa5f58..7e990a5fe 100644
--- 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