From 52a927a5ffe5315059df8484e71139481c327ce2 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Tue, 19 Jul 2011 10:56:21 -0700
Subject: Fixed axiom for Take/Update commuting.

---
 Binaries/DafnyPrelude.bpl | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'Binaries')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 50852724..32430fd3 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -201,8 +201,9 @@ axiom (forall<T> a: Seq T, b: Seq T ::
 // update axiom
 axiom (forall<T> s: Seq T, i: int, v: T, x: T ::
   { MultiSet#FromSeq(Seq#Update(s, i, v))[x] }
+    0 <= i && i < Seq#Length(s) ==>
     MultiSet#FromSeq(Seq#Update(s, i, v))[x] ==
-	  MultiSet#Union(MultiSet#Difference(MultiSet#FromSeq(s), MultiSet#Singleton(Seq#Index(s,i))), MultiSet#Singleton(v))[x] );
+      MultiSet#Union(MultiSet#Difference(MultiSet#FromSeq(s), MultiSet#Singleton(Seq#Index(s,i))), MultiSet#Singleton(v))[x] );
   // i.e. MS(Update(s, i, v)) == MS(s) - {{s[i]}} + {{v}}
 axiom (forall<T> s: Seq T, x: T :: { MultiSet#FromSeq(s)[x] }
   (exists i : int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && x == Seq#Index(s,i)) <==> 0 < MultiSet#FromSeq(s)[x] );
@@ -329,7 +330,7 @@ axiom (forall h: HeapType, i: int, v: BoxType, a: ref ::
 // Commutability of Take and Drop with Update.
 axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
   { Seq#Take(Seq#Update(s, i, v), n) }
-    0 <= i && i < n && i < Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Update(Seq#Take(s, n), i, v) );
+    0 <= i && i < n && n <= Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Update(Seq#Take(s, n), i, v) );
 axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
   { Seq#Take(Seq#Update(s, i, v), n) }
     n <= i && i < Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Take(s, n));
-- 
cgit v1.2.3