[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
# .	bag-union	f	bag → nat
# .	array	f	array → nat
. + .	array-splice	f	array × array → array
. + .	nat-basic2	f	nat × nat → nat
. ++ .	bag-basic	f	bag × elem → bag
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -- .	bag-union	f	bag × elem → bag
. -1	nat-basic1	f	nat → nat
. .elems	bag-array	f	array → bag
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	array	f	array × nat × elem → array
. [ . ]	array	f	array × nat → elem
. \ .	bag-union	f	bag × bag → bag
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ∈ .	array-copy	p	elem × array
. ∈ .	bag-union	p	elem × bag
. ∪ .	bag-union	f	bag × bag → bag
. ⊆ .	bag-union	p	bag × bag
. elems .	bag-array	f	array × nat → bag
{ . }	bag-union	f	elem → bag
∅	bag-basic	c	bag
a	elem	v	elem
ar	array	v	array
ar0	array	v	array
ar1	array	v	array
ar2	array	v	array
array	array	s
b	elem	v	elem
bag	bag-basic	s
bag	bag-basic	v	bag
bag0	bag-basic	v	bag
bag1	bag-basic	v	bag
bag2	bag-basic	v	bag
c	elem	v	elem
cmp	array-copy	p	array × elem × nat × nat
cmp	array-copy	p	array × nat × array × nat × nat
copy	array-copy	f	array × nat × array × nat × nat → array
count	bag-basic	f	elem × bag → nat
elem	elem	s
empty	array-splice	c	elem
fill	array-copy	f	array × elem × nat × nat → array
fill	array-copy	f	array × elem → array
id○	array-copy	p	array × array × nat
idrange	array-copy	p	array × nat × nat
m	nat-basic2	v	nat
m0	array-copy	v	nat
max	min-max	f	nat × nat → nat
min	min-max	f	nat × nat → nat
mkarray	array	f	nat → array
mkemparray	array-splice	f	nat → array
mkzarray	array-splice	f	nat → array
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
pos	array-copy	f	array × elem → nat
range=	array-splice	p	array × nat × array × nat × nat
resize	array-splice	f	array × nat → array
splice	array-splice	f	array × nat × array × nat × nat → array
subarray	array-copy	f	array × nat × nat → array
zero	array-splice	c	elem