[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	f	array × nat × elem → array
. \ .	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
⊑	sorted	v	elem × elem → bool
∅	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
R	order	v	elem × elem → bool
range=	array-splice	p	array × nat × array × nat × nat
reflexive	order	p	(elem × elem → bool)
resize	array-splice	f	array × nat → array
sorted	sorted	p	array × nat × nat × (elem × elem → bool)
sorted	sorted	p	array × (elem × elem → bool)
splice	array-splice	f	array × nat × array × nat × nat → array
subarray	array-copy	f	array × nat × nat → array
total	order	p	(elem × elem → bool)
transitive	order	p	(elem × elem → bool)
zero	array-splice	c	elem