[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
# .	set-basic	f	Set('a) → Nat
. + .	nat-basic	f	Nat × Nat → Nat
. ++ .	set-basic	f	Set('a) × 'a → Set('a)
. +1	nat-basic	f	Nat → Nat
. - .	nat	pf	Nat × Nat → Nat with λ n, m. n ≥ m
. -1	nat-basic	pf	Nat → Nat with λ n. n ≠ 0
. .b	Set	pp	SetAction with λ a. (∃ tid, b. a = ARetMember(tid, b)) ∨ (∃ tid, b. a = ARetInsert(tid, b)) ∨ (∃ tid, b. a = ADoInsert(tid, b))
. .e	Set	pf	SetAction → Elem with λ a. (∃ tid, e. a = AInvMember(tid, e)) ∨ (∃ tid, e. a = AInvInsert(tid, e))
. .gstate	Set	f	SetState → SetGState
. .gstate:= .	Set	f	SetState × SetGState → SetState
. .lb	Set	p	SetLState
. .lb:= .	Set	f	SetLState × Bool → SetLState
. .le	Set	f	SetLState → Elem
. .le:= .	Set	f	SetLState × Elem → SetLState
. .lsf	Set	f	SetState → Tid → SetLState
. .lsf:= .	Set	f	SetState × (Tid → SetLState) → SetState
. .pcf	Set	f	SetState → Tid → SetPC
. .pcf:= .	Set	f	SetState × (Tid → SetPC) → SetState
. .set	Set	f	SetGState → Set(Elem)
. .set:= .	Set	f	SetGState × Set(Elem) → SetGState
. .tid	Set	f	SetLState → Tid
. .tid	Set	pf	SetAction → Tid with λ a. a ≠ τ
. .tid:= .	Set	f	SetLState × Tid → SetLState
. < .	nat-basic	p	Nat × Nat
. > .	nat	p	Nat × Nat
. ∈ .	set-basic	p	'a × Set('a)
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
. ⊆ .	set-basic	p	Set('a) × Set('a)
τ	Set	c	SetAction
∅	set-basic	c	Set('a)
⊥	Set	c	Elem
ADoInsert	Set	f	Tid × Bool → SetAction
ADoMember	Set	f	Tid → SetAction
AInvInsert	Set	f	Tid × Elem → SetAction
AInvMember	Set	f	Tid × Elem → SetAction
ARetInsert	Set	f	Tid × Bool → SetAction
ARetMember	Set	f	Tid × Bool → SetAction
DOINSERT	Set	pr	Bool × Elem : Bool × Set(Elem)
DOMEMBER	Set	pr	Elem × Set(Elem) : Bool
Elem	Set	s
INVINSERT	Set	pr	Elem : Elem
INVMEMBER	Set	pr	Elem : Elem
Nat	nat-basic	s
RETINSERT	Set	pr	Bool : : Bool
RETMEMBER	Set	pr	Bool : : Bool
Set	set-basic	s
SetAction	Set	s
SetGInv	Set	p	SetGState
SetGState	Set	s
SetInv	Set	p	SetGState × (Tid → Type(SetLState)) × (Tid → Type(SetPC))
SetLInv	Set	p	SetGState × SetLState × SetPC
SetLState	Set	s
SetPC	Set	s
SetRely	Set	p	SetGState × Tid × SetGState
SetState	Set	s
Tid	tid	s
a	Set	v	SetAction
b	Set	v	Bool
dummytid	tid	c	Tid
e	Set	v	Elem
gs	Set	v	SetGState
gstate	Set	v	SetGState
gstepf	Set	f	SetGState × SetLState × SetPC × SetAction → SetGState
idle	Set	c	SetPC
invInsert	Set	c	SetPC
invMember	Set	c	SetPC
lb	Set	v	Bool
le	Set	v	Elem
ls	Set	v	SetLState
lsf	Set	v	Tid → SetLState
lstep	Set	p	SetGState × SetLState × SetPC × SetAction × SetGState × SetLState × SetPC
lstepf	Set	f	SetGState × SetLState × SetPC × SetAction → SetLState
mkgs	Set	f	Set(Elem) → SetGState
mkls	Set	f	Tid × Elem × Bool → SetLState
mkstate	Set	f	SetGState × (Tid → SetLState) × (Tid → SetPC) → SetState
pc	Set	v	SetPC
pcf	Set	v	Tid → SetPC
pcstepf	Set	f	SetGState × SetLState × SetPC × SetAction → SetPC
pre	Set	p	SetGState × SetLState × SetPC × SetAction
retInsert	Set	c	SetPC
retMember	Set	c	SetPC
s	Set	v	SetState
set	Set	v	Set(Elem)
setInit	Set	p	SetState
setStep	Set	p	SetState × SetAction × SetState
tid	Set	v	Tid