ih progress

dafny-lang · Jan 30, 2024 · 4f98c5a · 4f98c5a
1 parent addb406
commit 4f98c5a
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/Util/FisherYates/Model.dfy b/src/Util/FisherYates/Model.dfy
@@ -32,6 +32,10 @@ module FisherYates.Model {
     requires 0 <= j < |s|
     ensures multiset(s) == multiset(t)
     ensures |s| == |t|
+    ensures i == j ==> s == t
+    ensures t[..i] == s[..i]
+    ensures i < j ==> t[i+1..j] == s[i+1..j]
+    ensures t[j+1..] == s[j+1..]
   {
     if i == j then
       s