diff options
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index eeb4f103..8d89715f 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -39,6 +39,10 @@ axiom (forall<T> a, b: Set T, y: T :: { Set#Union(a, b), a[y] } a[y] ==> Set#Union(a, b)[y]);
axiom (forall<T> a, b: Set T, y: T :: { Set#Union(a, b), b[y] }
b[y] ==> Set#Union(a, b)[y]);
+axiom (forall<T> a, b: Set T :: { Set#Union(a, b) }
+ Set#Disjoint(a, b) ==>
+ Set#Difference(Set#Union(a, b), a) == b &&
+ Set#Difference(Set#Union(a, b), b) == a);
function Set#Intersection<T>(Set T, Set T) returns (Set T);
axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] }
|