[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
# .	natset	f	natset → nat
# .	matrixops	f	vector → nat
# .	sparsearray	f	sparsearray → nat
# .	sparsearray	f	npset → nat
# .	tidset-npset	f	Tidset → nat
#c .	matrix	f	matrix → nat
#r .	matrix	f	matrix → nat
. * .	ring	f	elem × elem → elem
. * .	matrixops	pf	matrix × matrix → matrix with λ mx1, mx2. #c mx1 = #r mx2
. * .	matrixops	pf	matrix × vector → vector with λ mx, vec. #r mx = # vec
. * .	matrixops	pf	vector × matrix → vector with λ vec, mx. #c mx = # vec
. * .	matrixops	pf	vector × vector → elem with λ vec1, vec2. # vec1 = # vec2
. + .	nat-basic	f	nat × nat → nat
. + .	ring	f	elem × elem → elem
. + .	matrixops	pf	matrix × matrix → matrix with λ mx1, mx2. #r mx1 = #r mx2 ∧ #r mxc = #c mx2
. + .	matrixops	pf	vector × vector → vector with λ vec1, vec2. # vec1 = # vec2
. ++ .	natset	f	natset × nat → natset
. ++ .	sparsearray	f	npset × natpair → npset
. ++ .	tidset-npset	f	Tidset × Tid → Tidset
. +1	nat-basic	f	nat → nat
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	natset	f	natset × nat → natset
. -- .	sparsearray	f	sparsearray × natpair → sparsearray
. -- .	sparsearray	f	npset × natpair → npset
. -- .	tidset-npset	f	Tidset × Tid → Tidset
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. .c	natpair	f	natpair → nat
. .ghostlspmxf	VF3conc	f	VF3concGState → Tid → sparsearray
. .ghostlspmxf:= .	VF3conc	f	VF3concGState × (Tid → sparsearray) → VF3concGState
. .gspmx	VF3conc	f	VF3concGState → sparsearray
. .gspmx:= .	VF3conc	f	VF3concGState × sparsearray → VF3concGState
. .gstate	VF3conc	f	VF3concState → VF3concGState
. .gstate:= .	VF3conc	f	VF3concState × VF3concGState → VF3concState
. .lsf	VF3conc	f	VF3concState → Tid → VF3concLState
. .lsf:= .	VF3conc	f	VF3concState × (Tid → VF3concLState) → VF3concState
. .lspmx	VF3conc	f	VF3concLState → sparsearray
. .lspmx	VF3conc	f	VF3concAction → sparsearray
. .lspmx:= .	VF3conc	f	VF3concLState × sparsearray → VF3concLState
. .np	VF3conc	f	VF3concLState → natpair
. .np	VF3conc	f	VF3concAction → natpair
. .np:= .	VF3conc	f	VF3concLState × natpair → VF3concLState
. .pcf	VF3conc	f	VF3concState → Tid → VF3concPC
. .pcf:= .	VF3conc	f	VF3concState × (Tid → VF3concPC) → VF3concState
. .r	natpair	f	natpair → nat
. .r	VF3conc	f	VF3concGState → nat
. .r:= .	VF3conc	f	VF3concGState × nat → VF3concGState
. .spmx	VF3conc	f	VF3concGState → sparsearray
. .spmx:= .	VF3conc	f	VF3concGState × sparsearray → VF3concGState
. .tid	VF3conc	f	VF3concLState → Tid
. .tid	VF3conc	f	VF3concAction → Tid
. .tid:= .	VF3conc	f	VF3concLState × Tid → VF3concLState
. .toMatrix ( . )	VerifyThis3-sequential	f	sparsearray × nat × nat → matrix
. .val	VF3conc	f	VF3concLState → elem
. .val:= .	VF3conc	f	VF3concLState × elem → VF3concLState
. .x	VF3conc	f	VF3concGState → vector
. .x:= .	VF3conc	f	VF3concGState × vector → VF3concGState
. .y	VF3conc	f	VF3concGState → vector
. .y:= .	VF3conc	f	VF3concGState × vector → VF3concGState
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	sparsearray	f	sparsearray × natpair × elem → sparsearray
. [ . ]	matrix	pf	matrix × nat × nat → elem with λ mx, r, c:nat. r < #r mx ∧ c < #c mx
. [ . ]	matrix	pf	matrix × nat × nat × elem → matrix with λ mx, r, c, a. r < #r m ∧ c < #c mx
. [ . ]	matrixops	pf	vector × nat → elem with λ ar, n. n < # ar
. [ . ]	matrixops	pf	vector × nat × elem → vector with λ ar, n, a. n < # ar
. [ . ]	sparsearray	pf	sparsearray × natpair → elem with λ st, a. a ∈ st
. [ . ]c	matrixops	pf	matrix × nat → vector with λ mx, c. c < #c mx
. [ . ]r	matrixops	pf	matrix × nat → vector with λ mx, r. r < #r mx
. \ .	natset	f	natset × natset → natset
. \ .	sparsearray	f	npset × npset → npset
. \ .	sparsearray	f	sparsearray × npset → sparsearray
. \ .	tidset-npset	f	Tidset × Tidset → Tidset
. \| .	sparsearray	f	sparsearray × npset → sparsearray
. × .	natpair	f	nat × nat → natpair
. ∈ .	natset	p	nat × natset
. ∈ .	sparsearray	p	natpair × sparsearray
. ∈ .	sparsearray	p	natpair × npset
. ∈ .	sparsearray	p	elem × sparsearray
. ∈ .	tidset-npset	p	Tid × Tidset
. ∩ .	natset	f	natset × natset → natset
. ∩ .	sparsearray	f	npset × npset → npset
. ∩ .	tidset-npset	f	Tidset × Tidset → Tidset
. ∪ .	natset	f	natset × natset → natset
. ∪ .	sparsearray	f	npset × npset → npset
. ∪ .	tidset-npset	f	Tidset × Tidset → Tidset
. ∪ .	tidset-npset	pf	sparsearray × sparsearray → sparsearray with disjointp
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	natset	p	natset × natset
. ⊆ .	sparsearray	p	sparsearray × sparsearray
. ⊆ .	sparsearray	p	npset × npset
. ⊆ .	tidset-npset	p	Tidset × Tidset
. ⊕ .	sparsearray	f	sparsearray × sparsearray → sparsearray
. to .	natset	f	nat × nat → natset
{ . }	natset	f	nat → natset
{ . }	sparsearray	f	natpair → npset
{ . }	tidset-npset	f	Tid → Tidset
Σ	matrixops	f	natset × (nat → elem) → elem
τ	VF3conc	c	VF3concAction
∅	natset	c	natset
∅	sparsearray	c	sparsearray
∅	sparsearray	c	npset
∅	tidset-npset	c	Tidset
F	VF3conc	c	VF3concPC
I	ring	c	elem
I	VF3conc	c	VF3concPC
L0	VF3conc	c	VF3concPC
L1	VF3conc	c	VF3concPC
L2	VF3conc	c	VF3concPC
L3	VF3conc	c	VF3concPC
L4	VF3conc	c	VF3concPC
L5	VF3conc	c	VF3concPC
L6	VF3conc	c	VF3concPC
L7	VF3conc	c	VF3concPC
L8	VF3conc	c	VF3concPC
MULT#	VerifyThis3-sequential	pr	sparsearray × nat × vector : : vector (nondeterministic)
O	ring	c	elem
O- .	ring	f	elem → elem
O- .	matrixops	f	matrix → matrix
O- .	matrixops	f	vector → vector
Tid	tidset-npset	s
Tidset	tidset-npset	s
U	tidset-npset	pf	Tidset × (Tid → sparsearray) → sparsearray with alldisjointp
VF3concAction	VF3conc	s
VF3concGInv	VF3conc	p	VF3concGState
VF3concGState	VF3conc	s
VF3concInv	VF3conc	p	VF3concGState × (Tid → VF3concLState) × (Tid → VF3concPC)
VF3concLInv	VF3conc	p	VF3concGState × VF3concLState × VF3concPC
VF3concLState	VF3conc	s
VF3concPC	VF3conc	s
VF3concRely	VF3conc	p	VF3concGState × Tid × VF3concGState
VF3concState	VF3conc	s
VF3concstep	VF3conc	p	VF3concState × VF3concAction × VF3concState
a	VF3conc	v	VF3concAction
alldisjointp	tidset-npset	p	Tidset × (Tid → sparsearray)
alltids	VF3conc	c	Tidset
chooseL2	VF3conc	f	sparsearray → VF3concAction
chooseL4	VF3conc	f	natpair → VF3concAction
disjointp	tidset-npset	p	sparsearray × sparsearray
dom .	sparsearray	f	sparsearray → npset
elem	elem	s
ghostlspmxf	VF3conc	v	Tid → sparsearray
gs	VF3conc	v	VF3concGState
gspmx	VF3conc	v	sparsearray
gstate	VF3conc	v	VF3concGState
gstepf	VF3conc	f	VF3concGState × VF3concLState × VF3concPC × VF3concAction → VF3concGState
invCMULT#	VF3conc	f	Tid → VF3concAction
ls	VF3conc	v	VF3concLState
lsf	VF3conc	v	Tid → VF3concLState
lspmx	VF3conc	v	sparsearray
lstep	VF3conc	p	VF3concGState × VF3concLState × VF3concPC × VF3concAction × VF3concGState × VF3concLState × VF3concPC
lstepf	VF3conc	f	VF3concGState × VF3concLState × VF3concPC × VF3concAction → VF3concLState
matrix	matrix	s
mkgs	VF3conc	f	sparsearray × sparsearray × nat × vector × vector × (Tid → sparsearray) → VF3concGState
mkls	VF3conc	f	Tid × sparsearray × natpair × elem → VF3concLState
mkmatrix	matrix	f	nat × nat × elem → matrix
mkstate	VF3conc	f	VF3concGState × (Tid → VF3concLState) × (Tid → VF3concPC) → VF3concState
mkvector	matrixops	f	nat → vector
nat	nat-basic	s
natpair	natpair	s
natset	natset	s
np	VF3conc	v	natpair
npset	sparsearray	s
okspmx	VerifyThis3-sequential	p	sparsearray × nat × nat
pc	VF3conc	v	VF3concPC
pcf	VF3conc	v	Tid → VF3concPC
pcstepf	VF3conc	f	VF3concGState × VF3concLState × VF3concPC × VF3concAction → VF3concPC
pre	VF3conc	p	VF3concGState × VF3concLState × VF3concPC × VF3concAction
r	VF3conc	v	nat
retCMULT#	VF3conc	f	Tid → VF3concAction
s	VF3conc	v	VF3concState
sparsearray	sparsearray	s
spmx	VF3conc	v	sparsearray
tid	VF3conc	v	Tid
val	VF3conc	v	elem
vector	matrixops	s
x	VF3conc	v	vector
y	VF3conc	v	vector