[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
# .	string-less	f	string → nat
# .	javatypes	f	javatypes → nat
# .	classnames	f	classnames → nat
# .	classnames	f	classnameset → nat
#oc	javatypes	f	javatype × javatypes → nat
#oc	classnames	f	classname × classnames → nat
. % .	int-div	f	int × int → int
. % .	nat-div	f	nat × nat → nat
. '	string-append	f	char → string
. '	javatypes	f	javatype → javatypes
. '	classnames	f	classname → classnames
. * .	int-mult	f	int × int → int
. * .	nat-mult	f	nat × nat → nat
. + .	string-data	f	char × string → string
. + .	string-append	f	string × string → string
. + .	nat-basic2	f	nat × nat → nat
. + .	javatypes	f	javatype × javatype → javatypes
. + .	int-basic2	f	int × int → int
. + .	javatypes	f	javatypes × javatype → javatypes
. + .	classnames	f	classname × classnames → classnames
. + .	javatypes	f	javatypes × javatypes → javatypes
. + .	classnames	f	classnames × classnames → classnames
. + .	javatypes	f	javatype × javatypes → javatypes
. + .	classnames	f	classnames × classname → classnames
. + .	classnames	f	classname × classname → classnames
. ++ .	javatypes	f	javatypes × javatype → javatypes
. ++ .	classnames	f	classnameset × classname → classnameset
. ++ .	classnames	f	classnames × classname → classnames
. +1	nat-basic1	f	nat → nat
. +1	int-basic1	f	int → int
. - .	nat	f	nat × nat → nat
. - .	int-abs	f	int × int → int
. -- .	classnames	f	classnameset × classname → classnameset
. -1	nat-basic1	f	nat → nat
. -1	int-basic1	f	int → int
. -1l .	javatypes	f	javatypes × nat → javatypes
. -1l .	javatypes	f	javatypes × javatype → javatypes
. -1l .	classnames	f	classnames × nat → classnames
. -1l .	classnames	f	classnames × classname → classnames
. -l .	classnames	f	classnames × classname → classnames
. -l .	javatypes	f	javatypes × javatype → javatypes
. .butlast	classnames	f	classnames → classnames
. .butlast	javatypes	f	javatypes → javatypes
. .butmax	classnames	f	classnameset → classnameset
. .butmin	classnames	f	classnameset → classnameset
. .char1	string-data	f	string → char
. .class	classname	f	string → classname
. .class	classname	f	classname → string
. .class	javatype	f	javatype → classname
. .first	javatypes	f	javatypes → javatype
. .first	classnames	f	classnames → classname
. .jtclass	typefuns	f	javatype → classname
. .jtdims	typefuns	f	javatype → int
. .jtelemtype	typefuns	f	javatype → javatype
. .last	javatypes	f	javatypes → javatype
. .last	classnames	f	classnames → classname
. .max	classnames	f	classnameset → classname
. .min	classnames	f	classnameset → classname
. .rest	classnames	f	classnames → classnames
. .rest	javatypes	f	javatypes → javatypes
. .rstring	string-data	f	string → string
. .type	javatype	f	javatype → javatype
. / .	nat-div	f	nat × nat → nat
. / .	int-div	f	int × int → int
. < .	javatypes	p	javatypes × javatypes
. < .	classnames	p	classnameset × classname
. < .	nat-basic1	p	nat × nat
. < .	classnames	p	classname × classnameset
. < .	classnames	p	classnames × classnames
. < .	string-less	p	string × string
. < .	string-less	p	char × char
. < .	int-basic1	p	int × int
. <_1 .	classnamefuns	p	classname × classname
. > .	nat	p	nat × nat
. > .	int-abs	p	int × int
. [ . ]	classnames	f	classnames × nat → classname
. [ . ]	classnames	f	classnames × nat × classname → classnames
. [ . ]	javatypes	f	javatypes × nat → javatype
. [ . ]	javatypes	f	javatypes × nat × javatype → javatypes
. \ .	javatypes	f	javatypes × javatypes → javatypes
. \ .	classnames	f	classnames × classnames → classnames
. \ .	classnames	f	classnameset × classnameset → classnameset
. ≤ .	typefuns	p	javatype × javatype
. ≤ .	nat	p	nat × nat
. ≤ .	classnamefuns	p	classname × classname
. ≤ .	int-abs	p	int × int
. ≥ .	nat	p	nat × nat
. ≥ .	int-abs	p	int × int
. ∈ .	javatypes	p	javatype × javatypes
. ∈ .	classnames	p	classname × classnameset
. ∈ .	classnames	p	classname × classnames
. ∪ .	classnames	f	classnames × classnames → classnames
. ∪ .	javatypes	f	javatypes × javatypes → javatypes
. ∪ .	classnames	f	classnameset × classnameset → classnameset
. ∩ .	classnames	f	classnameset × classnameset → classnameset
. ⊆ .	javatypes	p	javatypes × javatypes
. ⊆ .	classnames	p	classnames × classnames
. ⊆ .	classnames	p	classnameset × classnameset
. ⊆m .	javatypes	p	javatypes × javatypes
. ⊆m .	classnames	p	classnames × classnames
. ⊑ .	classnames	p	classnames × classnames
. ⊑ .	javatypes	p	javatypes × javatypes
. ⊒ .	javatypes	p	javatypes × javatypes
. ⊒ .	classnames	p	classnames × classnames
. l< .	classnamefuns	p	classname × classname
[]	classnames	c	classnames
[]	javatypes	c	javatypes
{ . }	classnames	f	classname → classnameset
~ .	int-abs	f	int → int
∅	classnames	c	classnameset
abs	int-abs	f	int → int
abstract_type	javatype	c	javatype
boolean_type	javatype	c	javatype
butlastn	javatypes	f	nat × javatypes → javatypes
butlastn	classnames	f	nat × classnames → classnames
byte_type	javatype	c	javatype
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
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
disj	javatypes	p	javatypes × javatypes
disj	classnames	p	classnames × classnames
double_type	javatype	c	javatype
dups	javatypes	p	javatypes
dups	classnames	p	classnames
fillfirst	classnames	f	nat × classname × classnames → classnames
fillfirst	javatypes	f	nat × javatype × javatypes → javatypes
filter	javatypes	f	javatypes × javatypes → javatypes
filter	classnames	f	classnames × classnames → classnames
firstn	classnames	f	nat × classnames → classnames
firstn	javatypes	f	nat × javatypes → javatypes
float_type	javatype	c	javatype
frome	classnames	f	classnames × classname → classnames
frome	javatypes	f	javatypes × javatype → javatypes
has_classtype	typefuns	p	javatype
i	int-basic1	v	int
i→n	intnat	f	int → nat
i0	int-basic1	v	int
ins≤	classnames	f	classname × classnames → classnames
int	int-basic1	s
int_type	javatype	c	javatype
interface∃	typefuns	p	string × classname
is_abstract	typefuns	p	classname
is_arraytype	javatype	p	javatype
is_classtype	javatype	p	javatype
is_predefined_class	predefined	p	classname
is_primtype	typefuns	p	javatype
is_reftype	typefuns	p	javatype
is_subclass	typefuns	p	classname × classnames × classname
is_subtype	typefuns	p	javatype × classnames × javatype
is_subtype	typefuns	p	string × javatype × javatype
is_subtype	typefuns	p	javatype × javatype × classnameset
is_void_type	javatype	p	javatype
j	int-basic1	v	int
j0	int-basic1	v	int
javatype	javatype	s
javatypes	javatypes	s
lastn	javatypes	f	nat × javatypes → javatypes
lastn	classnames	f	nat × classnames → classnames
list2set	classnames	f	classnames → classnameset
long_type	javatype	c	javatype
m	nat-basic2	v	nat
merge	classnames	f	classnames × classnames → classnames
mkarraytype	javatype	f	javatype → javatype
mkclasstype	javatype	f	classname → javatype
mklist	javatypes	f	javatype × nat → javatypes
mklist	classnames	f	classname × nat → classnames
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
ordered<	classnames	p	classnames
ordered≤	classnames	p	classnames
perm	javatypes	p	javatypes × javatypes
perm	classnames	p	classnames × classnames
pos	javatypes	f	javatype × javatypes → nat
pos	string-less	f	char × string → nat
pos	classnames	f	classname × classnames → nat
predef_superClass	predefined	f	classname → classname
predef_supers	predefined	f	classname → classnames
predefined_classes	predefined	c	classnames
restn	javatypes	f	nat × javatypes → javatypes
restn	classnames	f	nat × classnames → classnames
rev	javatypes	f	javatypes → javatypes
rev	classnames	f	classnames → classnames
rmdup	classnames	f	classnames → classnames
rmdup	javatypes	f	javatypes → javatypes
set2list	classnames	f	classnameset → classnames
short_type	javatype	c	javatype
sortedchars	string-less	c	string
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
stringvar	string-append	v	string
stringvar0	string-append	v	string
sublist	classnames	f	nat × nat × classnames → classnames
sublist	javatypes	f	nat × nat × javatypes → javatypes
tdname+∃	typefuns	p	string × classname
tdname∃	typefuns	p	string × classname
ty	javatype	v	javatype
ty0	javatype	v	javatype
ty1	javatype	v	javatype
ty2	javatype	v	javatype
type∃	typefuns	p	string × javatype
tys	javatypes	v	javatypes
tys0	javatypes	v	javatypes
tys1	javatypes	v	javatypes
tys10	javatypes	v	javatypes
tys2	javatypes	v	javatypes
tys3	javatypes	v	javatypes
tys4	javatypes	v	javatypes
tys5	javatypes	v	javatypes
tys6	javatypes	v	javatypes
tys7	javatypes	v	javatypes
tys8	javatypes	v	javatypes
tys9	javatypes	v	javatypes
void_type	javatype	c	javatype