[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
!	remtau	function, 'a → Opt('e) → List('a) → List('e)
!	remtau	function, 'a → Opt('e) → Stream('a) → Stream('e)
#	array	function, Array('a) → Nat
#	stream	function, Stream('a) → Natinf
#	list-data	function, List('a) → Nat
#	set-basic	function, Set('a) → Nat
%	nat-div	partial function, Nat × Nat → Nat
'	list	function, 'a → List('a)
*	nat-mult	function, Nat × Nat → Nat
+	nat-inf	function, Natinf × Natinf → Natinf
+	list	function, List('a) × 'a → List('a)
+	list	function, List('a) × List('a) → List('a)
+	stream	function, List('a) × Nat → 'a → Nat → 'a
+	stream	function, Stream('a) × Stream('a) → Stream('a)
+	stream	function, 'a × Stream('a) → Stream('a)
+	list-data	function, 'a × List('a) → List('a)
+	remtau	function, Opt('e) × Stream('e) → Stream('e)
+	nat-basic	function, Nat × Nat → Nat
++	list-dup	function, List('a) × 'a → List('a)
++	set-basic	function, Set('a) × 'a → Set('a)
+1	nat-basic	function, Nat → Nat
+2	list	function, 'a × 'a → List('a)
-	nat	partial function, Nat × Nat → Nat
-1	nat-basic	partial function, Nat → Nat
-1l	list-del	function, List('a) × 'a → List('a)
-l	list-del	function, List('a) × 'a → List('a)
-p	list-del	function, List('a) × Nat → List('a)
.ar	Hashset	function, HashsetGState → Array(Elem)
.ar:=	Hashset	function, HashsetGState × Array(Elem) → HashsetGState
.b	Set-Test-IOAut	partial predicate, EAction
.b	Hashset	partial predicate, HashsetAction
.b	Hashset	predicate, HashsetLState
.b	Set	partial predicate, SetAction
.b:=	Hashset	function, HashsetLState × Bool → HashsetLState
.butlast	list-last	partial function, List('a) → List('a)
.distinct	list-dup	function, List('a) → List('a)
.drop	list-del	partial function, List('a) × Nat → List('a)
.drop	stream	partial function, Stream('a) × Nat → Stream('a)
.drop	stream	function, Nat → 'a × Nat → Nat → 'a
.dropRight	list-last	partial function, List('a) × Nat → List('a)
.e	Set-Test-IOAut	partial function, EAction → Elem
.e	opt	partial function, Opt('e) → 'e
.e	Hashset	function, HashsetLState → Elem
.e	Set	partial function, SetAction → Elem
.e0	Hashset	function, HashsetLState → Elem
.e0:=	Hashset	function, HashsetLState × Elem → HashsetLState
.e:=	Hashset	function, HashsetLState × Elem → HashsetLState
.ext	IO-Aut-data	function, IOAutomaton('s, 'a, 'e) → 'a → Opt('e)
.f	stream-basic	partial function, Stream('a) → Nat → 'a
.foldLeft	list	function, List('a) × 'b × 'b × 'a → 'b → 'b
.getOrElse	optfuns	function, Opt('a) × 'a → 'a
.gstate	Hashset	function, HashsetState → HashsetGState
.gstate	Set	function, SetState → SetGState
.gstate:=	Hashset	function, HashsetState × HashsetGState → HashsetState
.gstate:=	Set	function, SetState × SetGState → SetState
.head	list-data	partial function, List('a) → 'a
.indexOf	list-del	function, List('a) × 'a → Nat
.invINSERTe	Hashset	partial function, HashsetAction → Elem
.invMEMBERe	Hashset	partial function, HashsetAction → Elem
.l	stream-basic	partial function, Stream('a) → List('a)
.last	list-last	partial function, List('a) → 'a
.lb	Set	predicate, SetLState
.lb:=	Set	function, SetLState × Bool → SetLState
.le	Set	function, SetLState → Elem
.le:=	Set	function, SetLState × Elem → SetLState
.lsf	Hashset	function, HashsetState → Tid → HashsetLState
.lsf	Set	function, SetState → Tid → SetLState
.lsf:=	Hashset	function, HashsetState × Tid → HashsetLState → HashsetState
.lsf:=	Set	function, SetState × Tid → SetLState → SetState
.map	list	function, List('a) × 'a → 'b → List('b)
.n	nat-inf	partial function, Natinf → Nat
.n	Hashset	function, HashsetLState → Nat
.n0	Hashset	function, HashsetLState → Nat
.n0:=	Hashset	function, HashsetLState × Nat → HashsetLState
.n:=	Hashset	function, HashsetLState × Nat → HashsetLState
.pcf	Hashset	function, HashsetState → Tid → HashsetPC
.pcf	Set	function, SetState → Tid → SetPC
.pcf:=	Hashset	function, HashsetState × Tid → HashsetPC → HashsetState
.pcf:=	Set	function, SetState × Tid → SetPC → SetState
.retINSERTb	Hashset	partial predicate, HashsetAction
.retMEMBERb	Hashset	partial predicate, HashsetAction
.set	Set	function, SetGState → Set(Elem)
.set:=	Set	function, SetGState × Set(Elem) → SetGState
.start	IO-Aut-data	function, IOAutomaton('s, 'a, 'e) → 's → Bool
.step	IO-Aut-data	function, IOAutomaton('s, 'a, 'e) → 's × 'a × 's → Bool
.sublist	list-del	partial function, List('a) × Nat × Nat → List('a)
.sz	Hashset	function, HashsetLState → Nat
.sz:=	Hashset	function, HashsetLState × Nat → HashsetLState
.tail	list-data	partial function, List('a) → List('a)
.take	list-del	partial function, List('a) × Nat → List('a)
.take	stream	partial function, Stream('a) × Natinf → Stream('a)
.take	stream	partial function, Stream('a) × Nat → List('a)
.take	stream	function, Nat → 'a × Nat → List('a)
.takeRight	list-del	partial function, List('a) × Nat → List('a)
.tid	Set-Test-IOAut	function, EAction → Tid
.tid	Hashset	partial function, HashsetAction → Tid
.tid	Hashset	function, HashsetLState → Tid
.tid	Set	partial function, SetAction → Tid
.tid	Set	function, SetLState → Tid
.tid:=	Hashset	function, HashsetLState × Tid → HashsetLState
.tid:=	Set	function, SetLState × Tid → SetLState
/	nat-div	partial function, Nat × Nat → Nat
<	nat-inf	predicate, Natinf × Natinf
<	list-data	predicate, List('a) × List('a)
<	nat-basic	predicate, Nat × Nat
>	nat	predicate, Nat × Nat
ADoInsert	Set	function, Tid × Bool → SetAction
ADoMember	Set	function, Tid → SetAction
AInvInsert	Set	function, Tid × Elem → SetAction
AInvMember	Set	function, Tid × Elem → SetAction
ARetInsert	Set	function, Tid × Bool → SetAction
ARetMember	Set	function, Tid × Bool → SetAction
Array	array	sort,
C_≡*T_A	IOrefine-def	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
C_≡T_A	IOrefine-def	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
C_≡ωT_A	IOrefine-def	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
C_≤*T_A	IOrefine-def	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
C_≤T_A	IOrefine-def	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
C_≤ωT_A	IOrefine-def	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
DOINSERT	Set	procedure, Bool × Elem : Bool × Set(Elem)
DOMEMBER	Set	procedure, Elem × Set(Elem) : Bool
EAction	Set-Test-IOAut	sort,
Elem	elem	sort,
Elem	Set	sort,
HashsetAction	Hashset	sort,
HashsetGInv	Hashset	predicate, HashsetGState
HashsetGState	Hashset	sort,
HashsetIOA	Hashset-refines-Set-Theory-Instance	constant, IOAutomaton(HashsetState, HashsetAction, EAction)
HashsetInv	Hashset	predicate, HashsetGState × Tid → HashsetLState × Tid → HashsetPC
HashsetLInv	Hashset	predicate, HashsetGState × HashsetLState × HashsetPC
HashsetLState	Hashset	sort,
HashsetPC	Hashset	sort,
HashsetRely	Hashset	predicate, HashsetGState × Tid × HashsetGState
HashsetState	Hashset	sort,
I1	Hashset	constant, HashsetPC
I10	Hashset	constant, HashsetPC
I11	Hashset	constant, HashsetPC
I12	Hashset	constant, HashsetPC
I13	Hashset	constant, HashsetPC
I14	Hashset	constant, HashsetPC
I15	Hashset	constant, HashsetPC
I16	Hashset	constant, HashsetPC
I17	Hashset	constant, HashsetPC
I18	Hashset	constant, HashsetPC
I19	Hashset	constant, HashsetPC
I2	Hashset	constant, HashsetPC
I20	Hashset	constant, HashsetPC
I21	Hashset	constant, HashsetPC
I3	Hashset	constant, HashsetPC
I4	Hashset	constant, HashsetPC
I5	Hashset	constant, HashsetPC
I6	Hashset	constant, HashsetPC
I7	Hashset	constant, HashsetPC
I8	Hashset	constant, HashsetPC
I9	Hashset	constant, HashsetPC
INVINSERT	Set	procedure, Elem : Elem
INVMEMBER	Set	procedure, Elem : Elem
IOAut	IO-Aut-data	function, 's → Bool × 's × 'a × 's → Bool × 'a → Opt('e) → IOAutomaton('s, 'a, 'e)
IOAut?	IO-Automaton	predicate, IOAutomaton('s, 'a, 'e)
IOAutomaton	IO-Aut-data	sort,
InvInsert	Set-Test-IOAut	function, Tid × Elem → EAction
InvMember	Set-Test-IOAut	function, Tid × Elem → EAction
List	list-data	sort,
M1	Hashset	constant, HashsetPC
M10	Hashset	constant, HashsetPC
M11	Hashset	constant, HashsetPC
M12	Hashset	constant, HashsetPC
M13	Hashset	constant, HashsetPC
M14	Hashset	constant, HashsetPC
M15	Hashset	constant, HashsetPC
M16	Hashset	constant, HashsetPC
M17	Hashset	constant, HashsetPC
M18	Hashset	constant, HashsetPC
M2	Hashset	constant, HashsetPC
M3	Hashset	constant, HashsetPC
M4	Hashset	constant, HashsetPC
M5	Hashset	constant, HashsetPC
M6	Hashset	constant, HashsetPC
M7	Hashset	constant, HashsetPC
M8	Hashset	constant, HashsetPC
M9	Hashset	constant, HashsetPC
Nat	nat-basic	sort,
Natinf	nat-inf	sort,
Opt	opt	sort,
RETINSERT	Set	procedure, Bool : : Bool
RETMEMBER	Set	procedure, Bool : : Bool
RetInsert	Set-Test-IOAut	function, Tid × Bool → EAction
RetMember	Set-Test-IOAut	function, Tid × Bool → EAction
Set	set-basic	sort,
SetAction	Set	sort,
SetGInv	Set	predicate, SetGState
SetGState	Set	sort,
SetIOA	Set-Test-IOAut	constant, IOAutomaton(SetState, SetAction, EAction)
SetInv	Set	predicate, SetGState × Tid → SetLState × Tid → SetPC
SetLInv	Set	predicate, SetGState × SetLState × SetPC
SetLState	Set	sort,
SetPC	Set	sort,
SetRely	Set	predicate, SetGState × Tid × SetGState
SetState	Set	sort,
Stream	stream-basic	sort,
Tid	tid	sort,
Tid	hashset-preds	variable, Tid,flexible
[]	stream	constant, Stream('a)
[]	list-data	constant, List('a)
]	list-getput	partial function, List('a) × Nat × 'a → List('a)
]	list-getput	partial function, List('a) × Nat → 'a
]	array	partial function, Array('a) × Nat × 'a → Array('a)
]	array	partial function, Array('a) × Nat → 'a
]	stream	partial function, Stream('a) × Nat × 'a → Stream('a)
]	stream	partial function, Stream('a) × Nat → 'a
a	list-getput	variable, 'a
a	array	variable, 'a
a	list-del	variable, 'a
a	optfuns	variable, 'a
a	list-dup	variable, 'a
a	Set-proofs	variable, SetAction
a	list	variable, 'a
a	infinite-append	variable, 'a
a	IOtrace	variable, 'a
a	stream	variable, 'a
a	Set-Test-IOAut	variable, SetAction
a	Hashset-proofs	variable, HashsetAction
a	list-data	variable, 'a
a	list-last	variable, 'a
a	set-basic	variable, 'a
a	remtau	variable, 'a
a	Hashset	variable, HashsetAction
a	Hashset-refines-Set	variable, HashsetAction
a	IO-Automaton	variable, 'a
a	IO-Aut-data	variable, 'a
a	Set	variable, SetAction
aa	Hashset-refines-Set	variable, SetAction
aa	IOforward	variable, 'aa
aa	IOrefine-def	variable, 'aa
aa	IOforward-is-leqrefine	variable, 'aa
aaf	IOforward-is-leqrefine	variable, Nat → 'aa
aal	IOforward	variable, List('aa)
aal	IOrefine-def	variable, List('aa)
aal	IOforward-is-leqrefine	variable, List('aa)
aalf	IOforward-is-leqrefine	variable, Nat → List('aa)
abs	Hashset-refines-Set	predicate, HashsetState × SetState
absset	abs	predicate, Array(Elem) × Set(Elem)
aext	IOforward	variable, 'aa → Opt('e)
aext	IOrefine-def	variable, 'aa → Opt('e)
aext	IOforward-is-leqrefine	variable, 'aa → Opt('e)
af	IOtrace	variable, Nat → 'a
af	remtau	variable, Nat → 'a
ags	Hashset-refines-Set	variable, SetGState
ags	Hashset-refines-Set-Theory-Instance	variable, SetGState
aioaut	IOforward	variable, IOAutomaton('as, 'aa, 'e)
aioaut	IOrefine-def	variable, IOAutomaton('as, 'aa, 'e)
aioaut	IOforward-is-leqrefine	variable, IOAutomaton('as, 'aa, 'e)
al	IOtrace	variable, List('a)
al	Set-Test-IOAut	variable, List(SetAction)
al	remtau	variable, List('a)
alf	IOtrace	variable, Nat → List('a)
allslotsfull	hashset-preds	predicate, Array(Elem) × Nat × Nat × Elem × Bool
als	Hashset-refines-Set	variable, SetLState
als	Hashset-refines-Set-Theory-Instance	variable, SetLState
alsf	Hashset-refines-Set	variable, Tid → SetLState
alsf	Hashset-refines-Set-Theory-Instance	variable, Tid → SetLState
apc	Hashset-refines-Set	variable, SetPC
apc	Hashset-refines-Set-Theory-Instance	variable, SetPC
apcf	Hashset-refines-Set	variable, Tid → SetPC
apcf	Hashset-refines-Set-Theory-Instance	variable, Tid → SetPC
ar	array	variable, Array('a)
ar	abs	variable, Array(Elem)
ar	Hashset-proofs	variable, Array(Elem)
ar	hashset-preds	variable, Array(Elem)
ar	Hashset	variable, Array(Elem)
ar	Hashset-refines-Set	variable, Array(Elem)
as	Hashset-refines-Set	variable, SetState
as	IOforward	variable, 'as
as	IOrefine-def	variable, 'as
as	IOforward-is-leqrefine	variable, 'as
as	Hashset-refines-Set-Theory-Instance	variable, SetState
asf	IOforward	variable, Nat → 'as
asf	IOrefine-def	variable, Nat → 'as
asf	IOforward-is-leqrefine	variable, Nat → 'as
asl	IOforward	variable, List('as)
asl	IOrefine-def	variable, List('as)
asl	IOforward-is-leqrefine	variable, List('as)
aslf	IOforward-is-leqrefine	variable, Nat → List('as)
astart	IOforward	variable, 'as → Bool
astart	IOrefine-def	variable, 'as → Bool
astart	IOforward-is-leqrefine	variable, 'as → Bool
astep	IOforward	variable, 'as × 'aa × 'as → Bool
astep	IOrefine-def	variable, 'as × 'aa × 'as → Bool
astep	IOforward-is-leqrefine	variable, 'as × 'aa × 'as → Bool
aα	IOforward	variable, Stream('aa)
aα	IOrefine-def	variable, Stream('aa)
aα	IOforward-is-leqrefine	variable, Stream('aa)
aσ	IOforward	variable, Stream('as)
aσ	IOrefine-def	variable, Stream('as)
aσ	IOforward-is-leqrefine	variable, Stream('as)
b	list-getput	variable, 'a
b	array	variable, 'a
b	list-del	variable, 'a
b	optfuns	variable, 'b
b	list-dup	variable, 'a
b	Set-proofs	variable, Bool
b	list	variable, 'b
b	abs	variable, Bool
b	Set-Test-IOAut	variable, Bool
b	Hashset-proofs	variable, Bool
b	list-last	variable, 'a
b	hashset-preds	variable, Bool
b	Hashset	variable, Bool
b	Hashset-refines-Set	variable, Bool
b	Set	variable, Bool
b	Hashset-refines-Set-Theory-Instance	variable, Bool
ba	IOforward	variable, 'ba
bal	IOforward	variable, List('ba)
between	hashset-preds	predicate, Nat × Nat × Nat × Bool
bext	IOforward	variable, 'ba → Opt('e)
bioaut	IOforward	variable, IOAutomaton('bs, 'ba, 'e)
bs	IOforward	variable, 'bs
bsf	IOforward	variable, Nat → 'bs
bsl	IOforward	variable, List('bs)
bstart	IOforward	variable, 'bs → Bool
bstep	IOforward	variable, 'bs × 'ba × 'bs → Bool
bα	IOforward	variable, Stream('ba)
bσ	IOforward	variable, Stream('bs)
c	list-getput	variable, 'a
c	array	variable, 'a
c	list-dup	variable, 'a
c	list-last	variable, 'a
ca	IOforward	variable, 'ca
ca	IOrefine-def	variable, 'ca
ca	IOforward-is-leqrefine	variable, 'ca
caf	IOforward-is-leqrefine	variable, Nat → 'ca
cal	IOforward	variable, List('ca)
cal	IOrefine-def	variable, List('ca)
cal	IOforward-is-leqrefine	variable, List('ca)
cext	IOforward	variable, 'ca → Opt('e)
cext	IOrefine-def	variable, 'ca → Opt('e)
cext	IOforward-is-leqrefine	variable, 'ca → Opt('e)
cioaut	IOforward	variable, IOAutomaton('cs, 'ca, 'e)
cioaut	IOrefine-def	variable, IOAutomaton('cs, 'ca, 'e)
cioaut	IOforward-is-leqrefine	variable, IOAutomaton('cs, 'ca, 'e)
cs	IOforward	variable, 'cs
cs	IOrefine-def	variable, 'cs
cs	IOforward-is-leqrefine	variable, 'cs
cs	Hashset-refines-Set-Theory-Instance	variable, HashsetState
csf	IOforward	variable, Nat → 'cs
csf	IOrefine-def	variable, Nat → 'cs
csf	IOforward-is-leqrefine	variable, Nat → 'cs
csl	IOforward	variable, List('cs)
csl	IOrefine-def	variable, List('cs)
csl	IOforward-is-leqrefine	variable, List('cs)
cstart	IOforward	variable, 'cs → Bool
cstart	IOrefine-def	variable, 'cs → Bool
cstart	IOforward-is-leqrefine	variable, 'cs → Bool
cstep	IOforward	variable, 'cs × 'ca × 'cs → Bool
cstep	IOrefine-def	variable, 'cs × 'ca × 'cs → Bool
cstep	IOforward-is-leqrefine	variable, 'cs × 'ca × 'cs → Bool
cα	IOforward	variable, Stream('aa)
cα	IOrefine-def	variable, Stream('aa)
cα	IOforward-is-leqrefine	variable, Stream('aa)
cσ	IOforward	variable, Stream('cs)
cσ	IOrefine-def	variable, Stream('cs)
cσ	IOforward-is-leqrefine	variable, Stream('cs)
disj	list-dup	predicate, List('a) × List('a)
doINSERT	Hashset	function, Tid × Bool → HashsetAction
doMEMBER	Hashset	function, Tid → HashsetAction
done	hashset-preds	variable, Bool
dummytid	tid	constant, Tid
dups	list-dup	predicate, List('a)
e	Set-proofs	variable, Elem
e	abs	variable, Elem
e	IOtrace	variable, 'e
e	elem	variable, Elem
e	Set-Test-IOAut	variable, Elem
e	Hashset-proofs	variable, Elem
e	opt	variable, 'e
e	remtau	variable, 'e
e	hashset-preds	variable, Elem
e	Hashset	variable, Elem
e	Hashset-refines-Set	variable, Elem
e	IO-Automaton	variable, 'e
e	IO-Aut-data	variable, 'e
e	Set	variable, Elem
e	Hashset-refines-Set-Theory-Instance	variable, Elem
ea	Set-Test-IOAut	variable, EAction
ef	IOtrace	variable, Nat → 'e
ef	remtau	variable, Nat → 'e
ef	IOforward-is-leqrefine	variable, Nat → 'e
el	IOtrace	variable, List('e)
el	Set-Test-IOAut	variable, List(EAction)
el	remtau	variable, List('e)
el	IOforward	variable, List('e)
el	IOrefine-def	variable, List('e)
el	IOforward-is-leqrefine	variable, List('e)
exec	IOtrace	function, IOAutomaton('s, 'a, 'e) → Stream('s) × Stream('a) → Bool
exec*	IOtrace	function, IOAutomaton('s, 'a, 'e) → List('s) × List('a) → Bool
execω	IOtrace	function, IOAutomaton('s, 'a, 'e) → (Nat → 's) × (Nat → 'a) → Bool
ext	IOtrace	variable, 'a → Opt('e)
ext	remtau	variable, 'a → Opt('e)
ext	IO-Automaton	variable, 'a → Opt('e)
ext	IO-Aut-data	variable, 'a → Opt('e)
f	list-del	variable, 'a → 'b
f	optfuns	variable, 'a → Opt('b)
f	stream-basic	variable, Nat → 'a
f	list	variable, 'a → 'b
f	infinite-append	variable, 'a → 'a
fillfirst	list-last	function, Nat × 'a × List('a) → List('a)
finp	stream-basic	predicate, Stream('a)
found	Hashset-proofs	variable, Bool
found	Hashset	variable, Bool
frag	IOtrace	function, IOAutomaton('s, 'a, 'e) → Stream('s) × Stream('a) → Bool
frag*	IOtrace	function, IOAutomaton('s, 'a, 'e) → List('s) × List('a) → Bool
fragv	IOtrace	variable, Stream('s) × Stream('a) → Bool
fragω	IOtrace	function, IOAutomaton('s, 'a, 'e) → (Nat → 's) × (Nat → 'a) → Bool
frome	list-del	function, List('a) × 'a → List('a)
fwsim	IOforward	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × 'as × 'cs → Bool
g	optfuns	variable, 'b → Opt('c)
gabs	Hashset-refines-Set	predicate, HashsetGState × Tid → HashsetLState × Tid → HashsetPC × SetGState × Tid → SetLState × Tid → SetPC
get_hash	hashset-preds	function, Elem × Nat → Nat
gs	Set-proofs	variable, SetGState
gs	Hashset-proofs	variable, HashsetGState
gs	Hashset	variable, HashsetGState
gs	Hashset-refines-Set	variable, HashsetGState
gs	Set	variable, SetGState
gs	Hashset-refines-Set-Theory-Instance	variable, HashsetGState
gstate	Set-proofs	variable, SetGState
gstate	Set-Test-IOAut	variable, SetGState
gstate	Hashset-proofs	variable, HashsetGState
gstate	Hashset	variable, HashsetGState
gstate	Set	variable, SetGState
gstepf	Hashset	function, HashsetGState × HashsetLState × HashsetPC × HashsetAction → HashsetGState
gstepf	Set	function, SetGState × SetLState × SetPC × SetAction → SetGState
hashsetExt	Hashset-refines-Set-Theory-Instance	function, HashsetAction → Opt(EAction)
hashsetInit	Hashset	predicate, HashsetState
hashsetStep	Hashset	predicate, HashsetState × HashsetAction × HashsetState
hd	stream	partial function, Stream('a) → 'a
head	list-data	variable, 'a
htok	hashset-preds	predicate, Array(Elem)
iNV	IOtrace	variable, 's → Bool
idle	Hashset	constant, HashsetPC
idle	Set	constant, SetPC
ii	infinite-append	variable, Nat → Nat
ii	IOtrace	variable, Nat → Nat
iigen	infinite-append	variable, Nat → Nat → Nat
invINSERT	Hashset	function, Tid × Elem → HashsetAction
invINSERTe	Hashset-proofs	variable, Elem
invINSERTe	Hashset	variable, Elem
invInsert	Set	constant, SetPC
invMEMBER	Hashset	function, Tid × Elem → HashsetAction
invMEMBERe	Hashset-proofs	variable, Elem
invMEMBERe	Hashset	variable, Elem
invMember	Set	constant, SetPC
ioa	IOtrace	variable, IOAutomaton('s, 'a, 'e)
ioa	IO-Automaton	variable, IOAutomaton('s, 'a, 'e)
ioaut	IO-Aut-data	variable, IOAutomaton('s, 'a, 'e)
jj	infinite-append	variable, Nat → Nat
l	stream-basic	variable, List('a)
labs	Hashset-refines-Set	predicate, HashsetGState × HashsetLState × HashsetPC × SetGState × SetLState × SetPC
lb	Set-proofs	variable, Bool
lb	Hashset-refines-Set	variable, Bool
lb	Set	variable, Bool
le	Set-proofs	variable, Elem
le	Hashset-refines-Set	variable, Elem
le	Set	variable, Elem
lf	infinite-append	variable, Nat → List('a)
lfgen	infinite-append	variable, Nat → Nat → List('a)
ls	Set-proofs	variable, SetLState
ls	Hashset-proofs	variable, HashsetLState
ls	Hashset	variable, HashsetLState
ls	Hashset-refines-Set	variable, HashsetLState
ls	Set	variable, SetLState
ls	Hashset-refines-Set-Theory-Instance	variable, HashsetLState
lsf	Set-proofs	variable, Tid → SetLState
lsf	Set-Test-IOAut	variable, Tid → SetLState
lsf	Hashset-proofs	variable, Tid → HashsetLState
lsf	Hashset	variable, Tid → HashsetLState
lsf	Hashset-refines-Set	variable, Tid → HashsetLState
lsf	Set	variable, Tid → SetLState
lsf	Hashset-refines-Set-Theory-Instance	variable, Tid → HashsetLState
lstep	Hashset	predicate, HashsetGState × HashsetLState × HashsetPC × HashsetAction × HashsetGState × HashsetLState × HashsetPC
lstep	Set	predicate, SetGState × SetLState × SetPC × SetAction × SetGState × SetLState × SetPC
lstepf	Hashset	function, HashsetGState × HashsetLState × HashsetPC × HashsetAction → HashsetLState
lstepf	Set	function, SetGState × SetLState × SetPC × SetAction → SetLState
m	list-getput	variable, Nat
m	nat-div	variable, Nat
m	array	variable, Nat
m	list-del	variable, Nat
m	nat-mult	variable, Nat
m	nat-inf	variable, Nat
m	stream-basic	variable, Nat
m	infinite-append	variable, Nat
m	IOtrace	variable, Nat
m	stream	variable, Nat
m	Set-Test-IOAut	variable, Nat
m	Hashset-proofs	variable, Nat
m	list-last	variable, Nat
m	remtau	variable, Nat
m	hashset-preds	variable, Nat
m	Hashset	variable, Nat
min	nat-inf	function, Natinf × Natinf → Natinf
mkar	hashset-preds	function, Nat × Elem → Array(Elem)
mkarray	array	function, Nat × 'a → Array('a)
mkarray	array	function, Nat → Array('a)
mkgs	Hashset	function, Array(Elem) → HashsetGState
mkgs	Set	function, Set(Elem) → SetGState
mklist	list-last	function, 'a × Nat → List('a)
mkls	Hashset	function, Tid × Elem × Bool × Nat × Nat × Nat × Elem → HashsetLState
mkls	Set	function, Tid × Elem × Bool → SetLState
mkstate	Hashset	function, HashsetGState × Tid → HashsetLState × Tid → HashsetPC → HashsetState
mkstate	Set	function, SetGState × Tid → SetLState × Tid → SetPC → SetState
move	IOtrace	function, IOAutomaton('s, 'a, 'e) → 's × List('e) × 's → Bool
movev	IOtrace	variable, 's × Stream('e) × 's → Bool
n	list-getput	variable, Nat
n	nat-div	variable, Nat
n	array	variable, Nat
n	list-del	variable, Nat
n	nat-mult	variable, Nat
n	nat-inf	variable, Nat
n	infinite-append	variable, Nat
n	abs	variable, Nat
n	IOtrace	variable, Nat
n	stream	variable, Nat
n	Set-Test-IOAut	variable, Nat
n	Hashset-proofs	variable, Nat
n	list-data	variable, Nat
n	list-last	variable, Nat
n	remtau	variable, Nat
n	hashset-preds	variable, Nat
n	Hashset	variable, Nat
n	Hashset-refines-Set	variable, Nat
n	IOforward-is-leqrefine	variable, Nat
nexta	infinite-append	variable, Nat × 'a → 'a
nextaal	IOforward-is-leqrefine	variable, Nat × 'as → List('aa)
nextasl	IOforward-is-leqrefine	variable, Nat × 'as → List('as)
nextj	infinite-append	variable, Nat × 'a → Nat
nextl	infinite-append	variable, Nat × 'a → List('a)
nf	stream-basic	variable, Nat → 'a
nf	infinite-append	variable, Nat → 'a
nf	stream	variable, Nat → 'a
nfgen	infinite-append	variable, Nat → Nat → 'a
n∞	nat-inf	variable, Natinf
n∞	stream	variable, Natinf
o	optfuns	function, 'a → Opt('b) × 'b → Opt('c) → 'a → Opt('c)
oe	IOtrace	variable, Opt('e)
oe	opt	variable, Opt('e)
oe	remtau	variable, Opt('e)
oe	IO-Automaton	variable, Opt('e)
oe	IO-Aut-data	variable, Opt('e)
oinj	optfuns	predicate, 'a → Opt('b)
osurj	optfuns	predicate, 'a → Opt('b)
pc	Set-proofs	variable, SetPC
pc	Hashset-proofs	variable, HashsetPC
pc	Hashset	variable, HashsetPC
pc	Hashset-refines-Set	variable, HashsetPC
pc	Set	variable, SetPC
pc	Hashset-refines-Set-Theory-Instance	variable, HashsetPC
pcf	Set-proofs	variable, Tid → SetPC
pcf	Set-Test-IOAut	variable, Tid → SetPC
pcf	Hashset-proofs	variable, Tid → HashsetPC
pcf	Hashset	variable, Tid → HashsetPC
pcf	Hashset-refines-Set	variable, Tid → HashsetPC
pcf	Set	variable, Tid → SetPC
pcf	Hashset-refines-Set-Theory-Instance	variable, Tid → HashsetPC
pcstepf	Hashset	function, HashsetGState × HashsetLState × HashsetPC × HashsetAction → HashsetPC
pcstepf	Set	function, SetGState × SetLState × SetPC × SetAction → SetPC
pre	Hashset	predicate, HashsetGState × HashsetLState × HashsetPC × HashsetAction
pre	Set	predicate, SetGState × SetLState × SetPC × SetAction
r	IOforward	variable, 'as × 'cs → Bool
r	IOforward-is-leqrefine	variable, 'as × 'cs → Bool
rab	IOforward	variable, 'as × 'bs → Bool
rbc	IOforward	variable, 'bs × 'cs → Bool
rely	hashset-preds	predicate, Array(Elem) × Array(Elem)
ren	Hashset-refines-Set	function, HashsetAction × SetGState × Tid → SetLState → SetAction
retINSERT	Hashset	function, Tid × Bool → HashsetAction
retINSERTb	Hashset-proofs	variable, Bool
retINSERTb	Hashset	variable, Bool
retInsert	Set	constant, SetPC
retMEMBER	Hashset	function, Tid × Bool → HashsetAction
retMEMBERb	Hashset-proofs	variable, Bool
retMEMBERb	Hashset	variable, Bool
retMember	Set	constant, SetPC
rev	list-last	function, List('a) → List('a)
s	Set-proofs	variable, SetState
s	IOtrace	variable, 's
s	Set-Test-IOAut	variable, SetState
s	Hashset-proofs	variable, HashsetState
s	set-basic	variable, Set('a)
s	Hashset	variable, HashsetState
s	Hashset-refines-Set	variable, HashsetState
s	IO-Automaton	variable, 's
s	IO-Aut-data	variable, 's
s	Set	variable, SetState
set	Set-proofs	variable, Set(Elem)
set	abs	variable, Set(Elem)
set	Hashset-refines-Set	variable, Set(Elem)
set	Set	variable, Set(Elem)
setExt	Set-Test-IOAut	function, SetAction → Opt(EAction)
setInit	Set	predicate, SetState
setStep	Set	predicate, SetState × SetAction × SetState
sf	IOtrace	variable, Nat → 's
sl	IOtrace	variable, List('s)
sl	Set-Test-IOAut	variable, List(SetState)
slf	IOtrace	variable, Nat → List('s)
start	IOtrace	variable, 's → Bool
start	IO-Automaton	variable, 's → Bool
start	IO-Aut-data	variable, 's → Bool
step	IOtrace	variable, 's × 'a × 's → Bool
step	IO-Automaton	variable, 's × 'a × 's → Bool
step	IO-Aut-data	variable, 's × 'a × 's → Bool
sz	Hashset-proofs	variable, Nat
sz	hashset-preds	variable, Nat
sz	Hashset	variable, Nat
tail	list-data	variable, List('a)
tid	tid	variable, Tid
tid	Set-proofs	variable, Tid
tid	Set-Test-IOAut	variable, Tid
tid	Hashset-proofs	variable, Tid
tid	hashset-preds	variable, Tid
tid	Hashset	variable, Tid
tid	Hashset-refines-Set	variable, Tid
tid	Set	variable, Tid
tid	Hashset-refines-Set-Theory-Instance	variable, Tid
tl	stream	partial function, Stream('a) → Stream('a)
trace	IOtrace	function, IOAutomaton('s, 'a, 'e) → Stream('e) → Bool
trace*	IOtrace	function, IOAutomaton('s, 'a, 'e) → List('e) → Bool
tracev	IOtrace	variable, Stream('e) → Bool
traceω	IOtrace	function, IOAutomaton('s, 'a, 'e) → (Nat → 'e) → Bool
x	list-getput	variable, List('a)
x	list-del	variable, List('a)
x	stream-basic	variable, List('a)
x	list-dup	variable, List('a)
x	list	variable, List('a)
x	stream	variable, List('a)
x	list-data	variable, List('a)
x	list-last	variable, List('a)
y	list-getput	variable, List('a)
y	list-del	variable, List('a)
y	list-dup	variable, List('a)
y	list	variable, List('a)
y	stream	variable, List('a)
y	list-data	variable, List('a)
y	list-last	variable, List('a)
z	list-getput	variable, List('a)
z	list-del	variable, List('a)
z	list-dup	variable, List('a)
z	list	variable, List('a)
z	stream	variable, List('a)
z	list-data	variable, List('a)
z	list-last	variable, List('a)
α	IOtrace	variable, Stream('a)
α	remtau	variable, Stream('a)
β	IOtrace	variable, Stream('e)
β	remtau	variable, Stream('e)
β	IOforward	variable, Stream('e)
β	IOrefine-def	variable, Stream('e)
β	IOforward-is-leqrefine	variable, Stream('e)
σ	stream-basic	variable, Stream('a)
σ	infinite-append	variable, Stream('a)
σ	IOtrace	variable, Stream('s)
σ	stream	variable, Stream('a)
τ	opt	constant, Opt('e)
τ	Hashset	constant, HashsetAction
τ	Set	constant, SetAction
∅	set-basic	constant, Set('a)
∈	list	predicate, 'a × List('a)
∈	set-basic	predicate, 'a × Set('a)
∞	nat-inf	constant, Natinf
≤	nat	predicate, Nat × Nat
≤F	IOforward	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≥	nat	predicate, Nat × Nat
⊆	set-basic	predicate, Set('a) × Set('a)
⊑	stream	predicate, Stream('a) × Stream('a)
⊑	list-last	predicate, List('a) × List('a)
⊒	list-last	predicate, List('a) × List('a)
⊥	elem	constant, Elem
⊥	Set	constant, Elem
⌝	nat-inf	function, Nat → Natinf
⌝	stream-basic	function, Nat → 'a → Stream('a)
⌝	stream-basic	function, List('a) → Stream('a)
⌝	opt	function, 'e → Opt('e)