[Imprint][Data Privacy Statement][E-Mail]

Back to the index. View project statistic. View project symbols. View KIV symbols to check that all symbols are available.

All project symbols

symbol	specification	entry
#	javatypes	function, javatypes → nat
#	reflistset	function, referencesset → nat
#	javavalues	function, javavalues → nat
#	valuetypes	function, valuetypes → nat
#	refkeyvalues	function, refkeyvalues → nat
#	javastore	function, refkeys → nat
#	store	function, store → nat
#	fieldinit	function, fieldinits → nat
#	references	function, references → nat
#	references	function, referenceset → nat
#	storekeys	function, storekeys → nat
#	classnames	function, classnames → nat
#	classnames	function, classnameset → nat
#	set-basic	function, set → nat
#	string-less	function, string → nat
#	bytelist	function, bytelist → nat
#	bitlista	function, bitlist → nat
#	assoclista	function, assoclist → nat
#	intlista	function, intlist → nat
#	list-data	function, list → nat
#oc	javatypes	function, javatype × javatypes → nat
#oc	javavalues	function, javavalue × javavalues → nat
#oc	valuetypes	function, valuetype × valuetypes → nat
#oc	refkeyvalues	function, refkeyvalue × refkeyvalues → nat
#oc	fieldinit	function, fieldvalue × fieldinits → nat
#oc	references	function, reference × references → nat
#oc	storekeys	function, storekey × storekeys → nat
#oc	classnames	function, classname × classnames → nat
#oc	bytelist	function, byte × bytelist → nat
#oc	bitlista	function, bool × bitlist → nat
#oc	assoclista	function, pair × assoclist → nat
#oc	intlista	function, int × intlist → nat
#oc	list-perm	function, elem × list → nat
%	nat-div	function, nat × nat → nat
%	int-div	function, int × int → int
'	javatypes	function, javatype → javatypes
'	javavalues	function, javavalue → javavalues
'	valuetypes	function, valuetype → valuetypes
'	refkeyvalues	function, refkeyvalue → refkeyvalues
'	fieldinit	function, fieldvalue → fieldinits
'	references	function, reference → references
'	storekeys	function, storekey → storekeys
'	storekey	function, fieldspec → storekey
'	storekey	function, int → storekey
'	classnames	function, classname → classnames
'	bytelist	function, byte → bytelist
'	bitlista	function, bool → bitlist
'	string-append	function, char → string
'	assoclista	function, pair → assoclist
'	intlista	function, int → intlist
'	list	function, elem → list
*	nat-mult	function, nat × nat → nat
*	int-mult	function, int × int → int
+	javatypes	function, javatype × javatypes → javatypes
+	javatypes	function, javatypes × javatypes → javatypes
+	javatypes	function, javatypes × javatype → javatypes
+	javatypes	function, javatype × javatype → javatypes
+	javavalues	function, javavalue × javavalues → javavalues
+	javavalues	function, javavalues × javavalues → javavalues
+	javavalues	function, javavalues × javavalue → javavalues
+	javavalues	function, javavalue × javavalue → javavalues
+	valuetypes	function, valuetype × valuetypes → valuetypes
+	valuetypes	function, valuetypes × valuetypes → valuetypes
+	valuetypes	function, valuetypes × valuetype → valuetypes
+	valuetypes	function, valuetype × valuetype → valuetypes
+	refkeyvalues	function, refkeyvalue × refkeyvalues → refkeyvalues
+	refkeyvalues	function, refkeyvalues × refkeyvalues → refkeyvalues
+	refkeyvalues	function, refkeyvalues × refkeyvalue → refkeyvalues
+	refkeyvalues	function, refkeyvalue × refkeyvalue → refkeyvalues
+	fieldinit	function, fieldvalue × fieldinits → fieldinits
+	fieldinit	function, fieldinits × fieldinits → fieldinits
+	fieldinit	function, fieldinits × fieldvalue → fieldinits
+	fieldinit	function, fieldvalue × fieldvalue → fieldinits
+	references	function, reference × references → references
+	references	function, references × references → references
+	references	function, references × reference → references
+	references	function, reference × reference → references
+	storekeys	function, storekey × storekeys → storekeys
+	storekeys	function, storekeys × storekeys → storekeys
+	storekeys	function, storekeys × storekey → storekeys
+	storekeys	function, storekey × storekey → storekeys
+	classnames	function, classname × classnames → classnames
+	classnames	function, classnames × classnames → classnames
+	classnames	function, classnames × classname → classnames
+	classnames	function, classname × classname → classnames
+	bytelist	function, byte × bytelist → bytelist
+	bytelist	function, bytelist × bytelist → bytelist
+	bytelist	function, bytelist × byte → bytelist
+	bytelist	function, byte × byte → bytelist
+	bitlista	function, bool × bitlist → bitlist
+	bitlista	function, bitlist × bitlist → bitlist
+	bitlista	function, bitlist × bool → bitlist
+	bitlista	function, bool × bool → bitlist
+	string-append	function, string × string → string
+	string-data	function, char × string → string
+	assoclista	function, pair × assoclist → assoclist
+	assoclista	function, assoclist × assoclist → assoclist
+	assoclista	function, assoclist × pair → assoclist
+	assoclista	function, pair × pair → assoclist
+	intlista	function, int × intlist → intlist
+	intlista	function, intlist × intlist → intlist
+	intlista	function, intlist × int → intlist
+	intlista	function, int × int → intlist
+	int-basic2	function, int × int → int
+	list	function, list × list → list
+	list	function, list × elem → list
+	list	function, elem × elem → list
+	list-data	function, elem × list → list
+	nat-basic2	function, nat × nat → nat
++	javatypes	function, javatypes × javatype → javatypes
++	reflistset	function, referencesset × references → referencesset
++	javavalues	function, javavalues × javavalue → javavalues
++	valuetypes	function, valuetypes × valuetype → valuetypes
++	refkeyvalues	function, refkeyvalues × refkeyvalue → refkeyvalues
++	javastore	function, refkeys × refkey → refkeys
++	fieldinit	function, fieldinits × fieldvalue → fieldinits
++	javavalue	function, javavalue × javavalue → javavalue
++	references	function, references × reference → references
++	references	function, referenceset × reference → referenceset
++	storekeys	function, storekeys × storekey → storekeys
++	classnames	function, classnames × classname → classnames
++	classnames	function, classnameset × classname → classnameset
++	set-basic	function, set × elem → set
++	bytelist	function, bytelist × byte → bytelist
++	bitlista	function, bitlist × bool → bitlist
++	assoclista	function, assoclist × pair → assoclist
++	intlista	function, intlist × int → intlist
++	list-dup	function, list × elem → list
+1	bitopsaux	function, bitlist → bitlist
+1	int-basic1	function, int → int
+1	nat-basic1	function, nat → nat
-	int-abs	function, int × int → int
-	nat	function, nat × nat → nat
--	reflistset	function, referencesset × references → referencesset
--	storefuns	function, store × reference → store
--	refkeykeys	function, reference × storekeys → refkeykeys
--	javastore	function, refkeys × refkey → refkeys
--	javastore	function, store × refkey → store
--	store	function, store × elem → store
--	references	function, referenceset × reference → referenceset
--	refkey	function, reference × storekey → refkey
--	classnames	function, classnameset × classname → classnameset
--	set-union	function, set × elem → set
-1	int-basic1	function, int → int
-1	nat-basic1	function, nat → nat
-1l	javatypes	function, javatypes × javatype → javatypes
-1l	javatypes	function, javatypes × nat → javatypes
-1l	javavalues	function, javavalues × javavalue → javavalues
-1l	javavalues	function, javavalues × nat → javavalues
-1l	valuetypes	function, valuetypes × valuetype → valuetypes
-1l	valuetypes	function, valuetypes × nat → valuetypes
-1l	refkeyvalues	function, refkeyvalues × refkeyvalue → refkeyvalues
-1l	refkeyvalues	function, refkeyvalues × nat → refkeyvalues
-1l	fieldinit	function, fieldinits × fieldvalue → fieldinits
-1l	fieldinit	function, fieldinits × nat → fieldinits
-1l	references	function, references × reference → references
-1l	references	function, references × nat → references
-1l	storekeys	function, storekeys × storekey → storekeys
-1l	storekeys	function, storekeys × nat → storekeys
-1l	classnames	function, classnames × classname → classnames
-1l	classnames	function, classnames × nat → classnames
-1l	bytelist	function, bytelist × byte → bytelist
-1l	bytelist	function, bytelist × nat → bytelist
-1l	bitlista	function, bitlist × bool → bitlist
-1l	bitlista	function, bitlist × nat → bitlist
-1l	assoclista	function, assoclist × pair → assoclist
-1l	assoclista	function, assoclist × nat → assoclist
-1l	intlista	function, intlist × int → intlist
-1l	intlista	function, intlist × nat → intlist
-1l	list-del	function, list × elem → list
-1l	list-del	function, list × nat → list
-l	javatypes	function, javatypes × javatype → javatypes
-l	javavalues	function, javavalues × javavalue → javavalues
-l	valuetypes	function, valuetypes × valuetype → valuetypes
-l	refkeyvalues	function, refkeyvalues × refkeyvalue → refkeyvalues
-l	fieldinit	function, fieldinits × fieldvalue → fieldinits
-l	references	function, references × reference → references
-l	storekeys	function, storekeys × storekey → storekeys
-l	classnames	function, classnames × classname → classnames
-l	bytelist	function, bytelist × byte → bytelist
-l	bitlista	function, bitlist × bool → bitlist
-l	assoclista	function, assoclist × pair → assoclist
-l	intlista	function, intlist × int → intlist
-l	list-del	function, list × elem → list
.1	refkeyvalues	function, refkeyvalue → refkey
.1	fieldinit	function, fieldvalue → storekey
.1	pair	function, pair → elem
.2	refkeyvalues	function, refkeyvalue → javavalue
.2	fieldinit	function, fieldvalue → javavalue
.2	pair	function, pair → data
.boolval	javavalue	predicate, javavalue
.butlast	javatypes	function, javatypes → javatypes
.butlast	javavalues	function, javavalues → javavalues
.butlast	valuetypes	function, valuetypes → valuetypes
.butlast	refkeyvalues	function, refkeyvalues → refkeyvalues
.butlast	fieldinit	function, fieldinits → fieldinits
.butlast	references	function, references → references
.butlast	storekeys	function, storekeys → storekeys
.butlast	classnames	function, classnames → classnames
.butlast	bytelist	function, bytelist → bytelist
.butlast	bitlista	function, bitlist → bitlist
.butlast	assoclista	function, assoclist → assoclist
.butlast	intlista	function, intlist → intlist
.butlast	list-last	function, list → list
.butmax	javastore	function, refkeys → refkeys
.butmax	references	function, referenceset → referenceset
.butmax	classnames	function, classnameset → classnameset
.butmax	oset	function, set → set
.butmin	javastore	function, refkeys → refkeys
.butmin	ostore	function, store → store
.butmin	references	function, referenceset → referenceset
.butmin	classnames	function, classnameset → classnameset
.butmin	oset	function, set → set
.byteval	javavalue	function, javavalue → byte
.char1	string-data	function, string → char
.charval	javavalue	function, javavalue → javachar
.class	fieldspec	function, fieldspec → classname
.class	javatype	function, javatype → classname
.class	classname	function, string → classname
.class	classname	function, classname → string
.doubleval	javavalue	function, javavalue → double
.field	fieldspec	function, fieldspec → fieldname
.field	fieldname	function, string → fieldname
.field	fieldname	function, fieldname → string
.first	javatypes	function, javatypes → javatype
.first	javavalues	function, javavalues → javavalue
.first	valuetypes	function, valuetypes → valuetype
.first	refkeyvalues	function, refkeyvalues → refkeyvalue
.first	fieldinit	function, fieldinits → fieldvalue
.first	references	function, references → reference
.first	storekeys	function, storekeys → storekey
.first	classnames	function, classnames → classname
.first	bytelist	function, bytelist → byte
.first	bitlista	predicate, bitlist
.first	assoclista	function, assoclist → pair
.first	intlista	function, intlist → int
.first	list-data	function, list → elem
.firstval	javavalue	function, javavalue → javavalue
.floatval	javavalue	function, javavalue → float
.fs	storekey	function, storekey → fieldspec
.index	storekey	function, storekey → int
.int	javachar	function, javachar → int
.int	float	function, float → int
.int	float	function, double → int
.intval	javavalue	function, javavalue → int
.istate	javavalue	function, javavalue → initstate
.jtclass	typefuns	function, javatype → classname
.jtdims	typefuns	function, javatype → int
.jtelemtype	typefuns	function, javatype → javatype
.key	refkey	function, refkey → storekey
.keys	okfuns	function, fieldinits → storekeys
.keys	refkeykeys	function, refkeykeys → storekeys
.keys	javastore	function, store → refkeys
.keys	ostore	function, store → set
.label	javavalue	function, javavalue → label
.label	label	function, string → label
.label	label	function, label → string
.last	javatypes	function, javatypes → javatype
.last	javavalues	function, javavalues → javavalue
.last	valuetypes	function, valuetypes → valuetype
.last	refkeyvalues	function, refkeyvalues → refkeyvalue
.last	fieldinit	function, fieldinits → fieldvalue
.last	references	function, references → reference
.last	storekeys	function, storekeys → storekey
.last	classnames	function, classnames → classname
.last	bytelist	function, bytelist → byte
.last	bitlista	predicate, bitlist
.last	assoclista	function, assoclist → pair
.last	intlista	function, intlist → int
.last	list-last	function, list → elem
.longval	javavalue	function, javavalue → long
.max	javastore	function, refkeys → refkey
.max	references	function, referenceset → reference
.max	classnames	function, classnameset → classname
.max	oset	function, set → elem
.min	javastore	function, refkeys → refkey
.min	javastore	function, store → refkey
.min	ostore	function, store → elem
.min	references	function, referenceset → reference
.min	classnames	function, classnameset → classname
.min	oset	function, set → elem
.nonnullrefs	valuesfuns	function, javavalues → references
.ref	refkeykeys	function, refkeykeys → reference
.ref	refkey	function, refkey → reference
.refs	storefunsx	function, store → referenceset
.refval	javavalue	function, javavalue → reference
.rest	javatypes	function, javatypes → javatypes
.rest	javavalues	function, javavalues → javavalues
.rest	valuetypes	function, valuetypes → valuetypes
.rest	refkeyvalues	function, refkeyvalues → refkeyvalues
.rest	fieldinit	function, fieldinits → fieldinits
.rest	references	function, references → references
.rest	storekeys	function, storekeys → storekeys
.rest	classnames	function, classnames → classnames
.rest	bytelist	function, bytelist → bytelist
.rest	bitlista	function, bitlist → bitlist
.rest	assoclista	function, assoclist → assoclist
.rest	intlista	function, intlist → intlist
.rest	list-data	function, list → list
.restval	javavalue	function, javavalue → javavalue
.rstring	string-data	function, string → string
.shortval	javavalue	function, javavalue → short
.stringval	javavalue	function, javavalue → string
.type	value+type	function, valuetype → javatype
.type	javavalue	function, javavalue → javatype
.type	fieldspec	function, fieldspec → javatype
.type	javatype	function, javatype → javatype
.val	value+type	function, valuetype → javavalue
.val	javavalue	function, javavalue → javavalue
.vals	okfuns	function, fieldinits → javavalues
/	nat-div	function, nat × nat → nat
/	int-div	function, int × int → int
0b	byte	constant, byte
0bi	byte	constant, bint
0d	float	constant, double
0f	float	constant, float
0l	byte	constant, long
0s	byte	constant, short
<	javatypes	predicate, javatypes × javatypes
<	javavalues	predicate, javavalues × javavalues
<	valuetypes	predicate, valuetypes × valuetypes
<	refkeyvalues	predicate, refkeyvalues × refkeyvalues
<	javastore	predicate, refkey × refkeys
<	javastore	predicate, refkeys × refkey
<	fieldinit	predicate, fieldinits × fieldinits
<	references	predicate, references × references
<	references	predicate, reference × referenceset
<	references	predicate, referenceset × reference
<	storekeys	predicate, storekeys × storekeys
<	specialkeys	predicate, refkey × refkey
<	reference	predicate, reference × reference
<	classnames	predicate, classnames × classnames
<	classnames	predicate, classname × classnameset
<	classnames	predicate, classnameset × classname
<	oset	predicate, elem × set
<	oset	predicate, set × elem
<	string-less	predicate, string × string
<	string-less	predicate, char × char
<	bytelist	predicate, bytelist × bytelist
<	bitlista	predicate, bitlist × bitlist
<	assoclista	predicate, assoclist × assoclist
<	intlista	predicate, intlist × intlist
<	int-basic1	predicate, int × int
<	oelem	predicate, elem × elem
<	list-data	predicate, list × list
<	nat-basic1	predicate, nat × nat
<<	intops	function, int × int → int
<_1	classnamefuns	predicate, classname × classname
=mode	storefunsx	predicate, store × store
>	int-abs	predicate, int × int
>	nat	predicate, nat × nat
>>	intops	function, int × int → int
>>>	intops	function, nat × int × int → int
[]	javatypes	constant, javatypes
[]	javavalues	constant, javavalues
[]	valuetypes	constant, valuetypes
[]	refkeyvalues	constant, refkeyvalues
[]	fieldinit	constant, fieldinits
[]	references	constant, references
[]	storekeys	constant, storekeys
[]	classnames	constant, classnames
[]	bytelist	constant, bytelist
[]	bitlista	constant, bitlist
[]	assoclista	constant, assoclist
[]	intlista	constant, intlist
[]	list-data	constant, list
\	javatypes	function, javatypes × javatypes → javatypes
\	reflistset	function, referencesset × referencesset → referencesset
\	javavalues	function, javavalues × javavalues → javavalues
\	valuetypes	function, valuetypes × valuetypes → valuetypes
\	refkeyvalues	function, refkeyvalues × refkeyvalues → refkeyvalues
\	javastore	function, refkeys × refkeys → refkeys
\	fieldinit	function, fieldinits × fieldinits → fieldinits
\	references	function, references × references → references
\	references	function, referenceset × referenceset → referenceset
\	storekeys	function, storekeys × storekeys → storekeys
\	classnames	function, classnames × classnames → classnames
\	classnames	function, classnameset × classnameset → classnameset
\	set-union	function, set × set → set
\	bytelist	function, bytelist × bytelist → bytelist
\	bitlista	function, bitlist × bitlist → bitlist
\	assoclista	function, assoclist × assoclist → assoclist
\	intlista	function, intlist × intlist → intlist
\	list-set	function, list × list → list
]	javatypes	function, javatypes × nat → javatype
]	javatypes	function, javatypes × nat × javatype → javatypes
]	javavalues	function, javavalues × nat → javavalue
]	javavalues	function, javavalues × nat × javavalue → javavalues
]	valuetypes	function, valuetypes × nat → valuetype
]	valuetypes	function, valuetypes × nat × valuetype → valuetypes
]	storefuns	function, store × storekey → javavalue
]	storefuns	function, store × storekeys → javavalue
]	storefuns	function, store × refkeykeys → javavalue
]	storefuns	function, store × storekey × javavalue → store
]	storefuns	function, store × storekeys × javavalue → store
]	storefuns	function, store × refkeykeys × javavalue → store
]	storefuns	function, store × refkeyvalues → store
]	refkeyvalues	function, refkeyvalues × nat → refkeyvalue
]	refkeyvalues	function, refkeyvalues × nat × refkeyvalue → refkeyvalues
]	refkeyvalues	function, refkeyvalues × refkey → javavalue
]	refkeyvalues	function, refkeyvalues × javavalue → refkey
]	refkeyvalues	function, refkeyvalues × refkey × javavalue → refkeyvalues
]	javastore	function, store × refkey × javavalue → store
]	javastore	function, store × refkey → javavalue
]	store	function, store × elem × data → store
]	store	function, store × elem → data
]	fieldinit	function, fieldinits × nat → fieldvalue
]	fieldinit	function, fieldinits × nat × fieldvalue → fieldinits
]	fieldinit	function, fieldinits × storekey → javavalue
]	fieldinit	function, fieldinits × javavalue → storekey
]	fieldinit	function, fieldinits × storekey × javavalue → fieldinits
]	valuefuns	function, javavalue × reference × reference → javavalue
]	references	function, references × nat → reference
]	references	function, references × nat × reference → references
]	storekeys	function, storekeys × nat → storekey
]	storekeys	function, storekeys × nat × storekey → storekeys
]	classnames	function, classnames × nat → classname
]	classnames	function, classnames × nat × classname → classnames
]	bytelist	function, bytelist × nat → byte
]	bytelist	function, bytelist × nat × byte → bytelist
]	bitlista	predicate, bitlist × nat
]	bitlista	function, bitlist × nat × bool → bitlist
]	assoclist	function, assoclist × elem → data
]	assoclist	function, assoclist × data → elem
]	assoclist	function, assoclist × elem × data → assoclist
]	assoclista	function, assoclist × nat → pair
]	assoclista	function, assoclist × nat × pair → assoclist
]	intlista	function, intlist × nat → int
]	intlista	function, intlist × nat × int → intlist
]	list-del	function, list × nat → elem
]	list-del	function, list × nat × elem → list
^	int-pot	function, int × int → int
^2	int-square	function, int → int
_endfinallymode	specialkeys	constant, refkey
_initfield	specialkeys	constant, fieldname
_length	specialkeys	constant, storekey
_mode	specialkeys	constant, refkey
_out	storefuns	function, store → javavalue
_out	specialkeys	constant, refkey
_type	specialkeys	constant, storekey
_uninit	specialkeys	constant, refkey
a	elem	variable, elem
a0	store	variable, elem
a0	pair	variable, elem
a0	list-data	variable, elem
abs	int-abs	function, int → int
abstract_type	javatype	constant, javatype
acc	multiarrays	variable, references
addarray	addarray	function, reference × javatype × int × store → store
addarray	addarray	function, reference × javatype × javavalues × store → store
addarray	addarray	function, reference × javatype × bytelist × store → store
addarray	addarray	function, reference × javavalue × int × store → store
addarray	addarray	function, reference × javavalues × int × store → store
addarraymult	multiarrays	function, reference × javatype × store × references × intlist × int → store
addarraymultlist	multiarrays	function, reference × javatype × store × references × intlist × intlist × int → store
addarrays	multiarrays	function, references × javatype × intlist × int × store → store
addbytearray	addarray	function, reference × intlist × store → store
addclass	addfuns	function, classname × fieldinits × store → store
addmultiarrays	multiarrays	function, references × int × references × javatype × intlist × store → store
addobj	addfuns	function, reference × classname × fieldinits × store → store
addobj	addfuns	function, reference × classname × storekeys × store → store
addobj	addfuns	function, reference × classname × store → store
arraycomp	storearrays	predicate, reference × int × reference × int × int × store
arraycopy	storearrays	function, reference × int × reference × int × int × store → store
asgcomp	okfuns	predicate, string × javavalue × javatype × store
assoclist	assoclista	sort,
ax	assoclista	variable, assoclist
ax0	assoclista	variable, assoclist
ax1	assoclista	variable, assoclist
ax2	assoclista	variable, assoclist
ay	assoclista	variable, assoclist
ay0	assoclista	variable, assoclist
ay1	assoclista	variable, assoclist
ay2	assoclista	variable, assoclist
az	assoclista	variable, assoclist
az0	assoclista	variable, assoclist
az1	assoclista	variable, assoclist
az2	assoclista	variable, assoclist
b	elem	variable, elem
b2bi	byte	function, byte → bint
b2i	byte	function, byte → int
b2s	byte	function, byte → short
band	intops	function, int × int → int
bcompl	intops	function, int → int
bi	byte	variable, bint
bi2b	byte	function, bint → byte
bi2i	byte	function, bint → int
bi2s	byte	function, bint → short
bint	byte	sort,
bitlist	bitlista	sort,
bits	bitlista	variable, bitlist
bits0	bitlista	variable, bitlist
bits1	bitlista	variable, bitlist
bits10	bitlista	variable, bitlist
bits2	bitlista	variable, bitlist
bits2bytes	bytes	function, bitlist → bytelist
bits2int	int2bits	function, bitlist → int
bits2uint	int2bits	function, bitlist → int
bits3	bitlista	variable, bitlist
bits4	bitlista	variable, bitlist
bits5	bitlista	variable, bitlist
bits6	bitlista	variable, bitlist
bits7	bitlista	variable, bitlist
bits8	bitlista	variable, bitlist
bits9	bitlista	variable, bitlist
bitsand	intops	function, bitlist × bitlist → bitlist
bitsinvert	bitopsaux	function, bitlist → bitlist
bitsor	intops	function, bitlist × bitlist → bitlist
bitsxor	intops	function, bitlist × bitlist → bitlist
bj	byte	variable, bint
bool	bool	sort,
boolean_type	javatype	constant, javatype
boolval	javavalue	function, bool → javavalue
boolvar	bool	variable, bool
boolvar0	bool	variable, bool
boolvar1	bitlista	variable, bool
boolvar2	bitlista	variable, bool
bor	intops	function, int × int → int
break	javavalue	function, label → javavalue
bs2is	valuesfuns	function, bytelist → intlist
butlastn	javatypes	function, nat × javatypes → javatypes
butlastn	javavalues	function, nat × javavalues → javavalues
butlastn	valuetypes	function, nat × valuetypes → valuetypes
butlastn	refkeyvalues	function, nat × refkeyvalues → refkeyvalues
butlastn	fieldinit	function, nat × fieldinits → fieldinits
butlastn	references	function, nat × references → references
butlastn	storekeys	function, nat × storekeys → storekeys
butlastn	classnames	function, nat × classnames → classnames
butlastn	bytelist	function, nat × bytelist → bytelist
butlastn	bitlista	function, nat × bitlist → bitlist
butlastn	assoclista	function, nat × assoclist → assoclist
butlastn	intlista	function, nat × intlist → intlist
butlastn	list-last	function, nat × list → list
bxor	intops	function, int × int → int
by	byte	variable, byte
by0	bytelist	variable, byte
by1	bytelist	variable, byte
by2	bytelist	variable, byte
byi	byte	variable, byte
byj	byte	variable, byte
byte	byte	sort,
byte2bits	bytes	function, byte → bitlist
byte_type	javatype	constant, javatype
bytelist	bytelist	sort,
bytes	bytelist	variable, bytelist
bytes0	bytelist	variable, bytelist
bytes1	bytelist	variable, bytelist
bytes10	bytelist	variable, bytelist
bytes2	bytelist	variable, bytelist
bytes2bits	bytes	function, bytelist → bitlist
bytes2int	bytes	function, bytelist → int
bytes3	bytelist	variable, bytelist
bytes4	bytelist	variable, bytelist
bytes5	bytelist	variable, bytelist
bytes6	bytelist	variable, bytelist
bytes7	bytelist	variable, bytelist
bytes8	bytelist	variable, bytelist
bytes9	bytelist	variable, bytelist
byteval	javavalue	function, byte → javavalue
bytevalues	valuesfuns	function, javavalues → bytelist
c	elem	variable, elem
cast	intops	function, int × int → int
catch_break	storefuns	function, store → store
catch_continue	storefuns	function, store → store
char	char	variable, char
char	char	sort,
char0	char	variable, char
char1	char	variable, char
char2	char	variable, char
char3	string-less	variable, char
char_type	javatype	constant, javatype
charval	javavalue	function, javachar → javavalue
claset	classnames	variable, classnameset
claset0	classnames	variable, classnameset
claset1	classnames	variable, classnameset
claset2	classnames	variable, classnameset
class	classname	variable, classname
class+∃	typefuns	predicate, string × classname
class0	classname	variable, classname
class1	classname	variable, classname
class2	classname	variable, classname
class3	classname	variable, classname
classes	classnames	variable, classnames
classes0	classnames	variable, classnames
classes1	classnames	variable, classnames
classes10	classnames	variable, classnames
classes2	classnames	variable, classnames
classes3	classnames	variable, classnames
classes4	classnames	variable, classnames
classes5	classnames	variable, classnames
classes6	classnames	variable, classnames
classes7	classnames	variable, classnames
classes8	classnames	variable, classnames
classes9	classnames	variable, classnames
classname	classname	sort,
classnames	classnames	sort,
classnameset	classnames	sort,
classof	storefunsx	predicate, reference × classname × store
class∃	typefuns	predicate, string × classname
coerce	valuefuns	function, javavalue × javatype → javavalue
contains	contains	predicate, string × javatype × javatype
contains	contains	predicate, string × javatypes
contains	contains	predicate, string × javatype × fieldspec
continue	javavalue	function, label → javavalue
count-i2j	intlist	function, int × int → intlist
countFun	intlist	function, int × int × int → int → intlist
countdims	multiarrays	function, intlist × int → int
countrefs	multiarrays	function, intlist → int
countrefs2	multiarrays	function, intlist → int
cyclic	cyclic	predicate, string × reference × store
d	data	variable, data
d0	data	variable, data
d1	data	variable, data
d2	data	variable, data
data	data	sort,
disj	javatypes	predicate, javatypes × javatypes
disj	javavalues	predicate, javavalues × javavalues
disj	valuetypes	predicate, valuetypes × valuetypes
disj	refkeyvalues	predicate, refkeyvalues × refkeyvalues
disj	fieldinit	predicate, fieldinits × fieldinits
disj	references	predicate, references × references
disj	storekeys	predicate, storekeys × storekeys
disj	classnames	predicate, classnames × classnames
disj	bytelist	predicate, bytelist × bytelist
disj	bitlista	predicate, bitlist × bitlist
disj	assoclista	predicate, assoclist × assoclist
disj	intlista	predicate, intlist × intlist
disj	list-dup	predicate, list × list
done	initstate	constant, initstate
double	float	sort,
double_type	javatype	constant, javatype
doubleval	javavalue	function, double → javavalue
doublevar	float	variable, double
doublevar0	javavalue	variable, double
dups	javatypes	predicate, javatypes
dups	javavalues	predicate, javavalues
dups	valuetypes	predicate, valuetypes
dups	refkeyvalues	predicate, refkeyvalues
dups	fieldinit	predicate, fieldinits
dups	references	predicate, references
dups	storekeys	predicate, storekeys
dups	classnames	predicate, classnames
dups	bytelist	predicate, bytelist
dups	bitlista	predicate, bitlist
dups	assoclista	predicate, assoclist
dups	intlista	predicate, intlist
dups	list-dup	predicate, list
elem	elem	sort,
elemdata	store	sort,
elemdatavar	store	variable, elemdata
eqex	storefunsx	predicate, store × store × reference
eqexmode	storefunsx	predicate, store × store × reference
eqkeys	storefunsx	predicate, store × store
eqobj	storefunsx	predicate, reference × store × store
eqobjid	storefunsx	predicate, reference × store × store
eqref	okfuns	predicate, reference × reference × store × store
eqval	okfuns	predicate, javavalue × javavalue × store × store
error	initstate	constant, initstate
even	int-min	predicate, int
exactarray	okfuns	predicate, reference × javatype × store
exactarray	okfuns	predicate, javavalue × javatype × int × store
exactfieldandtype	okfuns	predicate, reference × storekey × store
exactfieldsandtypes	okfuns	predicate, reference × storekeys × store
exactreftype	okfuns	predicate, javavalue × javatype × store
exacttype	okfuns	predicate, javavalue × javatype × store
exception	storefunsx	predicate, classname × store
fieldinits	fieldinit	sort,
fieldname	fieldname	sort,
fieldspec	fieldspec	sort,
fieldvalue	fieldinit	sort,
fieldvar	fieldname	variable, fieldname
fieldvar0	fieldname	variable, fieldname
fieldvar1	fieldname	variable, fieldname
fieldvar2	fieldname	variable, fieldname
fieldvar3	fieldname	variable, fieldname
fillfirst	javatypes	function, nat × javatype × javatypes → javatypes
fillfirst	javavalues	function, nat × javavalue × javavalues → javavalues
fillfirst	valuetypes	function, nat × valuetype × valuetypes → valuetypes
fillfirst	refkeyvalues	function, nat × refkeyvalue × refkeyvalues → refkeyvalues
fillfirst	fieldinit	function, nat × fieldvalue × fieldinits → fieldinits
fillfirst	references	function, nat × reference × references → references
fillfirst	storekeys	function, nat × storekey × storekeys → storekeys
fillfirst	classnames	function, nat × classname × classnames → classnames
fillfirst	bytelist	function, nat × byte × bytelist → bytelist
fillfirst	bitlista	function, nat × bool × bitlist → bitlist
fillfirst	assoclista	function, nat × pair × assoclist → assoclist
fillfirst	intlista	function, nat × int × intlist → intlist
fillfirst	list-last	function, nat × elem × list → list
fillsgn	bytes	function, nat × bytelist → bytelist
fillsgn	bitopsaux	function, nat × bitlist → bitlist
filter	javatypes	function, javatypes × javatypes → javatypes
filter	javavalues	function, javavalues × javavalues → javavalues
filter	valuetypes	function, valuetypes × valuetypes → valuetypes
filter	refkeyvalues	function, refkeyvalues × refkeyvalues → refkeyvalues
filter	fieldinit	function, fieldinits × fieldinits → fieldinits
filter	references	function, references × references → references
filter	storekeys	function, storekeys × storekeys → storekeys
filter	classnames	function, classnames × classnames → classnames
filter	bytelist	function, bytelist × bytelist → bytelist
filter	bitlista	function, bitlist × bitlist → bitlist
filter	assoclista	function, assoclist × assoclist → assoclist
filter	intlista	function, intlist × intlist → intlist
filter	list-set	function, list × list → list
firstn	javatypes	function, nat × javatypes → javatypes
firstn	javavalues	function, nat × javavalues → javavalues
firstn	valuetypes	function, nat × valuetypes → valuetypes
firstn	refkeyvalues	function, nat × refkeyvalues → refkeyvalues
firstn	fieldinit	function, nat × fieldinits → fieldinits
firstn	references	function, nat × references → references
firstn	storekeys	function, nat × storekeys → storekeys
firstn	classnames	function, nat × classnames → classnames
firstn	bytelist	function, nat × bytelist → bytelist
firstn	bitlista	function, nat × bitlist → bitlist
firstn	assoclista	function, nat × assoclist → assoclist
firstn	intlista	function, nat × intlist → intlist
firstn	list-del	function, nat × list → list
fis	fieldinit	variable, fieldinits
fis0	fieldinit	variable, fieldinits
fis1	fieldinit	variable, fieldinits
fis10	fieldinit	variable, fieldinits
fis2	fieldinit	variable, fieldinits
fis3	fieldinit	variable, fieldinits
fis4	fieldinit	variable, fieldinits
fis5	fieldinit	variable, fieldinits
fis6	fieldinit	variable, fieldinits
fis7	fieldinit	variable, fieldinits
fis8	fieldinit	variable, fieldinits
fis9	fieldinit	variable, fieldinits
fix	bytes	function, nat × bytelist → bytelist
fix	bitopsaux	function, nat × bitlist → bitlist
flatten	valuefuns	function, javavalue → javavalue
float	float	sort,
float_type	javatype	constant, javatype
floatval	javavalue	function, float → javavalue
floatvar	float	variable, float
floatvar0	javavalue	variable, float
frome	javatypes	function, javatypes × javatype → javatypes
frome	javavalues	function, javavalues × javavalue → javavalues
frome	valuetypes	function, valuetypes × valuetype → valuetypes
frome	refkeyvalues	function, refkeyvalues × refkeyvalue → refkeyvalues
frome	fieldinit	function, fieldinits × fieldvalue → fieldinits
frome	references	function, references × reference → references
frome	storekeys	function, storekeys × storekey → storekeys
frome	classnames	function, classnames × classname → classnames
frome	bytelist	function, bytelist × byte → bytelist
frome	bitlista	function, bitlist × bool → bitlist
frome	assoclista	function, assoclist × pair → assoclist
frome	intlista	function, intlist × int → intlist
frome	list-del	function, list × elem → list
fs	fieldspec	variable, fieldspec
fs0	fieldspec	variable, fieldspec
fs1	fieldspec	variable, fieldspec
fv	fieldinit	variable, fieldvalue
fv0	fieldinit	variable, fieldvalue
fv1	fieldinit	variable, fieldvalue
fv2	fieldinit	variable, fieldvalue
get	valuefuns	function, nat × javavalue → javavalue
getarray	storearrays	function, reference × store → javavalues
getarray	storearrays	function, reference × int × int × store → javavalues
getarrayv	storearrays	function, reference × int × int × store → javavalue
getarrayv	storearrays	function, reference × store → javavalue
getbytearray	storearrays	function, reference × store → bytelist
getbytearray	storearrays	function, reference × int × int × store → bytelist
getdims	multiarrays	function, intlist → intlist
getintarray	storearrays	function, reference × store → intlist
getintarray	storearrays	function, reference × int × int × store → intlist
getrange	valuefuns	function, nat × nat × javavalue → javavalue
getrefs	storefuns	function, reference × storekeys × store → references
goodfieldandtype	okfuns	predicate, reference × storekey × store
goodfieldsandtypes	okfuns	predicate, reference × storekeys × store
hasKeys	okfuns	predicate, reference × storekeys × store
has_classtype	typefuns	predicate, javatype
has_reffield	addfuns	predicate, reference × store
has_type	storefunsx	predicate, reference × store
i	int-basic1	variable, int
i0	int-basic1	variable, int
i1	storefuns	variable, int
i1	intlista	variable, int
i2	storefuns	variable, int
i2	intlista	variable, int
i2b	byte	function, int → byte
i2bi	byte	function, int → bint
i2l	byte	function, int → long
i2s	byte	function, int → short
i<<	intops	function, int × int → int
i>>	intops	function, int × int → int
i>>>	intops	function, int × int → int
incdec	valuefuns	function, javavalue × int → javavalue
init	storefunsx	predicate, classnameset × store
init	storefunsx	function, classname × store → store
init	storefuns	predicate, store
init	storefuns	predicate, string × store
initdone	storefunsx	predicate, classnames × store
initdone	storefuns	predicate, classname × store
initdoneP	storefuns	predicate, classname × store
initerror	storefunsx	predicate, classnameset × store
initerror	storefuns	predicate, classname × store
initial_value	valuefuns	function, javatype → javavalue
initstate	initstate	sort,
initundone	storefuns	predicate, classname × store
initundoneP	storefuns	predicate, classname × store
initval	javavalue	function, initstate → javavalue
init⊆	junkrefs	predicate, string × store × store
instfields	addfuns	function, classname → storekeys
instore	okfuns	predicate, reference × classname × fieldinits × store
ins≤	references	function, reference × references → references
ins≤	classnames	function, classname × classnames → classnames
ins≤	intlista	function, int × intlist → intlist
ins≤	olist	function, elem × list → list
int	int-basic1	sort,
int2bits	int2bits	function, int → bitlist
int2bytes	bytes	function, int → bytelist
int_type	javatype	constant, javatype
interface∃	typefuns	predicate, string × classname
intfun	intlist	variable, int → int
intlist	intlista	sort,
ints	intlista	variable, intlist
ints#	multiarrays	function, intlist → nat
ints0	intlista	variable, intlist
ints1	intlista	variable, intlist
ints10	intlista	variable, intlist
ints2	intlista	variable, intlist
ints3	intlista	variable, intlist
ints4	intlista	variable, intlist
ints5	intlista	variable, intlist
ints6	intlista	variable, intlist
ints7	intlista	variable, intlist
ints8	intlista	variable, intlist
ints9	intlista	variable, intlist
intval	javavalue	function, int → javavalue
intvalues	valuesfuns	function, javavalues → intlist
intvalues	valuesfuns	function, intlist → javavalues
is2bs	valuesfuns	function, intlist → bytelist
is_a_newref	storefuns	predicate, reference × store
is_abstract	typefuns	predicate, classname
is_array	okfuns	predicate, reference × store
is_array	okfuns	predicate, string × reference × store
is_arrayref	storearrays	predicate, reference × int × store
is_arraytype	javatype	predicate, javatype
is_boolvalue	javavalue	predicate, javavalue
is_break_mode	javavalue	predicate, javavalue
is_bytelist	valuesfuns	predicate, javavalues
is_bytelistlist	valuesfuns	predicate, javavalues
is_bytevalue	javavalue	predicate, javavalue
is_charvalue	javavalue	predicate, javavalue
is_classtype	javatype	predicate, javatype
is_continue_mode	javavalue	predicate, javavalue
is_doublevalue	javavalue	predicate, javavalue
is_floatvalue	javavalue	predicate, javavalue
is_fskey	storekey	predicate, storekey
is_indexkey	storekey	predicate, storekey
is_initvalue	javavalue	predicate, javavalue
is_integervalue	javavalue	predicate, javavalue
is_javastore	okfuns	predicate, store
is_longvalue	javavalue	predicate, javavalue
is_newref_list	storefuns	predicate, references × store
is_normal_mode	valuefuns	predicate, javavalue
is_novalue	javavalue	predicate, javavalue
is_obj	addfuns	predicate, reference × classname × storekeys × store
is_obj	addfuns	predicate, reference × classname × store
is_obj	addfuns	predicate, reference × store
is_obj	addfuns	predicate, string × reference × store
is_obj_exact	addfuns	predicate, reference × classname × storekeys × store
is_predefined_class	predefined	predicate, classname
is_primtype	typefuns	predicate, javatype
is_referencevalue	javavalue	predicate, javavalue
is_reftype	typefuns	predicate, javatype
is_return_mode	javavalue	predicate, javavalue
is_shortvalue	javavalue	predicate, javavalue
is_stringvalue	javavalue	predicate, javavalue
is_subclass	typefuns	predicate, classname × classnames × classname
is_subtype	typefuns	predicate, string × javatype × javatype
is_subtype	typefuns	predicate, javatype × javatype × classnameset
is_subtype	typefuns	predicate, javatype × classnames × javatype
is_the_newref	storefuns	predicate, reference × store
is_throw_mode	javavalue	predicate, javavalue
is_typevalue	javavalue	predicate, javavalue
is_valid_ref	addfuns	predicate, string × reference × store
is_valid_ref	addfuns	predicate, reference × store
is_valuelist	javavalue	predicate, javavalue
is_void_type	javatype	predicate, javatype
istate	initstate	variable, initstate
istate0	javavalue	variable, initstate
i→n	intnat	function, int → nat
j	int-basic1	variable, int
j0	int-basic1	variable, int
javachar	javachar	sort,
javatype	javatype	sort,
javatypes	javatypes	sort,
javavalue	javavalue	sort,
javavalues	javavalues	sort,
jchar	javachar	variable, javachar
jchar0	javachar	variable, javachar
jchar1	javachar	variable, javachar
jchar2	javachar	variable, javachar
jump	storefuns	predicate, store
junkref	junkrefs	predicate, string × reference × store
junkrefs	junkrefs	predicate, string × javavalues × store
junkrefs	junkrefs	predicate, string × references × javatype × store
jvmref	reference	constant, reference
l2i	byte	function, long → int
l<	classnamefuns	predicate, classname × classname
l<<	intops	function, int × int → int
l>>	intops	function, int × int → int
l>>>	intops	function, int × int → int
label	label	sort,
lastn	javatypes	function, nat × javatypes → javatypes
lastn	javavalues	function, nat × javavalues → javavalues
lastn	valuetypes	function, nat × valuetypes → valuetypes
lastn	refkeyvalues	function, nat × refkeyvalues → refkeyvalues
lastn	fieldinit	function, nat × fieldinits → fieldinits
lastn	references	function, nat × references → references
lastn	storekeys	function, nat × storekeys → storekeys
lastn	classnames	function, nat × classnames → classnames
lastn	bytelist	function, nat × bytelist → bytelist
lastn	bitlista	function, nat × bitlist → bitlist
lastn	assoclista	function, nat × assoclist → assoclist
lastn	intlista	function, nat × intlist → intlist
lastn	list-del	function, nat × list → list
lbl	label	variable, label
lbl0	label	variable, label
lbl1	label	variable, label
lbl2	label	variable, label
level⊆	junkrefs	predicate, string × string
list	list-data	sort,
list2set	references	function, references → referenceset
list2set	classnames	function, classnames → classnameset
list2set	setlist	function, list → set
lo	byte	variable, long
lo0	javavalue	variable, long
loi	byte	variable, long
loj	byte	variable, long
long	byte	sort,
long_type	javatype	constant, javatype
longval	javavalue	function, long → javavalue
m	nat-basic2	variable, nat
mapFun	intlist	function, int → int × intlist → intlist
max	intlist	function, intlist → int
max	int-min	function, int × int → int
maxpath	pointers	function, string × reference × store → nat
maxref	storefuns	function, store → reference
merge	references	function, references × references → references
merge	classnames	function, classnames × classnames → classnames
merge	intlista	function, intlist × intlist → intlist
merge	olist	function, list × list → list
min	int-min	function, int × int → int
mkarraytype	javatype	function, javatype → javatype
mkchar	javachar	function, int → javachar
mkchar	javachar	function, string → javachar
mkclasstype	javatype	function, classname → javatype
mkdouble	float	function, string → double
mkfloat	float	function, string → float
mkfs	fieldspec	function, classname × javatype × fieldname → fieldspec
mkjavavalue	valuesfuns	function, bytelist → javavalue
mkjavavalues	valuesfuns	function, bytelist → javavalues
mkjavavalues	valuesfuns	function, references → javavalues
mklist	javatypes	function, javatype × nat → javatypes
mklist	javavalues	function, javavalue × nat → javavalues
mklist	valuetypes	function, valuetype × nat → valuetypes
mklist	refkeyvalues	function, refkeyvalue × nat → refkeyvalues
mklist	fieldinit	function, fieldvalue × nat → fieldinits
mklist	references	function, reference × nat → references
mklist	storekeys	function, storekey × nat → storekeys
mklist	classnames	function, classname × nat → classnames
mklist	bytelist	function, byte × nat → bytelist
mklist	bitlista	function, bool × nat → bitlist
mklist	assoclista	function, pair × nat → assoclist
mklist	intlista	function, int × nat → intlist
mklist	list-last	function, elem × nat → list
mktype_from_dims	typefuns	function, javatype × int → javatype
n	nat-basic1	variable, nat
n0	nat-basic1	variable, nat
n1	nat-basic1	variable, nat
nat	nat-basic1	sort,
newref	storefuns	predicate, reference × store
newref	storefuns	function, store → reference
newref_list	storefuns	function, nat × store → references
next	reference	function, reference → reference
noiniterror	storefunsx	predicate, classnameset × store
normalmode	storefuns	predicate, store
nouninit	storefunsx	predicate, classnameset × store
noval	javavalue	constant, javavalue
n→i	intnat	function, nat → int
odd	int-min	predicate, int
okValues	okfuns	predicate, reference × fieldinits × store
okarray	okfuns	predicate, reference × javatype × store
okarray	okfuns	predicate, javavalue × javatype × int × store
okarrays	okfuns	predicate, reference × fieldinits × store
okarraytype	okfuns	predicate, javavalue × javatype × store
okbytearray	okfuns	predicate, reference × store
okclass	okfuns	predicate, javavalue × classname × store
okfieldinits	addfuns	predicate, classname × fieldinits
okprimtype	valuefuns	predicate, javavalue × javatype
okreftype	okfuns	predicate, javavalue × javatype × store
okstatfields	addfuns	predicate, classname × store
okstore	okfuns	predicate, store
oksubtype	okfuns	predicate, javavalue × classname × store
oktype	okfuns	predicate, javavalue × javatype × store
okval	valuefuns	predicate, javavalue × javatype
onlyModified	storefunsx	predicate, reference × store × store
onlyModified	storefunsx	predicate, references × store × store
ordered<	references	predicate, references
ordered<	classnames	predicate, classnames
ordered<	intlista	predicate, intlist
ordered<	olist	predicate, list
ordered≤	references	predicate, references
ordered≤	classnames	predicate, classnames
ordered≤	intlista	predicate, intlist
ordered≤	olist	predicate, list
p	pair	variable, pair
p0	pair	variable, pair
p1	pair	variable, pair
p2	pair	variable, pair
pair	pair	sort,
path∃	cyclic	predicate, string × reference × reference × store
path∃+	cyclic	predicate, string × reference × reference × store
perm	javatypes	predicate, javatypes × javatypes
perm	javavalues	predicate, javavalues × javavalues
perm	valuetypes	predicate, valuetypes × valuetypes
perm	refkeyvalues	predicate, refkeyvalues × refkeyvalues
perm	fieldinit	predicate, fieldinits × fieldinits
perm	references	predicate, references × references
perm	storekeys	predicate, storekeys × storekeys
perm	classnames	predicate, classnames × classnames
perm	bytelist	predicate, bytelist × bytelist
perm	bitlista	predicate, bitlist × bitlist
perm	assoclista	predicate, assoclist × assoclist
perm	intlista	predicate, intlist × intlist
perm	list-perm	predicate, list × list
pos	javatypes	function, javatype × javatypes → nat
pos	javavalues	function, javavalue × javavalues → nat
pos	valuetypes	function, valuetype × valuetypes → nat
pos	refkeyvalues	function, refkeyvalue × refkeyvalues → nat
pos	fieldinit	function, fieldvalue × fieldinits → nat
pos	references	function, reference × references → nat
pos	storekeys	function, storekey × storekeys → nat
pos	classnames	function, classname × classnames → nat
pos	string-less	function, char × string → nat
pos	bytelist	function, byte × bytelist → nat
pos	bitlista	function, bool × bitlist → nat
pos	assoclista	function, pair × assoclist → nat
pos	intlista	function, int × intlist → nat
pos	list-del	function, elem × list → nat
posints	valuesfuns	predicate, intlist
posints	valuesfuns	predicate, javavalue
posints	valuesfuns	predicate, javavalues
predef_superClass	predefined	function, classname → classname
predef_supers	predefined	function, classname → classnames
predefined_classes	predefined	constant, classnames
ps=	pointers	predicate, reference × store × reference × store
putArray	storearrays	function, javavalues × reference × store → store
putArray	storearrays	function, javavalues × reference × int × store → store
putByteArray	storearrays	function, bytelist × reference × store → store
putByteArray	storearrays	function, bytelist × reference × int × store → store
r	reference	variable, reference
r0	reference	variable, reference
r1	reference	variable, reference
r2	reference	variable, reference
reference	reference	sort,
references	references	sort,
referenceset	references	sort,
referencesset	reflistset	sort,
refkey	refkey	sort,
refkeykeys	refkeykeys	sort,
refkeys	javastore	sort,
refkeyvalue	refkeyvalues	sort,
refkeyvalues	refkeyvalues	sort,
refp	valuefuns	predicate, javavalue
refs	references	variable, references
refs0	references	variable, references
refs1	references	variable, references
refs10	references	variable, references
refs2	references	variable, references
refs3	references	variable, references
refs4	references	variable, references
refs5	references	variable, references
refs6	references	variable, references
refs7	references	variable, references
refs8	references	variable, references
refs9	references	variable, references
refsset	reflistset	variable, referencesset
refsset0	reflistset	variable, referencesset
refsset1	reflistset	variable, referencesset
refsset2	reflistset	variable, referencesset
reftypep	storefunsx	predicate, javavalue × store
refval	javavalue	function, reference → javavalue
restn	javatypes	function, nat × javatypes → javatypes
restn	javavalues	function, nat × javavalues → javavalues
restn	valuetypes	function, nat × valuetypes → valuetypes
restn	refkeyvalues	function, nat × refkeyvalues → refkeyvalues
restn	fieldinit	function, nat × fieldinits → fieldinits
restn	references	function, nat × references → references
restn	storekeys	function, nat × storekeys → storekeys
restn	classnames	function, nat × classnames → classnames
restn	bytelist	function, nat × bytelist → bytelist
restn	bitlista	function, nat × bitlist → bitlist
restn	assoclista	function, nat × assoclist → assoclist
restn	intlista	function, nat × intlist → intlist
restn	list-del	function, nat × list → list
return	javavalue	function, javavalue × javatype → javavalue
rev	javatypes	function, javatypes → javatypes
rev	javavalues	function, javavalues → javavalues
rev	valuetypes	function, valuetypes → valuetypes
rev	refkeyvalues	function, refkeyvalues → refkeyvalues
rev	fieldinit	function, fieldinits → fieldinits
rev	references	function, references → references
rev	storekeys	function, storekeys → storekeys
rev	classnames	function, classnames → classnames
rev	bytelist	function, bytelist → bytelist
rev	bitlista	function, bitlist → bitlist
rev	assoclista	function, assoclist → assoclist
rev	intlista	function, intlist → intlist
rev	list-last	function, list → list
rk	refkey	variable, refkey
rk0	refkey	variable, refkey
rk1	refkey	variable, refkey
rk2	refkey	variable, refkey
rkks	refkeykeys	variable, refkeykeys
rkks0	refkeykeys	variable, refkeykeys
rkks1	refkeykeys	variable, refkeykeys
rkks2	refkeykeys	variable, refkeykeys
rks	javastore	variable, refkeys
rks0	javastore	variable, refkeys
rks1	javastore	variable, refkeys
rks2	javastore	variable, refkeys
rkv	refkeyvalues	variable, refkeyvalue
rkv0	refkeyvalues	variable, refkeyvalue
rkv1	refkeyvalues	variable, refkeyvalue
rkv2	refkeyvalues	variable, refkeyvalue
rkvs	refkeyvalues	variable, refkeyvalues
rkvs0	refkeyvalues	variable, refkeyvalues
rkvs1	refkeyvalues	variable, refkeyvalues
rkvs10	refkeyvalues	variable, refkeyvalues
rkvs2	refkeyvalues	variable, refkeyvalues
rkvs3	refkeyvalues	variable, refkeyvalues
rkvs4	refkeyvalues	variable, refkeyvalues
rkvs5	refkeyvalues	variable, refkeyvalues
rkvs6	refkeyvalues	variable, refkeyvalues
rkvs7	refkeyvalues	variable, refkeyvalues
rkvs8	refkeyvalues	variable, refkeyvalues
rkvs9	refkeyvalues	variable, refkeyvalues
rmdup	javatypes	function, javatypes → javatypes
rmdup	javavalues	function, javavalues → javavalues
rmdup	valuetypes	function, valuetypes → valuetypes
rmdup	refkeyvalues	function, refkeyvalues → refkeyvalues
rmdup	fieldinit	function, fieldinits → fieldinits
rmdup	references	function, references → references
rmdup	storekeys	function, storekeys → storekeys
rmdup	classnames	function, classnames → classnames
rmdup	bytelist	function, bytelist → bytelist
rmdup	bitlista	function, bitlist → bitlist
rmdup	assoclista	function, assoclist → assoclist
rmdup	intlista	function, intlist → intlist
rmdup	list-dup	function, list → list
rset	references	variable, referenceset
rset0	references	variable, referenceset
rset1	references	variable, referenceset
rset2	references	variable, referenceset
s	set-basic	variable, set
s0	set-basic	variable, set
s1	set-basic	variable, set
s2	set-basic	variable, set
s2b	byte	function, short → byte
s2bi	byte	function, short → bint
s2i	byte	function, short → int
same-subclasses	junkrefs	predicate, classname × string × string
same-subclasses-contains	contains	predicate, classname × string × string
set	set-basic	sort,
set2list	references	function, referenceset → references
set2list	classnames	function, classnameset → classnames
set2list	setlist	function, set → list
sgn	bitopsaux	function, bitlist → bitlist
sgn	int-min	function, int → int
shiftright	valuefuns	function, javavalue → javavalue
sho	byte	variable, short
sho0	javavalue	variable, short
shoi	byte	variable, short
shoj	byte	variable, short
short	byte	sort,
shortOverflow	byte	predicate, int
short_type	javatype	constant, javatype
shortval	javavalue	function, short → javavalue
sk	storekey	variable, storekey
sk0	storekey	variable, storekey
sk1	storekey	variable, storekey
sk2	storekeys	variable, storekey
sks	storekeys	variable, storekeys
sks0	storekeys	variable, storekeys
sks1	storekeys	variable, storekeys
sks10	storekeys	variable, storekeys
sks2	storekeys	variable, storekeys
sks3	storekeys	variable, storekeys
sks4	storekeys	variable, storekeys
sks5	storekeys	variable, storekeys
sks6	storekeys	variable, storekeys
sks7	storekeys	variable, storekeys
sks8	storekeys	variable, storekeys
sks9	storekeys	variable, storekeys
sort	intlista	function, intlist → intlist
sort	olist-sort	function, list → list
sortedchars	string-less	constant, string
sqrt	int-square	function, int → int
st	store	variable, store
st0	store	variable, store
st1	store	variable, store
st2	store	variable, store
statfields	addfuns	function, classname → storekeys
step∃	cyclic	predicate, string × reference × reference × store
store	store	sort,
storekey	storekey	sort,
storekeys	storekeys	sort,
str	string-data	variable, string
str0	string-data	variable, string
str1	string-data	variable, string
str2	string-data	variable, string
str3	string-data	variable, string
string	string-data	sort,
stringval	javavalue	function, string → javavalue
stringvar	string-append	variable, string
stringvar0	string-append	variable, string
sublist	javatypes	function, nat × nat × javatypes → javatypes
sublist	javavalues	function, nat × nat × javavalues → javavalues
sublist	valuetypes	function, nat × nat × valuetypes → valuetypes
sublist	refkeyvalues	function, nat × nat × refkeyvalues → refkeyvalues
sublist	fieldinit	function, nat × nat × fieldinits → fieldinits
sublist	references	function, nat × nat × references → references
sublist	storekeys	function, nat × nat × storekeys → storekeys
sublist	classnames	function, nat × nat × classnames → classnames
sublist	bytelist	function, nat × nat × bytelist → bytelist
sublist	bitlista	function, nat × nat × bitlist → bitlist
sublist	assoclista	function, nat × nat × assoclist → assoclist
sublist	intlista	function, nat × nat × intlist → intlist
sublist	list-del	function, nat × nat × list → list
s→r	valuefuns	function, string → reference
tdname+∃	typefuns	predicate, string × classname
tdname∃	typefuns	predicate, string × classname
this	reference	variable, reference
throw	javavalue	function, reference × javatype → javavalue
ty	javatype	variable, javatype
ty0	javatype	variable, javatype
ty1	javatype	variable, javatype
ty2	javatype	variable, javatype
type4value	valuefuns	function, javavalue → javatype
typeof	storefunsx	predicate, reference × javatype × store
typeval	javavalue	function, javatype → javavalue
type∃	typefuns	predicate, string × javatype
tys	javatypes	variable, javatypes
tys0	javatypes	variable, javatypes
tys1	javatypes	variable, javatypes
tys10	javatypes	variable, javatypes
tys2	javatypes	variable, javatypes
tys3	javatypes	variable, javatypes
tys4	javatypes	variable, javatypes
tys5	javatypes	variable, javatypes
tys6	javatypes	variable, javatypes
tys7	javatypes	variable, javatypes
tys8	javatypes	variable, javatypes
tys9	javatypes	variable, javatypes
ub2i	byte	function, byte → int
uint2bits	int2bits	function, int → bitlist
unchanged	pointers	predicate, string × reference × store × store
unchangedNorec	pointers	predicate, reference × store × store
undone	initstate	constant, initstate
uninit	storefunsx	predicate, classnameset × store
uninit	storefuns	predicate, store
uninit	storefuns	predicate, string × store
unique_al	refkeyvalues	predicate, refkeyvalues
unique_al	fieldinit	predicate, fieldinits
unique_al	assoclist	predicate, assoclist
update	okfuns	function, reference × fieldinits × store → store
us2i	byte	function, short → int
val	javavalue	variable, javavalue
val0	javavalue	variable, javavalue
val1	javavalue	variable, javavalue
val2	javavalue	variable, javavalue
val2int	valuefuns	function, javavalue → int
val2vals	valuesfuns	function, javavalue → javavalues
validFieldValue	okfuns	predicate, reference × storekey × store
validFieldValues	okfuns	predicate, reference × storekeys × store
validFields	okfuns	predicate, reference × fieldinits × store
validfield	junkrefs	predicate, string × reference × storekey × store
validfieldinits	junkrefs	predicate, string × fieldinits × store
validfieldinits	addfuns	predicate, fieldinits × store
validfieldlist	junkrefs	predicate, string × reference × storekeys × store
validmode	junkrefs	predicate, string × store
validmode	junkrefs	predicate, string × javavalue × store
validref	junkrefs	predicate, string × reference × javatype × store
validrefkeynotnull	junkrefs	predicate, string × refkey × javatype × store
validreflist	junkrefs	predicate, string × javavalues × javatype × store
validrefnotnull	junkrefs	predicate, string × reference × javatype × store
validrefs	cyclic	predicate, string × references × javatype × store
validrefset	pointers	function, string × reference × store → referencesset
validrefval	junkrefs	predicate, string × javavalue × javatype × store
validrefvalnotnull	junkrefs	predicate, string × javavalue × javatype × store
validstatfield	junkrefs	predicate, string × storekey × store
validstatfields	junkrefs	predicate, string × store
validstatfields	junkrefs	predicate, string × classname × store
validstatfields	junkrefs	predicate, string × storekeys × store
validval	junkrefs	predicate, string × javavalue × javatype × store
validval	junkrefs	predicate, string × refkey × javavalue × store
validvals	junkrefs	predicate, string × refkeyvalues × store
valid⊆	junkrefs	predicate, string × store × store
vals	javavalues	variable, javavalues
vals0	javavalues	variable, javavalues
vals1	javavalues	variable, javavalues
vals10	javavalues	variable, javavalues
vals2	javavalues	variable, javavalues
vals2ints	valuesfuns	function, javavalues → intlist
vals2val	valuesfuns	function, javavalues → javavalue
vals3	javavalues	variable, javavalues
vals4	javavalues	variable, javavalues
vals5	javavalues	variable, javavalues
vals6	javavalues	variable, javavalues
vals7	javavalues	variable, javavalues
vals8	javavalues	variable, javavalues
vals9	javavalues	variable, javavalues
valuetype	value+type	sort,
valuetypes	valuetypes	sort,
void_type	javatype	constant, javatype
vt	value+type	variable, valuetype
vt0	value+type	variable, valuetype
vt1	value+type	variable, valuetype
vt2	value+type	variable, valuetype
vts	valuetypes	variable, valuetypes
vts0	valuetypes	variable, valuetypes
vts1	valuetypes	variable, valuetypes
vts10	valuetypes	variable, valuetypes
vts2	valuetypes	variable, valuetypes
vts3	valuetypes	variable, valuetypes
vts4	valuetypes	variable, valuetypes
vts5	valuetypes	variable, valuetypes
vts6	valuetypes	variable, valuetypes
vts7	valuetypes	variable, valuetypes
vts8	valuetypes	variable, valuetypes
vts9	valuetypes	variable, valuetypes
x	list-data	variable, list
x0	list-data	variable, list
x1	list-data	variable, list
x2	list-data	variable, list
y	list-data	variable, list
y0	list-data	variable, list
y1	list-data	variable, list
y2	list-data	variable, list
z	list-data	variable, list
z0	list-data	variable, list
z1	list-data	variable, list
z2	list-data	variable, list
}	reflistset	function, references → referencesset
}	javastore	function, refkey → refkeys
}	references	function, reference → referenceset
}	classnames	function, classname → classnameset
}	set-union	function, elem → set
~	int-abs	function, int → int
≤	typefuns	predicate, javatype × javatype
≤	classnamefuns	predicate, classname × classname
≤	int-abs	predicate, int × int
≤	nat	predicate, nat × nat
≥	int-abs	predicate, int × int
≥	nat	predicate, nat × nat
∈	javatypes	predicate, javatype × javatypes
∈	reflistset	predicate, references × referencesset
∈	okfuns	predicate, fieldinits × store
∈	javavalues	predicate, javavalue × javavalues
∈	valuetypes	predicate, valuetype × valuetypes
∈	storefuns	predicate, reference × store
∈	storefuns	predicate, refkeykeys × store
∈	refkeyvalues	predicate, refkeyvalue × refkeyvalues
∈	refkeyvalues	predicate, refkey × refkeyvalues
∈	javastore	predicate, refkey × refkeys
∈	javastore	predicate, refkey × store
∈	store	predicate, elem × store
∈	store	predicate, elemdata × store
∈	fieldinit	predicate, fieldvalue × fieldinits
∈	fieldinit	predicate, storekey × fieldinits
∈	valuefuns	predicate, reference × javavalue
∈	references	predicate, reference × references
∈	references	predicate, reference × referenceset
∈	storekeys	predicate, storekey × storekeys
∈	classnames	predicate, classname × classnames
∈	classnames	predicate, classname × classnameset
∈	set-basic	predicate, elem × set
∈	bytelist	predicate, byte × bytelist
∈	bitlista	predicate, bool × bitlist
∈	assoclist	predicate, elem × assoclist
∈	assoclista	predicate, pair × assoclist
∈	intlista	predicate, int × intlist
∈	list	predicate, elem × list
∈bint	byte	predicate, int
∈byte	byte	predicate, int
∈long	byte	predicate, int
∈short	byte	predicate, int
∪	javatypes	function, javatypes × javatypes → javatypes
∪	reflistset	function, referencesset × referencesset → referencesset
∪	javavalues	function, javavalues × javavalues → javavalues
∪	valuetypes	function, valuetypes × valuetypes → valuetypes
∪	storefunsx	function, store × store → store
∪	refkeyvalues	function, refkeyvalues × refkeyvalues → refkeyvalues
∪	javastore	function, refkeys × refkeys → refkeys
∪	fieldinit	function, fieldinits × fieldinits → fieldinits
∪	references	function, references × references → references
∪	references	function, referenceset × referenceset → referenceset
∪	storekeys	function, storekeys × storekeys → storekeys
∪	classnames	function, classnames × classnames → classnames
∪	classnames	function, classnameset × classnameset → classnameset
∪	set-union	function, set × set → set
∪	bytelist	function, bytelist × bytelist → bytelist
∪	bitlista	function, bitlist × bitlist → bitlist
∪	assoclista	function, assoclist × assoclist → assoclist
∪	intlista	function, intlist × intlist → intlist
∪	list-set	function, list × list → list
∩	reflistset	function, referencesset × referencesset → referencesset
∩	javastore	function, refkeys × refkeys → refkeys
∩	references	function, referenceset × referenceset → referenceset
∩	classnames	function, classnameset × classnameset → classnameset
∩	set-union	function, set × set → set
⊆	javatypes	predicate, javatypes × javatypes
⊆	reflistset	predicate, referencesset × referencesset
⊆	javavalues	predicate, javavalues × javavalues
⊆	valuetypes	predicate, valuetypes × valuetypes
⊆	refkeyvalues	predicate, refkeyvalues × refkeyvalues
⊆	javastore	predicate, refkeys × refkeys
⊆	store	predicate, store × store
⊆	fieldinit	predicate, fieldinits × fieldinits
⊆	references	predicate, references × references
⊆	references	predicate, referenceset × referenceset
⊆	storekeys	predicate, storekeys × storekeys
⊆	classnames	predicate, classnames × classnames
⊆	classnames	predicate, classnameset × classnameset
⊆	set-basic	predicate, set × set
⊆	bytelist	predicate, bytelist × bytelist
⊆	bitlista	predicate, bitlist × bitlist
⊆	assoclista	predicate, assoclist × assoclist
⊆	intlista	predicate, intlist × intlist
⊆	list-set	predicate, list × list
⊆m	javatypes	predicate, javatypes × javatypes
⊆m	javavalues	predicate, javavalues × javavalues
⊆m	valuetypes	predicate, valuetypes × valuetypes
⊆m	refkeyvalues	predicate, refkeyvalues × refkeyvalues
⊆m	fieldinit	predicate, fieldinits × fieldinits
⊆m	references	predicate, references × references
⊆m	storekeys	predicate, storekeys × storekeys
⊆m	classnames	predicate, classnames × classnames
⊆m	bytelist	predicate, bytelist × bytelist
⊆m	bitlista	predicate, bitlist × bitlist
⊆m	assoclista	predicate, assoclist × assoclist
⊆m	intlista	predicate, intlist × intlist
⊆m	list-perm	predicate, list × list
Π	intlist	function, intlist → int
Σ	intlist	function, intlist → int
×	value+type	function, javavalue × javatype → valuetype
×	refkeyvalues	function, refkey × javavalue → refkeyvalue
×	javastore	function, refkey × javavalue → elemdata
×	store	function, elem × data → elemdata
×	fieldinit	function, storekey × javavalue → fieldvalue
×	pair	function, elem × data → pair
⊑	javatypes	predicate, javatypes × javatypes
⊑	javavalues	predicate, javavalues × javavalues
⊑	valuetypes	predicate, valuetypes × valuetypes
⊑	refkeyvalues	predicate, refkeyvalues × refkeyvalues
⊑	fieldinit	predicate, fieldinits × fieldinits
⊑	references	predicate, references × references
⊑	storekeys	predicate, storekeys × storekeys
⊑	classnames	predicate, classnames × classnames
⊑	bytelist	predicate, bytelist × bytelist
⊑	bitlista	predicate, bitlist × bitlist
⊑	assoclista	predicate, assoclist × assoclist
⊑	intlista	predicate, intlist × intlist
⊑	list-last	predicate, list × list
⊒	javatypes	predicate, javatypes × javatypes
⊒	javavalues	predicate, javavalues × javavalues
⊒	valuetypes	predicate, valuetypes × valuetypes
⊒	refkeyvalues	predicate, refkeyvalues × refkeyvalues
⊒	fieldinit	predicate, fieldinits × fieldinits
⊒	references	predicate, references × references
⊒	storekeys	predicate, storekeys × storekeys
⊒	classnames	predicate, classnames × classnames
⊒	bytelist	predicate, bytelist × bytelist
⊒	bitlista	predicate, bitlist × bitlist
⊒	assoclista	predicate, assoclist × assoclist
⊒	intlista	predicate, intlist × intlist
⊒	list-last	predicate, list × list
∅	reflistset	constant, referencesset
∅	javastore	constant, refkeys
∅	store	constant, store
∅	references	constant, referenceset
∅	classnames	constant, classnameset
∅	set-basic	constant, set