[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
# .refsetfrefset → nat
# .heapfheap → nat
# .heap-aux-instfheap-aux → nat
# .list-dataflist → nat
. 'listfelem → list
. * .heap-sepf(heap → bool) × (heap → bool) → heap → bool
. * .heap-aux-instf(heap-aux → bool) × (heap-aux → bool) → heap-aux → bool
. + .nat-basicfnat × nat → nat
. + .list-datafelem × list → list
. + .listflist × list → list
. + .listflist × elem → list
. ++ .refsetfrefset × ref → refset
. ++ .heapfheap × ref → heap
. ++ .heap-aux-instfheap-aux × ref → heap-aux
. +1nat-basicfnat → nat
. +2 .listfelem × elem → list
. - .natpfnat × nat → nat with λ n, m. n ≥ m
. -* .heap-sepf(heap → bool) × (heap → bool) → heap → bool
. -* .heap-aux-instf(heap-aux → bool) × (heap-aux → bool) → heap-aux → bool
. -- .refsetfrefset × ref → refset
. -- .heapfheap × ref → heap
. -- .heap-aux-instfheap-aux × ref → heap-aux
. -> .heap-sepf(heap → bool) × (heap → bool) → heap → bool
. -> .heap-aux-instf(heap-aux → bool) × (heap-aux → bool) → heap-aux → bool
. -⊗ .heap-sepf(heap → bool) × (heap → bool) → heap → bool
. -⊗ .heap-aux-instf(heap-aux → bool) × (heap-aux → bool) → heap-aux → bool
. -1nat-basicpfnat → nat with λ n. n ≠ 0
. .auxobj-auxfobjaux → aux
. .headlist-datapflist → elem with λ x. x ≠ []
. .nxtcellfcell → ref
. .nxt:= .cellfcell × ref → cell
. .objcell-heap-auxfobjaux → cell
. .taillist-datapflist → list with λ x. x ≠ []
. .valcellfcell → elem
. .val:= .cellfcell × elem → cell
. < .nat-basicpnat × nat
. < .list-dataplist × list
. ==> ( . )cell-heap-auxfref × cell × aux → heap-aux → bool
. ==>?heap-aux-instfref → heap-aux → bool
. ==>_heap-aux-instfref → heap-aux → bool
. => .cell-heap-auxfref × cell → heap → bool
. =>?mapletfref → heap → bool
. =>_mapletfref → heap → bool
. > .natpnat × nat
. [ . ]cell-heap-auxfheap × ref → cell
. [ . ]cell-heap-auxfheap × ref × cell → heap
. [ . ]cell-heap-auxfheap-aux × ref × cell × aux → heap-aux
. [ . ]embed-auxfaux × (heap → bool) → heap-aux → bool
. [ . ]cell-heap-auxp(heap → bool) × refset × (ref → cell)
. [ . ]cell-heap-auxp(heap-aux → bool) × refset × (ref → cell) × (ref → aux)
. [ . ]__heap-aux-instfheap-aux × ref → objaux
. [ . ]__heap-aux-instfheap-aux × ref × objaux → heap-aux
. [ . ]__heap-aux-instp(heap-aux → bool) × refset × (ref → objaux)
. [ . ]aheap-auxfheap-aux × ref → aux
. [ . ]ocell-heap-auxfheap-aux × ref → cell
. \ .refsetfrefset × refset → refset
. \ .heapfheap × refset → heap
. \ .heapfheap × heap → heap
. \ .heap-aux-instfheap-aux × refset → heap-aux
. \ .heap-aux-instfheap-aux × heap-aux → heap-aux
. __=> ( . )heap-aux-instfref × objaux → heap-aux → bool
. × .cellfelem × ref → cell
. ×× .cell-heap-auxfcell × aux → objaux
. ∈ .refsetpref × refset
. ∈ .heappref × heap
. ∈ .heap-aux-instpref × heap-aux
. ∈ .listpelem × list
. ∩ .refsetfrefset × refset → refset
. ∪ .refsetfrefset × refset → refset
. ∪ .heapfheap × heap → heap
. ∪ .heap-aux-instfheap-aux × heap-aux → heap-aux
. ≤ .natpnat × nat
. ≥ .natpnat × nat
. ⊆ .refsetprefset × refset
. ⊆ .heappheap × heap
. ⊆ .heap-sepp(heap → bool) × (heap → bool)
. ⊆ .heap-aux-instpheap-aux × heap-aux
. ⊆ .heap-aux-instp(heap-aux → bool) × (heap-aux → bool)
. ⊗ .heap-sepf(heap → bool) × (heap → bool) → heap → bool
. ⊗ .heap-aux-instf(heap-aux → bool) × (heap-aux → bool) → heap-aux → bool
. ⊥ .heappheap × heap
. ⊥ .heap-aux-instpheap-aux × heap-aux
. and .heap-sepf(heap → bool) × (heap → bool) → heap → bool
. and .heap-aux-instf(heap-aux → bool) × (heap-aux → bool) → heap-aux → bool
. or .heap-sepf(heap → bool) × (heap → bool) → heap → bool
. or .heap-aux-instf(heap-aux → bool) × (heap-aux → bool) → heap-aux → bool
[]list-dataclist
__∃ .heap-aux-instf(objaux → heap-aux → bool) → heap-aux → bool
__mkheap-aux-instfrefset × (ref → objaux) → heap-aux
_∃ .mapletf(ref → heap → bool) → heap → bool
_∃ .mapletf(ref × ref → heap → bool) → heap → bool
_∃ .cell-heap-auxf(cell → heap → bool) → heap → bool
_∃ .heap-aux-instf(ref → heap-aux → bool) → heap-aux → bool
_∃ .heap-aux-instf(ref × ref → heap-aux → bool) → heap-aux → bool
_∃ .cell-heap-auxf(cell × aux → heap-aux → bool) → heap-aux → bool
_∃ .linked-list-auxf(list → heap → bool) → heap → bool
{ . }refsetfref → refset
{ . }heap-sepfheap → heap → bool
{ . }heap-aux-instfheap-aux → heap-aux → bool
∅refsetcrefset
∅heapcheap
∅heap-aux-instcheap-aux
⌜ . ⌝heap-sepfbool → heap → bool
⌜ . ⌝heap-aux-instfbool → heap-aux → bool
alinked-list-auxvelem
aflinked-list-auxvref → aux
auxauxs
celinked-list-auxvcell
cellcells
cflinked-list-auxvref → cell
dom .heapfheap → refset
dom .heap-aux-instfheap-aux → refset
elemelems
empheap-seppheap
empheap-aux-instpheap-aux
falseheap-seppheap
falseheap-aux-instpheap-aux
hlinked-list-auxvheap
hPlinked-list-auxvheap → bool
hRlinked-list-auxvheap-aux → bool
heapheaps
heap-auxheap-aux-insts
iteheap-sepfbool × (heap → bool) × (heap → bool) → heap → bool
iteheap-aux-instfbool × (heap-aux → bool) × (heap-aux → bool) → heap-aux → bool
listlist-datas
lslinked-list-auxfref × list → heap → bool
lstlinked-list-auxfref → heap → bool
mkcell-heap-auxfrefset × (ref → cell) → heap
mkcell-heap-auxfrefset × (ref → cell) × (ref → aux) → heap-aux
natnat-basics
not .heap-sepf(heap → bool) → heap → bool
not .heap-aux-instf(heap-aux → bool) → heap-aux → bool
nullrefcref
olinked-list-auxvaux
objauxobj-auxs
owns-nonergpaux × refset × (ref → aux)
owns-onergpaux × ref × refset × (ref → aux)
preciseheap-sepp(heap → bool)
preciseheap-aux-instp(heap-aux → bool)
rlinked-list-auxvref
refrefs
refsetrefsets
relycell-heap-auxpaux × refset × (ref → cell) × (ref → aux) × refset × (ref → cell) × (ref → aux)
rslinked-list-auxvrefset
trueheap-seppheap
trueheap-aux-instpheap-aux
xlinked-list-auxvlist
xvlinked-list-auxvlist → heap → bool
ylinked-list-auxvlist