[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
aHashsetvHashsetAction
allslotsfullhashset-predspArray(Elem) × Nat × Nat × Elem × Bool
arHashsetvArray(Elem)
bHashsetvBool
betweenhashset-predspNat × Nat × Nat × Bool
doINSERTHashsetfTid × Bool → HashsetAction
doMEMBERHashsetfTid → HashsetAction
dummytidtidcTid
eHashsetvElem
foundHashsetvBool
get_hashhashset-predsfElem × Nat → Nat
gsHashsetvHashsetGState
gstateHashsetvHashsetGState
gstepfHashsetfHashsetGState × HashsetLState × HashsetPC × HashsetAction → HashsetGState
hashsetInitHashsetpHashsetState
hashsetStepHashsetpHashsetState × HashsetAction × HashsetState
htokhashset-predspArray(Elem)
idleHashsetcHashsetPC
invINSERTHashsetfTid × Elem → HashsetAction
invINSERTeHashsetvElem
invMEMBERHashsetfTid × Elem → HashsetAction
invMEMBEReHashsetvElem
lsHashsetvHashsetLState
lsfHashsetvTid → HashsetLState
lstepHashsetpHashsetGState × HashsetLState × HashsetPC × HashsetAction × HashsetGState × HashsetLState × HashsetPC
lstepfHashsetfHashsetGState × HashsetLState × HashsetPC × HashsetAction → HashsetLState
mHashsetvNat
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
nHashsetvNat
pcHashsetvHashsetPC
pcfHashsetvTid → HashsetPC
pcstepfHashsetfHashsetGState × HashsetLState × HashsetPC × HashsetAction → HashsetPC
preHashsetpHashsetGState × HashsetLState × HashsetPC × HashsetAction
relyhashset-predspArray(Elem) × Array(Elem)
retINSERTHashsetfTid × Bool → HashsetAction
retINSERTbHashsetvBool
retMEMBERHashsetfTid × Bool → HashsetAction
retMEMBERbHashsetvBool
sHashsetvHashsetState
szHashsetvNat
tidHashsetvTid