[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 store+set
Used from specification znode-ops
- znode-ops/load-node
is used by
unmodified-load,
- znode-ops/save-branches-last
is used by
save-same-payload-same,
- znode-ops/save-load-save
is used by
unmodified-reload,
payload-save-load-same,
- znode-ops/save-node
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-save,
unmodified-same-payload-subseteq,
unmodified-same-payload,
unmodified-reload,
unmodified-payload,
unmodified-load-key-node,
unmodified-load-key-leaf,
unmodified-load-adr-node,
unmodified-key-range-node,
unmodified-clean-leaf-subseteq,
unmodified-clean-leaf,
unmodified-clean-fwd-zbrar2,
unmodified-clean-fwd-zbrar,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
unmodified-clean-eq-adr-subseteq,
- znode-ops/scan-last
is used by
look-scan-range,
- znode-ops/scan-le-0
is used by
look-scan-range,
- znode-ops/scan-lt-0
is used by
look-scan-range,
- znode-ops/at-load-0
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-payload,
unmodified-key-range-node,
range-load-save,
- znode-ops/at-save-0
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-payload,
unmodified-load-key-node,
unmodified-load-key-leaf,
unmodified-load-adr-node,
unmodified-key-range-node,
unmodified-clean-fwd-zbrar2,
unmodified-clean-fwd-zbrar,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
unmodified-clean-eq-adr-subseteq,
range-load-save,
- znode-ops/at-save-out-upper
is used by
save-same-payload-same,
- znode-ops/at-shl
is used by
sorted-shift-left,
payload-shift-left,
keys-shift-left,
- znode-ops/load-branch
is used by
unmodified-load-adr-node,
- znode-ops/load-entry
is used by
unmodified-payload,
unmodified-load-adr-node,
- znode-ops/load-save-entry
is used by
unmodified-payload,
- znode-ops/load-save-key
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-payload,
unmodified-load-key-node,
unmodified-load-key-leaf,
unmodified-key-range-node,
range-load-save,
- znode-ops/load-size
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-payload,
unmodified-key-range-node,
range-load-save,
payload-save-load-same,
- znode-ops/save-branch
is used by
unmodified-load-adr-node,
unmodified-clean-fwd-zbrar2,
unmodified-clean-fwd-zbrar,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
unmodified-clean-eq-adr-subseteq,
save-same-payload-same,
- znode-ops/save-branches-base
is used by
save-same-payload-same,
- znode-ops/save-entry
is used by
unmodified-payload,
unmodified-load-adr-node,
unmodified-clean-fwd-zbrar2,
unmodified-clean-fwd-zbrar,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
save-same-payload-same,
- znode-ops/save-properties
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-same-payload-subseteq,
unmodified-same-payload,
unmodified-reload,
unmodified-payload,
unmodified-load-key-node,
unmodified-load-key-leaf,
unmodified-load-adr-node,
unmodified-load,
unmodified-key-range-node,
unmodified-clean-leaf-subseteq,
unmodified-clean-leaf,
unmodified-clean-fwd-zbrar2,
unmodified-clean-fwd-zbrar,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
unmodified-clean-eq-adr-subseteq,
- znode-ops/save-size
is used by
unmodified-clean-fwd-zbrar2,
unmodified-clean-fwd-zbrar,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
unmodified-clean-eq-adr-subseteq,
save-same-payload-same,
- znode-ops/scan-base
is used by
look-scan-range,
- znode-ops/scan-max-0
is used by
look-scan-range,
- znode-ops/scan-min-eq
is used by
look-scan-range,
- znode-ops/scan-rec
is used by
look-scan-range,
- znode-ops/size-shl
is used by
sorted-shift-left,
payload-shift-left,
keys-shift-left,
Used from specification nat-basic
- nat-basic/a
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-same-payload-subseteq,
unmodified-same-payload,
unmodified-reload,
unmodified-payload,
unmodified-load-key-node,
unmodified-load-adr-node,
unmodified-key-range-node,
sorted-shift-left,
save-same-payload-same,
range-put,
range-load-save,
range-le,
range-last-2,
range-gt,
range,
payload-split,
payload-shift-left,
payload-save-load-same,
payload-one,
payload-mod-0,
payload-mod,
payload-keys-0,
payload-drop-upper,
payload-drop-lower,
payload-copy-right-upper,
payload-copy-right-lower-0,
payload-copy-right-lower,
look-subrange,
look-scan-range,
keys-shift-left,
keys-mod-0,
keys-mod,
keys-drop-upper,
keys-drop-lower,
key-range-replace-branches,
keep-range,
in-playload-data,
in-payload,
in-keys,
in-keyrange-in-ri-data,
in-keyrange-in-ri,
at-range,
at-payload,
- nat-basic/add-base
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-same-payload-subseteq,
unmodified-same-payload,
unmodified-reload,
unmodified-payload,
sorted-shift-left,
range-last-2,
payload-split,
payload-shift-left,
payload-save-load-same,
payload-mod-0,
payload-mod,
payload-keys-0,
payload-copy-right-lower-0,
payload-copy-right-lower,
keys-shift-left,
keys-mod-0,
keys-mod,
in-playload-data,
in-payload,
in-keys,
at-payload,
- nat-basic/c
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-same-payload-subseteq,
unmodified-same-payload,
unmodified-reload,
unmodified-payload,
unmodified-load-key-node,
unmodified-load-adr-node,
unmodified-key-range-node,
sorted-shift-left,
save-same-payload-same,
range-put,
range-load-save,
range-le,
range-last-2,
range-gt,
range,
payload-split,
payload-shift-left,
payload-save-load-same,
payload-one,
payload-mod-0,
payload-mod,
payload-keys-0,
payload-keys,
payload-drop-upper,
payload-drop-lower,
payload-copy-right-upper,
payload-copy-right-lower-0,
payload-copy-right-lower,
look-subrange,
look-scan-range,
keys-shift-left,
keys-mod-0,
keys-mod,
keys-drop-upper,
keys-drop-lower,
key-range-replace-branches,
keep-range,
in-playload-data,
in-payload,
in-keys,
in-keyrange-in-ri-data,
in-keyrange-in-ri,
at-range,
at-payload,
- nat-basic/eq-01
is used by
unmodified-sorted-node,
unmodified-load-key-node,
unmodified-load-adr-node,
unmodified-key-range-node,
payload-shift-left,
look-scan-range,
- nat-basic/eq-02
is used by
payload-mod,
payload-drop-lower,
look-scan-range,
keys-mod,
keys-drop-lower,
keep-range,
in-playload-data,
- nat-basic/f
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-payload,
unmodified-load-key-node,
unmodified-load-key-leaf,
unmodified-load-adr-node,
unmodified-key-range-node,
unmodified-clean-fwd-zbrar2,
unmodified-clean-fwd-zbrar,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
unmodified-clean-eq-adr-subseteq,
sorted-shift-left,
save-same-payload-same,
range-put,
range-load-save,
range-le,
range-last-2,
range-gt,
range-emp,
range,
payload-split,
payload-shift-left,
payload-one,
payload-mod-0,
payload-mod,
payload-keys,
payload-drop-upper,
payload-drop-lower,
payload-copy-right-upper,
payload-copy-right-lower-0,
payload-copy-right-lower,
nsize-size,
look-subrange,
look-scan-range,
keys-shift-left,
keys-mod-0,
keys-mod,
keys-drop-upper,
keys-drop-lower,
key-range-replace-branches,
keep-range,
in-playload-data,
in-payload,
in-keys,
in-keyrange-in-ri-data,
in-keyrange-in-ri,
at-range,
at-payload,
- nat-basic/l
is used by
sorted-shift-left,
payload-shift-left,
payload-drop-lower,
payload-copy-right-upper,
keys-drop-lower,
in-playload-data,
- nat-basic/l-01
is used by
unmodified-key-range-node,
range-load-save,
payload-copy-right-upper,
payload-copy-right-lower,
in-playload-data,
- nat-basic/l-02
is used by
unmodified-sorted-node,
unmodified-key-range-node,
sorted-shift-left,
payload-shift-left,
payload-mod,
payload-drop-upper,
payload-drop-lower,
payload-copy-right-lower,
keys-shift-left,
keys-mod,
keys-drop-upper,
keys-drop-lower,
in-playload-data,
- nat-basic/l-05
is used by
payload-shift-left,
key-range-replace-branches,
- nat-basic/l-08
is used by
sorted-shift-left,
payload-shift-left,
- nat-basic/lf
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-payload,
unmodified-load-key-node,
unmodified-key-range-node,
sorted-shift-left,
range-load-save,
payload-shift-left,
payload-copy-right-upper,
keys-shift-left,
key-range-replace-branches,
in-playload-data,
at-payload,
- nat-basic/lf-01
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-payload,
unmodified-key-range-node,
unmodified-clean-fwd-zbrar2,
unmodified-clean-fwd-zbrar,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
unmodified-clean-eq-adr-subseteq,
save-same-payload-same,
range-put,
range-load-save,
range-gt,
payload-shift-left,
look-scan-range,
key-range-replace-branches,
keep-range,
at-range,
- nat-basic/lf-02
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-payload,
range-put,
range-load-save,
payload-shift-left,
look-scan-range,
key-range-replace-branches,
keep-range,
at-range,
- nat-basic/ls-02
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-payload,
unmodified-load-key-node,
unmodified-key-range-node,
sorted-shift-left,
range-load-save,
payload-shift-left,
nsize-size,
keys-shift-left,
- nat-basic/neq-04
is used by
unmodified-key-range-node,
- nat-basic/nls-fst
is used by
payload-split,
payload-copy-right-upper,
key-range-replace-branches,
in-playload-data,
in-payload,
in-keys,
at-payload,
- nat-basic/one
is used by
range-le,
payload-copy-right-upper,
- nat-basic/one-01
is used by
unmodified-key-range-node,
range-load-save,
payload-shift-left,
look-subrange,
keep-range,
- nat-basic/one-03
is used by
range-le,
range,
look-subrange,
- nat-basic/one-06
is used by
unmodified-key-range-node,
look-subrange,
look-scan-range,
- nat-basic/oz
is used by
unmodified-key-range-node,
range-put,
range-le,
range-last-2,
range,
payload-shift-left,
payload-mod,
payload-drop-lower,
look-scan-range,
keys-shift-left,
keys-mod,
keys-drop-lower,
key-range-replace-branches,
keep-range,
in-playload-data,
in-keyrange-in-ri-data,
at-range,
- nat-basic/s-04
is used by
unmodified-sorted-node,
unmodified-load-key-node,
unmodified-load-adr-node,
unmodified-key-range-node,
sorted-shift-left,
range-put,
range-load-save,
payload-shift-left,
payload-mod,
look-scan-range,
keys-shift-left,
keys-mod,
key-range-replace-branches,
keep-range,
in-playload-data,
in-payload,
in-keys,
in-keyrange-in-ri-data,
at-range,
at-payload,
- nat-basic/succ
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-payload,
unmodified-load-key-node,
sorted-shift-left,
save-same-payload-same,
range-put,
range-le,
range,
payload-split,
payload-shift-left,
payload-mod,
payload-drop-upper,
payload-drop-lower,
payload-copy-right-upper,
payload-copy-right-lower,
look-scan-range,
keys-shift-left,
keys-mod,
keys-drop-upper,
keys-drop-lower,
key-range-replace-branches,
keep-range,
in-playload-data,
in-payload,
in-keys,
at-range,
at-payload,
- nat-basic/succ-03
is used by
range,
key-range-replace-branches,
in-keyrange-in-ri-data,
- nat-basic/z-01
is used by
look-scan-range,
- nat-basic/zero
is used by
unmodified-key-range-node,
range-put,
range-load-save,
range,
payload-shift-left,
payload-mod,
key-range-replace-branches,
keep-range,
in-keyrange-in-ri-data,
in-keyrange-in-ri,
at-range,
- nat-basic/zero-01
is used by
payload-shift-left,
payload-mod,
keys-mod,
in-payload,
in-keys,
at-payload,
Used from specification zbranch
- zbranch/disj-02
is used by
unmodified-clean-fwd-zbrar2,
unmodified-clean-fwd-zbrar,
- zbranch/elim-03
is used by
unmodified-payload,
save-same-payload-same,
payload-split,
payload-shift-left,
payload-mod,
payload-keys,
payload-drop-upper,
payload-drop-lower,
payload-copy-right-upper,
in-playload-data,
in-payload,
at-payload,
- zbranch/inj
is used by
unmodified-clean-fwd-zbrar,
- zbranch/inj-01
is used by
payload-shift-left,
in-playload-data,
in-payload,
- zbranch/sel-02
is used by
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
- zbranch/sel-03
is used by
unmodified-load-adr-node,
- zbranch/sel-04
is used by
unmodified-payload,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
save-same-payload-same,
payload-shift-left,
payload-mod,
payload-keys,
keys-mod,
in-payload,
at-payload,
- zbranch/sel-08
is used by
unmodified-load-adr-node,
save-same-payload-same,
payload-mod,
in-playload-data,
at-payload,
- zbranch/test-05
is used by
unmodified-payload,
save-same-payload-same,
payload-split,
payload-shift-left,
payload-mod,
payload-keys,
payload-drop-upper,
payload-drop-lower,
payload-copy-right-upper,
in-playload-data,
in-payload,
at-payload,
- zbranch/test-06
is used by
save-same-payload-same,
Used from specification znode
- znode/sel-02
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-save,
unmodified-same-payload-subseteq,
unmodified-same-payload,
unmodified-reload,
unmodified-payload,
unmodified-load-key-node,
unmodified-load-key-leaf,
unmodified-load-adr-node,
unmodified-key-range-node,
unmodified-clean-leaf-subseteq,
unmodified-clean-leaf,
unmodified-clean-fwd-zbrar2,
unmodified-clean-fwd-zbrar,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
unmodified-clean-eq-adr-subseteq,
- znode/sel-03
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-save,
unmodified-same-payload-subseteq,
unmodified-same-payload,
unmodified-reload,
unmodified-payload,
unmodified-load-key-node,
unmodified-load-key-leaf,
unmodified-load-adr-node,
unmodified-load,
unmodified-key-range-node,
unmodified-clean-leaf-subseteq,
unmodified-clean-leaf,
unmodified-clean-fwd-zbrar2,
unmodified-clean-fwd-zbrar,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
unmodified-clean-eq-adr-subseteq,
- znode/sel-04
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-save,
unmodified-same-payload-subseteq,
unmodified-same-payload,
unmodified-reload,
unmodified-payload,
unmodified-load-key-node,
unmodified-load-key-leaf,
unmodified-load-adr-node,
unmodified-load,
unmodified-key-range-node,
unmodified-dirty,
unmodified-clean-leaf-subseteq,
unmodified-clean-leaf,
unmodified-clean-fwd-zbrar2,
unmodified-clean-fwd-zbrar,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
unmodified-clean-eq-adr-subseteq,
- znode/sel-05
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-save,
unmodified-same-payload-subseteq,
unmodified-same-payload,
unmodified-reload,
unmodified-payload,
unmodified-load-key-node,
unmodified-load-key-leaf,
unmodified-load-adr-node,
unmodified-load,
unmodified-key-range-node,
unmodified-clean-leaf-subseteq,
unmodified-clean-leaf,
unmodified-clean-fwd-zbrar2,
unmodified-clean-fwd-zbrar,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
unmodified-clean-eq-adr-subseteq,
Used from specification nat
- nat/add-01
is used by
sorted-shift-left,
range-last-2,
payload-shift-left,
keys-shift-left,
- nat/add-num-03
is used by
payload-copy-right-upper,
payload-copy-right-lower,
- nat/anti
is used by
payload-shift-left,
in-playload-data,
- nat/cancel-01
is used by
payload-copy-right-upper,
- nat/elim-pred-c
is used by
range-put,
range-le,
payload-shift-left,
look-scan-range,
keys-shift-left,
key-range-replace-branches,
keep-range,
in-keyrange-in-ri-data,
at-range,
- nat/elim-sub
is used by
payload-split,
payload-copy-right-upper,
- nat/eq
is used by
payload-shift-left,
look-scan-range,
- nat/eq-01
is used by
save-same-payload-same,
- nat/eqle-one
is used by
range-put,
range-gt,
payload-shift-left,
look-scan-range,
keep-range,
at-range,
- nat/fle
is used by
unmodified-sorted-leaf,
unmodified-payload,
unmodified-load-key-leaf,
unmodified-key-range-node,
unmodified-clean-fwd-zbrar2,
unmodified-clean-fwd-zbrar,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
unmodified-clean-eq-adr-subseteq,
sorted-shift-left,
save-same-payload-same,
range-put,
range-load-save,
range-le,
range-gt,
range-emp,
range,
payload-shift-left,
payload-mod-0,
payload-mod,
payload-drop-upper,
payload-drop-lower,
payload-copy-right-upper,
payload-copy-right-lower,
look-subrange,
keys-shift-left,
keys-mod-0,
keys-mod,
keys-drop-upper,
keys-drop-lower,
key-range-replace-branches,
keep-range,
in-playload-data,
in-keyrange-in-ri-data,
in-keyrange-in-ri,
at-range,
- nat/fle-01
is used by
unmodified-sorted-leaf,
unmodified-payload,
unmodified-load-adr-node,
unmodified-key-range-node,
sorted-shift-left,
save-same-payload-same,
range-load-save,
payload-shift-left,
keys-shift-left,
key-range-replace-branches,
in-playload-data,
- nat/le
is used by
sorted-shift-left,
payload-shift-left,
keys-shift-left,
- nat/le-def
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-reload,
unmodified-payload,
unmodified-key-range-node,
sorted-shift-left,
range-load-save,
payload-shift-left,
payload-save-load-same,
payload-copy-right-upper,
keys-shift-left,
key-range-replace-branches,
keep-range,
- nat/le-ls-simp
is used by
unmodified-sorted-leaf,
unmodified-reload,
unmodified-payload,
unmodified-load-adr-node,
unmodified-key-range-node,
sorted-shift-left,
payload-shift-left,
payload-save-load-same,
payload-mod,
keys-shift-left,
keys-mod,
in-playload-data,
- nat/le-num-06
is used by
payload-copy-right-upper,
- nat/le-one
is used by
payload-shift-left,
keys-shift-left,
- nat/lels
is used by
unmodified-sorted-leaf,
unmodified-payload,
unmodified-key-range-node,
sorted-shift-left,
range-put,
range-gt,
payload-shift-left,
payload-mod,
payload-drop-upper,
payload-drop-lower,
payload-copy-right-upper,
payload-copy-right-lower-0,
payload-copy-right-lower,
look-scan-range,
keys-shift-left,
keys-mod,
keys-drop-upper,
keys-drop-lower,
keep-range,
in-playload-data,
in-payload,
in-keys,
at-range,
at-payload,
- nat/lels-02
is used by
unmodified-key-range-node,
- nat/lels-03
is used by
unmodified-sorted-node,
sorted-shift-left,
save-same-payload-same,
payload-shift-left,
keys-shift-left,
key-range-replace-branches,
in-playload-data,
- nat/lep
is used by
save-same-payload-same,
payload-split,
look-scan-range,
key-range-replace-branches,
in-playload-data,
- nat/lep-02
is used by
sorted-shift-left,
save-same-payload-same,
range-put,
payload-shift-left,
payload-copy-right-upper,
keys-shift-left,
key-range-replace-branches,
keep-range,
at-range,
- nat/ler
is used by
save-same-payload-same,
payload-shift-left,
look-scan-range,
in-playload-data,
- nat/les
is used by
range-put,
range-gt,
payload-shift-left,
keys-shift-left,
keep-range,
at-range,
- nat/let
is used by
payload-shift-left,
payload-drop-upper,
keys-shift-left,
keys-drop-upper,
key-range-replace-branches,
in-playload-data,
- nat/lez
is used by
payload-shift-left,
payload-mod,
look-scan-range,
keys-mod,
key-range-replace-branches,
in-payload,
at-payload,
- nat/lez-01
is used by
payload-shift-left,
keys-shift-left,
key-range-replace-branches,
- nat/ls-01
is used by
unmodified-key-range-node,
range-load-save,
payload-shift-left,
keep-range,
- nat/ls-le-simp
is used by
sorted-shift-left,
save-same-payload-same,
payload-shift-left,
payload-mod,
payload-copy-right-lower-0,
nsize-size,
keys-shift-left,
in-playload-data,
- nat/succ-01
is used by
unmodified-sorted-node,
unmodified-load-key-node,
unmodified-load-adr-node,
unmodified-key-range-node,
save-same-payload-same,
range-put,
range-load-save,
range-le,
range,
payload-split,
payload-shift-left,
payload-mod,
payload-drop-upper,
payload-drop-lower,
look-subrange,
look-scan-range,
keys-shift-left,
keys-mod,
keys-drop-upper,
keys-drop-lower,
key-range-replace-branches,
keep-range,
in-playload-data,
in-payload,
in-keys,
in-keyrange-in-ri-data,
in-keyrange-in-ri,
at-range,
at-payload,
Used from specification store
- store/node-index/At-other
is used by
range-put,
at-payload,
- store/node-index/In-insert
is used by
range-put,
in-payload,
- store/index-store-address-store/Subset
is used by
unmodified-same-payload-subseteq,
unmodified-clean-leaf-subseteq,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-adr-subseteq,
- store/node-index/k-Extension
is used by
unmodified-payload,
unmodified-key-range-node,
range-put,
payload-shift-left,
- store/node-index/rew
is used by
payload-mod,
- store/index-store-address-store/At-other
is used by
unmodified-write-other,
- store/node-index/At-other
is used by
range-put,
- store/node-index/At-same
is used by
range-put,
at-payload,
- store/index-store-address-store/At-same
is used by
unmodified-save,
- store/node-index/Del-at-strong
is used by
payload-shift-left,
- store/node-index/Del-in
is used by
payload-shift-left,
- store/node-index/In-empty
is used by
look-empty,
in-playload-data,
in-payload,
- store/node-index/In-insert
is used by
range-put,
- store/index-store-address-store/in-neq
is used by
unmodified-write-other,
- store/node-index/in-neq
is used by
range-put,
- store/index-store-address-store/insin
is used by
unmodified-save,
- store/node-index/insin
is used by
range-put,
- store/node-index/insins
is used by
payload-mod,
- store/node-index/neq
is used by
payload-mod,
- node-index-restrict/at-le
is used by
range-put,
look-scan-range,
in-keyrange-in-ri-data,
at-range,
- node-index-restrict/restrict-norm
is used by
range-le,
- node-index-restrict/at-gt
is used by
range-put,
look-scan-range,
in-keyrange-in-ri-data,
at-range,
- node-index-restrict/gt-emp
is used by
range-emp,
- node-index-restrict/in-gt
is used by
unmodified-key-range-node,
range-put,
look-subrange,
look-scan-range,
in-keyrange-in-ri-data,
in-keyrange-in-ri,
at-range,
- node-index-restrict/in-le
is used by
unmodified-key-range-node,
range-put,
look-subrange,
look-scan-range,
in-keyrange-in-ri-data,
in-keyrange-in-ri,
at-range,
- node-index-restrict/le-emp
is used by
range-emp,
- node-index-restrict/put-gt
is used by
range-put,
- node-index-restrict/put-le
is used by
range-put,
- node-index-restrict/restrict-gt4
is used by
range-gt,
- node-index-restrict/restrict-le3
is used by
range-le,
Used from specification set-union
Used from specification set-basic
Used from specification constants
- constants/branchsize-0
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-payload,
unmodified-load-key-node,
unmodified-load-key-leaf,
unmodified-load-adr-node,
unmodified-key-range-node,
unmodified-clean-fwd-zbrar2,
unmodified-clean-fwd-zbrar,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
unmodified-clean-eq-adr-subseteq,
save-same-payload-same,
range-load-save,
Used from specification branch
- branch/disj-03
is used by
unmodified-clean-fwd-zbrar2,
unmodified-clean-fwd-zbrar,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
save-same-payload-same,
- branch/inj
is used by
unmodified-clean-fwd-zbrar,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
unmodified-clean-eq-adr-subseteq,
- branch/inj-01
is used by
unmodified-clean-fwd-zbrar2,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
save-same-payload-same,
Used from specification indexnode
- indexnode/inj-05
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-same-payload-subseteq,
unmodified-same-payload,
unmodified-reload,
unmodified-payload,
unmodified-load-key-node,
unmodified-load-key-leaf,
unmodified-load-adr-node,
unmodified-key-range-node,
unmodified-clean-fwd-zbrar2,
unmodified-clean-fwd-zbrar,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
unmodified-clean-eq-adr-subseteq,
- indexnode/sel-13
is used by
unmodified-load,
- indexnode/sel-14
is used by
unmodified-load,
- indexnode/sel-15
is used by
unmodified-load,
Used from specification array-copy
Used from specification nat-mult
Used from specification oelem
- oelem/nat-set/irreflexivity
is used by
unmodified-sorted-leaf,
unmodified-payload,
unmodified-key-range-node,
save-same-payload-same,
range-put,
range-load-save,
payload-shift-left,
payload-copy-right-upper,
look-scan-range,
key-range-replace-branches,
keep-range,
in-keyrange-in-ri-data,
at-range,
- oelem/key-order/irreflexivity
is used by
payload-mod,
keys-shift-left,
- oelem/key-order/lel
is used by
keys-shift-left,
- oelem/nat-set/ls-le
is used by
sorted-shift-left,
payload-shift-left,
keep-range,
- oelem/nat-set/sls
is used by
unmodified-key-range-node,
look-scan-range,
- oelem/nat-set/transitivity
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
unmodified-payload,
unmodified-load-key-node,
sorted-shift-left,
range-load-save,
payload-shift-left,
payload-copy-right-upper,
keys-shift-left,
key-range-replace-branches,
in-playload-data,
at-payload,
- zbranch-array-sorted/sorted-all
is used by
unmodified-sorted-node,
unmodified-sorted-leaf,
sorted-shift-left,
payload-mod,
keys-shift-left,
- zbranch-array-sorted/sorted-lt
is used by
sorted-shift-left,
- zbranch-array-sorted/le-key
is used by
range-put,
range-le,
range-gt,
look-scan-range,
- zbranch-array-sorted/sorted-base
is used by
payload-mod,
keys-mod,
- zbranch-array-sorted/sorted-eq-entry-strong
is used by
unmodified-payload,
payload-shift-left,
in-playload-data,
- zbranch-array-sorted/sorted-rec1
is used by
payload-mod,
keys-mod,
Used from specification array
- array/branch-array/Extension
is used by
unmodified-clean-fwd-zbrar2,
unmodified-clean-fwd-zbrar,
unmodified-clean-eq-keys-subseteq,
unmodified-clean-eq-keys,
unmodified-clean-eq-adr-subseteq,
save-same-payload-same,
- array/branch-array/Put-other
is used by
save-same-payload-same,
- array/zbranch-array/Put-other
is used by
keep-range,
- array/zbranch-array/Put-same
is used by
keep-range,
- array/zbranch-array/Size-put
is used by
payload-mod,
payload-drop-upper,
payload-drop-lower,
keys-mod,
keys-drop-upper,
keys-drop-lower,
keep-range,
- array/branch-array/Size-put
is used by
save-same-payload-same,
- array/branch-array/cgetput
is used by
save-same-payload-same,
- array/zbranch-array/cgetput
is used by
payload-mod,
keys-mod,
- array/zbranch-array/cngetput
is used by
payload-mod,
payload-drop-lower,
keys-mod,
keys-drop-lower,
- array/zbranch-array/ngp-09
is used by
payload-drop-upper,
keys-drop-upper,
- array/zbranch-array/ngp-10
is used by
keep-range,
Used from specification Unknown