From f219d60eb2ef256196b1dce457fd2e85ea7c0add Mon Sep 17 00:00:00 2001
From: Jan Tusil <jenda.tusil@gmail.com>
Date: Fri, 20 Dec 2019 14:15:06 +0100
Subject: [PATCH 1/2] just-left-unfold-Nth

---
 prover/prover.md               |  1 +
 prover/strategies/unfolding.md | 29 +++++++++++++++++++++++++++++
 2 files changed, 30 insertions(+)

diff --git a/prover/prover.md b/prover/prover.md
index f9f657136..6d2072b5a 100644
--- a/prover/prover.md
+++ b/prover/prover.md
@@ -31,6 +31,7 @@ module STRATEGIES-EXPORTED-SYNTAX
                     | "direct-proof"
                     | "check-lhs-constraint-unsat"
                     | "smt" | "smt-z3" | "smt-cvc4" | "smt-debug"
+                    | "just-left-unfold-Nth" "(" Int ")"
                     | "left-unfold" | "left-unfold-Nth" "(" Int ")"
                     | "right-unfold" | "right-unfold-Nth" "(" Int "," Int ")" | "right-unfold" "(" Symbol ")"
                     | "right-unfold-all"  "(" "bound" ":" Int ")"
diff --git a/prover/strategies/unfolding.md b/prover/strategies/unfolding.md
index 543a12faa..e0ce522d4 100644
--- a/prover/strategies/unfolding.md
+++ b/prover/strategies/unfolding.md
@@ -62,6 +62,35 @@ module STRATEGY-UNFOLDING
     => getUnfoldables(P) ++Patterns getUnfoldables(REST)
 ```
 
+### Just Left Unfold Nth
+
+Just unfolds the Nth predicate on the LHS.
+
+```k
+  rule <strategy> just-left-unfold-Nth(M)
+               => just-left-unfold-Nth-#1(M, getUnfoldables(LHS))
+                  ...
+       </strategy>
+       <claim> \implies(\and(LHS), RHS) </claim>
+
+  syntax Strategy ::= "just-left-unfold-Nth-#1"  "(" Int "," Patterns ")"
+                    | "just-left-unfold-Nth-#2"  "(" Pattern "," Pattern ")"
+
+
+  rule <strategy> just-left-unfold-Nth-#1(M, PS)
+               => just-left-unfold-Nth-#2(getMember(M, PS), unfold(getMember(M, PS)))
+                  ...
+       </strategy>
+  requires 0 <=Int M andBool M <Int getLength(PS)
+
+  rule <claim> \implies(LHS => subst(LHS, PATTERN, BODY), RHS) </claim>
+       <strategy> just-left-unfold-Nth-#2(PATTERN, BODY)
+               => noop
+                  ...
+       </strategy>
+
+```
+
 ### Left Unfold (incomplete)
 
 ```k

From 3e1008a0941d0a01ae82f523f7981b8faa8a7fc7 Mon Sep 17 00:00:00 2001
From: Jan Tusil <jenda.tusil@gmail.com>
Date: Sun, 12 Jan 2020 16:28:57 +0100
Subject: [PATCH 2/2] just-right-unfold-Nth

---
 prover/prover.md               |  1 +
 prover/strategies/unfolding.md | 28 ++++++++++++++++++++++++++++
 2 files changed, 29 insertions(+)

diff --git a/prover/prover.md b/prover/prover.md
index 6d2072b5a..b198676cb 100644
--- a/prover/prover.md
+++ b/prover/prover.md
@@ -32,6 +32,7 @@ module STRATEGIES-EXPORTED-SYNTAX
                     | "check-lhs-constraint-unsat"
                     | "smt" | "smt-z3" | "smt-cvc4" | "smt-debug"
                     | "just-left-unfold-Nth" "(" Int ")"
+                    | "just-right-unfold-Nth" "(" Int ")"
                     | "left-unfold" | "left-unfold-Nth" "(" Int ")"
                     | "right-unfold" | "right-unfold-Nth" "(" Int "," Int ")" | "right-unfold" "(" Symbol ")"
                     | "right-unfold-all"  "(" "bound" ":" Int ")"
diff --git a/prover/strategies/unfolding.md b/prover/strategies/unfolding.md
index e0ce522d4..e69f5fadb 100644
--- a/prover/strategies/unfolding.md
+++ b/prover/strategies/unfolding.md
@@ -62,6 +62,34 @@ module STRATEGY-UNFOLDING
     => getUnfoldables(P) ++Patterns getUnfoldables(REST)
 ```
 
+### Just Right Unfold
+
+```k
+
+  rule <strategy> just-right-unfold-Nth(M)
+               => just-right-unfold-Nth-#1(M, getUnfoldables(RHS))
+                  ...
+       </strategy>
+       <claim> \implies(\and(LHS), RHS) </claim>
+
+  syntax Strategy ::= "just-right-unfold-Nth-#1"  "(" Int "," Patterns ")"
+                    | "just-right-unfold-Nth-#2"  "(" Pattern "," Pattern ")"
+
+
+  rule <strategy> just-right-unfold-Nth-#1(M, PS)
+               => just-right-unfold-Nth-#2(getMember(M, PS), unfold(getMember(M, PS)))
+                  ...
+       </strategy>
+  requires 0 <=Int M andBool M <Int getLength(PS)
+
+  rule <claim> \implies(LHS, RHS => subst(RHS, PATTERN, BODY)) </claim>
+       <strategy> just-right-unfold-Nth-#2(PATTERN, BODY)
+               => noop
+                  ...
+       </strategy>
+```
+
+
 ### Just Left Unfold Nth
 
 Just unfolds the Nth predicate on the LHS.