[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
# .	indexseq	f	ilist → nat
# .	stackseq	f	llist → nat
# .	list-data	f	list → nat
# .	indexseq	f	illist → nat
#oc	indexseq	f	nat × ilist → nat
#oc	list-perm	f	elem × list → nat
. '	stackseq	f	list → llist
. '	indexseq	f	nat → ilist
. '	list	f	elem → list
. '	indexseq	f	ilist → illist
. + .	nat-basic2	f	nat × nat → nat
. + .	stackseq	f	llist × list → llist
. + .	indexseq	f	nat × ilist → ilist
. + .	stackseq	f	llist × llist → llist
. + .	indexseq	f	ilist × ilist → ilist
. + .	stackseq	f	list × llist → llist
. + .	indexseq	f	ilist × nat → ilist
. + .	list	f	elem × elem → list
. + .	indexseq	f	ilist × illist → illist
. + .	list	f	list × elem → list
. + .	indexseq	f	illist × illist → illist
. + .	list	f	list × list → list
. + .	indexseq	f	illist × ilist → illist
. + .	list-data	f	elem × list → list
. ++ .	stackseq	f	llist × list → llist
. ++ .	indexseq	f	ilist × nat → ilist
. ++ .	list-dup	f	list × elem → list
. ++ .	indexseq	f	illist × ilist → illist
. +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 .	indexseq	f	ilist × nat → ilist
. -1l .	list-del	f	list × elem → list
. -1l .	indexseq	f	illist × nat → illist
. -1l .	indexseq	f	illist × ilist → illist
. -1p .	indexseq	f	ilist × nat → ilist
. -l .	indexseq	f	ilist × nat → ilist
. -l .	stackseq	f	llist × list → llist
. -l .	indexseq	f	illist × ilist → illist
. -l .	list-del	f	list × elem → list
. .butlast	indexseq	f	ilist → ilist
. .butlast	stackseq	f	llist → llist
. .butlast	indexseq	f	illist → illist
. .butlast	list-last	f	list → list
. .first	indexseq	f	ilist → nat
. .first	indexseq	f	illist → ilist
. .first	stackseq	f	llist → list
. .first	list-data	f	list → elem
. .last	stackseq	f	llist → list
. .last	indexseq	f	ilist → nat
. .last	list-last	f	list → elem
. .last	indexseq	f	illist → ilist
. .rest	indexseq	f	ilist → ilist
. .rest	indexseq	f	illist → illist
. .rest	stackseq	f	llist → llist
. .rest	list-data	f	list → list
. .tolist .	solitaire	f	ilist × list → list
. .tolist .	solitaire	f	illist × list → llist
. < .	stackseq	p	llist × llist
. < .	list-data	p	list × list
. < .	nat-basic1	p	nat × nat
. < .	oelem	p	elem × elem
. < .	indexseq	p	illist × illist
. < .	indexseq	p	ilist × ilist
. > .	nat	p	nat × nat
. [ . ]	indexseq	f	ilist × nat → nat
. [ . ]	stackseq	f	llist × nat × list → llist
. [ . ]	indexseq	f	ilist × nat × nat → ilist
. [ . ]	stackseq	f	llist × nat → list
. [ . ]	list-del	f	list × nat × elem → list
. [ . ]	indexseq	f	illist × nat → ilist
. [ . ]	list-del	f	list × nat → elem
. [ . ]	indexseq	f	illist × nat × ilist → illist
. \ .	indexseq	f	ilist × ilist → ilist
. \ .	list-set	f	list × list → list
. ∈ .	stackseq	p	list × llist
. ∈ .	list	p	elem × list
. ∈ .	indexseq	p	nat × ilist
. ∈ .	indexseq	p	ilist × illist
. ∪ .	indexseq	f	ilist × ilist → ilist
. ∪ .	list-set	f	list × list → list
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	list-set	p	list × list
. ⊆ .	indexseq	p	ilist × ilist
. ⊆m .	list-perm	p	list × list
. ⊆m .	indexseq	p	ilist × ilist
. ⊑ .	stackseq	p	llist × llist
. ⊑ .	indexseq	p	ilist × ilist
. ⊑ .	list-last	p	list × list
. ⊑ .	indexseq	p	illist × illist
. ⊒ .	stackseq	p	llist × llist
. ⊒ .	list-last	p	list × list
. ⊒ .	indexseq	p	ilist × ilist
. ⊒ .	indexseq	p	illist × illist
. plus .	indexseq	f	nat × nat → ilist
. plus .	stackseq	f	list × list → llist
. plus .	indexseq	f	ilist × ilist → illist
[]	indexseq	c	ilist
[]	indexseq	c	illist
[]	stackseq	c	llist
[]	list-data	c	list
a	elem	v	elem
a0	list-data	v	elem
all<	solitaire	p	ilist × nat
ascsubseq	solitaire	p	ilist × list
b	elem	v	elem
butlastn	indexseq	f	nat × ilist → ilist
butlastn	stackseq	f	nat × llist → llist
butlastn	indexseq	f	nat × illist → illist
butlastn	list-last	f	nat × list → list
c	elem	v	elem
covers	solitaire	p	illist × ilist
covers	solitaire	p	illist × nat
disj	indexseq	p	ilist × ilist
disj	stackseq	p	llist × llist
disj	indexseq	p	illist × illist
disj	list-dup	p	list × list
dups	indexseq	p	ilist
dups	stackseq	p	llist
dups	indexseq	p	illist
dups	list-dup	p	list
elem	elem	s
fillfirst	indexseq	f	nat × nat × ilist → ilist
fillfirst	stackseq	f	nat × list × llist → llist
fillfirst	indexseq	f	nat × ilist × illist → illist
fillfirst	list-last	f	nat × elem × list → list
filter	indexseq	f	ilist × ilist → ilist
filter	list-set	f	list × list → list
firstn	stackseq	f	nat × llist → llist
firstn	indexseq	f	nat × ilist → ilist
firstn	list-del	f	nat × list → list
firstn	indexseq	f	nat × illist → illist
frome	stackseq	f	llist × list → llist
frome	indexseq	f	ilist × nat → ilist
frome	list-del	f	list × elem → list
frome	indexseq	f	illist × ilist → illist
ilist	indexseq	s
illist	indexseq	s
ins≤	indexseq	f	nat × ilist → ilist
ins≤	olist	f	elem × list → list
inv	solitaire	p	illist × nat
ix	indexseq	v	ilist
ix0	indexseq	v	ilist
ix1	indexseq	v	ilist
ix10	indexseq	v	ilist
ix2	indexseq	v	ilist
ix3	indexseq	v	ilist
ix4	indexseq	v	ilist
ix5	indexseq	v	ilist
ix6	indexseq	v	ilist
ix7	indexseq	v	ilist
ix8	indexseq	v	ilist
ix9	indexseq	v	ilist
ixs	indexseq	v	illist
ixs0	indexseq	v	illist
ixs1	indexseq	v	illist
ixs10	indexseq	v	illist
ixs2	indexseq	v	illist
ixs3	indexseq	v	illist
ixs4	indexseq	v	illist
ixs5	indexseq	v	illist
ixs6	indexseq	v	illist
ixs7	indexseq	v	illist
ixs8	indexseq	v	illist
ixs9	indexseq	v	illist
lastn	indexseq	f	nat × ilist → ilist
lastn	stackseq	f	nat × llist → llist
lastn	indexseq	f	nat × illist → illist
lastn	list-del	f	nat × list → list
list	list-data	s
llist	stackseq	s
m	nat-basic2	v	nat
maxincseq#	solitaire	f	list → nat
merge	indexseq	f	ilist × ilist → ilist
merge	olist	f	list × list → list
mklist	indexseq	f	nat × nat → ilist
mklist	indexseq	f	ilist × nat → illist
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
n3	indexseq	v	nat
n4	indexseq	v	nat
n5	indexseq	v	nat
n6	indexseq	v	nat
nat	nat-basic1	s
ordered	solitaire	p	illist × list
ordered	solitaire	p	ilist × list
ordered<	olist	p	list
ordered<	indexseq	p	ilist
ordered≤	olist	p	list
ordered≤	indexseq	p	ilist
perm	indexseq	p	ilist × ilist
perm	list-perm	p	list × list
pos	indexseq	f	nat × ilist → nat
pos	indexseq	f	ilist × illist → nat
pos	list-del	f	elem × list → nat
pos	stackseq	f	list × llist → nat
precedes	solitaire	p	nat × nat × list
precedes∃	solitaire	p	illist × list
push	solitaire	f	elem × llist → llist
pushx	solitaire	f	nat × illist × list → illist
restn	indexseq	f	nat × ilist → ilist
restn	stackseq	f	nat × llist → llist
restn	indexseq	f	nat × illist → illist
restn	list-del	f	nat × list → list
rev	indexseq	f	ilist → ilist
rev	stackseq	f	llist → llist
rev	indexseq	f	illist → illist
rev	list-last	f	list → list
rmdup	indexseq	f	ilist → ilist
rmdup	indexseq	f	illist → illist
rmdup	list-dup	f	list → list
rmdup	stackseq	f	llist → llist
solitaire	solitaire	f	list → llist
solitaireh	solitaire	f	list × llist → llist
solix	solitaire	f	list → illist
solixh	solitaire	f	list × nat × illist → illist
sublist	indexseq	f	nat × nat × ilist → ilist
sublist	indexseq	f	nat × nat × illist → illist
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