[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
# .arrayfArray('a) → Nat
. % .nat-divpfNat × Nat → Nat with λ n, m. m ≠ 0
. * .nat-multfNat × Nat → Nat
. + .nat-basicfNat × Nat → Nat
. +1nat-basicfNat → Nat
. - .natpfNat × Nat → Nat with λ n, m. n ≥ m
. -1nat-basicpfNat → Nat with λ n. n ≠ 0
. .arHashsetfHashsetGState → Array(Elem)
. .ar:= .HashsetfHashsetGState × Array(Elem) → HashsetGState
. .bHashsetpHashsetLState
. .bHashsetppHashsetAction with λ a. ∃ tid, b. a = doINSERT(tid, b)
. .b:= .HashsetfHashsetLState × Bool → HashsetLState
. .eHashsetfHashsetLState → Elem
. .e:= .HashsetfHashsetLState × Elem → HashsetLState
. .e0HashsetfHashsetLState → Elem
. .e0:= .HashsetfHashsetLState × Elem → HashsetLState
. .gstateHashsetfHashsetState → HashsetGState
. .gstate:= .HashsetfHashsetState × HashsetGState → HashsetState
. .invINSERTeHashsetpfHashsetAction → Elem with λ a. ∃ tid, invINSERTe. a = invINSERT(tid, invINSERTe)
. .invMEMBEReHashsetpfHashsetAction → Elem with λ a. ∃ tid, invINSERTe. a = invMEMBER(tid, invINSERTe)
. .lsfHashsetfHashsetState → Tid → HashsetLState
. .lsf:= .HashsetfHashsetState × (Tid → HashsetLState) → HashsetState
. .nHashsetfHashsetLState → Nat
. .n:= .HashsetfHashsetLState × Nat → HashsetLState
. .n0HashsetfHashsetLState → Nat
. .n0:= .HashsetfHashsetLState × Nat → HashsetLState
. .pcfHashsetfHashsetState → Tid → HashsetPC
. .pcf:= .HashsetfHashsetState × (Tid → HashsetPC) → HashsetState
. .retINSERTbHashsetppHashsetAction with λ a. ∃ tid, b. a = retINSERT(tid, b)
. .retMEMBERbHashsetppHashsetAction with λ a. ∃ tid, b. a = retMEMBER(tid, b)
. .szHashsetfHashsetLState → Nat
. .sz:= .HashsetfHashsetLState × Nat → HashsetLState
. .tidHashsetfHashsetLState → Tid
. .tidHashsetpfHashsetAction → Tid with λ a. a ≠ τ
. .tid:= .HashsetfHashsetLState × Tid → HashsetLState
. / .nat-divpfNat × Nat → Nat with λ n, m. m ≠ 0
. < .nat-basicpNat × Nat
. > .natpNat × Nat
. [ . := . ]arraypfArray('a) × Nat × 'a → Array('a) with λ ar, n, a. n < # ar
. [ . ]arraypfArray('a) × Nat → 'a with λ ar, n. n < # ar
. ≤ .natpNat × Nat
. ≥ .natpNat × Nat
τHashsetcHashsetAction
⊥elemcElem
Arrayarrays
Elemelems
HashsetActionHashsets
HashsetGInvHashsetpHashsetGState
HashsetGStateHashsets
HashsetInvHashsetpHashsetGState × (Tid → Type(HashsetLState)) × (Tid → Type(HashsetPC))
HashsetLInvHashsetpHashsetGState × HashsetLState × HashsetPC
HashsetLStateHashsets
HashsetPCHashsets
HashsetRelyHashsetpHashsetGState × Tid × HashsetGState
HashsetStateHashsets
I1HashsetcHashsetPC
I10HashsetcHashsetPC
I11HashsetcHashsetPC
I12HashsetcHashsetPC
I13HashsetcHashsetPC
I14HashsetcHashsetPC
I15HashsetcHashsetPC
I16HashsetcHashsetPC
I17HashsetcHashsetPC
I18HashsetcHashsetPC
I19HashsetcHashsetPC
I2HashsetcHashsetPC
I20HashsetcHashsetPC
I21HashsetcHashsetPC
I3HashsetcHashsetPC
I4HashsetcHashsetPC
I5HashsetcHashsetPC
I6HashsetcHashsetPC
I7HashsetcHashsetPC
I8HashsetcHashsetPC
I9HashsetcHashsetPC
M1HashsetcHashsetPC
M10HashsetcHashsetPC
M11HashsetcHashsetPC
M12HashsetcHashsetPC
M13HashsetcHashsetPC
M14HashsetcHashsetPC
M15HashsetcHashsetPC
M16HashsetcHashsetPC
M17HashsetcHashsetPC
M18HashsetcHashsetPC
M2HashsetcHashsetPC
M3HashsetcHashsetPC
M4HashsetcHashsetPC
M5HashsetcHashsetPC
M6HashsetcHashsetPC
M7HashsetcHashsetPC
M8HashsetcHashsetPC
M9HashsetcHashsetPC
Natnat-basics
Tidtids
aHashset-proofsvHashsetAction
allslotsfullhashset-predspArray(Elem) × Nat × Nat × Elem × Bool
arHashset-proofsvArray(Elem)
bHashset-proofsvBool
betweenhashset-predspNat × Nat × Nat × Bool
doINSERTHashsetfTid × Bool → HashsetAction
doMEMBERHashsetfTid → HashsetAction
dummytidtidcTid
eHashset-proofsvElem
foundHashset-proofsvBool
get_hashhashset-predsfElem × Nat → Nat
gsHashset-proofsvHashsetGState
gstateHashset-proofsvHashsetGState
gstepfHashsetfHashsetGState × HashsetLState × HashsetPC × HashsetAction → HashsetGState
hashsetInitHashsetpHashsetState
hashsetStepHashsetpHashsetState × HashsetAction × HashsetState
htokhashset-predspArray(Elem)
idleHashsetcHashsetPC
invINSERTHashsetfTid × Elem → HashsetAction
invINSERTeHashset-proofsvElem
invMEMBERHashsetfTid × Elem → HashsetAction
invMEMBEReHashset-proofsvElem
lsHashset-proofsvHashsetLState
lsfHashset-proofsvTid → HashsetLState
lstepHashsetpHashsetGState × HashsetLState × HashsetPC × HashsetAction × HashsetGState × HashsetLState × HashsetPC
lstepfHashsetfHashsetGState × HashsetLState × HashsetPC × HashsetAction → HashsetLState
mHashset-proofsvNat
mkarhashset-predsfNat × Elem → Array(Elem)
mkarrayarrayfNat → Array('a)
mkarrayarrayfNat × 'a → Array('a)
mkgsHashsetfArray(Elem) → HashsetGState
mklsHashsetfTid × Elem × Bool × Nat × Nat × Nat × Elem → HashsetLState
mkstateHashsetfHashsetGState × (Tid → HashsetLState) × (Tid → HashsetPC) → HashsetState
nHashset-proofsvNat
pcHashset-proofsvHashsetPC
pcfHashset-proofsvTid → HashsetPC
pcstepfHashsetfHashsetGState × HashsetLState × HashsetPC × HashsetAction → HashsetPC
preHashsetpHashsetGState × HashsetLState × HashsetPC × HashsetAction
relyhashset-predspArray(Elem) × Array(Elem)
retINSERTHashsetfTid × Bool → HashsetAction
retINSERTbHashset-proofsvBool
retMEMBERHashsetfTid × Bool → HashsetAction
retMEMBERbHashset-proofsvBool
sHashset-proofsvHashsetState
szHashset-proofsvNat
tidHashset-proofsvTid