[Imprint][Data Privacy Statement][E-Mail]

Back to the index. View project statistic. View project symbols. View KIV symbols to check that all symbols are available.

All project symbols

symbol	specification	entry
#	set-basic	function, set → nat
#	natset	function, natset → nat
#	array	function, array → nat
#	matrixops	function, vector → nat
#	store	function, store → nat
#	sparsearray	function, npset → nat
#	sparsearray	function, sparsearray → nat
#	tidset-npset	function, Tidset → nat
#c	matrix	function, matrix → nat
#r	matrix	function, matrix → nat
*	ring	function, elem × elem → elem
*	matrixops	partial function, vector × vector → elem
*	matrixops	partial function, vector × matrix → vector
*	matrixops	partial function, matrix × vector → vector
*	matrixops	partial function, matrix × matrix → matrix
+	nat-basic	function, nat × nat → nat
+	ring	function, elem × elem → elem
+	matrixops	partial function, vector × vector → vector
+	matrixops	partial function, matrix × matrix → matrix
++	set-basic	function, set × elem → set
++	natset	function, natset × nat → natset
++	sparsearray	function, npset × natpair → npset
++	tidset-npset	function, Tidset × Tid → Tidset
+1	nat-basic	function, nat → nat
-	nat	partial function, nat × nat → nat
--	set-union	function, set × elem → set
--	natset	function, natset × nat → natset
--	store	function, store × elem → store
--	sparsearray	function, npset × natpair → npset
--	sparsearray	function, sparsearray × natpair → sparsearray
--	tidset-npset	function, Tidset × Tid → Tidset
-1	nat-basic	partial function, nat → nat
.c	natpair	function, natpair → nat
.ghostlspmxf	VF3conc	function, VF3concGState → Tid → sparsearray
.ghostlspmxf:=	VF3conc	function, VF3concGState × Tid → sparsearray → VF3concGState
.gspmx	VF3conc	function, VF3concGState → sparsearray
.gspmx:=	VF3conc	function, VF3concGState × sparsearray → VF3concGState
.gstate	VF3conc	function, VF3concState → VF3concGState
.gstate:=	VF3conc	function, VF3concState × VF3concGState → VF3concState
.lsf	VF3conc	function, VF3concState → Tid → VF3concLState
.lsf:=	VF3conc	function, VF3concState × Tid → VF3concLState → VF3concState
.lspmx	VF3conc	function, VF3concAction → sparsearray
.lspmx	VF3conc	function, VF3concLState → sparsearray
.lspmx:=	VF3conc	function, VF3concLState × sparsearray → VF3concLState
.np	VF3conc	function, VF3concAction → natpair
.np	VF3conc	function, VF3concLState → natpair
.np:=	VF3conc	function, VF3concLState × natpair → VF3concLState
.pcf	VF3conc	function, VF3concState → Tid → VF3concPC
.pcf:=	VF3conc	function, VF3concState × Tid → VF3concPC → VF3concState
.r	natpair	function, natpair → nat
.r	VF3conc	function, VF3concGState → nat
.r:=	VF3conc	function, VF3concGState × nat → VF3concGState
.spmx	VF3conc	function, VF3concGState → sparsearray
.spmx:=	VF3conc	function, VF3concGState × sparsearray → VF3concGState
.tid	VF3conc	function, VF3concAction → Tid
.tid	VF3conc	function, VF3concLState → Tid
.tid:=	VF3conc	function, VF3concLState × Tid → VF3concLState
.toMatrix	VerifyThis3-sequential	function, sparsearray × nat × nat → matrix
.val	VF3conc	function, VF3concLState → elem
.val:=	VF3conc	function, VF3concLState × elem → VF3concLState
.x	VF3conc	function, VF3concGState → vector
.x:=	VF3conc	function, VF3concGState × vector → VF3concGState
.y	VF3conc	function, VF3concGState → vector
.y:=	VF3conc	function, VF3concGState × vector → VF3concGState
<	nat-basic	predicate, nat × nat
>	nat	predicate, nat × nat
F	VF3conc	constant, VF3concPC
I	ring	constant, elem
I	VF3conc	constant, VF3concPC
L0	VF3conc	constant, VF3concPC
L1	VF3conc	constant, VF3concPC
L2	VF3conc	constant, VF3concPC
L3	VF3conc	constant, VF3concPC
L4	VF3conc	constant, VF3concPC
L5	VF3conc	constant, VF3concPC
L6	VF3conc	constant, VF3concPC
L7	VF3conc	constant, VF3concPC
L8	VF3conc	constant, VF3concPC
MULT#	VerifyThis3-sequential	procedure, sparsearray × nat × vector : : vector
O	ring	constant, elem
O-	ring	function, elem → elem
O-	matrixops	function, vector → vector
O-	matrixops	function, matrix → matrix
Tid	tidset-npset	sort,
Tidset	tidset-npset	sort,
U	tidset-npset	partial function, Tidset × Tid → sparsearray → sparsearray
VF3concAction	VF3conc	sort,
VF3concGInv	VF3conc	predicate, VF3concGState
VF3concGState	VF3conc	sort,
VF3concInv	VF3conc	predicate, VF3concGState × Tid → VF3concLState × Tid → VF3concPC
VF3concLInv	VF3conc	predicate, VF3concGState × VF3concLState × VF3concPC
VF3concLState	VF3conc	sort,
VF3concPC	VF3conc	sort,
VF3concRely	VF3conc	predicate, VF3concGState × Tid × VF3concGState
VF3concState	VF3conc	sort,
VF3concstep	VF3conc	predicate, VF3concState × VF3concAction × VF3concState
\	set-union	function, set × set → set
\	natset	function, natset × natset → natset
\	store+set	function, store × set → store
\	sparsearray	function, sparsearray × npset → sparsearray
\	sparsearray	function, npset × npset → npset
\	tidset-npset	function, Tidset × Tidset → Tidset
]	matrix	partial function, matrix × nat × nat × elem → matrix
]	matrix	partial function, matrix × nat × nat → elem
]	array	partial function, array × nat × elem → array
]	array	partial function, array × nat → elem
]	matrixops	partial function, vector × nat × elem → vector
]	matrixops	partial function, vector × nat → elem
]	store	partial function, store × elem → data
]	store	function, store × elem × data → store
]	sparsearray	partial function, sparsearray × natpair → elem
]	sparsearray	function, sparsearray × natpair × elem → sparsearray
]c	matrix+array	partial function, matrix × nat → array
]c	matrixops	partial function, matrix × nat → vector
]r	matrix+array	partial function, matrix × nat → array
]r	matrixops	partial function, matrix × nat → vector
a	elem	variable, elem
a	matrix	variable, elem
a	array	variable, elem
a	ring	variable, elem
a	matrixops	variable, elem
a	VerifyThis3-sequential	variable, elem
a	store+set	variable, elem
a	VF3conc	variable, VF3concAction
alldisjointp	tidset-npset	predicate, Tidset × Tid → sparsearray
alltids	VF3conc	constant, Tidset
ar	array	variable, array
array	array	sort,
b	elem	variable, elem
b	ring	variable, elem
c	elem	variable, elem
c	matrix	variable, nat
c	matrix+array	variable, nat
c	ring	variable, elem
c	matrixops	variable, nat
c	VerifyThis3-sequential	variable, nat
c	natpair	variable, nat
chooseL2	VF3conc	function, sparsearray → VF3concAction
chooseL4	VF3conc	function, natpair → VF3concAction
d	data	variable, data
d	store+set	variable, data
data	data	sort,
disjointp	tidset-npset	predicate, sparsearray × sparsearray
dom	store+set	function, store → set
dom	sparsearray	function, sparsearray → npset
elem	elem	sort,
f	matrixops	variable, nat → elem
f	tidset-npset	variable, Tid → sparsearray
g	matrixops	variable, nat × nat → elem
ghostlspmxf	VF3conc	variable, Tid → sparsearray
gs	VF3conc	variable, VF3concGState
gspmx	VF3conc	variable, sparsearray
gstate	VF3conc	variable, VF3concGState
gstepf	VF3conc	function, VF3concGState × VF3concLState × VF3concPC × VF3concAction → VF3concGState
invCMULT#	VF3conc	function, Tid → VF3concAction
ls	VF3conc	variable, VF3concLState
lsf	VF3conc	variable, Tid → VF3concLState
lspmx	VF3conc	variable, sparsearray
lstep	VF3conc	predicate, VF3concGState × VF3concLState × VF3concPC × VF3concAction × VF3concGState × VF3concLState × VF3concPC
lstepf	VF3conc	function, VF3concGState × VF3concLState × VF3concPC × VF3concAction → VF3concLState
m	natset	variable, nat
m	array	variable, nat
m	matrixops	variable, nat
m	VerifyThis3-sequential	variable, nat
matrix	matrix	sort,
mkarray	array	function, nat → array
mkgs	VF3conc	function, sparsearray × sparsearray × nat × vector × vector × Tid → sparsearray → VF3concGState
mkls	VF3conc	function, Tid × sparsearray × natpair × elem → VF3concLState
mkmatrix	matrix	function, nat × nat × elem → matrix
mkstate	VF3conc	function, VF3concGState × Tid → VF3concLState × Tid → VF3concPC → VF3concState
mkvector	matrixops	function, nat → vector
mx	matrix	variable, matrix
mx	matrix+array	variable, matrix
mx	matrixops	variable, matrix
n	natset	variable, nat
n	array	variable, nat
n	matrixops	variable, nat
n	VerifyThis3-sequential	variable, nat
n	natpair	variable, nat
nat	nat-basic	sort,
natpair	natpair	sort,
natset	natset	sort,
np	VerifyThis3-sequential	variable, natpair
np	natpair	variable, natpair
np	VF3conc	variable, natpair
np	tidset-npset	variable, natpair
npset	sparsearray	sort,
ns	natset	variable, natset
ns	matrixops	variable, natset
okspmx	VerifyThis3-sequential	predicate, sparsearray × nat × nat
pc	VF3conc	variable, VF3concPC
pcf	VF3conc	variable, Tid → VF3concPC
pcstepf	VF3conc	function, VF3concGState × VF3concLState × VF3concPC × VF3concAction → VF3concPC
pre	VF3conc	predicate, VF3concGState × VF3concLState × VF3concPC × VF3concAction
r	matrix	variable, nat
r	matrix+array	variable, nat
r	matrixops	variable, nat
r	VerifyThis3-sequential	variable, nat
r	natpair	variable, nat
r	VF3conc	variable, nat
retCMULT#	VF3conc	function, Tid → VF3concAction
s	set-basic	variable, set
s	VF3conc	variable, VF3concState
sa	tidset-npset	variable, sparsearray
set	set-basic	sort,
sparsearray	sparsearray	sort,
spmx	VerifyThis3-sequential	variable, sparsearray
spmx	VF3conc	variable, sparsearray
st	store	variable, store
st	store+set	variable, store
store	store	sort,
tid	VF3conc	variable, Tid
tid	tidset-npset	variable, Tid
to	natset	function, nat × nat → natset
ts	tidset-npset	variable, Tidset
val	VF3conc	variable, elem
vec	matrixops	variable, vector
vector	matrixops	sort,
x	VerifyThis3-sequential	variable, vector
x	VF3conc	variable, vector
y	VerifyThis3-sequential	variable, vector
y	VF3conc	variable, vector
\|	store+set	function, store × set → store
\|	sparsearray	function, sparsearray × npset → sparsearray
}	set-union	function, elem → set
}	natset	function, nat → natset
}	sparsearray	function, natpair → npset
}	tidset-npset	function, Tid → Tidset
×	natpair	function, nat × nat → natpair
Σ	matrixops	function, natset × nat → elem → elem
τ	VF3conc	constant, VF3concAction
∅	set-basic	constant, set
∅	natset	constant, natset
∅	store	constant, store
∅	sparsearray	constant, npset
∅	sparsearray	constant, sparsearray
∅	tidset-npset	constant, Tidset
∈	set-basic	predicate, elem × set
∈	natset	predicate, nat × natset
∈	store	predicate, elem × store
∈	store+set	predicate, data × store
∈	sparsearray	predicate, elem × sparsearray
∈	sparsearray	predicate, natpair × npset
∈	sparsearray	predicate, natpair × sparsearray
∈	tidset-npset	predicate, Tid × Tidset
∩	set-union	function, set × set → set
∩	natset	function, natset × natset → natset
∩	sparsearray	function, npset × npset → npset
∩	tidset-npset	function, Tidset × Tidset → Tidset
∪	set-union	function, set × set → set
∪	natset	function, natset × natset → natset
∪	sparsearray	function, npset × npset → npset
∪	tidset-npset	partial function, sparsearray × sparsearray → sparsearray
∪	tidset-npset	function, Tidset × Tidset → Tidset
≤	nat	predicate, nat × nat
≥	nat	predicate, nat × nat
⊆	set-basic	predicate, set × set
⊆	natset	predicate, natset × natset
⊆	store	predicate, store × store
⊆	sparsearray	predicate, npset × npset
⊆	sparsearray	predicate, sparsearray × sparsearray
⊆	tidset-npset	predicate, Tidset × Tidset
⊕	store+set	function, store × store → store
⊕	sparsearray	function, sparsearray × sparsearray → sparsearray