update

boogie-org · Dec 6, 2023 · 3b42eea · 3b42eea
1 parent 0e4cea1
commit 3b42eea
Showing 1 changed file with 7 additions and 3 deletions.
diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl
@@ -156,12 +156,16 @@ axiom (forall<T> a: Set T, t: T :: {Set_Add(a, t)} Set_Size(Set_Add(a, t)) == if
 axiom (forall<T> a: Set T, t: T :: {Set_Remove(a, t)} Set_Size(Set_Remove(a, t)) == if Set_Contains(a, t) then Set_Size(a) - 1 else Set_Size(a));
 
 axiom (forall<T> a: Set T, b: Set T ::
-        {Set_Difference(a, b)} {Set_Intersection(a, b)}
+        {Set_Difference(a, b)} {Set_Intersection(a, b)} {Set_Union(a, b)}
         Set_Size(a) == Set_Size(Set_Difference(a, b)) + Set_Size(Set_Intersection(a, b)));
 
 axiom (forall<T> a: Set T, b: Set T ::
-        {Set_Union(a, b)} {Set_Difference(a, b)} {Set_Difference(b, a)} {Set_Intersection(a, b)}
-        Set_Size(Set_Union(a, b)) == Set_Size(Set_Difference(a, b)) + Set_Size(Set_Difference(b, a)) + Set_Size(Set_Intersection(a, b)));
+        {Set_Union(a, b)} {Set_Intersection(a, b)}
+        Set_Size(Set_Union(a, b)) + Set_Size(Set_Intersection(a, b)) == Set_Size(a) + Set_Size(b));
+
+axiom (forall<T> a: Set T, b: Set T :: Set_Union(a, b) == Set_Union(b, a));
+
+axiom (forall<T> a: Set T, b: Set T :: Set_Intersection(a, b) == Set_Intersection(b, a));
 
 function {:inline} Set_Empty<T>(): Set T
 {