[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,
Used simplifier rules/spec theorems by specification
Used from specification linked-tree
Used from specification heap-sep
Used from specification set-union
Used from specification search-tree
- search-tree/delete-prepost
is used by
refine-delete-min,
- search-tree/insert-prepost
is used by
refine-insert,
- search-tree/leftmost-ismin
is used by
set-min,
- search-tree/butleftmost-bst
is used by
refine-delete-min,
- search-tree/butleftmost-in
is used by
set-butmin,
- search-tree/in-branch
is used by
set-branch,
- search-tree/in-leaf
is used by
set-leaf,
- search-tree/insert-bst
is used by
refine-insert,
- search-tree/insert-in
is used by
set-insert,
- search-tree/leftmost-in
is used by
set-min,
set-butmin,
Used from specification set-basic
- set-basic/Extension
is used by
set-leaf,
set-insert,
set-butmin,
set-branch,
- set-basic/In-empty
is used by
set-leaf,
set-butmin,
- set-basic/rax
is used by
set-insert,
set-branch,
- set-basic/size-zero
is used by
set-leaf,
refine-delete-min,
- set-basic/size-zero-01
is used by
set-leaf,
refine-delete-min,
Used from specification oelem
Used from specification oset