summaryrefslogtreecommitdiff
path: root/Test/dafny4/Bug136.dfy.expect
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny4/Bug136.dfy.expect')
-rw-r--r--Test/dafny4/Bug136.dfy.expect1772
1 files changed, 1772 insertions, 0 deletions
diff --git a/Test/dafny4/Bug136.dfy.expect b/Test/dafny4/Bug136.dfy.expect
new file mode 100644
index 00000000..8b9d32a8
--- /dev/null
+++ b/Test/dafny4/Bug136.dfy.expect
@@ -0,0 +1,1772 @@
+// Dafny program verifier version 1.9.6.21116, Copyright (c) 2003-2015, Microsoft.
+// Command Line Options: -nologo -countVerificationErrors:0 -useBaseNameForFileName /compile:0 /print:- c:\dafny\Test\dafny4\Bug136.dfy
+
+const $$Language$Dafny: bool;
+
+axiom $$Language$Dafny;
+
+type Ty;
+
+const unique TBool: Ty;
+
+const unique TChar: Ty;
+
+const unique TInt: Ty;
+
+const unique TNat: Ty;
+
+const unique TReal: Ty;
+
+function TSet(Ty) : Ty;
+
+function TISet(Ty) : Ty;
+
+function TMultiSet(Ty) : Ty;
+
+function TSeq(Ty) : Ty;
+
+function TMap(Ty, Ty) : Ty;
+
+function TIMap(Ty, Ty) : Ty;
+
+function Inv0_TSet(Ty) : Ty;
+
+axiom (forall t: Ty :: { TSet(t) } Inv0_TSet(TSet(t)) == t);
+
+function Inv0_TISet(Ty) : Ty;
+
+axiom (forall t: Ty :: { TISet(t) } Inv0_TISet(TISet(t)) == t);
+
+function Inv0_TSeq(Ty) : Ty;
+
+axiom (forall t: Ty :: { TSeq(t) } Inv0_TSeq(TSeq(t)) == t);
+
+function Inv0_TMultiSet(Ty) : Ty;
+
+axiom (forall t: Ty :: { TMultiSet(t) } Inv0_TMultiSet(TMultiSet(t)) == t);
+
+function Inv0_TMap(Ty) : Ty;
+
+function Inv1_TMap(Ty) : Ty;
+
+axiom (forall t: Ty, u: Ty :: { TMap(t, u) } Inv0_TMap(TMap(t, u)) == t);
+
+axiom (forall t: Ty, u: Ty :: { TMap(t, u) } Inv1_TMap(TMap(t, u)) == u);
+
+function Inv0_TIMap(Ty) : Ty;
+
+function Inv1_TIMap(Ty) : Ty;
+
+axiom (forall t: Ty, u: Ty :: { TIMap(t, u) } Inv0_TIMap(TIMap(t, u)) == t);
+
+axiom (forall t: Ty, u: Ty :: { TIMap(t, u) } Inv1_TIMap(TIMap(t, u)) == u);
+
+type TyTag;
+
+function Tag(Ty) : TyTag;
+
+const unique TagBool: TyTag;
+
+const unique TagChar: TyTag;
+
+const unique TagInt: TyTag;
+
+const unique TagNat: TyTag;
+
+const unique TagReal: TyTag;
+
+const unique TagSet: TyTag;
+
+const unique TagISet: TyTag;
+
+const unique TagMultiSet: TyTag;
+
+const unique TagSeq: TyTag;
+
+const unique TagMap: TyTag;
+
+const unique TagIMap: TyTag;
+
+const unique TagClass: TyTag;
+
+axiom Tag(TBool) == TagBool;
+
+axiom Tag(TChar) == TagChar;
+
+axiom Tag(TInt) == TagInt;
+
+axiom Tag(TNat) == TagNat;
+
+axiom Tag(TReal) == TagReal;
+
+axiom (forall t: Ty :: { TSet(t) } Tag(TSet(t)) == TagSet);
+
+axiom (forall t: Ty :: { TISet(t) } Tag(TISet(t)) == TagISet);
+
+axiom (forall t: Ty :: { TMultiSet(t) } Tag(TMultiSet(t)) == TagMultiSet);
+
+axiom (forall t: Ty :: { TSeq(t) } Tag(TSeq(t)) == TagSeq);
+
+axiom (forall t: Ty, u: Ty :: { TMap(t, u) } Tag(TMap(t, u)) == TagMap);
+
+axiom (forall t: Ty, u: Ty :: { TIMap(t, u) } Tag(TIMap(t, u)) == TagIMap);
+
+function {:identity} LitInt(x: int) : int;
+
+axiom (forall x: int :: {:identity} { LitInt(x): int } LitInt(x): int == x);
+
+axiom (forall x: int :: { $Box(LitInt(x)) } $Box(LitInt(x)) == Lit($Box(x)));
+
+function {:identity} LitReal(x: real) : real;
+
+axiom (forall x: real :: {:identity} { LitReal(x): real } LitReal(x): real == x);
+
+axiom (forall x: real :: { $Box(LitReal(x)) } $Box(LitReal(x)) == Lit($Box(x)));
+
+function {:identity} Lit<T>(x: T) : T;
+
+axiom (forall<T> x: T :: {:identity} { Lit(x): T } Lit(x): T == x);
+
+axiom (forall<T> x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)));
+
+type char;
+
+function char#FromInt(int) : char;
+
+function char#ToInt(char) : int;
+
+axiom (forall ch: char :: { char#ToInt(ch) } char#FromInt(char#ToInt(ch)) == ch);
+
+axiom (forall n: int ::
+ { char#FromInt(n) }
+ 0 <= n && n < 65536 ==> char#ToInt(char#FromInt(n)) == n);
+
+type ref;
+
+const null: ref;
+
+const unique NoTraitAtAll: ClassName;
+
+function TraitParent(ClassName) : ClassName;
+
+type Box;
+
+const $ArbitraryBoxValue: Box;
+
+function $Box<T>(T) : Box;
+
+function $Unbox<T>(Box) : T;
+
+axiom (forall<T> x: T :: { $Box(x) } $Unbox($Box(x)) == x);
+
+axiom (forall bx: Box ::
+ { $IsBox(bx, TInt) }
+ $IsBox(bx, TInt) ==> $Box($Unbox(bx): int) == bx && $Is($Unbox(bx): int, TInt));
+
+axiom (forall bx: Box ::
+ { $IsBox(bx, TNat) }
+ $IsBox(bx, TNat) ==> $Box($Unbox(bx): int) == bx && $Is($Unbox(bx): int, TNat));
+
+axiom (forall bx: Box ::
+ { $IsBox(bx, TReal) }
+ $IsBox(bx, TReal)
+ ==> $Box($Unbox(bx): real) == bx && $Is($Unbox(bx): real, TReal));
+
+axiom (forall bx: Box ::
+ { $IsBox(bx, TBool) }
+ $IsBox(bx, TBool)
+ ==> $Box($Unbox(bx): bool) == bx && $Is($Unbox(bx): bool, TBool));
+
+axiom (forall bx: Box ::
+ { $IsBox(bx, TChar) }
+ $IsBox(bx, TChar)
+ ==> $Box($Unbox(bx): char) == bx && $Is($Unbox(bx): char, TChar));
+
+axiom (forall bx: Box, t: Ty ::
+ { $IsBox(bx, TSet(t)) }
+ $IsBox(bx, TSet(t))
+ ==> $Box($Unbox(bx): Set Box) == bx && $Is($Unbox(bx): Set Box, TSet(t)));
+
+axiom (forall bx: Box, t: Ty ::
+ { $IsBox(bx, TISet(t)) }
+ $IsBox(bx, TISet(t))
+ ==> $Box($Unbox(bx): ISet Box) == bx && $Is($Unbox(bx): ISet Box, TISet(t)));
+
+axiom (forall bx: Box, t: Ty ::
+ { $IsBox(bx, TMultiSet(t)) }
+ $IsBox(bx, TMultiSet(t))
+ ==> $Box($Unbox(bx): MultiSet Box) == bx
+ && $Is($Unbox(bx): MultiSet Box, TMultiSet(t)));
+
+axiom (forall bx: Box, t: Ty ::
+ { $IsBox(bx, TSeq(t)) }
+ $IsBox(bx, TSeq(t))
+ ==> $Box($Unbox(bx): Seq Box) == bx && $Is($Unbox(bx): Seq Box, TSeq(t)));
+
+axiom (forall bx: Box, s: Ty, t: Ty ::
+ { $IsBox(bx, TMap(s, t)) }
+ $IsBox(bx, TMap(s, t))
+ ==> $Box($Unbox(bx): Map Box Box) == bx && $Is($Unbox(bx): Map Box Box, TMap(s, t)));
+
+axiom (forall bx: Box, s: Ty, t: Ty ::
+ { $IsBox(bx, TIMap(s, t)) }
+ $IsBox(bx, TIMap(s, t))
+ ==> $Box($Unbox(bx): IMap Box Box) == bx
+ && $Is($Unbox(bx): IMap Box Box, TIMap(s, t)));
+
+axiom (forall<T> v: T, t: Ty ::
+ { $IsBox($Box(v), t) }
+ $IsBox($Box(v), t) <==> $Is(v, t));
+
+axiom (forall<T> v: T, t: Ty, h: Heap ::
+ { $IsAllocBox($Box(v), t, h) }
+ $IsAllocBox($Box(v), t, h) <==> $IsAlloc(v, t, h));
+
+function $Is<T>(T, Ty) : bool;
+
+function $IsAlloc<T>(T, Ty, Heap) : bool;
+
+function $IsBox<T>(T, Ty) : bool;
+
+function $IsAllocBox<T>(T, Ty, Heap) : bool;
+
+axiom (forall v: int :: { $Is(v, TInt) } $Is(v, TInt));
+
+axiom (forall v: int :: { $Is(v, TNat) } $Is(v, TNat) <==> v >= 0);
+
+axiom (forall v: real :: { $Is(v, TReal) } $Is(v, TReal));
+
+axiom (forall v: bool :: { $Is(v, TBool) } $Is(v, TBool));
+
+axiom (forall v: char :: { $Is(v, TChar) } $Is(v, TChar));
+
+axiom (forall h: Heap, v: int :: { $IsAlloc(v, TInt, h) } $IsAlloc(v, TInt, h));
+
+axiom (forall h: Heap, v: int :: { $IsAlloc(v, TNat, h) } $IsAlloc(v, TNat, h));
+
+axiom (forall h: Heap, v: real :: { $IsAlloc(v, TReal, h) } $IsAlloc(v, TReal, h));
+
+axiom (forall h: Heap, v: bool :: { $IsAlloc(v, TBool, h) } $IsAlloc(v, TBool, h));
+
+axiom (forall h: Heap, v: char :: { $IsAlloc(v, TChar, h) } $IsAlloc(v, TChar, h));
+
+axiom (forall v: Set Box, t0: Ty ::
+ { $Is(v, TSet(t0)) }
+ $Is(v, TSet(t0)) <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsBox(bx, t0)));
+
+axiom (forall v: ISet Box, t0: Ty ::
+ { $Is(v, TISet(t0)) }
+ $Is(v, TISet(t0)) <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsBox(bx, t0)));
+
+axiom (forall v: MultiSet Box, t0: Ty ::
+ { $Is(v, TMultiSet(t0)) }
+ $Is(v, TMultiSet(t0))
+ <==> (forall bx: Box :: { v[bx] } 0 < v[bx] ==> $IsBox(bx, t0)));
+
+axiom (forall v: MultiSet Box, t0: Ty ::
+ { $Is(v, TMultiSet(t0)) }
+ $Is(v, TMultiSet(t0)) ==> $IsGoodMultiSet(v));
+
+axiom (forall v: Seq Box, t0: Ty ::
+ { $Is(v, TSeq(t0)) }
+ $Is(v, TSeq(t0))
+ <==> (forall i: int ::
+ { Seq#Index(v, i) }
+ 0 <= i && i < Seq#Length(v) ==> $IsBox(Seq#Index(v, i), t0)));
+
+axiom (forall v: Set Box, t0: Ty, h: Heap ::
+ { $IsAlloc(v, TSet(t0), h) }
+ $IsAlloc(v, TSet(t0), h)
+ <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsAllocBox(bx, t0, h)));
+
+axiom (forall v: ISet Box, t0: Ty, h: Heap ::
+ { $IsAlloc(v, TISet(t0), h) }
+ $IsAlloc(v, TISet(t0), h)
+ <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsAllocBox(bx, t0, h)));
+
+axiom (forall v: MultiSet Box, t0: Ty, h: Heap ::
+ { $IsAlloc(v, TMultiSet(t0), h) }
+ $IsAlloc(v, TMultiSet(t0), h)
+ <==> (forall bx: Box :: { v[bx] } 0 < v[bx] ==> $IsAllocBox(bx, t0, h)));
+
+axiom (forall v: Seq Box, t0: Ty, h: Heap ::
+ { $IsAlloc(v, TSeq(t0), h) }
+ $IsAlloc(v, TSeq(t0), h)
+ <==> (forall i: int ::
+ { Seq#Index(v, i) }
+ 0 <= i && i < Seq#Length(v) ==> $IsAllocBox(Seq#Index(v, i), t0, h)));
+
+axiom (forall v: Map Box Box, t0: Ty, t1: Ty ::
+ { $Is(v, TMap(t0, t1)) }
+ $Is(v, TMap(t0, t1))
+ <==> (forall bx: Box ::
+ { Map#Elements(v)[bx] } { Map#Domain(v)[bx] }
+ Map#Domain(v)[bx] ==> $IsBox(Map#Elements(v)[bx], t1) && $IsBox(bx, t0)));
+
+axiom (forall v: Map Box Box, t0: Ty, t1: Ty, h: Heap ::
+ { $IsAlloc(v, TMap(t0, t1), h) }
+ $IsAlloc(v, TMap(t0, t1), h)
+ <==> (forall bx: Box ::
+ { Map#Elements(v)[bx] } { Map#Domain(v)[bx] }
+ Map#Domain(v)[bx]
+ ==> $IsAllocBox(Map#Elements(v)[bx], t1, h) && $IsAllocBox(bx, t0, h)));
+
+axiom (forall v: IMap Box Box, t0: Ty, t1: Ty ::
+ { $Is(v, TIMap(t0, t1)) }
+ $Is(v, TIMap(t0, t1))
+ <==> (forall bx: Box ::
+ { IMap#Elements(v)[bx] } { IMap#Domain(v)[bx] }
+ IMap#Domain(v)[bx] ==> $IsBox(IMap#Elements(v)[bx], t1) && $IsBox(bx, t0)));
+
+axiom (forall v: IMap Box Box, t0: Ty, t1: Ty, h: Heap ::
+ { $IsAlloc(v, TIMap(t0, t1), h) }
+ $IsAlloc(v, TIMap(t0, t1), h)
+ <==> (forall bx: Box ::
+ { IMap#Elements(v)[bx] } { IMap#Domain(v)[bx] }
+ IMap#Domain(v)[bx]
+ ==> $IsAllocBox(IMap#Elements(v)[bx], t1, h) && $IsAllocBox(bx, t0, h)));
+
+type ClassName;
+
+const unique class._System.int: ClassName;
+
+const unique class._System.bool: ClassName;
+
+const unique class._System.set: ClassName;
+
+const unique class._System.seq: ClassName;
+
+const unique class._System.multiset: ClassName;
+
+function Tclass._System.object() : Ty;
+
+function dtype(ref) : Ty;
+
+function TypeTuple(a: ClassName, b: ClassName) : ClassName;
+
+function TypeTupleCar(ClassName) : ClassName;
+
+function TypeTupleCdr(ClassName) : ClassName;
+
+axiom (forall a: ClassName, b: ClassName ::
+ { TypeTuple(a, b) }
+ TypeTupleCar(TypeTuple(a, b)) == a && TypeTupleCdr(TypeTuple(a, b)) == b);
+
+type HandleType;
+
+function SetRef_to_SetBox(s: [ref]bool) : Set Box;
+
+axiom (forall s: [ref]bool, bx: Box ::
+ { SetRef_to_SetBox(s)[bx] }
+ SetRef_to_SetBox(s)[bx] == s[$Unbox(bx): ref]);
+
+axiom (forall s: [ref]bool ::
+ { SetRef_to_SetBox(s) }
+ $Is(SetRef_to_SetBox(s), TSet(Tclass._System.object())));
+
+type DatatypeType;
+
+type DtCtorId;
+
+function DatatypeCtorId(DatatypeType) : DtCtorId;
+
+function DtRank(DatatypeType) : int;
+
+function BoxRank(Box) : int;
+
+axiom (forall d: DatatypeType :: { BoxRank($Box(d)) } BoxRank($Box(d)) == DtRank(d));
+
+const $ModuleContextHeight: int;
+
+const $FunctionContextHeight: int;
+
+type LayerType;
+
+const $LZ: LayerType;
+
+function $LS(LayerType) : LayerType;
+
+function AtLayer<A>([LayerType]A, LayerType) : A;
+
+axiom (forall<A> f: [LayerType]A, ly: LayerType ::
+ { AtLayer(f, ly) }
+ AtLayer(f, ly) == f[ly]);
+
+axiom (forall<A> f: [LayerType]A, ly: LayerType ::
+ { AtLayer(f, $LS(ly)) }
+ AtLayer(f, $LS(ly)) == AtLayer(f, ly));
+
+type Field _;
+
+function FDim<T>(Field T) : int;
+
+function IndexField(int) : Field Box;
+
+axiom (forall i: int :: { IndexField(i) } FDim(IndexField(i)) == 1);
+
+function IndexField_Inverse<T>(Field T) : int;
+
+axiom (forall i: int :: { IndexField(i) } IndexField_Inverse(IndexField(i)) == i);
+
+function MultiIndexField(Field Box, int) : Field Box;
+
+axiom (forall f: Field Box, i: int ::
+ { MultiIndexField(f, i) }
+ FDim(MultiIndexField(f, i)) == FDim(f) + 1);
+
+function MultiIndexField_Inverse0<T>(Field T) : Field T;
+
+function MultiIndexField_Inverse1<T>(Field T) : int;
+
+axiom (forall f: Field Box, i: int ::
+ { MultiIndexField(f, i) }
+ MultiIndexField_Inverse0(MultiIndexField(f, i)) == f
+ && MultiIndexField_Inverse1(MultiIndexField(f, i)) == i);
+
+function DeclType<T>(Field T) : ClassName;
+
+type NameFamily;
+
+function DeclName<T>(Field T) : NameFamily;
+
+function FieldOfDecl<alpha>(ClassName, NameFamily) : Field alpha;
+
+axiom (forall<T> cl: ClassName, nm: NameFamily ::
+ { FieldOfDecl(cl, nm): Field T }
+ DeclType(FieldOfDecl(cl, nm): Field T) == cl
+ && DeclName(FieldOfDecl(cl, nm): Field T) == nm);
+
+function $IsGhostField<T>(Field T) : bool;
+
+axiom (forall<T> h: Heap, k: Heap, v: T, t: Ty ::
+ { $HeapSucc(h, k), $IsAlloc(v, t, h) }
+ $HeapSucc(h, k) ==> $IsAlloc(v, t, h) ==> $IsAlloc(v, t, k));
+
+axiom (forall h: Heap, k: Heap, bx: Box, t: Ty ::
+ { $HeapSucc(h, k), $IsAllocBox(bx, t, h) }
+ $HeapSucc(h, k) ==> $IsAllocBox(bx, t, h) ==> $IsAllocBox(bx, t, k));
+
+const unique alloc: Field bool;
+
+axiom FDim(alloc) == 0 && !$IsGhostField(alloc);
+
+function _System.array.Length(a: ref) : int;
+
+axiom (forall o: ref :: 0 <= _System.array.Length(o));
+
+function Int(x: real) : int;
+
+axiom (forall x: real :: { Int(x): int } Int(x): int == int(x));
+
+function Real(x: int) : real;
+
+axiom (forall x: int :: { Real(x): real } Real(x): real == real(x));
+
+axiom (forall i: int :: { Int(Real(i)) } Int(Real(i)) == i);
+
+function {:inline true} _System.real.Trunc(x: real) : int
+{
+ Int(x)
+}
+
+type Heap = <alpha>[ref,Field alpha]alpha;
+
+function {:inline true} read<alpha>(H: Heap, r: ref, f: Field alpha) : alpha
+{
+ H[r, f]
+}
+
+function {:inline true} update<alpha>(H: Heap, r: ref, f: Field alpha, v: alpha) : Heap
+{
+ H[r, f := v]
+}
+
+function $IsGoodHeap(Heap) : bool;
+
+function $IsHeapAnchor(Heap) : bool;
+
+var $Heap: Heap where $IsGoodHeap($Heap) && $IsHeapAnchor($Heap);
+
+function $HeapSucc(Heap, Heap) : bool;
+
+axiom (forall<alpha> h: Heap, r: ref, f: Field alpha, x: alpha ::
+ { update(h, r, f, x) }
+ $IsGoodHeap(update(h, r, f, x)) ==> $HeapSucc(h, update(h, r, f, x)));
+
+axiom (forall a: Heap, b: Heap, c: Heap ::
+ { $HeapSucc(a, b), $HeapSucc(b, c) }
+ $HeapSucc(a, b) && $HeapSucc(b, c) ==> $HeapSucc(a, c));
+
+axiom (forall h: Heap, k: Heap ::
+ { $HeapSucc(h, k) }
+ $HeapSucc(h, k)
+ ==> (forall o: ref :: { read(k, o, alloc) } read(h, o, alloc) ==> read(k, o, alloc)));
+
+function $HeapSuccGhost(Heap, Heap) : bool;
+
+axiom (forall h: Heap, k: Heap ::
+ { $HeapSuccGhost(h, k) }
+ $HeapSuccGhost(h, k)
+ ==> $HeapSucc(h, k)
+ && (forall<alpha> o: ref, f: Field alpha ::
+ { read(k, o, f) }
+ !$IsGhostField(f) ==> read(h, o, f) == read(k, o, f)));
+
+type TickType;
+
+var $Tick: TickType;
+
+procedure $YieldHavoc(this: ref, rds: Set Box, nw: Set Box);
+ modifies $Heap;
+ ensures (forall<alpha> $o: ref, $f: Field alpha ::
+ { read($Heap, $o, $f) }
+ $o != null && read(old($Heap), $o, alloc)
+ ==>
+ $o == this || rds[$Box($o)] || nw[$Box($o)]
+ ==> read($Heap, $o, $f) == read(old($Heap), $o, $f));
+ ensures $HeapSucc(old($Heap), $Heap);
+
+
+
+procedure $IterHavoc0(this: ref, rds: Set Box, modi: Set Box);
+ modifies $Heap;
+ ensures (forall<alpha> $o: ref, $f: Field alpha ::
+ { read($Heap, $o, $f) }
+ $o != null && read(old($Heap), $o, alloc)
+ ==>
+ rds[$Box($o)] && !modi[$Box($o)] && $o != this
+ ==> read($Heap, $o, $f) == read(old($Heap), $o, $f));
+ ensures $HeapSucc(old($Heap), $Heap);
+
+
+
+procedure $IterHavoc1(this: ref, modi: Set Box, nw: Set Box);
+ modifies $Heap;
+ ensures (forall<alpha> $o: ref, $f: Field alpha ::
+ { read($Heap, $o, $f) }
+ $o != null && read(old($Heap), $o, alloc)
+ ==> read($Heap, $o, $f) == read(old($Heap), $o, $f)
+ || $o == this
+ || modi[$Box($o)]
+ || nw[$Box($o)]);
+ ensures $HeapSucc(old($Heap), $Heap);
+
+
+
+procedure $IterCollectNewObjects(prevHeap: Heap, newHeap: Heap, this: ref, NW: Field (Set Box))
+ returns (s: Set Box);
+ ensures (forall bx: Box ::
+ { s[bx] }
+ s[bx]
+ <==> read(newHeap, this, NW)[bx]
+ || (
+ $Unbox(bx) != null
+ && !read(prevHeap, $Unbox(bx): ref, alloc)
+ && read(newHeap, $Unbox(bx): ref, alloc)));
+
+
+
+type Set T = [T]bool;
+
+function Set#Card<T>(Set T) : int;
+
+axiom (forall<T> s: Set T :: { Set#Card(s) } 0 <= Set#Card(s));
+
+function Set#Empty<T>() : Set T;
+
+axiom (forall<T> o: T :: { Set#Empty()[o] } !Set#Empty()[o]);
+
+axiom (forall<T> s: Set T ::
+ { Set#Card(s) }
+ (Set#Card(s) == 0 <==> s == Set#Empty())
+ && (Set#Card(s) != 0 ==> (exists x: T :: s[x])));
+
+function Set#Singleton<T>(T) : Set T;
+
+axiom (forall<T> r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]);
+
+axiom (forall<T> r: T, o: T ::
+ { Set#Singleton(r)[o] }
+ Set#Singleton(r)[o] <==> r == o);
+
+axiom (forall<T> r: T ::
+ { Set#Card(Set#Singleton(r)) }
+ Set#Card(Set#Singleton(r)) == 1);
+
+function Set#UnionOne<T>(Set T, T) : Set T;
+
+axiom (forall<T> a: Set T, x: T, o: T ::
+ { Set#UnionOne(a, x)[o] }
+ Set#UnionOne(a, x)[o] <==> o == x || a[o]);
+
+axiom (forall<T> a: Set T, x: T :: { Set#UnionOne(a, x) } Set#UnionOne(a, x)[x]);
+
+axiom (forall<T> a: Set T, x: T, y: T ::
+ { Set#UnionOne(a, x), a[y] }
+ a[y] ==> Set#UnionOne(a, x)[y]);
+
+axiom (forall<T> a: Set T, x: T ::
+ { Set#Card(Set#UnionOne(a, x)) }
+ a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a));
+
+axiom (forall<T> a: Set T, x: T ::
+ { Set#Card(Set#UnionOne(a, x)) }
+ !a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a) + 1);
+
+function Set#Union<T>(Set T, Set T) : Set T;
+
+axiom (forall<T> a: Set T, b: Set T, o: T ::
+ { Set#Union(a, b)[o] }
+ Set#Union(a, b)[o] <==> a[o] || b[o]);
+
+axiom (forall<T> a: Set T, b: Set T, y: T ::
+ { Set#Union(a, b), a[y] }
+ a[y] ==> Set#Union(a, b)[y]);
+
+axiom (forall<T> a: Set T, b: Set T, y: T ::
+ { Set#Union(a, b), b[y] }
+ b[y] ==> Set#Union(a, b)[y]);
+
+axiom (forall<T> a: Set T, 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) : Set T;
+
+axiom (forall<T> a: Set T, b: Set T, o: T ::
+ { Set#Intersection(a, b)[o] }
+ Set#Intersection(a, b)[o] <==> a[o] && b[o]);
+
+axiom (forall<T> a: Set T, b: Set T ::
+ { Set#Union(Set#Union(a, b), b) }
+ Set#Union(Set#Union(a, b), b) == Set#Union(a, b));
+
+axiom (forall<T> a: Set T, b: Set T ::
+ { Set#Union(a, Set#Union(a, b)) }
+ Set#Union(a, Set#Union(a, b)) == Set#Union(a, b));
+
+axiom (forall<T> a: Set T, b: Set T ::
+ { Set#Intersection(Set#Intersection(a, b), b) }
+ Set#Intersection(Set#Intersection(a, b), b) == Set#Intersection(a, b));
+
+axiom (forall<T> a: Set T, b: Set T ::
+ { Set#Intersection(a, Set#Intersection(a, b)) }
+ Set#Intersection(a, Set#Intersection(a, b)) == Set#Intersection(a, b));
+
+axiom (forall<T> a: Set T, b: Set T ::
+ { Set#Card(Set#Union(a, b)) } { Set#Card(Set#Intersection(a, b)) }
+ Set#Card(Set#Union(a, b)) + Set#Card(Set#Intersection(a, b))
+ == Set#Card(a) + Set#Card(b));
+
+function Set#Difference<T>(Set T, Set T) : Set T;
+
+axiom (forall<T> a: Set T, b: Set T, o: T ::
+ { Set#Difference(a, b)[o] }
+ Set#Difference(a, b)[o] <==> a[o] && !b[o]);
+
+axiom (forall<T> a: Set T, b: Set T, y: T ::
+ { Set#Difference(a, b), b[y] }
+ b[y] ==> !Set#Difference(a, b)[y]);
+
+axiom (forall<T> a: Set T, b: Set T ::
+ { Set#Card(Set#Difference(a, b)) }
+ Set#Card(Set#Difference(a, b))
+ + Set#Card(Set#Difference(b, a))
+ + Set#Card(Set#Intersection(a, b))
+ == Set#Card(Set#Union(a, b))
+ && Set#Card(Set#Difference(a, b)) == Set#Card(a) - Set#Card(Set#Intersection(a, b)));
+
+function Set#Subset<T>(Set T, Set T) : bool;
+
+axiom (forall<T> a: Set T, b: Set T ::
+ { Set#Subset(a, b) }
+ Set#Subset(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] ==> b[o]));
+
+function Set#Equal<T>(Set T, Set T) : bool;
+
+axiom (forall<T> a: Set T, b: Set T ::
+ { Set#Equal(a, b) }
+ Set#Equal(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] <==> b[o]));
+
+axiom (forall<T> a: Set T, b: Set T :: { Set#Equal(a, b) } Set#Equal(a, b) ==> a == b);
+
+function Set#Disjoint<T>(Set T, Set T) : bool;
+
+axiom (forall<T> a: Set T, b: Set T ::
+ { Set#Disjoint(a, b) }
+ Set#Disjoint(a, b) <==> (forall o: T :: { a[o] } { b[o] } !a[o] || !b[o]));
+
+type ISet T = [T]bool;
+
+function ISet#Empty<T>() : Set T;
+
+axiom (forall<T> o: T :: { ISet#Empty()[o] } !ISet#Empty()[o]);
+
+function ISet#UnionOne<T>(ISet T, T) : ISet T;
+
+axiom (forall<T> a: ISet T, x: T, o: T ::
+ { ISet#UnionOne(a, x)[o] }
+ ISet#UnionOne(a, x)[o] <==> o == x || a[o]);
+
+axiom (forall<T> a: ISet T, x: T :: { ISet#UnionOne(a, x) } ISet#UnionOne(a, x)[x]);
+
+axiom (forall<T> a: ISet T, x: T, y: T ::
+ { ISet#UnionOne(a, x), a[y] }
+ a[y] ==> ISet#UnionOne(a, x)[y]);
+
+function ISet#Union<T>(ISet T, ISet T) : ISet T;
+
+axiom (forall<T> a: ISet T, b: ISet T, o: T ::
+ { ISet#Union(a, b)[o] }
+ ISet#Union(a, b)[o] <==> a[o] || b[o]);
+
+axiom (forall<T> a: ISet T, b: ISet T, y: T ::
+ { ISet#Union(a, b), a[y] }
+ a[y] ==> ISet#Union(a, b)[y]);
+
+axiom (forall<T> a: Set T, b: Set T, y: T ::
+ { ISet#Union(a, b), b[y] }
+ b[y] ==> ISet#Union(a, b)[y]);
+
+axiom (forall<T> a: ISet T, b: ISet T ::
+ { ISet#Union(a, b) }
+ ISet#Disjoint(a, b)
+ ==> ISet#Difference(ISet#Union(a, b), a) == b
+ && ISet#Difference(ISet#Union(a, b), b) == a);
+
+function ISet#Intersection<T>(ISet T, ISet T) : ISet T;
+
+axiom (forall<T> a: ISet T, b: ISet T, o: T ::
+ { ISet#Intersection(a, b)[o] }
+ ISet#Intersection(a, b)[o] <==> a[o] && b[o]);
+
+axiom (forall<T> a: ISet T, b: ISet T ::
+ { ISet#Union(ISet#Union(a, b), b) }
+ ISet#Union(ISet#Union(a, b), b) == ISet#Union(a, b));
+
+axiom (forall<T> a: Set T, b: Set T ::
+ { ISet#Union(a, ISet#Union(a, b)) }
+ ISet#Union(a, ISet#Union(a, b)) == ISet#Union(a, b));
+
+axiom (forall<T> a: ISet T, b: ISet T ::
+ { ISet#Intersection(ISet#Intersection(a, b), b) }
+ ISet#Intersection(ISet#Intersection(a, b), b) == ISet#Intersection(a, b));
+
+axiom (forall<T> a: ISet T, b: ISet T ::
+ { ISet#Intersection(a, ISet#Intersection(a, b)) }
+ ISet#Intersection(a, ISet#Intersection(a, b)) == ISet#Intersection(a, b));
+
+function ISet#Difference<T>(ISet T, ISet T) : ISet T;
+
+axiom (forall<T> a: ISet T, b: ISet T, o: T ::
+ { ISet#Difference(a, b)[o] }
+ ISet#Difference(a, b)[o] <==> a[o] && !b[o]);
+
+axiom (forall<T> a: ISet T, b: ISet T, y: T ::
+ { ISet#Difference(a, b), b[y] }
+ b[y] ==> !ISet#Difference(a, b)[y]);
+
+function ISet#Subset<T>(ISet T, ISet T) : bool;
+
+axiom (forall<T> a: ISet T, b: ISet T ::
+ { ISet#Subset(a, b) }
+ ISet#Subset(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] ==> b[o]));
+
+function ISet#Equal<T>(ISet T, ISet T) : bool;
+
+axiom (forall<T> a: ISet T, b: ISet T ::
+ { ISet#Equal(a, b) }
+ ISet#Equal(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] <==> b[o]));
+
+axiom (forall<T> a: ISet T, b: ISet T ::
+ { ISet#Equal(a, b) }
+ ISet#Equal(a, b) ==> a == b);
+
+function ISet#Disjoint<T>(ISet T, ISet T) : bool;
+
+axiom (forall<T> a: ISet T, b: ISet T ::
+ { ISet#Disjoint(a, b) }
+ ISet#Disjoint(a, b) <==> (forall o: T :: { a[o] } { b[o] } !a[o] || !b[o]));
+
+function Math#min(a: int, b: int) : int;
+
+axiom (forall a: int, b: int :: { Math#min(a, b) } a <= b <==> Math#min(a, b) == a);
+
+axiom (forall a: int, b: int :: { Math#min(a, b) } b <= a <==> Math#min(a, b) == b);
+
+axiom (forall a: int, b: int ::
+ { Math#min(a, b) }
+ Math#min(a, b) == a || Math#min(a, b) == b);
+
+function Math#clip(a: int) : int;
+
+axiom (forall a: int :: { Math#clip(a) } 0 <= a ==> Math#clip(a) == a);
+
+axiom (forall a: int :: { Math#clip(a) } a < 0 ==> Math#clip(a) == 0);
+
+type MultiSet T = [T]int;
+
+function $IsGoodMultiSet<T>(ms: MultiSet T) : bool;
+
+axiom (forall<T> ms: MultiSet T ::
+ { $IsGoodMultiSet(ms) }
+ $IsGoodMultiSet(ms)
+ <==> (forall bx: T :: { ms[bx] } 0 <= ms[bx] && ms[bx] <= MultiSet#Card(ms)));
+
+function MultiSet#Card<T>(MultiSet T) : int;
+
+axiom (forall<T> s: MultiSet T :: { MultiSet#Card(s) } 0 <= MultiSet#Card(s));
+
+axiom (forall<T> s: MultiSet T, x: T, n: int ::
+ { MultiSet#Card(s[x := n]) }
+ 0 <= n ==> MultiSet#Card(s[x := n]) == MultiSet#Card(s) - s[x] + n);
+
+function MultiSet#Empty<T>() : MultiSet T;
+
+axiom (forall<T> o: T :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0);
+
+axiom (forall<T> s: MultiSet T ::
+ { MultiSet#Card(s) }
+ (MultiSet#Card(s) == 0 <==> s == MultiSet#Empty())
+ && (MultiSet#Card(s) != 0 ==> (exists x: T :: 0 < s[x])));
+
+function MultiSet#Singleton<T>(T) : MultiSet T;
+
+axiom (forall<T> r: T, o: T ::
+ { MultiSet#Singleton(r)[o] }
+ (MultiSet#Singleton(r)[o] == 1 <==> r == o)
+ && (MultiSet#Singleton(r)[o] == 0 <==> r != o));
+
+axiom (forall<T> r: T ::
+ { MultiSet#Singleton(r) }
+ MultiSet#Singleton(r) == MultiSet#UnionOne(MultiSet#Empty(), r));
+
+function MultiSet#UnionOne<T>(MultiSet T, T) : MultiSet T;
+
+axiom (forall<T> a: MultiSet T, x: T, o: T ::
+ { MultiSet#UnionOne(a, x)[o] }
+ 0 < MultiSet#UnionOne(a, x)[o] <==> o == x || 0 < a[o]);
+
+axiom (forall<T> a: MultiSet T, x: T ::
+ { MultiSet#UnionOne(a, x) }
+ MultiSet#UnionOne(a, x)[x] == a[x] + 1);
+
+axiom (forall<T> a: MultiSet T, x: T, y: T ::
+ { MultiSet#UnionOne(a, x), a[y] }
+ 0 < a[y] ==> 0 < MultiSet#UnionOne(a, x)[y]);
+
+axiom (forall<T> a: MultiSet T, x: T, y: T ::
+ { MultiSet#UnionOne(a, x), a[y] }
+ x != y ==> a[y] == MultiSet#UnionOne(a, x)[y]);
+
+axiom (forall<T> a: MultiSet T, x: T ::
+ { MultiSet#Card(MultiSet#UnionOne(a, x)) }
+ MultiSet#Card(MultiSet#UnionOne(a, x)) == MultiSet#Card(a) + 1);
+
+function MultiSet#Union<T>(MultiSet T, MultiSet T) : MultiSet T;
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T ::
+ { MultiSet#Union(a, b)[o] }
+ MultiSet#Union(a, b)[o] == a[o] + b[o]);
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T ::
+ { MultiSet#Card(MultiSet#Union(a, b)) }
+ MultiSet#Card(MultiSet#Union(a, b)) == MultiSet#Card(a) + MultiSet#Card(b));
+
+function MultiSet#Intersection<T>(MultiSet T, MultiSet T) : MultiSet T;
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T ::
+ { MultiSet#Intersection(a, b)[o] }
+ MultiSet#Intersection(a, b)[o] == Math#min(a[o], b[o]));
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T ::
+ { MultiSet#Intersection(MultiSet#Intersection(a, b), b) }
+ MultiSet#Intersection(MultiSet#Intersection(a, b), b)
+ == MultiSet#Intersection(a, b));
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T ::
+ { MultiSet#Intersection(a, MultiSet#Intersection(a, b)) }
+ MultiSet#Intersection(a, MultiSet#Intersection(a, b))
+ == MultiSet#Intersection(a, b));
+
+function MultiSet#Difference<T>(MultiSet T, MultiSet T) : MultiSet T;
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T ::
+ { MultiSet#Difference(a, b)[o] }
+ MultiSet#Difference(a, b)[o] == Math#clip(a[o] - b[o]));
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T, y: T ::
+ { MultiSet#Difference(a, b), b[y], a[y] }
+ a[y] <= b[y] ==> MultiSet#Difference(a, b)[y] == 0);
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T ::
+ { MultiSet#Card(MultiSet#Difference(a, b)) }
+ MultiSet#Card(MultiSet#Difference(a, b))
+ + MultiSet#Card(MultiSet#Difference(b, a))
+ + 2 * MultiSet#Card(MultiSet#Intersection(a, b))
+ == MultiSet#Card(MultiSet#Union(a, b))
+ && MultiSet#Card(MultiSet#Difference(a, b))
+ == MultiSet#Card(a) - MultiSet#Card(MultiSet#Intersection(a, b)));
+
+function MultiSet#Subset<T>(MultiSet T, MultiSet T) : bool;
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T ::
+ { MultiSet#Subset(a, b) }
+ MultiSet#Subset(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] <= b[o]));
+
+function MultiSet#Equal<T>(MultiSet T, MultiSet T) : bool;
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T ::
+ { MultiSet#Equal(a, b) }
+ MultiSet#Equal(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] == b[o]));
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T ::
+ { MultiSet#Equal(a, b) }
+ MultiSet#Equal(a, b) ==> a == b);
+
+function MultiSet#Disjoint<T>(MultiSet T, MultiSet T) : bool;
+
+axiom (forall<T> a: MultiSet T, b: MultiSet T ::
+ { MultiSet#Disjoint(a, b) }
+ MultiSet#Disjoint(a, b)
+ <==> (forall o: T :: { a[o] } { b[o] } a[o] == 0 || b[o] == 0));
+
+function MultiSet#FromSet<T>(Set T) : MultiSet T;
+
+axiom (forall<T> s: Set T, a: T ::
+ { MultiSet#FromSet(s)[a] }
+ (MultiSet#FromSet(s)[a] == 0 <==> !s[a])
+ && (MultiSet#FromSet(s)[a] == 1 <==> s[a]));
+
+axiom (forall<T> s: Set T ::
+ { MultiSet#Card(MultiSet#FromSet(s)) }
+ MultiSet#Card(MultiSet#FromSet(s)) == Set#Card(s));
+
+function MultiSet#FromSeq<T>(Seq T) : MultiSet T;
+
+axiom (forall<T> s: Seq T ::
+ { MultiSet#FromSeq(s) }
+ $IsGoodMultiSet(MultiSet#FromSeq(s)));
+
+axiom (forall<T> s: Seq T ::
+ { MultiSet#Card(MultiSet#FromSeq(s)) }
+ MultiSet#Card(MultiSet#FromSeq(s)) == Seq#Length(s));
+
+axiom (forall<T> s: Seq T, v: T ::
+ { MultiSet#FromSeq(Seq#Build(s, v)) }
+ MultiSet#FromSeq(Seq#Build(s, v)) == MultiSet#UnionOne(MultiSet#FromSeq(s), v));
+
+axiom (forall<T> ::
+ MultiSet#FromSeq(Seq#Empty(): Seq T) == MultiSet#Empty(): MultiSet T);
+
+axiom (forall<T> a: Seq T, b: Seq T ::
+ { MultiSet#FromSeq(Seq#Append(a, b)) }
+ MultiSet#FromSeq(Seq#Append(a, b))
+ == MultiSet#Union(MultiSet#FromSeq(a), MultiSet#FromSeq(b)));
+
+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]);
+
+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]);
+
+type Seq _;
+
+function Seq#Length<T>(Seq T) : int;
+
+axiom (forall<T> s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s));
+
+function Seq#Empty<T>() : Seq T;
+
+axiom (forall<T> :: Seq#Length(Seq#Empty(): Seq T) == 0);
+
+axiom (forall<T> s: Seq T ::
+ { Seq#Length(s) }
+ Seq#Length(s) == 0 ==> s == Seq#Empty());
+
+axiom (forall<T> t: Ty :: { $Is(Seq#Empty(): Seq T, t) } $Is(Seq#Empty(): Seq T, t));
+
+function Seq#Singleton<T>(T) : Seq T;
+
+axiom (forall<T> t: T ::
+ { Seq#Length(Seq#Singleton(t)) }
+ Seq#Length(Seq#Singleton(t)) == 1);
+
+function Seq#Build<T>(s: Seq T, val: T) : Seq T;
+
+axiom (forall<T> s: Seq T, v: T ::
+ { Seq#Length(Seq#Build(s, v)) }
+ Seq#Length(Seq#Build(s, v)) == 1 + Seq#Length(s));
+
+axiom (forall<T> s: Seq T, i: int, v: T ::
+ { Seq#Index(Seq#Build(s, v), i) }
+ (i == Seq#Length(s) ==> Seq#Index(Seq#Build(s, v), i) == v)
+ && (i != Seq#Length(s) ==> Seq#Index(Seq#Build(s, v), i) == Seq#Index(s, i)));
+
+axiom (forall s: Seq Box, bx: Box, t: Ty ::
+ { $Is(Seq#Build(s, bx), TSeq(t)) }
+ $Is(s, TSeq(t)) && $IsBox(bx, t) ==> $Is(Seq#Build(s, bx), TSeq(t)));
+
+function Seq#Append<T>(Seq T, Seq T) : Seq T;
+
+axiom (forall<T> s0: Seq T, s1: Seq T ::
+ { Seq#Length(Seq#Append(s0, s1)) }
+ Seq#Length(Seq#Append(s0, s1)) == Seq#Length(s0) + Seq#Length(s1));
+
+axiom (forall s0: Seq Box, s1: Seq Box, t: Ty ::
+ { $Is(Seq#Append(s0, s1), t) }
+ $Is(s0, t) && $Is(s1, t) ==> $Is(Seq#Append(s0, s1), t));
+
+function Seq#Index<T>(Seq T, int) : T;
+
+axiom (forall<T> t: T ::
+ { Seq#Index(Seq#Singleton(t), 0) }
+ Seq#Index(Seq#Singleton(t), 0) == t);
+
+axiom (forall<T> s0: Seq T, s1: Seq T, n: int ::
+ { Seq#Index(Seq#Append(s0, s1), n) }
+ (n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0, s1), n) == Seq#Index(s0, n))
+ && (Seq#Length(s0) <= n
+ ==> Seq#Index(Seq#Append(s0, s1), n) == Seq#Index(s1, n - Seq#Length(s0))));
+
+function Seq#Update<T>(Seq T, int, T) : Seq T;
+
+axiom (forall<T> s: Seq T, i: int, v: T ::
+ { Seq#Length(Seq#Update(s, i, v)) }
+ 0 <= i && i < Seq#Length(s) ==> Seq#Length(Seq#Update(s, i, v)) == Seq#Length(s));
+
+axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
+ { Seq#Index(Seq#Update(s, i, v), n) }
+ 0 <= n && n < Seq#Length(s)
+ ==> (i == n ==> Seq#Index(Seq#Update(s, i, v), n) == v)
+ && (i != n ==> Seq#Index(Seq#Update(s, i, v), n) == Seq#Index(s, n)));
+
+function Seq#Contains<T>(Seq T, T) : bool;
+
+axiom (forall<T> s: Seq T, x: T ::
+ { Seq#Contains(s, x) }
+ Seq#Contains(s, x)
+ <==> (exists i: int ::
+ { Seq#Index(s, i) }
+ 0 <= i && i < Seq#Length(s) && Seq#Index(s, i) == x));
+
+axiom (forall<T> x: T ::
+ { Seq#Contains(Seq#Empty(), x) }
+ !Seq#Contains(Seq#Empty(), x));
+
+axiom (forall<T> s0: Seq T, s1: Seq T, x: T ::
+ { Seq#Contains(Seq#Append(s0, s1), x) }
+ Seq#Contains(Seq#Append(s0, s1), x)
+ <==> Seq#Contains(s0, x) || Seq#Contains(s1, x));
+
+axiom (forall<T> s: Seq T, v: T, x: T ::
+ { Seq#Contains(Seq#Build(s, v), x) }
+ Seq#Contains(Seq#Build(s, v), x) <==> v == x || Seq#Contains(s, x));
+
+axiom (forall<T> s: Seq T, n: int, x: T ::
+ { Seq#Contains(Seq#Take(s, n), x) }
+ Seq#Contains(Seq#Take(s, n), x)
+ <==> (exists i: int ::
+ { Seq#Index(s, i) }
+ 0 <= i && i < n && i < Seq#Length(s) && Seq#Index(s, i) == x));
+
+axiom (forall<T> s: Seq T, n: int, x: T ::
+ { Seq#Contains(Seq#Drop(s, n), x) }
+ Seq#Contains(Seq#Drop(s, n), x)
+ <==> (exists i: int ::
+ { Seq#Index(s, i) }
+ 0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x));
+
+function Seq#Equal<T>(Seq T, Seq T) : bool;
+
+axiom (forall<T> s0: Seq T, s1: Seq T ::
+ { Seq#Equal(s0, s1) }
+ Seq#Equal(s0, s1)
+ <==> Seq#Length(s0) == Seq#Length(s1)
+ && (forall j: int ::
+ { Seq#Index(s0, j) } { Seq#Index(s1, j) }
+ 0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0, j) == Seq#Index(s1, j)));
+
+axiom (forall<T> a: Seq T, b: Seq T :: { Seq#Equal(a, b) } Seq#Equal(a, b) ==> a == b);
+
+function Seq#SameUntil<T>(Seq T, Seq T, int) : bool;
+
+axiom (forall<T> s0: Seq T, s1: Seq T, n: int ::
+ { Seq#SameUntil(s0, s1, n) }
+ Seq#SameUntil(s0, s1, n)
+ <==> (forall j: int ::
+ { Seq#Index(s0, j) } { Seq#Index(s1, j) }
+ 0 <= j && j < n ==> Seq#Index(s0, j) == Seq#Index(s1, j)));
+
+function Seq#Take<T>(s: Seq T, howMany: int) : Seq T;
+
+axiom (forall<T> s: Seq T, n: int ::
+ { Seq#Length(Seq#Take(s, n)) }
+ 0 <= n && n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s, n)) == n);
+
+axiom (forall<T> s: Seq T, n: int, j: int ::
+ {:weight 25} { Seq#Index(Seq#Take(s, n), j) } { Seq#Index(s, j), Seq#Take(s, n) }
+ 0 <= j && j < n && j < Seq#Length(s)
+ ==> Seq#Index(Seq#Take(s, n), j) == Seq#Index(s, j));
+
+function Seq#Drop<T>(s: Seq T, howMany: int) : Seq T;
+
+axiom (forall<T> s: Seq T, n: int ::
+ { Seq#Length(Seq#Drop(s, n)) }
+ 0 <= n && n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s, n)) == Seq#Length(s) - n);
+
+axiom (forall<T> s: Seq T, n: int, j: int ::
+ {:weight 25} { Seq#Index(Seq#Drop(s, n), j) }
+ 0 <= n && 0 <= j && j < Seq#Length(s) - n
+ ==> Seq#Index(Seq#Drop(s, n), j) == Seq#Index(s, j + n));
+
+axiom (forall<T> s: Seq T, n: int, k: int ::
+ {:weight 25} { Seq#Index(s, k), Seq#Drop(s, n) }
+ 0 <= n && n <= k && k < Seq#Length(s)
+ ==> Seq#Index(Seq#Drop(s, n), k - n) == Seq#Index(s, k));
+
+axiom (forall<T> s: Seq T, t: Seq T ::
+ { Seq#Append(s, t) }
+ Seq#Take(Seq#Append(s, t), Seq#Length(s)) == s
+ && Seq#Drop(Seq#Append(s, t), Seq#Length(s)) == t);
+
+function Seq#FromArray(h: Heap, a: ref) : Seq Box;
+
+axiom (forall h: Heap, a: ref ::
+ { Seq#Length(Seq#FromArray(h, a)) }
+ Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a));
+
+axiom (forall h: Heap, a: ref ::
+ { Seq#FromArray(h, a) }
+ (forall i: int ::
+ { read(h, a, IndexField(i)) } { Seq#Index(Seq#FromArray(h, a): Seq Box, i) }
+ 0 <= i && i < Seq#Length(Seq#FromArray(h, a))
+ ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i))));
+
+axiom (forall h0: Heap, h1: Heap, a: ref ::
+ { Seq#FromArray(h1, a), $HeapSucc(h0, h1) }
+ $IsGoodHeap(h0)
+ && $IsGoodHeap(h1)
+ && $HeapSucc(h0, h1)
+ && (forall i: int ::
+ 0 <= i && i < _System.array.Length(a)
+ ==> read(h0, a, IndexField(i)) == read(h1, a, IndexField(i)))
+ ==> Seq#FromArray(h0, a) == Seq#FromArray(h1, a));
+
+axiom (forall h: Heap, i: int, v: Box, a: ref ::
+ { Seq#FromArray(update(h, a, IndexField(i), v), a) }
+ 0 <= i && i < _System.array.Length(a)
+ ==> Seq#FromArray(update(h, a, IndexField(i), v), a)
+ == Seq#Update(Seq#FromArray(h, a), i, v));
+
+axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
+ { Seq#Take(Seq#Update(s, i, v), n) }
+ 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));
+
+axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
+ { Seq#Drop(Seq#Update(s, i, v), n) }
+ 0 <= n && n <= i && i < Seq#Length(s)
+ ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Update(Seq#Drop(s, n), i - n, v));
+
+axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
+ { Seq#Drop(Seq#Update(s, i, v), n) }
+ 0 <= i && i < n && n < Seq#Length(s)
+ ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Drop(s, n));
+
+axiom (forall h: Heap, a: ref, n0: int, n1: int ::
+ { Seq#Take(Seq#FromArray(h, a), n0), Seq#Take(Seq#FromArray(h, a), n1) }
+ n0 + 1 == n1 && 0 <= n0 && n1 <= _System.array.Length(a)
+ ==> Seq#Take(Seq#FromArray(h, a), n1)
+ == Seq#Build(Seq#Take(Seq#FromArray(h, a), n0), read(h, a, IndexField(n0): Field Box)));
+
+axiom (forall<T> s: Seq T, v: T, n: int ::
+ { Seq#Drop(Seq#Build(s, v), n) }
+ 0 <= n && n <= Seq#Length(s)
+ ==> Seq#Drop(Seq#Build(s, v), n) == Seq#Build(Seq#Drop(s, n), v));
+
+function Seq#Rank<T>(Seq T) : int;
+
+axiom (forall s: Seq Box, i: int ::
+ { DtRank($Unbox(Seq#Index(s, i)): DatatypeType) }
+ 0 <= i && i < Seq#Length(s)
+ ==> DtRank($Unbox(Seq#Index(s, i)): DatatypeType) < Seq#Rank(s));
+
+axiom (forall<T> s: Seq T, i: int ::
+ { Seq#Rank(Seq#Drop(s, i)) }
+ 0 < i && i <= Seq#Length(s) ==> Seq#Rank(Seq#Drop(s, i)) < Seq#Rank(s));
+
+axiom (forall<T> s: Seq T, i: int ::
+ { Seq#Rank(Seq#Take(s, i)) }
+ 0 <= i && i < Seq#Length(s) ==> Seq#Rank(Seq#Take(s, i)) < Seq#Rank(s));
+
+axiom (forall<T> s: Seq T, i: int, j: int ::
+ { Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) }
+ 0 <= i && i < j && j <= Seq#Length(s)
+ ==> Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) < Seq#Rank(s));
+
+axiom (forall<T> s: Seq T, n: int ::
+ { Seq#Drop(s, n) }
+ n == 0 ==> Seq#Drop(s, n) == s);
+
+axiom (forall<T> s: Seq T, n: int ::
+ { Seq#Take(s, n) }
+ n == 0 ==> Seq#Take(s, n) == Seq#Empty());
+
+axiom (forall<T> s: Seq T, m: int, n: int ::
+ { Seq#Drop(Seq#Drop(s, m), n) }
+ 0 <= m && 0 <= n && m + n <= Seq#Length(s)
+ ==> Seq#Drop(Seq#Drop(s, m), n) == Seq#Drop(s, m + n));
+
+type Map _ _;
+
+function Map#Domain<U,V>(Map U V) : [U]bool;
+
+function Map#Elements<U,V>(Map U V) : [U]V;
+
+function Map#Card<U,V>(Map U V) : int;
+
+axiom (forall<U,V> m: Map U V :: { Map#Card(m) } 0 <= Map#Card(m));
+
+function Map#Empty<U,V>() : Map U V;
+
+axiom (forall<U,V> u: U ::
+ { Map#Domain(Map#Empty(): Map U V)[u] }
+ !Map#Domain(Map#Empty(): Map U V)[u]);
+
+axiom (forall<U,V> m: Map U V ::
+ { Map#Card(m) }
+ (Map#Card(m) == 0 <==> m == Map#Empty())
+ && (Map#Card(m) != 0 ==> (exists x: U :: Map#Domain(m)[x])));
+
+function Map#Glue<U,V>([U]bool, [U]V, Ty) : Map U V;
+
+axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty ::
+ { Map#Domain(Map#Glue(a, b, t)) }
+ Map#Domain(Map#Glue(a, b, t)) == a);
+
+axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty ::
+ { Map#Elements(Map#Glue(a, b, t)) }
+ Map#Elements(Map#Glue(a, b, t)) == b);
+
+axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty ::
+ { $Is(Map#Glue(a, b, t), t) }
+ $Is(Map#Glue(a, b, t), t));
+
+function Map#Build<U,V>(Map U V, U, V) : Map U V;
+
+axiom (forall<U,V> m: Map U V, u: U, u': U, v: V ::
+ { Map#Domain(Map#Build(m, u, v))[u'] } { Map#Elements(Map#Build(m, u, v))[u'] }
+ (u' == u
+ ==> Map#Domain(Map#Build(m, u, v))[u'] && Map#Elements(Map#Build(m, u, v))[u'] == v)
+ && (u' != u
+ ==> Map#Domain(Map#Build(m, u, v))[u'] == Map#Domain(m)[u']
+ && Map#Elements(Map#Build(m, u, v))[u'] == Map#Elements(m)[u']));
+
+axiom (forall<U,V> m: Map U V, u: U, v: V ::
+ { Map#Card(Map#Build(m, u, v)) }
+ Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m));
+
+axiom (forall<U,V> m: Map U V, u: U, v: V ::
+ { Map#Card(Map#Build(m, u, v)) }
+ !Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m) + 1);
+
+function Map#Equal<U,V>(Map U V, Map U V) : bool;
+
+axiom (forall<U,V> m: Map U V, m': Map U V ::
+ { Map#Equal(m, m') }
+ Map#Equal(m, m')
+ <==> (forall u: U :: Map#Domain(m)[u] == Map#Domain(m')[u])
+ && (forall u: U :: Map#Domain(m)[u] ==> Map#Elements(m)[u] == Map#Elements(m')[u]));
+
+axiom (forall<U,V> m: Map U V, m': Map U V ::
+ { Map#Equal(m, m') }
+ Map#Equal(m, m') ==> m == m');
+
+function Map#Disjoint<U,V>(Map U V, Map U V) : bool;
+
+axiom (forall<U,V> m: Map U V, m': Map U V ::
+ { Map#Disjoint(m, m') }
+ Map#Disjoint(m, m')
+ <==> (forall o: U ::
+ { Map#Domain(m)[o] } { Map#Domain(m')[o] }
+ !Map#Domain(m)[o] || !Map#Domain(m')[o]));
+
+type IMap _ _;
+
+function IMap#Domain<U,V>(IMap U V) : [U]bool;
+
+function IMap#Elements<U,V>(IMap U V) : [U]V;
+
+function IMap#Empty<U,V>() : IMap U V;
+
+axiom (forall<U,V> u: U ::
+ { IMap#Domain(IMap#Empty(): IMap U V)[u] }
+ !IMap#Domain(IMap#Empty(): IMap U V)[u]);
+
+function IMap#Glue<U,V>([U]bool, [U]V, Ty) : IMap U V;
+
+axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty ::
+ { IMap#Domain(IMap#Glue(a, b, t)) }
+ IMap#Domain(IMap#Glue(a, b, t)) == a);
+
+axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty ::
+ { IMap#Elements(IMap#Glue(a, b, t)) }
+ IMap#Elements(IMap#Glue(a, b, t)) == b);
+
+axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty ::
+ { $Is(IMap#Glue(a, b, t), t) }
+ $Is(IMap#Glue(a, b, t), t));
+
+function IMap#Build<U,V>(IMap U V, U, V) : IMap U V;
+
+axiom (forall<U,V> m: IMap U V, u: U, u': U, v: V ::
+ { IMap#Domain(IMap#Build(m, u, v))[u'] }
+ { IMap#Elements(IMap#Build(m, u, v))[u'] }
+ (u' == u
+ ==> IMap#Domain(IMap#Build(m, u, v))[u']
+ && IMap#Elements(IMap#Build(m, u, v))[u'] == v)
+ && (u' != u
+ ==> IMap#Domain(IMap#Build(m, u, v))[u'] == IMap#Domain(m)[u']
+ && IMap#Elements(IMap#Build(m, u, v))[u'] == IMap#Elements(m)[u']));
+
+function IMap#Equal<U,V>(IMap U V, IMap U V) : bool;
+
+axiom (forall<U,V> m: IMap U V, m': IMap U V ::
+ { IMap#Equal(m, m') }
+ IMap#Equal(m, m')
+ <==> (forall u: U :: IMap#Domain(m)[u] == IMap#Domain(m')[u])
+ && (forall u: U ::
+ IMap#Domain(m)[u] ==> IMap#Elements(m)[u] == IMap#Elements(m')[u]));
+
+axiom (forall<U,V> m: IMap U V, m': IMap U V ::
+ { IMap#Equal(m, m') }
+ IMap#Equal(m, m') ==> m == m');
+
+function INTERNAL_add_boogie(x: int, y: int) : int;
+
+axiom (forall x: int, y: int ::
+ { INTERNAL_add_boogie(x, y): int }
+ INTERNAL_add_boogie(x, y): int == x + y);
+
+function INTERNAL_sub_boogie(x: int, y: int) : int;
+
+axiom (forall x: int, y: int ::
+ { INTERNAL_sub_boogie(x, y): int }
+ INTERNAL_sub_boogie(x, y): int == x - y);
+
+function INTERNAL_mul_boogie(x: int, y: int) : int;
+
+axiom (forall x: int, y: int ::
+ { INTERNAL_mul_boogie(x, y): int }
+ INTERNAL_mul_boogie(x, y): int == x * y);
+
+function INTERNAL_div_boogie(x: int, y: int) : int;
+
+axiom (forall x: int, y: int ::
+ { INTERNAL_div_boogie(x, y): int }
+ INTERNAL_div_boogie(x, y): int == x div y);
+
+function INTERNAL_mod_boogie(x: int, y: int) : int;
+
+axiom (forall x: int, y: int ::
+ { INTERNAL_mod_boogie(x, y): int }
+ INTERNAL_mod_boogie(x, y): int == x mod y);
+
+function {:never_pattern true} INTERNAL_lt_boogie(x: int, y: int) : bool;
+
+axiom (forall x: int, y: int ::
+ {:never_pattern true} { INTERNAL_lt_boogie(x, y): bool }
+ INTERNAL_lt_boogie(x, y): bool == (x < y));
+
+function {:never_pattern true} INTERNAL_le_boogie(x: int, y: int) : bool;
+
+axiom (forall x: int, y: int ::
+ {:never_pattern true} { INTERNAL_le_boogie(x, y): bool }
+ INTERNAL_le_boogie(x, y): bool == (x <= y));
+
+function {:never_pattern true} INTERNAL_gt_boogie(x: int, y: int) : bool;
+
+axiom (forall x: int, y: int ::
+ {:never_pattern true} { INTERNAL_gt_boogie(x, y): bool }
+ INTERNAL_gt_boogie(x, y): bool == (x > y));
+
+function {:never_pattern true} INTERNAL_ge_boogie(x: int, y: int) : bool;
+
+axiom (forall x: int, y: int ::
+ {:never_pattern true} { INTERNAL_ge_boogie(x, y): bool }
+ INTERNAL_ge_boogie(x, y): bool == (x >= y));
+
+const unique class._System.object: ClassName;
+
+// Tclass._System.object Tag
+axiom Tag(Tclass._System.object()) == Tagclass._System.object;
+
+const unique Tagclass._System.object: TyTag;
+
+// Box/unbox axiom for Tclass._System.object
+axiom (forall bx: Box ::
+ { $IsBox(bx, Tclass._System.object()) }
+ $IsBox(bx, Tclass._System.object())
+ ==> $Box($Unbox(bx): ref) == bx && $Is($Unbox(bx): ref, Tclass._System.object()));
+
+// object: Class $Is
+axiom (forall $o: ref ::
+ { $Is($o, Tclass._System.object()) }
+ $Is($o, Tclass._System.object()));
+
+// object: Class $IsAlloc
+axiom (forall $o: ref, $h: Heap ::
+ { $IsAlloc($o, Tclass._System.object(), $h) }
+ $IsAlloc($o, Tclass._System.object(), $h) <==> $o == null || read($h, $o, alloc));
+
+const unique class._System.array: ClassName;
+
+function Tclass._System.array(Ty) : Ty;
+
+// Tclass._System.array Tag
+axiom (forall #$arg: Ty ::
+ { Tclass._System.array(#$arg) }
+ Tag(Tclass._System.array(#$arg)) == Tagclass._System.array);
+
+const unique Tagclass._System.array: TyTag;
+
+// Tclass._System.array injectivity 0
+axiom (forall #$arg: Ty ::
+ { Tclass._System.array(#$arg) }
+ Tclass._System.array_0(Tclass._System.array(#$arg)) == #$arg);
+
+function Tclass._System.array_0(Ty) : Ty;
+
+// Box/unbox axiom for Tclass._System.array
+axiom (forall #$arg: Ty, bx: Box ::
+ { $IsBox(bx, Tclass._System.array(#$arg)) }
+ $IsBox(bx, Tclass._System.array(#$arg))
+ ==> $Box($Unbox(bx): ref) == bx && $Is($Unbox(bx): ref, Tclass._System.array(#$arg)));
+
+// array.: Allocation axiom
+axiom (forall #$arg: Ty, $i0: int, $h: Heap, $o: ref ::
+ { read($h, $o, IndexField($i0)), Tclass._System.array(#$arg) }
+ $IsGoodHeap($h)
+ && $o != null
+ && dtype($o) == Tclass._System.array(#$arg)
+ &&
+ 0 <= $i0
+ && $i0 < _System.array.Length($o)
+ ==> $IsBox(read($h, $o, IndexField($i0)), #$arg)
+ && (read($h, $o, alloc) ==> $IsAllocBox(read($h, $o, IndexField($i0)), #$arg, $h)));
+
+// array: Class $Is
+axiom (forall #$arg: Ty, $o: ref ::
+ { $Is($o, Tclass._System.array(#$arg)) }
+ $Is($o, Tclass._System.array(#$arg))
+ <==> $o == null || dtype($o) == Tclass._System.array(#$arg));
+
+// array: Class $IsAlloc
+axiom (forall #$arg: Ty, $o: ref, $h: Heap ::
+ { $IsAlloc($o, Tclass._System.array(#$arg), $h) }
+ $IsAlloc($o, Tclass._System.array(#$arg), $h)
+ <==> $o == null || read($h, $o, alloc));
+
+// array.Length: Allocation axiom
+axiom (forall #$arg: Ty, $h: Heap, $o: ref ::
+ $IsGoodHeap($h) && $o != null && dtype($o) == Tclass._System.array(#$arg)
+ ==> $Is(_System.array.Length($o), TInt)
+ && (read($h, $o, alloc) ==> $IsAlloc(_System.array.Length($o), TInt, $h)));
+
+function Tclass._System.___hFunc0(Ty) : Ty;
+
+// Tclass._System.___hFunc0 Tag
+axiom (forall #$T0: Ty ::
+ { Tclass._System.___hFunc0(#$T0) }
+ Tag(Tclass._System.___hFunc0(#$T0)) == Tagclass._System.___hFunc0);
+
+const unique Tagclass._System.___hFunc0: TyTag;
+
+// Tclass._System.___hFunc0 injectivity 0
+axiom (forall #$T0: Ty ::
+ { Tclass._System.___hFunc0(#$T0) }
+ Tclass._System.___hFunc0_0(Tclass._System.___hFunc0(#$T0)) == #$T0);
+
+function Tclass._System.___hFunc0_0(Ty) : Ty;
+
+// Box/unbox axiom for Tclass._System.___hFunc0
+axiom (forall #$T0: Ty, bx: Box ::
+ { $IsBox(bx, Tclass._System.___hFunc0(#$T0)) }
+ $IsBox(bx, Tclass._System.___hFunc0(#$T0))
+ ==> $Box($Unbox(bx): HandleType) == bx
+ && $Is($Unbox(bx): HandleType, Tclass._System.___hFunc0(#$T0)));
+
+function Handle0([Heap]Box, [Heap]bool, [Heap]Set Box) : HandleType;
+
+function Apply0(Ty, HandleType, Heap) : Box;
+
+function Requires0(Ty, HandleType, Heap) : bool;
+
+function Reads0(Ty, HandleType, Heap) : Set Box;
+
+axiom (forall t0: Ty, heap: Heap, h: [Heap]Box, r: [Heap]bool, rd: [Heap]Set Box ::
+ { Apply0(t0, Handle0(h, r, rd), heap) }
+ Apply0(t0, Handle0(h, r, rd), heap) == h[heap]);
+
+axiom (forall t0: Ty, heap: Heap, h: [Heap]Box, r: [Heap]bool, rd: [Heap]Set Box ::
+ { Requires0(t0, Handle0(h, r, rd), heap) }
+ r[heap] ==> Requires0(t0, Handle0(h, r, rd), heap));
+
+axiom (forall t0: Ty, heap: Heap, h: [Heap]Box, r: [Heap]bool, rd: [Heap]Set Box, bx: Box ::
+ { Reads0(t0, Handle0(h, r, rd), heap)[bx] }
+ Reads0(t0, Handle0(h, r, rd), heap)[bx] == rd[heap][bx]);
+
+function {:inline true} _System.___hFunc0.requires(t0: Ty, heap: Heap, f: HandleType) : bool
+{
+ Requires0(t0, f, heap)
+}
+
+function {:inline true} _System.___hFunc0.requires#canCall(t0: Ty, heap: Heap, f: HandleType) : bool
+{
+ true
+}
+
+function {:inline true} _System.___hFunc0.reads(t0: Ty, heap: Heap, f: HandleType) : Set Box
+{
+ Reads0(t0, f, heap)
+}
+
+function {:inline true} _System.___hFunc0.reads#canCall(t0: Ty, heap: Heap, f: HandleType) : bool
+{
+ true
+}
+
+axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType ::
+ { $HeapSucc(h0, h1), Reads0(t0, f, h1) }
+ $HeapSucc(h0, h1)
+ &&
+ $IsGoodHeap(h0)
+ && $IsGoodHeap(h1)
+ &&
+ $Is(f, Tclass._System.___hFunc0(t0))
+ && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)
+ && (forall<a> o: ref, fld: Field a ::
+ o != null
+ && read(h0, o, alloc)
+ && read(h1, o, alloc)
+ && Reads0(t0, f, h0)[$Box(o)]
+ ==> read(h0, o, fld) == read(h1, o, fld))
+ ==> Reads0(t0, f, h0) == Reads0(t0, f, h1));
+
+axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType ::
+ { $HeapSucc(h0, h1), Reads0(t0, f, h1) }
+ $HeapSucc(h0, h1)
+ &&
+ $IsGoodHeap(h0)
+ && $IsGoodHeap(h1)
+ &&
+ $Is(f, Tclass._System.___hFunc0(t0))
+ && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)
+ && (forall<a> o: ref, fld: Field a ::
+ o != null
+ && read(h0, o, alloc)
+ && read(h1, o, alloc)
+ && Reads0(t0, f, h1)[$Box(o)]
+ ==> read(h0, o, fld) == read(h1, o, fld))
+ ==> Reads0(t0, f, h0) == Reads0(t0, f, h1));
+
+axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType ::
+ { $HeapSucc(h0, h1), Requires0(t0, f, h1) }
+ $HeapSucc(h0, h1)
+ &&
+ $IsGoodHeap(h0)
+ && $IsGoodHeap(h1)
+ &&
+ $Is(f, Tclass._System.___hFunc0(t0))
+ && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)
+ && (forall<a> o: ref, fld: Field a ::
+ o != null
+ && read(h0, o, alloc)
+ && read(h1, o, alloc)
+ && Reads0(t0, f, h0)[$Box(o)]
+ ==> read(h0, o, fld) == read(h1, o, fld))
+ ==> Requires0(t0, f, h0) == Requires0(t0, f, h1));
+
+axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType ::
+ { $HeapSucc(h0, h1), Requires0(t0, f, h1) }
+ $HeapSucc(h0, h1)
+ &&
+ $IsGoodHeap(h0)
+ && $IsGoodHeap(h1)
+ &&
+ $Is(f, Tclass._System.___hFunc0(t0))
+ && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)
+ && (forall<a> o: ref, fld: Field a ::
+ o != null
+ && read(h0, o, alloc)
+ && read(h1, o, alloc)
+ && Reads0(t0, f, h1)[$Box(o)]
+ ==> read(h0, o, fld) == read(h1, o, fld))
+ ==> Requires0(t0, f, h0) == Requires0(t0, f, h1));
+
+axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType ::
+ { $HeapSucc(h0, h1), Apply0(t0, f, h1) }
+ $HeapSucc(h0, h1)
+ &&
+ $IsGoodHeap(h0)
+ && $IsGoodHeap(h1)
+ &&
+ $Is(f, Tclass._System.___hFunc0(t0))
+ && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)
+ && (forall<a> o: ref, fld: Field a ::
+ o != null
+ && read(h0, o, alloc)
+ && read(h1, o, alloc)
+ && Reads0(t0, f, h0)[$Box(o)]
+ ==> read(h0, o, fld) == read(h1, o, fld))
+ ==> Apply0(t0, f, h0) == Apply0(t0, f, h1));
+
+axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType ::
+ { $HeapSucc(h0, h1), Apply0(t0, f, h1) }
+ $HeapSucc(h0, h1)
+ &&
+ $IsGoodHeap(h0)
+ && $IsGoodHeap(h1)
+ &&
+ $Is(f, Tclass._System.___hFunc0(t0))
+ && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)
+ && (forall<a> o: ref, fld: Field a ::
+ o != null
+ && read(h0, o, alloc)
+ && read(h1, o, alloc)
+ && Reads0(t0, f, h1)[$Box(o)]
+ ==> read(h0, o, fld) == read(h1, o, fld))
+ ==> Apply0(t0, f, h0) == Apply0(t0, f, h1));
+
+axiom (forall t0: Ty, h: Heap, f: HandleType ::
+ { Apply0(t0, f, h) }
+ $IsGoodHeap(h)
+ &&
+ $Is(f, Tclass._System.___hFunc0(t0))
+ && $IsAlloc(f, Tclass._System.___hFunc0(t0), h)
+ ==> $IsBox(Apply0(t0, f, h), t0) && $IsAllocBox(Apply0(t0, f, h), t0, h));
+
+const unique class._module.__default: ClassName;
+
+function Tclass._module.__default() : Ty;
+
+// Tclass._module.__default Tag
+axiom Tag(Tclass._module.__default()) == Tagclass._module.__default;
+
+const unique Tagclass._module.__default: TyTag;
+
+// Box/unbox axiom for Tclass._module.__default
+axiom (forall bx: Box ::
+ { $IsBox(bx, Tclass._module.__default()) }
+ $IsBox(bx, Tclass._module.__default())
+ ==> $Box($Unbox(bx): ref) == bx && $Is($Unbox(bx): ref, Tclass._module.__default()));
+
+// _default: Class $Is
+axiom (forall $o: ref ::
+ { $Is($o, Tclass._module.__default()) }
+ $Is($o, Tclass._module.__default())
+ <==> $o == null || dtype($o) == Tclass._module.__default());
+
+// _default: Class $IsAlloc
+axiom (forall $o: ref, $h: Heap ::
+ { $IsAlloc($o, Tclass._module.__default(), $h) }
+ $IsAlloc($o, Tclass._module.__default(), $h)
+ <==> $o == null || read($h, $o, alloc));
+
+procedure CheckWellformed$$_module.__default.test();
+ free requires 0 == $ModuleContextHeight && 0 == $FunctionContextHeight;
+ modifies $Heap, $Tick;
+
+
+
+implementation CheckWellformed$$_module.__default.test()
+{
+ var $_Frame: <beta>[ref,Field beta]bool;
+
+ // AddMethodImpl: test, CheckWellformed$$_module.__default.test
+ $_Frame := (lambda<alpha> $o: ref, $f: Field alpha ::
+ $o != null && read($Heap, $o, alloc) ==> false);
+ assume {:captureState "Bug136.dfy(4,7): initial state"} true;
+ havoc $Heap;
+ assume (forall<alpha> $o: ref, $f: Field alpha ::
+ { read($Heap, $o, $f) }
+ $o != null && read(old($Heap), $o, alloc)
+ ==> read($Heap, $o, $f) == read(old($Heap), $o, $f));
+ assume $HeapSucc(old($Heap), $Heap);
+}
+
+
+
+procedure InterModuleCall$$_module.__default.test();
+ modifies $Heap, $Tick;
+ // frame condition
+ free ensures (forall<alpha> $o: ref, $f: Field alpha ::
+ { read($Heap, $o, $f) }
+ $o != null && read(old($Heap), $o, alloc)
+ ==> read($Heap, $o, $f) == read(old($Heap), $o, $f));
+ // boilerplate
+ free ensures $HeapSucc(old($Heap), $Heap);
+
+
+
+procedure IntraModuleCall$$_module.__default.test();
+ modifies $Heap, $Tick;
+ // frame condition
+ free ensures (forall<alpha> $o: ref, $f: Field alpha ::
+ { read($Heap, $o, $f) }
+ $o != null && read(old($Heap), $o, alloc)
+ ==> read($Heap, $o, $f) == read(old($Heap), $o, $f));
+ // boilerplate
+ free ensures $HeapSucc(old($Heap), $Heap);
+
+
+
+procedure Impl$$_module.__default.test() returns ($_reverifyPost: bool);
+ free requires 0 == $ModuleContextHeight && 0 == $FunctionContextHeight;
+ modifies $Heap, $Tick;
+ // frame condition
+ free ensures (forall<alpha> $o: ref, $f: Field alpha ::
+ { read($Heap, $o, $f) }
+ $o != null && read(old($Heap), $o, alloc)
+ ==> read($Heap, $o, $f) == read(old($Heap), $o, $f));
+ // boilerplate
+ free ensures $HeapSucc(old($Heap), $Heap);
+
+
+
+implementation Impl$$_module.__default.test() returns ($_reverifyPost: bool)
+{
+ var $_Frame: <beta>[ref,Field beta]bool;
+
+ // AddMethodImpl: test, Impl$$_module.__default.test
+ $_Frame := (lambda<alpha> $o: ref, $f: Field alpha ::
+ $o != null && read($Heap, $o, alloc) ==> false);
+ assume {:captureState "Bug136.dfy(5,1): initial state"} true;
+ $_reverifyPost := false;
+ // ----- assume statement ----- Bug136.dfy(6,5)
+ assume true;
+ assume false;
+ // ----- assert statement ----- Bug136.dfy(7,5)
+ assume true;
+ assert true;
+}
+
+
+
+Dafny program verifier finished with 2 verified, 0 errors
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-30 05:51:02 +0000