[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
. * .heap-sepf(heap → bool) × (heap → bool) → heap → bool
. * .heap-aux-instf(heap-aux → bool) × (heap-aux → bool) → heap-aux → bool
. + .nat-basicfnat × nat → nat
. ++ .refsetfrefset × ref → refset
. ++ .heapfheap × ref → heap
. ++ .heap-aux-instfheap-aux × ref → heap-aux
. +1nat-basicfnat → nat
. - .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
. .nxtcellfcell → ref
. .nxt:= .cellfcell × ref → cell
. .objcell-heap-auxfobjaux → cell
. .valcellfcell → elem
. .val:= .cellfcell × elem → cell
. < .nat-basicpnat × nat
. ==> ( . )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
. ∩ .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
__∃ .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
{ . }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
auxauxs
cellcells
dom .heapfheap → refset
dom .heap-aux-instfheap-aux → refset
elemelems
empheap-seppheap
empheap-aux-instpheap-aux
falseheap-seppheap
falseheap-aux-instpheap-aux
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
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
objauxobj-auxs
owns-nonergpaux × refset × (ref → aux)
owns-onergpaux × ref × refset × (ref → aux)
preciseheap-sepp(heap → bool)
preciseheap-aux-instp(heap-aux → bool)
refrefs
refsetrefsets
relycell-heap-auxpaux × refset × (ref → cell) × (ref → aux) × refset × (ref → cell) × (ref → aux)
trueheap-seppheap
trueheap-aux-instpheap-aux