[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
# .	list-data	f	list → nat
# .	stackseq	f	llist → nat
#oc	list-perm	f	elem × list → nat
. '	stackseq	f	list → llist
. '	list	f	elem → list
. + .	nat-basic2	f	nat × nat → nat
. + .	stackseq	f	llist × list → llist
. + .	list-data	f	elem × list → list
. + .	stackseq	f	llist × llist → llist
. + .	list	f	list × list → list
. + .	stackseq	f	list × llist → llist
. + .	list	f	list × elem → list
. + .	list	f	elem × elem → list
. ++ .	stackseq	f	llist × list → llist
. ++ .	list-dup	f	list × elem → list
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -1	nat-basic1	f	nat → nat
. -1l .	stackseq	f	llist × nat → llist
. -1l .	stackseq	f	llist × list → llist
. -1l .	list-del	f	list × nat → list
. -1l .	list-del	f	list × elem → list
. -l .	list-del	f	list × elem → list
. -l .	stackseq	f	llist × list → llist
. .butlast	list-last	f	list → list
. .butlast	stackseq	f	llist → llist
. .first	list-data	f	list → elem
. .first	stackseq	f	llist → list
. .last	stackseq	f	llist → list
. .last	list-last	f	list → elem
. .rest	list-data	f	list → list
. .rest	stackseq	f	llist → llist
. < .	stackseq	p	llist × llist
. < .	list-data	p	list × list
. < .	oelem	p	elem × elem
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	list-del	f	list × nat → elem
. [ . ]	stackseq	f	llist × nat × list → llist
. [ . ]	list-del	f	list × nat × elem → list
. [ . ]	stackseq	f	llist × nat → list
. \ .	list-set	f	list × list → list
. ∈ .	stackseq	p	list × llist
. ∈ .	list	p	elem × list
. ∪ .	list-set	f	list × list → list
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	list-set	p	list × list
. ⊆m .	list-perm	p	list × list
. ⊑ .	stackseq	p	llist × llist
. ⊑ .	list-last	p	list × list
. ⊒ .	stackseq	p	llist × llist
. ⊒ .	list-last	p	list × list
. plus .	stackseq	f	list × list → llist
[]	list-data	c	list
[]	stackseq	c	llist
a	elem	v	elem
a0	list-data	v	elem
b	elem	v	elem
butlastn	list-last	f	nat × list → list
butlastn	stackseq	f	nat × llist → llist
c	elem	v	elem
disj	stackseq	p	llist × llist
disj	list-dup	p	list × list
dups	list-dup	p	list
dups	stackseq	p	llist
elem	elem	s
fillfirst	list-last	f	nat × elem × list → list
fillfirst	stackseq	f	nat × list × llist → llist
filter	list-set	f	list × list → list
firstn	stackseq	f	nat × llist → llist
firstn	list-del	f	nat × list → list
frome	stackseq	f	llist × list → llist
frome	list-del	f	list × elem → list
ins≤	olist	f	elem × list → list
lastn	list-del	f	nat × list → list
lastn	stackseq	f	nat × llist → llist
list	list-data	s
llist	stackseq	s
m	nat-basic2	v	nat
merge	olist	f	list × list → list
mklist	list-last	f	elem × nat → list
mklist	stackseq	f	list × nat → llist
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
ordered<	olist	p	list
ordered≤	olist	p	list
perm	list-perm	p	list × list
pos	list-del	f	elem × list → nat
pos	stackseq	f	list × llist → nat
restn	stackseq	f	nat × llist → llist
restn	list-del	f	nat × list → list
rev	list-last	f	list → list
rev	stackseq	f	llist → llist
rmdup	list-dup	f	list → list
rmdup	stackseq	f	llist → llist
sublist	list-del	f	nat × nat × list → list
sublist	stackseq	f	nat × nat × llist → llist
x	list-data	v	list
x0	list-data	v	list
x1	list-data	v	list
x2	list-data	v	list
xs	stackseq	v	llist
xs0	stackseq	v	llist
xs1	stackseq	v	llist
xs10	stackseq	v	llist
xs2	stackseq	v	llist
xs3	stackseq	v	llist
xs4	stackseq	v	llist
xs5	stackseq	v	llist
xs6	stackseq	v	llist
xs7	stackseq	v	llist
xs8	stackseq	v	llist
xs9	stackseq	v	llist
y	list-data	v	list
y0	list-data	v	list
y1	list-data	v	list
y2	list-data	v	list
z	list-data	v	list
z0	list-data	v	list
z1	list-data	v	list
z2	list-data	v	list