[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
# .	list-data	f	List('a) → Nat
# .	stream	f	Stream('a) → Natinf
# .	array	f	Array('a) → Nat
. !	remtau	f	('a → Opt('e)) → Stream('a) → Stream('e)
. !	remtau	f	('a → Opt('e)) → List('a) → List('e)
. % .	nat-div	pf	Nat × Nat → Nat with λ n, m. m ≠ 0
. '	list	f	'a → List('a)
. * .	nat-mult	f	Nat × Nat → Nat
. + .	nat-basic	f	Nat × Nat → Nat
. + .	list-data	f	'a × List('a) → List('a)
. + .	list	f	List('a) × List('a) → List('a)
. + .	list	f	List('a) × 'a → List('a)
. + .	nat-inf	f	Natinf × Natinf → Natinf
. + .	stream	f	'a × Stream('a) → Stream('a)
. + .	stream	f	Stream('a) × Stream('a) → Stream('a)
. + .	stream	f	List('a) × (Nat → 'a) → Nat → 'a
. + .	remtau	f	Opt('e) × Stream('e) → Stream('e)
. ++ .	set-basic	f	Set('a) × 'a → Set('a)
. ++ .	list-dup	f	List('a) × 'a → List('a)
. +1	nat-basic	f	Nat → Nat
. +2 .	list	f	'a × 'a → List('a)
. - .	nat	pf	Nat × Nat → Nat with λ n, m. n ≥ m
. -1	nat-basic	pf	Nat → Nat with λ n. n ≠ 0
. -1l .	list-del	f	List('a) × 'a → List('a)
. -l .	list-del	f	List('a) × 'a → List('a)
. -p .	list-del	f	List('a) × Nat → List('a)
. .ar	Hashset	f	HashsetGState → Array(Elem)
. .ar:= .	Hashset	f	HashsetGState × Array(Elem) → HashsetGState
. .b	Hashset	p	HashsetLState
. .b	Set	pp	SetAction with λ a. (∃ tid, b. a = ARetMember(tid, b)) ∨ (∃ tid, b. a = ARetInsert(tid, b)) ∨ (∃ tid, b. a = ADoInsert(tid, b))
. .b	Set-Test-IOAut	pp	EAction with λ ea. (∃ tid, b. ea = RetMember(tid, b)) ∨ (∃ tid, b. ea = RetInsert(tid, b))
. .b	Hashset	pp	HashsetAction with λ a. ∃ tid, b. a = doINSERT(tid, b)
. .b:= .	Hashset	f	HashsetLState × Bool → HashsetLState
. .butlast	list-last	pf	List('a) → List('a) with λ x. x ≠ []
. .distinct	list-dup	f	List('a) → List('a)
. .drop ( . )	stream	f	(Nat → 'a) × Nat → Nat → 'a
. .drop ( . )	list-del	pf	List('a) × Nat → List('a) with λ x, n. n ≤ # x
. .drop ( . )	stream	pf	Stream('a) × Nat → Stream('a) with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. .dropRight ( . )	list-last	pf	List('a) × Nat → List('a) with λ x, n. n ≤ # x
. .e	Hashset	f	HashsetLState → Elem
. .e	Set	pf	SetAction → Elem with λ a. (∃ tid, e. a = AInvMember(tid, e)) ∨ (∃ tid, e. a = AInvInsert(tid, e))
. .e	opt	pf	Opt('e) → 'e with λ oe. oe ≠ τ
. .e	Set-Test-IOAut	pf	EAction → Elem with λ ea. (∃ tid, e. ea = InvMember(tid, e)) ∨ (∃ tid, e. ea = InvInsert(tid, e))
. .e:= .	Hashset	f	HashsetLState × Elem → HashsetLState
. .e0	Hashset	f	HashsetLState → Elem
. .e0:= .	Hashset	f	HashsetLState × Elem → HashsetLState
. .ext	IO-Aut-data	f	IOAutomaton('s, 'a, 'e) → 'a → Opt('e)
. .f	stream-basic	pf	Stream('a) → Nat → 'a with λ σ. λ m. ∃ nf. σ = ⌜nf⌝
. .foldLeft ( . )	list	f	List('a) × 'b × ('b × 'a → 'b) → 'b
. .getOrElse ( . )	optfuns	f	Opt('a) × 'a → 'a
. .gstate	Set	f	SetState → SetGState
. .gstate	Hashset	f	HashsetState → HashsetGState
. .gstate:= .	Set	f	SetState × SetGState → SetState
. .gstate:= .	Hashset	f	HashsetState × HashsetGState → HashsetState
. .head	list-data	pf	List('a) → 'a with λ x. x ≠ []
. .indexOf ( . )	list-del	f	List('a) × 'a → Nat
. .invINSERTe	Hashset	pf	HashsetAction → Elem with λ a. ∃ tid, invINSERTe. a = invINSERT(tid, invINSERTe)
. .invMEMBERe	Hashset	pf	HashsetAction → Elem with λ a. ∃ tid, invINSERTe. a = invMEMBER(tid, invINSERTe)
. .l	stream-basic	pf	Stream('a) → List('a) with λ σ. finp(σ)
. .last	list-last	pf	List('a) → 'a with λ x. x ≠ []
. .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	Hashset	f	HashsetState → Tid → HashsetLState
. .lsf:= .	Set	f	SetState × (Tid → SetLState) → SetState
. .lsf:= .	Hashset	f	HashsetState × (Tid → HashsetLState) → HashsetState
. .map ( . )	list	f	List('a) × ('a → 'b) → List('b)
. .n	Hashset	f	HashsetLState → Nat
. .n	nat-inf	pf	Natinf → Nat with λ n∞. n∞ ≠ ∞
. .n:= .	Hashset	f	HashsetLState × Nat → HashsetLState
. .n0	Hashset	f	HashsetLState → Nat
. .n0:= .	Hashset	f	HashsetLState × Nat → HashsetLState
. .pcf	Set	f	SetState → Tid → SetPC
. .pcf	Hashset	f	HashsetState → Tid → HashsetPC
. .pcf:= .	Set	f	SetState × (Tid → SetPC) → SetState
. .pcf:= .	Hashset	f	HashsetState × (Tid → HashsetPC) → HashsetState
. .retINSERTb	Hashset	pp	HashsetAction with λ a. ∃ tid, b. a = retINSERT(tid, b)
. .retMEMBERb	Hashset	pp	HashsetAction with λ a. ∃ tid, b. a = retMEMBER(tid, b)
. .set	Set	f	SetGState → Set(Elem)
. .set:= .	Set	f	SetGState × Set(Elem) → SetGState
. .start	IO-Aut-data	f	IOAutomaton('s, 'a, 'e) → 's → Bool
. .step	IO-Aut-data	f	IOAutomaton('s, 'a, 'e) → 's × 'a × 's → Bool
. .sublist ( . )	list-del	pf	List('a) × Nat × Nat → List('a) with λ x, n, m. n + m ≤ # x
. .sz	Hashset	f	HashsetLState → Nat
. .sz:= .	Hashset	f	HashsetLState × Nat → HashsetLState
. .tail	list-data	pf	List('a) → List('a) with λ x. x ≠ []
. .take ( . )	stream	f	(Nat → 'a) × Nat → List('a)
. .take ( . )	list-del	pf	List('a) × Nat → List('a) with λ x, n. n ≤ # x
. .take ( . )	stream	pf	Stream('a) × Nat → List('a) with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. .take ( . )	stream	pf	Stream('a) × Natinf → Stream('a) with λ σ, n∞. finp(σ) → n∞ < # σ ∨ n∞ = # σ
. .takeRight ( . )	list-del	pf	List('a) × Nat → List('a) with λ x, n. n ≤ # x
. .tid	Set	f	SetLState → Tid
. .tid	Set-Test-IOAut	f	EAction → Tid
. .tid	Hashset	f	HashsetLState → Tid
. .tid	Set	pf	SetAction → Tid with λ a. a ≠ τ
. .tid	Hashset	pf	HashsetAction → Tid with λ a. a ≠ τ
. .tid:= .	Set	f	SetLState × Tid → SetLState
. .tid:= .	Hashset	f	HashsetLState × Tid → HashsetLState
. / .	nat-div	pf	Nat × Nat → Nat with λ n, m. m ≠ 0
. < .	nat-basic	p	Nat × Nat
. < .	list-data	p	List('a) × List('a)
. < .	nat-inf	p	Natinf × Natinf
. > .	nat	p	Nat × Nat
. [ . := . ]	list-getput	pf	List('a) × Nat × 'a → List('a) with λ x, n, a. n < # x
. [ . := . ]	stream	pf	Stream('a) × Nat × 'a → Stream('a) with λ σ, n, a. finp(σ) → ⌜n⌝ < # σ
. [ . := . ]	array	pf	Array('a) × Nat × 'a → Array('a) with λ ar, n, a. n < # ar
. [ . ]	list-getput	pf	List('a) × Nat → 'a with λ x, n. n < # x
. [ . ]	stream	pf	Stream('a) × Nat → 'a with λ σ, n. finp(σ) → ⌜n⌝ < # σ
. [ . ]	array	pf	Array('a) × Nat → 'a with λ ar, n. n < # ar
. ∈ .	set-basic	p	'a × Set('a)
. ∈ .	list	p	'a × List('a)
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
. ⊆ .	set-basic	p	Set('a) × Set('a)
. ⊑ .	list-last	p	List('a) × List('a)
. ⊑ .	stream	p	Stream('a) × Stream('a)
. ⊒ .	list-last	p	List('a) × List('a)
. o .	optfuns	f	('a → Opt('b)) × ('b → Opt('c)) → 'a → Opt('c)
[]	list-data	c	List('a)
[]	stream	c	Stream('a)
τ	Set	c	SetAction
τ	opt	c	Opt('e)
τ	Hashset	c	HashsetAction
∅	set-basic	c	Set('a)
∞	nat-inf	c	Natinf
≤F	IOforward	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
⊥	Set	c	Elem
⌜ . ⌝	opt	f	'e → Opt('e)
⌜ . ⌝	stream-basic	f	List('a) → Stream('a)
⌜ . ⌝	stream-basic	f	(Nat → 'a) → Stream('a)
⌜ . ⌝	nat-inf	f	Nat → Natinf
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
Array	array	s
C_≡*T_A	IOrefine-def	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
C_≡ωT_A	IOrefine-def	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
C_≡T_A	IOrefine-def	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
C_≤*T_A	IOrefine-def	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
C_≤ωT_A	IOrefine-def	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
C_≤T_A	IOrefine-def	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
DOINSERT	Set	pr	Bool × Elem : Bool × Set(Elem)
DOMEMBER	Set	pr	Elem × Set(Elem) : Bool
EAction	Set-Test-IOAut	s
Elem	Set	s
HashsetAction	Hashset	s
HashsetGInv	Hashset	p	HashsetGState
HashsetGState	Hashset	s
HashsetIOA	Hashset-refines-Set-Theory-Instance	c	IOAutomaton(HashsetState, HashsetAction, EAction)
HashsetInv	Hashset	p	HashsetGState × (Tid → Type(HashsetLState)) × (Tid → Type(HashsetPC))
HashsetLInv	Hashset	p	HashsetGState × HashsetLState × HashsetPC
HashsetLState	Hashset	s
HashsetPC	Hashset	s
HashsetRely	Hashset	p	HashsetGState × Tid × HashsetGState
HashsetState	Hashset	s
I1	Hashset	c	HashsetPC
I10	Hashset	c	HashsetPC
I11	Hashset	c	HashsetPC
I12	Hashset	c	HashsetPC
I13	Hashset	c	HashsetPC
I14	Hashset	c	HashsetPC
I15	Hashset	c	HashsetPC
I16	Hashset	c	HashsetPC
I17	Hashset	c	HashsetPC
I18	Hashset	c	HashsetPC
I19	Hashset	c	HashsetPC
I2	Hashset	c	HashsetPC
I20	Hashset	c	HashsetPC
I21	Hashset	c	HashsetPC
I3	Hashset	c	HashsetPC
I4	Hashset	c	HashsetPC
I5	Hashset	c	HashsetPC
I6	Hashset	c	HashsetPC
I7	Hashset	c	HashsetPC
I8	Hashset	c	HashsetPC
I9	Hashset	c	HashsetPC
INVINSERT	Set	pr	Elem : Elem
INVMEMBER	Set	pr	Elem : Elem
IOAut	IO-Aut-data	f	('s → Bool) × ('s × 'a × 's → Bool) × ('a → Opt('e)) → IOAutomaton('s, 'a, 'e)
IOAut?	IO-Automaton	p	IOAutomaton('s, 'a, 'e)
IOAutomaton	IO-Aut-data	s
InvInsert	Set-Test-IOAut	f	Tid × Elem → EAction
InvMember	Set-Test-IOAut	f	Tid × Elem → EAction
List	list-data	s
M1	Hashset	c	HashsetPC
M10	Hashset	c	HashsetPC
M11	Hashset	c	HashsetPC
M12	Hashset	c	HashsetPC
M13	Hashset	c	HashsetPC
M14	Hashset	c	HashsetPC
M15	Hashset	c	HashsetPC
M16	Hashset	c	HashsetPC
M17	Hashset	c	HashsetPC
M18	Hashset	c	HashsetPC
M2	Hashset	c	HashsetPC
M3	Hashset	c	HashsetPC
M4	Hashset	c	HashsetPC
M5	Hashset	c	HashsetPC
M6	Hashset	c	HashsetPC
M7	Hashset	c	HashsetPC
M8	Hashset	c	HashsetPC
M9	Hashset	c	HashsetPC
Nat	nat-basic	s
Natinf	nat-inf	s
Opt	opt	s
RETINSERT	Set	pr	Bool : : Bool
RETMEMBER	Set	pr	Bool : : Bool
RetInsert	Set-Test-IOAut	f	Tid × Bool → EAction
RetMember	Set-Test-IOAut	f	Tid × Bool → EAction
Set	set-basic	s
SetAction	Set	s
SetGInv	Set	p	SetGState
SetGState	Set	s
SetIOA	Set-Test-IOAut	c	IOAutomaton(SetState, SetAction, EAction)
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
Stream	stream-basic	s
Tid	tid	s
abs	Hashset-refines-Set	p	HashsetState × SetState
absset	abs	p	Array(Elem) × Set(Elem)
ags	Hashset-refines-Set-Theory-Instance	v	SetGState
allslotsfull	hashset-preds	p	Array(Elem) × Nat × Nat × Elem × Bool
als	Hashset-refines-Set-Theory-Instance	v	SetLState
alsf	Hashset-refines-Set-Theory-Instance	v	Tid → SetLState
apc	Hashset-refines-Set-Theory-Instance	v	SetPC
apcf	Hashset-refines-Set-Theory-Instance	v	Tid → SetPC
as	Hashset-refines-Set-Theory-Instance	v	SetState
b	Hashset-refines-Set-Theory-Instance	v	Bool
between	hashset-preds	p	Nat × Nat × Nat × Bool
cs	Hashset-refines-Set-Theory-Instance	v	HashsetState
disj	list-dup	p	List('a) × List('a)
doINSERT	Hashset	f	Tid × Bool → HashsetAction
doMEMBER	Hashset	f	Tid → HashsetAction
dummytid	tid	c	Tid
dups	list-dup	p	List('a)
e	Hashset-refines-Set-Theory-Instance	v	Elem
exec	IOtrace	f	IOAutomaton('s, 'a, 'e) → Stream('s) × Stream('a) → Bool
exec*	IOtrace	f	IOAutomaton('s, 'a, 'e) → List('s) × List('a) → Bool
execω	IOtrace	f	IOAutomaton('s, 'a, 'e) → (Nat → 's) × (Nat → 'a) → Bool
fillfirst	list-last	f	Nat × 'a × List('a) → List('a)
finp	stream-basic	p	Stream('a)
frag	IOtrace	f	IOAutomaton('s, 'a, 'e) → Stream('s) × Stream('a) → Bool
frag*	IOtrace	f	IOAutomaton('s, 'a, 'e) → List('s) × List('a) → Bool
fragω	IOtrace	f	IOAutomaton('s, 'a, 'e) → (Nat → 's) × (Nat → 'a) → Bool
frome	list-del	f	List('a) × 'a → List('a)
fwsim	IOforward	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('as × 'cs → Type(Bool))
gabs	Hashset-refines-Set	p	HashsetGState × (Tid → Type(HashsetLState)) × (Tid → Type(HashsetPC)) × SetGState × (Tid → Type(SetLState)) × (Tid → Type(SetPC))
get_hash	hashset-preds	f	Elem × Nat → Nat
gs	Hashset-refines-Set-Theory-Instance	v	HashsetGState
gstepf	Set	f	SetGState × SetLState × SetPC × SetAction → SetGState
gstepf	Hashset	f	HashsetGState × HashsetLState × HashsetPC × HashsetAction → HashsetGState
hashsetExt	Hashset-refines-Set-Theory-Instance	f	HashsetAction → Opt(EAction)
hashsetInit	Hashset	p	HashsetState
hashsetStep	Hashset	p	HashsetState × HashsetAction × HashsetState
hd	stream	pf	Stream('a) → 'a with λ σ. σ ≠ []
htok	hashset-preds	p	Array(Elem)
idle	Set	c	SetPC
idle	Hashset	c	HashsetPC
invINSERT	Hashset	f	Tid × Elem → HashsetAction
invInsert	Set	c	SetPC
invMEMBER	Hashset	f	Tid × Elem → HashsetAction
invMember	Set	c	SetPC
labs	Hashset-refines-Set	p	HashsetGState × HashsetLState × HashsetPC × SetGState × SetLState × SetPC
ls	Hashset-refines-Set-Theory-Instance	v	HashsetLState
lsf	Hashset-refines-Set-Theory-Instance	v	Tid → HashsetLState
lstep	Set	p	SetGState × SetLState × SetPC × SetAction × SetGState × SetLState × SetPC
lstep	Hashset	p	HashsetGState × HashsetLState × HashsetPC × HashsetAction × HashsetGState × HashsetLState × HashsetPC
lstepf	Set	f	SetGState × SetLState × SetPC × SetAction → SetLState
lstepf	Hashset	f	HashsetGState × HashsetLState × HashsetPC × HashsetAction → HashsetLState
min	nat-inf	f	Natinf × Natinf → Natinf
mkar	hashset-preds	f	Nat × Elem → Array(Elem)
mkarray	array	f	Nat → Array('a)
mkarray	array	f	Nat × 'a → Array('a)
mkgs	Set	f	Set(Elem) → SetGState
mkgs	Hashset	f	Array(Elem) → HashsetGState
mklist	list-last	f	'a × Nat → List('a)
mkls	Set	f	Tid × Elem × Bool → SetLState
mkls	Hashset	f	Tid × Elem × Bool × Nat × Nat × Nat × Elem → HashsetLState
mkstate	Set	f	SetGState × (Tid → SetLState) × (Tid → SetPC) → SetState
mkstate	Hashset	f	HashsetGState × (Tid → HashsetLState) × (Tid → HashsetPC) → HashsetState
move	IOtrace	f	IOAutomaton('s, 'a, 'e) → 's × List('e) × 's → Bool
oinj	optfuns	p	('a → Type(Opt('b)))
osurj	optfuns	p	('a → Type(Opt('b)))
pc	Hashset-refines-Set-Theory-Instance	v	HashsetPC
pcf	Hashset-refines-Set-Theory-Instance	v	Tid → HashsetPC
pcstepf	Set	f	SetGState × SetLState × SetPC × SetAction → SetPC
pcstepf	Hashset	f	HashsetGState × HashsetLState × HashsetPC × HashsetAction → HashsetPC
pre	Set	p	SetGState × SetLState × SetPC × SetAction
pre	Hashset	p	HashsetGState × HashsetLState × HashsetPC × HashsetAction
rely	hashset-preds	p	Array(Elem) × Array(Elem)
ren	Hashset-refines-Set	f	HashsetAction × SetGState × (Tid → SetLState) → SetAction
retINSERT	Hashset	f	Tid × Bool → HashsetAction
retInsert	Set	c	SetPC
retMEMBER	Hashset	f	Tid × Bool → HashsetAction
retMember	Set	c	SetPC
rev	list-last	f	List('a) → List('a)
setExt	Set-Test-IOAut	f	SetAction → Opt(EAction)
setInit	Set	p	SetState
setStep	Set	p	SetState × SetAction × SetState
tid	Hashset-refines-Set-Theory-Instance	v	Tid
tl	stream	pf	Stream('a) → Stream('a) with λ σ. σ ≠ []
trace	IOtrace	f	IOAutomaton('s, 'a, 'e) → Stream('e) → Bool
trace*	IOtrace	f	IOAutomaton('s, 'a, 'e) → List('e) → Bool
traceω	IOtrace	f	IOAutomaton('s, 'a, 'e) → (Nat → 'e) → Bool