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

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Signature symbols in this unit

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