[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

store+set/node-index/Data-in is used by size-0, ri-cons-range-restrict-notin-gstore, refsize-nonzero-notin-ginval, range-rem-in, range-in-ri-keys-in-ri, nodes-referenced-adrs-leb, lebs-dom-remove-refsize0, keys-remove-leb, keys-nodes-in-ri, index-update-adr-in, adr-in-ri-notin-nodes, adr-in-index-node-key,
store+set/node-store/Diff-ext is used by nodes-remove-refsize0, nodes-dealloc,
store+set/node-index/Diff-get is used by toSet-diff-get,
store+set/group-store-ablock-store-nat-store/Diff-get is used by gstore-dom-eq-hole,
store+set/node-store/Diff-get is used by nodes-remove-refsize0, nodes-dealloc,
store+set/node-index/Diff-rec is used by index-update-adr-in,
store+set/node-store/restrict-at is used by keys-same-fs,
store+set/node-store/restrict-in is used by keys-same-fs,
store+set/node-index/Data-in-del is used by range-rem-in,
store+set/node-index/Diff-base is used by index-update-adr-in,
store+set/group-store-ablock-store-nat-store/Diff-ext is used by gstore-dom-eq-hole, ginval-down, down-store-at-diff,
store+set/node-index/Diff-ext is used by toSet-diff-in, keys-remove-leb, index-update-adr-in,
store+set/group-store-ablock-store-nat-store/Diff-get is used by nodes-remove-refsize0, gstore-dom-eq-hole, ginval-extract-abs-log, ginval-down, down-store-at-diff,
store+set/node-index/Diff-mems-get is used by toSet-diff-get,
store+set/node-store/Diff-mems-get is used by nodes-remove-refsize0, nodes-dealloc,
store+set/group-store-ablock-store-nat-store/Diff-mems-get is used by nodes-remove-refsize0, gstore-dom-eq-hole, ginval-down,
store+set/group-store-ablock-store-nat-store/Dom is used by restr-add-notin, nodes-remove-refsize0, nodes-ginval-rem-01, nodes-ginval-rem, lebs-dom-remove-refsize0, jnlhd-notin-istore, jnlhd-in-gstore, gstore-dom-eq-hole, dom-remove-refsize0-down, abs-log-new,
store+set/node-store/Dom is used by nodes-dealloc,
store+set/node-index/Dom is used by range-in-ri-keys-in-ri, keys-nodes-in-ri,
store+set/index-store-ablock-store-nat-store/Dom is used by inter-notin-add-empty,
store+set/node-index/In-data-in is used by in-ri,
store+set/node-store/restrict-empty is used by keys-same-fs,

Used from specification ablock

Used from specification nat-basic

nat-basic/a is used by valid-group-nodes-shorter-prefix-right, valid-group-nodes-shorter-prefix, valid-group-nodes-prefixn-append-nonend, valid-group-nodes-ls, valid-group-nodes-last-end, valid-group-nodes-entire, valid-group-nodes-drop-superfluous-prefixn, valid-group-nodes-app-transaction-prefix, valid-group-nodes-app-transaction, size-0, nodes-transaction, nodes-append-subseteq, new-prefixn, keys-size, keys-at, induction-rev-list, index-update-adr-in, adr-in-index-node-key,
nat-basic/add-base is used by nodes-transaction, adr-in-index-node-key,
nat-basic/c is used by valid-group-nodes-shorter-prefix-right, valid-group-nodes-shorter-prefix, valid-group-nodes-prefixn-append-nonend, valid-group-nodes-ls, valid-group-nodes-last-end, valid-group-nodes-entire, valid-group-nodes-drop-superfluous-prefixn, valid-group-nodes-app-transaction-prefix, valid-group-nodes-app-transaction, size-0, nodes-transaction, nodes-append-subseteq, new-prefixn, keys-size, keys-at, induction-rev-list, index-update-adr-in, adr-in-index-node-key,
nat-basic/eq-01 is used by valid-group-nodes-last-end, valid-group-nodes-entire, valid-group-nodes-drop-superfluous-prefixn, nodes-transaction, keys-size, index-update-adr-in, adr-in-index-node-key,
nat-basic/eq-02 is used by valid-group-nodes-entire,
nat-basic/f is used by valid-group-nodes-shorter-prefix-right, valid-group-nodes-shorter-prefix, valid-group-nodes-prefixn-append-nonend, valid-group-nodes-ls, valid-group-nodes-le, valid-group-nodes-entire, valid-group-nodes-drop, nodes-transaction, nodes-append-subseteq-nodown, nodes-append-subseteq, keys-at, adr-in-index-node-key,
nat-basic/l is used by valid-group-nodes-shorter-prefix-right, valid-group-nodes-shorter-prefix, valid-group-nodes-ls, nodes-transaction,
nat-basic/l-02 is used by valid-group-nodes-shorter-prefix-right, valid-group-nodes-shorter-prefix, valid-group-nodes-prefixn-append-nonend, valid-group-nodes-entire, size-0, nodes-transaction, adr-in-index-node-key,
nat-basic/lf is used by valid-group-nodes-ls, nodes-append-subseteq, adr-in-index-node-key,
nat-basic/lf-01 is used by valid-group-nodes-prefixn-append-nonend, nodes-append-subseteq, adr-in-index-node-key,
nat-basic/lf-02 is used by valid-group-nodes-entire, nodes-transaction, nodes-append-subseteq, adr-in-index-node-key,
nat-basic/ls-02 is used by nodes-append-subseteq, adr-in-index-node-key,
nat-basic/one-01 is used by keys-at,
nat-basic/oz is used by valid-group-nodes-prefixn-append-nonend, nodes-transaction, keys-at,
nat-basic/s-04 is used by valid-group-nodes-ls, valid-group-nodes-entire, valid-group-nodes-app-transaction-prefix, size-0, nodes-transaction, keys-at, induction-rev-list, adr-in-index-node-key,
nat-basic/succ is used by valid-group-nodes-ls, size-0, restr-add-01, nodes-transaction, nodes-append-subseteq, keys-size, keys-at, index-update-adr-in, adr-in-index-node-key,
nat-basic/succ-03 is used by adr-in-index-node-key,
nat-basic/z-01 is used by size-0, nodes-transaction, index-update-adr-in,
nat-basic/zero is used by nodes-transaction,
nat-basic/zero-01 is used by valid-group-nodes-ls, nodes-transaction,

Used from specification list+set

list+set/key-list-set/toSet-app is used by range-in-ri-keys-in-ri, index-update-adr-in,
list+set/address-list-set/toSet-app is used by range-in-ri-keys-in-ri, prefixn-toset-restr-empty, prefixn-toset-inter-empty, keys-same-fs, abs-log-toset-inter-restr-empty, abs-log-new,
list+set/address-list-set/toSet-empty is used by range-in-ri-keys-in-ri, keys-same-fs, abs-log-toset-inter-restr-empty, abs-log-new,
list+set/key-list-set/toSet-empty is used by range-in-ri-keys-in-ri, index-update-adr-in,
list+set/key-list-set/toSet-ext is used by toSet-diff-in, toSet-diff-get, keys-remove-leb, keys-nodes-in-ri, index-update-adr-in,
list+set/address-list-set/toSet-ext is used by restr-toset-empty-notin, prefixn-toset-subseteq, nodes-referenced-adrs-leb, keys-same-fs, keys-remove-leb, keys-nodes-in-ri, in-restr-notin-log, abs-log-toset-inter-restr-empty, abs-log-new,
list+set/address-list-set/toSet-one is used by range-in-ri-keys-in-ri, keys-same-fs,
list+set/key-list-set/toSet-one is used by range-in-ri-keys-in-ri, index-update-adr-in,

Used from specification aubifs-inv

aubifs-inv/key-cons is used by range-rem-in, keys-remove-leb, adr-in-index-node-key,
aubifs-inv/ri-cons is used by size-0, ri-cons-subseteq, ri-cons-range-restrict-notin-gstore, refsize-nonzero-notin-ginval, range-rem-in, nodes-referenced-adrs-leb, lebs-dom-remove-refsize0, keys-remove-leb, adr-in-ri-notin-nodes, adr-in-ri-leb-notin-ginval, adr-in-ri-in-gstore, adr-in-index-node-key,
aubifs-inv/ri-cons-in is used by key-in-ri-in-fs,
aubifs-inv/ri-cons-key is used by range-in-ri-keys-in-ri, keys-nodes-in-ri,
aubifs-inv/ri-cons-variant1-01 is used by ri-cons-subseteq,

Used from specification aubifs-base

aubifs-base/new-ext is used by new-adrs-gstore, abs-log-new,
aubifs-base/index-update-key-base is used by index-update-adr-in,
aubifs-base/index-update-key-rec is used by index-update-adr-in,
aubifs-base/keys-base is used by range-in-ri-keys-in-ri, keys-size, keys-same-fs, keys-eq-empty, keys-append, in-keys-elim,
aubifs-base/keys-rec is used by range-in-ri-keys-in-ri, keys-size, keys-same-fs, keys-eq-empty, keys-at, keys-append, in-keys-elim,
aubifs-base/new-append is used by new-prefixn,
aubifs-base/range is used by size-0, ri-cons-range-restrict-notin-gstore, refsize-nonzero-notin-ginval, refsize-0-notin-index, range-rem-in, range-in-ri-keys-in-ri, nodes-referenced-adrs-leb, lebs-dom-remove-refsize0, keys-nodes-in-ri, index-update-adr-in,
aubifs-base/update-index-app is used by index-update-append1,
aubifs-base/update-index-data-notin is used by index-update-adr-in,

Used from specification ablock-store-inv

ablock-store-inv/group-store/at is used by nodes-write-same-flushed, nodes-transaction, nodes-remove-refsize0, nodes-no-change-eq, nodes-except-refsize, nodes-crash-down, nodes-append-subseteq-nodown, nodes-append-subseteq, in-nodes-down-at-same, adr-in-index-node-key,
ablock-store-inv/group-store/at-remove-refsize0 is used by remove-refsize0-down, nodes-remove-refsize0,
ablock-store-inv/group-store/except-refsize-eq is used by nodes-except-refsize, down-except-refsize, abs-log-except-refsize,
ablock-store-inv/group-store/in is used by nodes-write-same-flushed, nodes-write-nochange, nodes-write-at-other, nodes-remove-refsize0, nodes-remove-ginval-notin, nodes-no-change-eq, nodes-ginval-rem-01, nodes-ginval-rem, nodes-ginval-inter, nodes-except-refsize, nodes-dealloc, nodes-crash-down, nodes-append-subseteq-nodown, nodes-append-subseteq, nodes-allocate, new-adrs-gstore, in-nodes-down-at-same, ginval-extract-nodes, down-store-notin-notin, down-store-adr-in-explicit,
ablock-store-inv/group-store/in-remove-refsize0 is used by remove-refsize0-down, dom-remove-refsize0-down,
ablock-store-inv/group-store/inv-block is used by size-0, adr-in-index-node-key,
ablock-store-inv/group-store/inv-flashsize is used by size-0,
ablock-store-inv/group-store/addresslist-in-lnum-simp is used by nodes-transaction, nodes-referenced-adrs-leb, abs-log-adr-explicit-in-leb-notin,
ablock-store-inv/group-store/addresslist-length is used by nodes-transaction,
ablock-store-inv/group-store/adrs-empty is used by ladr-split,
ablock-store-inv/group-store/adrs-rec is used by nodes-transaction, ladr-split,
ablock-store-inv/group-store/at-dealloc is used by nodes-dealloc,
ablock-store-inv/group-store/at-diff is used by ginval-extract-nodes,
ablock-store-inv/group-store/at-explicit-other is used by nodes-write-at-other, nodes-allocate,
ablock-store-inv/group-store/at-write-app is used by nodes-transaction,
ablock-store-inv/group-store/at-write-same is used by nodes-write-nochange,
ablock-store-inv/group-store/except-refsizeeq-comm is used by nodes-except-refsize,
ablock-store-inv/group-store/flashsize-neq-0 is used by size-0,
ablock-store-inv/group-store/in-adr-in is used by nodes-write-at-other, nodes-remove-refsize0,
ablock-store-inv/group-store/in-alloc is used by nodes-allocate,
ablock-store-inv/group-store/in-dealloc is used by nodes-dealloc,
ablock-store-inv/group-store/in-diff is used by nodes-remove-refsize0, ginval-extract-nodes,
ablock-store-inv/group-store/in-diff-explicit is used by nodes-remove-refsize0, ginval-extract-nodes,
ablock-store-inv/group-store/in-empty is used by nodes-empty,
ablock-store-inv/group-store/in-in-adr is used by nodes-write-nochange, nodes-write-at-other, nodes-remove-refsize0, nodes-remove-ginval-notin, nodes-no-change-eq, nodes-ginval-rem-01, nodes-ginval-rem, nodes-ginval-inter, nodes-dealloc, nodes-allocate, ginval-extract-nodes, abs-log-new,
ablock-store-inv/group-store/in-remove-refsize0 is used by nodes-remove-refsize0, lebs-dom-remove-refsize0,
ablock-store-inv/group-store/in-write-app is used by nodes-transaction,
ablock-store-inv/group-store/in-write-explicit is used by nodes-transaction, down-store-write-same,
ablock-store-inv/group-store/in-write-same is used by nodes-write-nochange,
ablock-store-inv/group-store/inv-nodups-app-left is used by size-0,
ablock-store-inv/group-store/notin-notin is used by ri-cons-range-restrict-notin-gstore, nodes-write-at-other, nodes-remove-refsize0, nodes-remove-ginval-notin, nodes-except-refsize, down-store-adr-in-explicit-simp,
ablock-store-inv/group-store/to-adrs-append is used by nodes-transaction, ladr-split,
ablock-store-inv/group-store/to-adrs-eq is used by ladr-split, abs-log-one, abs-log-no-change-eq, abs-log-except-refsize, abs-log-eq-butlast, abs-log-append-one,
ablock-store-inv/group-store/to-adrs-eq-empty is used by ladr-split,
ablock-store-inv/group-store/to-adrs-in is used by nodes-transaction, new-adrs-gstore, abs-log-toset-inter-restr-empty, abs-log-new,
ablock-store-inv/group-store/to-ards-no-dups is used by nodes-transaction,

Used from specification apersistence-base

apersistence-base/crash-group-in is used by nodes-crash-down,
apersistence-base/crash-group-at is used by nodes-crash-down, abs-log-gcrash-down,
apersistence-base/crash-group-in is used by nodes-crash-down, abs-log-gcrash-down,
apersistence-base/dom-disj-in-r is used by jnlhd-notin-istore,
apersistence-base/dom-gstore-intersect-in-gstore is used by nodes-remove-refsize0, nodes-ginval-inter,
apersistence-base/elems-def is used by jnlhd-notin-istore, jnlhd-notin-ginval, jnlhd-in-gstore,
apersistence-base/elems-empty is used by ginval-extract-abs-log, abs-log-new, abs-log-gcrash-down,
apersistence-base/elems-prepend is used by ginval-extract-abs-log, abs-log-new, abs-log-gcrash-down,
apersistence-base/fwd-inv-gblock-rem is used by size-0, nodes-crash-down, abs-log-gcrash-down,

Used from specification set-union

set-union/nat-set/Difference is used by sub-restr-sub, restr-add-notin, nodes-ginval-rem-01, nodes-ginval-rem,
set-union/node-store/subdef is used by prefixn-toset-subseteq, in-restr-notin-log, adresses-restr-subseteq,
set-union/nat-set/subdef is used by lebs-dom-remove-refsize0, jnlhd-notin-istore, jnlhd-in-gstore,
set-union/node-index/subdef is used by keys-nodes-in-ri, insert-subset-old,
set-union/node-store/Delete is used by range-rem-in,
set-union/nat-set/Delete is used by sub-restr-sub, nodes-remove-ginval-notin, nodes-allocate,
set-union/nat-set/Difference is used by sub-restr-sub, restr-add-notin, nodes-ginval-rem-01, nodes-ginval-rem, inter-subset-rem-empty,
set-union/node-store/Intersect is used by in-restr-notin-log, abs-log-toset-inter-restr-empty, abs-log-new,
set-union/nat-set/Intersect is used by nodes-remove-refsize0, jnlhd-notin-ginval, inter-subset-rem-empty,
set-union/nat-set/One is used by gstore-dom-eq-hole,
set-union/nat-set/del-d is used by sub-restr-sub,
set-union/nat-set/del-neq is used by sub-restr-sub,
set-union/nat-set/diff-del-minus-2 is used by sub-restr-sub,
set-union/nat-set/int-a is used by nodes-remove-refsize0, nodes-ginval-inter, jnlhd-notin-istore, jnlhd-notin-ginval, inter-subset-rem-empty, inter-notin-add-empty, ginval-extract-abs-log, abs-log-new, abs-log-gcrash-down,
set-union/node-store/int-a is used by prefixn-toset-inter-empty, in-restr-notin-log, in-restr-eq-notin-log, abs-log-toset-inter-restr-empty, abs-log-new,
set-union/nat-set/int-c is used by nodes-remove-refsize0, nodes-ginval-inter, jnlhd-notin-istore, jnlhd-notin-ginval, inter-subset-rem-empty, inter-notin-add-empty, ginval-extract-abs-log, abs-log-new, abs-log-gcrash-down,
set-union/node-store/int-c is used by prefixn-toset-inter-empty, in-restr-notin-log, in-restr-eq-notin-log, abs-log-toset-inter-restr-empty, abs-log-new,
set-union/nat-set/int-e is used by ginval-extract-abs-log, abs-log-new, abs-log-gcrash-down,
set-union/node-store/int-e is used by abs-log-toset-inter-restr-empty, abs-log-new,
set-union/nat-set/int-empty-02 is used by inter-subset-rem-empty,
set-union/nat-set/int-ins is used by inter-notin-add-empty, ginval-extract-abs-log, abs-log-new, abs-log-gcrash-down,
set-union/node-store/intu-empty is used by prefixn-toset-inter-empty, abs-log-toset-inter-restr-empty, abs-log-new,
set-union/node-index/sub-union is used by insert-subset-old,
set-union/node-store/una is used by restr-add-01, range-in-ri-keys-in-ri, prefixn-toset-restr-empty, prefixn-toset-inter-empty, keys-same-fs, abs-log-toset-inter-restr-empty, abs-log-new,
set-union/node-index/una is used by range-in-ri-keys-in-ri, insert-subset-old, index-update-adr-in,
set-union/node-store/unadd is used by restr-add-01, range-in-ri-keys-in-ri, keys-same-fs,
set-union/node-index/unadd is used by range-in-ri-keys-in-ri, index-update-adr-in,
set-union/node-store/unc is used by restr-add-01, range-in-ri-keys-in-ri, prefixn-toset-restr-empty, prefixn-toset-inter-empty, keys-same-fs, abs-log-toset-inter-restr-empty, abs-log-new,
set-union/node-index/unc is used by range-in-ri-keys-in-ri, insert-subset-old, index-update-adr-in,
set-union/node-store/une is used by restr-add-01, range-in-ri-keys-in-ri, keys-same-fs,
set-union/node-index/une is used by range-in-ri-keys-in-ri, index-update-adr-in,
set-union/node-store/une-01 is used by prefixn-toset-restr-empty,
set-union/node-index/unin is used by insert-subset-old,
set-union/node-index/unin-01 is used by insert-subset-old,

Used from specification store

store/group-store-ablock-store-nat-store/At-other is used by nodes-append-subseteq, gstore-dom-eq-hole,
store/node-store/Extension is used by nodes-except-refsize, keys-same-fs,
store/group-store-ablock-store-nat-store/Extension is used by gstore-dom-eq-hole,
store/group-store-ablock-store-nat-store/In-insert is used by nodes-write-same-flushed, nodes-allocate, gstore-dom-eq-hole,
store/node-store/Subset is used by ri-cons-subseteq, nodes-append-subseteq-nodown, nodes-append-subseteq,
store/node-index/exin is used by keys-remove-leb,
store/group-store-ablock-store-nat-store/k-Extension is used by remove-refsize0-down, gstore-dom-eq-hole, ginval-down, down-store-write, down-store-dealloc, down-empty,
store/node-store/k-Extension is used by nodes-write-same-flushed, nodes-write-nochange, nodes-transaction, nodes-remove-refsize0, nodes-remove-ginval-notin, nodes-no-change-eq, nodes-ginval-rem-01, nodes-ginval-rem, nodes-ginval-inter, nodes-empty, nodes-dealloc, nodes-crash-down, nodes-allocate, ginval-extract-nodes,
store/group-store-ablock-store-nat-store/notmemlookup is used by down-store-at-diff, down-except-refsize, abs-log-gcrash-down,
store/node-store/notmemlookup is used by nodes-write-at-other, nodes-except-refsize, keys-same-fs,
store/group-store-ablock-store-nat-store/At-in-out is used by nodes-allocate,
store/group-store-ablock-store-nat-store/At-other is used by nodes-write-same-flushed, nodes-write-at-other, nodes-append-subseteq-nodown, nodes-allocate, down-store-write, abs-log-write-nochange, abs-log-change-other,
store/node-index/At-other is used by index-update-adr-in,
store/group-store-ablock-store-nat-store/At-same is used by nodes-write-same-flushed, nodes-transaction, nodes-append-subseteq-nodown, nodes-append-subseteq, nodes-allocate, gstore-dom-eq-hole, down-store-write, abs-log-write-nochange, abs-log-write-last,
store/node-index/At-same is used by keys-remove-leb, index-update-adr-in,
store/node-index/Del-at is used by range-rem-in, index-update-adr-in,
store/group-store-ablock-store-nat-store/Del-at is used by nodes-dealloc, down-store-dealloc,
store/node-index/Del-at-strong is used by range-rem-in,
store/group-store-ablock-store-nat-store/Del-at-strong is used by abs-log-del,
store/group-store-ablock-store-nat-store/Del-in is used by nodes-dealloc, down-store-dealloc,
store/node-index/Del-in is used by range-rem-in, index-update-adr-in,
store/node-store/In-empty is used by nodes-empty,
store/group-store-ablock-store-nat-store/In-empty is used by down-empty,
store/group-store-ablock-store-nat-store/In-insert is used by nodes-append-subseteq-nodown, nodes-append-subseteq, nodes-allocate,
store/group-store-ablock-store-nat-store/in-neq is used by nodes-write-at-other, nodes-append-subseteq-nodown, nodes-append-subseteq, down-store-write,
store/node-index/in-neq is used by index-update-adr-in,
store/node-index/insin is used by keys-remove-leb, index-update-adr-in,
store/group-store-ablock-store-nat-store/insin is used by nodes-append-subseteq-nodown, nodes-append-subseteq, down-store-write,
store/group-store-ablock-store-nat-store/notmemlookup is used by nodes-write-same-flushed, nodes-remove-refsize0, nodes-except-refsize, nodes-crash-down, nodes-append-subseteq-nodown, nodes-allocate, lebs-dom-remove-refsize0, in-nodes-down-at-same, gstore-dom-eq-hole, down-store-at-diff, down-except-refsize, abs-log-no-change-eq,
store/node-index/notmemlookup is used by keys-nodes-in-ri,
store/node-store/notmemlookup is used by range-rem-in, nodes-write-same-flushed, nodes-write-nochange, nodes-write-at-other, nodes-transaction, nodes-remove-refsize0, nodes-remove-ginval-notin, nodes-no-change-eq, nodes-ginval-rem-01, nodes-ginval-rem, nodes-ginval-inter, nodes-dealloc, nodes-crash-down, nodes-append-subseteq-nodown, nodes-allocate, keys-same-fs, ginval-extract-nodes, adr-in-index-node-key,
store/node-store/superset-elem-in-01 is used by ri-cons-subseteq,

Used from specification nat

nat/anti is used by nodes-append-subseteq,
nat/elim-pred-c is used by keys-at,
nat/eqle-one is used by valid-group-nodes-prefixn-append-nonend, nodes-transaction,
nat/fle is used by valid-group-nodes-shorter-prefix-right, valid-group-nodes-shorter-prefix, valid-group-nodes-prefixn-append-nonend, valid-group-nodes-le, nodes-append-subseteq,
nat/fle-01 is used by valid-group-nodes-shorter-prefix, nodes-append-subseteq, adr-in-index-node-key,
nat/le-def is used by valid-group-nodes-shorter-prefix, valid-group-nodes-prefixn-append-nonend, valid-group-nodes-le, valid-group-nodes-entire, valid-group-nodes-drop, nodes-write-same-flushed, nodes-append-subseteq-nodown, nodes-append-subseteq, adr-in-index-node-key,
nat/le-ls-simp is used by valid-group-nodes-shorter-prefix, valid-group-nodes-drop-superfluous-prefixn, valid-group-nodes-drop, nodes-append-subseteq-nodown, nodes-append-subseteq,
nat/lels is used by valid-group-nodes-shorter-prefix-right, valid-group-nodes-shorter-prefix, valid-group-nodes-entire, valid-group-nodes-drop-superfluous-prefixn, nodes-append-subseteq-nodown, nodes-append-subseteq, keys-at, in-nodes-down-at-same, adr-in-index-node-key,
nat/lels-02 is used by valid-group-nodes-drop, nodes-append-subseteq,
nat/lels-03 is used by valid-group-nodes-entire, nodes-append-subseteq,
nat/lep is used by new-prefixn, adr-in-index-node-key,
nat/lep-02 is used by nodes-append-subseteq,
nat/ler is used by adr-in-index-node-key,
nat/les is used by valid-group-nodes-prefixn-append-nonend, adr-in-index-node-key,
nat/let is used by valid-group-nodes-shorter-prefix, valid-group-nodes-entire, nodes-write-same-flushed, nodes-append-subseteq,
nat/lez is used by valid-group-nodes-drop-superfluous-prefixn,
nat/ls-le-simp is used by valid-group-nodes-shorter-prefix, nodes-append-subseteq, adr-in-index-node-key,
nat/sub-base is used by size-0,
nat/succ-01 is used by valid-group-nodes-shorter-prefix-right, valid-group-nodes-shorter-prefix, valid-group-nodes-entire, valid-group-nodes-drop-superfluous-prefixn, nodes-append-subseteq, keys-at, adr-in-index-node-key,
nat/zero is used by adr-in-index-node-key,

Used from specification set-basic

set-basic/nat-set/Extension is used by sub-restr-sub, restr-add-notin, nodes-remove-refsize0, jnlhd-notin-ginval, inter-subset-rem-empty, gstore-dom-eq-hole, dom-remove-refsize0-down,
set-basic/node-store/Extension is used by size-0, ri-cons-range-restrict-notin-gstore, restr-toset-empty-notin, restr-empty-notin, range-rem-in, nodes-referenced-adrs-leb, keys-remove-leb, keys-nodes-in-ri, in-restr-notin-log, abs-log-toset-inter-restr-empty, abs-log-new,
set-basic/node-store/In-empty is used by size-0, ri-cons-range-restrict-notin-gstore, restr-toset-empty-notin, restr-empty-notin, in-restr-notin-log, abs-log-toset-inter-restr-empty, abs-log-new,
set-basic/nat-set/In-empty is used by nodes-remove-refsize0, nodes-ginval-inter, jnlhd-notin-ginval, inter-subset-rem-empty,
set-basic/nat-set/In-insert is used by restr-add-notin, nodes-dealloc,
set-basic/node-store/In-insert is used by keys-same-fs, keys-remove-leb,
set-basic/node-index/In-insert is used by insert-subset-old,
set-basic/node-store/Size-empty is used by in-restr-eq-notin-log,
set-basic/nat-set/in-02 is used by restr-add-notin, nodes-dealloc,
set-basic/nat-set/in-04 is used by gstore-dom-eq-hole,
set-basic/node-store/ne-01 is used by restr-empty-notin, in-restr-notin-log, abs-log-toset-inter-restr-empty,
set-basic/node-index/ne-01 is used by insert-subset-old,
set-basic/nat-set/ne-01 is used by sub-restr-sub, refsize-nonzero-notin-ginval, nodes-remove-refsize0, jnlhd-notin-ginval, inter-subset-rem-empty, ginval-down, adr-in-ri-leb-notin-ginval,
set-basic/node-store/size-zero is used by size-0, ri-cons-range-restrict-notin-gstore, prefixn-toset-restr-empty, prefixn-toset-inter-empty, in-restr-notin-log, abs-log-toset-inter-restr-empty, abs-log-new,
set-basic/nat-set/size-zero is used by inter-subset-rem-empty,
set-basic/node-store/size-zero-01 is used by size-0, ri-cons-range-restrict-notin-gstore, restr-empty-notin, prefixn-toset-restr-empty, prefixn-toset-inter-empty, in-restr-notin-log, in-restr-eq-notin-log, abs-log-toset-inter-restr-empty, abs-log-new,
set-basic/nat-set/size-zero-01 is used by refsize-nonzero-notin-ginval, nodes-remove-refsize0, jnlhd-notin-ginval, inter-subset-rem-empty, ginval-down, adr-in-ri-leb-notin-ginval,
set-basic/node-store/sub-add-03 is used by range-in-ri-keys-in-ri,
set-basic/nat-set/sub-add-03 is used by abs-log-new,
set-basic/node-index/sub-add-03 is used by range-in-ri-keys-in-ri, insert-subset-old,
set-basic/node-index/sub-e is used by range-in-ri-keys-in-ri,
set-basic/node-store/sub-e is used by range-in-ri-keys-in-ri,
set-basic/node-index/sub-in is used by insert-subset-old,
set-basic/nat-set/sub-in is used by inter-subset-rem-empty,
set-basic/node-store/sub-ntrans-01 is used by prefixn-toset-subseteq,

Used from specification list-last

list-last/nat-list-set/bin-01 is used by last-notin-butlast-nodups,
list-last/nat-list-set/butlast-def is used by last-notin-butlast-nodups, abs-log-write-last, abs-log-eq-butlast,
list-last/group-store/l-02 is used by nodes-transaction,
list-last/group-store/last-def is used by valid-group-nodes-last-end,
list-last/nat-list-set/last-def is used by last-notin-butlast-nodups, abs-log-write-last, abs-log-eq-butlast,
list-last/group-store/last-one is used by valid-group-nodes-single-end, nodes-transaction,
list-last/nat-list-set/lin-01 is used by last-notin-butlast-nodups, jnlhd-notin-istore, jnlhd-notin-ginval, jnlhd-in-gstore,
list-last/nat-list-set/prefix-app is used by prefix-append-prefix,

Used from specification gjournal-base

gjournal-base/at-write-at is used by nodes-transaction,
gjournal-base/at-write-other is used by nodes-transaction,
gjournal-base/range-add-explicit is used by size-0,
gjournal-base/referenced-adrs-in is used by nodes-referenced-adrs-leb,
gjournal-base/transaction is used by nodes-transaction,
gjournal-base/valid-journal-head is used by valid-journal-head-valid-group-nodes,
gjournal-base/in-write is used by nodes-transaction,
gjournal-base/lebs-index is used by lebs-dom-remove-refsize0,
gjournal-base/nds-app is used by nds-split,
gjournal-base/nds-base is used by nds-split,
gjournal-base/nds-eq-empty is used by nds-split,
gjournal-base/nds-rec is used by nds-split,
gjournal-base/range-write-notin is used by keys-remove-leb,
gjournal-base/transaction-last-nend is used by valid-group-nodes-app-transaction,
gjournal-base/transaction-length0 is used by nodes-transaction,
gjournal-base/transaction-prefix-app is used by valid-group-nodes-app-transaction-prefix,
gjournal-base/transaction-prefix-last-nonend is used by valid-group-nodes-app-transaction-prefix,

Used from specification list-prefixn

list-prefixn/group-store/in-prefixn-at-smaller is used by nodes-append-subseteq-nodown, nodes-append-subseteq, in-nodes-down-at-same, adr-in-index-node-key,
list-prefixn/group-store/prefixn is used by valid-group-nodes-prefixn-append-nonend, valid-group-nodes-drop,
list-prefixn/address-list-set/prefixn is used by prefixn-toset-restr-empty, prefixn-toset-inter-empty, new-prefixn,
list-prefixn/group-store/prefixn-append-left is used by valid-group-nodes-shorter-prefix, nodes-append-subseteq,
list-prefixn/laddress-list/prefixn-notin is used by size-0,
list-prefixn/laddress-list/prefixn-shift-right is used by nodes-append-subseteq,
list-prefixn/laddress-list/in-prefixn-pos-smaller is used by nodes-append-subseteq-nodown, nodes-append-subseteq, in-nodes-down-at-same,
list-prefixn/laddress-list/in-prefixn-pos-smaller0 is used by nodes-append-subseteq-nodown, nodes-append-subseteq, in-nodes-down-at-same,
list-prefixn/laddress-list/in-prefixn-samepos is used by nodes-write-same-flushed, nodes-crash-down, nodes-append-subseteq-nodown, nodes-append-subseteq, in-nodes-down-at-same, adr-in-index-node-key,
list-prefixn/group-store/prefixn-append-left is used by valid-group-nodes-shorter-prefix-right, valid-group-nodes-shorter-prefix, nodes-append-subseteq, adr-in-index-node-key,
list-prefixn/laddress-list/prefixn-append-left is used by nodes-append-subseteq, adr-in-index-node-key,
list-prefixn/group-store/prefixn-empty is used by valid-group-nodes-drop-superfluous-prefixn,
list-prefixn/group-store/prefixn-eq-empty is used by valid-group-nodes-shorter-prefix-right, valid-group-nodes-shorter-prefix,
list-prefixn/laddress-list/prefixn-fulln is used by nodes-write-same-flushed, nodes-append-subseteq, adr-in-index-node-key,
list-prefixn/group-store/prefixn-fulln is used by valid-group-nodes-shorter-prefix-right, valid-group-nodes-shorter-prefix, valid-group-nodes-drop-superfluous-prefixn, remove-refsize0-down, nodes-write-same-flushed, nodes-crash-down, nodes-append-subseteq-nodown, nodes-append-subseteq, in-nodes-down-at-same, down-store-notin-notin, dom-remove-refsize0-down,
list-prefixn/address-list-set/prefixn-in is used by prefixn-toset-subseteq,
list-prefixn/laddress-list/prefixn-in is used by nodes-append-subseteq-nodown, nodes-append-subseteq, in-nodes-down-at-same,
list-prefixn/group-store/prefixn-len-n is used by valid-group-nodes-shorter-prefix-right, valid-group-nodes-shorter-prefix,
list-prefixn/laddress-list/prefixn-notin is used by nodes-referenced-adrs-leb, nodes-append-subseteq-nodown, nodes-append-subseteq, down-store-notin-notin, adr-in-index-node-key,

Used from specification list-data

list-data/group-store/elim-list-c is used by nodes-transaction,
list-data/group-store/l is used by valid-group-nodes-shorter-prefix-right, valid-group-nodes-shorter-prefix, valid-group-nodes-entire, nodes-append-subseteq, adr-in-index-node-key,
list-data/key-list-set/l is used by index-update-adr-in,
list-data/laddress-list/l is used by nodes-transaction, nodes-append-subseteq, adr-in-index-node-key,
list-data/address-list-set/l is used by keys-at, index-update-adr-in,
list-data/laddress-list/size-01 is used by nodes-transaction,
list-data/key-list-set/size-01 is used by keys-size, index-update-adr-in,
list-data/group-store/size-01 is used by valid-journal-head-valid-group-nodes, valid-group-nodes-last-end, valid-group-nodes-entire, nodes-transaction,
list-data/address-list-set/size-01 is used by keys-size, index-update-adr-in,

Used from specification laddress

laddress/elim is used by ladr-split,
laddress/sel-01 is used by size-0, nodes-transaction, ladr-split,
laddress/sel-02 is used by nodes-transaction, ladr-split,

Used from specification list

list/nat-list-set/One is used by abs-log-one,
list/address-list-set/One is used by keys-one, index-update-one,
list/nat-list-set/c is used by abs-log-one,
list/key-list-set/firsteq is used by keys-same-fs,
list/laddress-list/in-def is used by size-0, nodes-transaction,
list/nat-list-set/lastdiv-rew is used by last-notin-butlast-nodups, abs-log-write-last, abs-log-eq-butlast,
list/group-store/lastdiv-rew is used by valid-group-nodes-last-end, valid-group-nodes-app-transaction-prefix, valid-group-nodes-app-transaction, induction-rev-list,
list/group-store/Last is used by valid-group-nodes-shorter-prefix-right, valid-group-nodes-shorter-prefix, valid-group-nodes-ls, valid-group-nodes-entire, valid-group-nodes-drop-superfluous-prefixn, induction-rev-list,
list/group-store/Nil is used by nds-split,
list/nat-list-set/Nil is used by abs-log-append-one,
list/node-list/Nil is used by nds-split,
list/address-list-set/Nil is used by ladr-split, keys-append, abs-log-append-one,
list/laddress-list/Nil is used by ladr-split,
list/key-list-set/Nil is used by keys-same-fs, keys-append,
list/address-list-set/a is used by range-in-ri-keys-in-ri, prefixn-toset-restr-empty, prefixn-toset-inter-empty, nodes-transaction, new-prefixn, ladr-split, keys-size, keys-same-fs, keys-one, keys-eq-empty, keys-at, keys-append, index-update-one, index-update-append1, index-update-adr-in, in-keys-elim, ginval-extract-abs-log, abs-log-write-nochange, abs-log-write-last, abs-log-toset-inter-restr-empty, abs-log-split-head, abs-log-one, abs-log-no-change-eq, abs-log-new, abs-log-gcrash-down, abs-log-except-refsize, abs-log-eq-butlast, abs-log-del, abs-log-change-other, abs-log-append-one, abs-log-adr-explicit-in-leb-notin,
list/nat-list-set/a is used by prefix-append-prefix, last-notin-butlast-nodups, ginval-extract-abs-log, abs-log-write-nochange, abs-log-write-last, abs-log-toset-inter-restr-empty, abs-log-no-change-eq, abs-log-new, abs-log-gcrash-down, abs-log-except-refsize, abs-log-eq-butlast, abs-log-del, abs-log-change-other, abs-log-append-one, abs-log-adr-explicit-in-leb-notin,
list/node-list/a is used by nds-split,
list/group-store/a is used by valid-group-nodes-shorter-prefix-right, valid-group-nodes-shorter-prefix, valid-group-nodes-prefixn-append-nonend, valid-group-nodes-ls, valid-group-nodes-last-end, valid-group-nodes-entire, valid-group-nodes-drop-superfluous-prefixn, valid-group-nodes-app-transaction-prefix, valid-group-nodes-app-transaction, nodes-transaction, nodes-append-subseteq-nodown, nodes-append-subseteq, nds-split, induction-rev-list, adr-in-index-node-key,
list/key-list-set/a is used by range-in-ri-keys-in-ri, keys-size, keys-same-fs, keys-eq-empty, keys-at, keys-append, index-update-append1, index-update-adr-in, in-keys-elim,
list/laddress-list/a is used by size-0, nodes-transaction, nodes-append-subseteq-nodown, nodes-append-subseteq, new-adrs-gstore, ladr-split, adr-in-index-node-key,
list/group-store/app is used by valid-group-nodes-app-transaction-prefix, valid-group-nodes-app-transaction, nodes-transaction,
list/address-list-set/app is used by keys-one, index-update-one, abs-log-one,
list/address-list-set/app-01 is used by ladr-split, ginval-extract-abs-log, abs-log-write-nochange, abs-log-gcrash-down, abs-log-eq-butlast, abs-log-del, abs-log-change-other, abs-log-append-one,
list/node-list/app-01 is used by nds-split,
list/node-list/app-02 is used by nds-split,
list/address-list-set/app-02 is used by ladr-split,
list/key-list-set/app-02 is used by keys-eq-empty,
list/address-list-set/app-03 is used by abs-log-write-last, abs-log-no-change-eq, abs-log-except-refsize,
list/laddress-list/app-03 is used by ladr-split,
list/node-list/app-08 is used by nds-split,
list/key-list-set/app-08 is used by keys-append,
list/address-list-set/app-08 is used by ladr-split,
list/nat-list-set/c is used by ginval-extract-abs-log, abs-log-write-nochange, abs-log-toset-inter-restr-empty, abs-log-no-change-eq, abs-log-new, abs-log-gcrash-down, abs-log-except-refsize, abs-log-del, abs-log-change-other, abs-log-append-one, abs-log-adr-explicit-in-leb-notin,
list/key-list-set/c is used by range-in-ri-keys-in-ri, keys-size, keys-same-fs, keys-eq-empty, keys-at, keys-append, index-update-adr-in, in-keys-elim,
list/node-list/c is used by nds-split,
list/address-list-set/c is used by range-in-ri-keys-in-ri, nodes-transaction, ladr-split, keys-size, keys-same-fs, keys-one, keys-eq-empty, keys-at, keys-append, index-update-one, index-update-adr-in, in-keys-elim,
list/group-store/c is used by nodes-transaction, nds-split,
list/laddress-list/c is used by size-0, nodes-transaction, ladr-split,
list/key-list-set/c-04 is used by keys-one,
list/node-list/c-06 is used by nds-split,
list/address-list-set/c-06 is used by ladr-split,
list/key-list-set/e is used by keys-same-fs, keys-eq-empty,
list/group-store/e-01 is used by nodes-transaction,
list/address-list-set/e-01 is used by keys-at,
list/group-store/e-02 is used by valid-group-nodes-shorter-prefix-right, valid-group-nodes-shorter-prefix,
list/key-list-set/first is used by keys-same-fs,
list/nat-list-set/in-06 is used by abs-log-toset-inter-restr-empty, abs-log-del, abs-log-change-other, abs-log-adr-explicit-in-leb-notin,
list/laddress-list/in-10 is used by nodes-transaction,
list/laddress-list/in-11 is used by nodes-append-subseteq-nodown, nodes-append-subseteq,
list/address-list-set/in-14 is used by ladr-split,
list/node-list/in-14 is used by nds-split,
list/group-store/in-15 is used by valid-group-nodes-ls, valid-group-nodes-entire, valid-group-nodes-drop-superfluous-prefixn,
list/group-store/in-17 is used by valid-group-nodes-ls, valid-group-nodes-entire, valid-group-nodes-drop-superfluous-prefixn,
list/laddress-list/in-17 is used by nodes-append-subseteq, adr-in-index-node-key,
list/address-list-set/in-append is used by ladr-split, abs-log-adr-explicit-in-leb-notin,
list/group-store/in-append is used by valid-group-nodes-ls, valid-group-nodes-entire, valid-group-nodes-drop-superfluous-prefixn,
list/laddress-list/in-append is used by nodes-transaction, nodes-append-subseteq-nodown, nodes-append-subseteq, adr-in-index-node-key,
list/node-list/in-append is used by nds-split,
list/address-list-set/in-empty is used by ladr-split, index-update-adr-in, in-keys-elim, abs-log-adr-explicit-in-leb-notin,
list/laddress-list/in-empty is used by nodes-allocate,
list/key-list-set/in-empty is used by in-keys-elim,
list/node-list/in-empty is used by nds-split,
list/node-list/in-rec is used by nds-split,
list/address-list-set/in-rec is used by ladr-split, index-update-adr-in, in-keys-elim,
list/key-list-set/in-rec is used by in-keys-elim,
list/address-list-set/len is used by new-prefixn,
list/group-store/len is used by valid-group-nodes-shorter-prefix-right, valid-group-nodes-shorter-prefix, valid-group-nodes-prefixn-append-nonend, valid-group-nodes-ls, valid-group-nodes-last-end, valid-group-nodes-entire, valid-group-nodes-drop-superfluous-prefixn, valid-group-nodes-app-transaction-prefix, valid-group-nodes-app-transaction, nodes-append-subseteq, induction-rev-list, adr-in-index-node-key,
list/laddress-list/len is used by size-0, nodes-transaction, nodes-append-subseteq, adr-in-index-node-key,
list/key-list-set/len-02 is used by keys-at,
list/laddress-list/len-02 is used by nodes-append-subseteq, adr-in-index-node-key,
list/group-store/len-02 is used by valid-group-nodes-single-end, valid-group-nodes-shorter-prefix-right, valid-group-nodes-shorter-prefix, valid-group-nodes-prefixn-append-nonend, valid-group-nodes-ls, valid-group-nodes-last-end, valid-group-nodes-entire, valid-group-nodes-drop-superfluous-prefixn, valid-group-nodes-app-transaction-prefix, valid-group-nodes-app-transaction, nodes-append-subseteq, induction-rev-list,
list/laddress-list/len-05 is used by size-0, nodes-transaction, adr-in-index-node-key,
list/group-store/len-05 is used by nodes-transaction, adr-in-index-node-key,
list/address-list-set/len-05 is used by keys-size, keys-at, index-update-adr-in,
list/key-list-set/len-05 is used by keys-size, index-update-adr-in,
list/key-list-set/rest is used by keys-same-fs,

Used from specification list-dup

list-dup/laddress-list/a is used by size-0, nodes-transaction, new-adrs-gstore, adr-in-index-node-key,
list-dup/laddress-list/d is used by nodes-transaction,
list-dup/key-list-set/dups-cons is used by index-update-adr-in,
list-dup/key-list-set/e-01 is used by index-update-adr-in,
list-dup/nat-list-set/f is used by abs-log-write-last,
list-dup/laddress-list/f-01 is used by size-0, nodes-transaction, adr-in-index-node-key,
list-dup/laddress-list/in-06 is used by new-adrs-gstore,
list-dup/nat-list-set/l is used by last-notin-butlast-nodups,

Used from specification ablock-store-refsize-cons

ablock-store-refsize-cons/group-store/refsize-cons-def is used by refsize-nonzero-notin-ginval, refsize-0-notin-index, lebs-dom-remove-refsize0,
ablock-store-refsize-cons/group-store/restrict-add is used by size-0,
ablock-store-refsize-cons/group-store/restrict-leb is used by nodes-referenced-adrs-leb, nodes-dealloc,
ablock-store-refsize-cons/group-store/size-rec-rem is used by size-0,
ablock-store-refsize-cons/group-store/refsize-cons-dealloc is used by refsize-cons-remove,
ablock-store-refsize-cons/group-store/restrict-add is used by restr-add-01, keys-remove-leb,
ablock-store-refsize-cons/group-store/restrict-add-other is used by restr-add-01,
ablock-store-refsize-cons/group-store/restrict-in is used by size-0, restr-toset-empty-notin, restr-empty-notin, nodes-dealloc,
ablock-store-refsize-cons/group-store/restrict-leb is used by size-0, ri-cons-range-restrict-notin-gstore, nodes-dealloc, keys-nodes-in-ri, in-restr-notin-log, adresses-restr-subseteq, abs-log-toset-inter-restr-empty,
ablock-store-refsize-cons/group-store/restrict-union is used by prefixn-toset-restr-empty,
ablock-store-refsize-cons/group-store/size-emp is used by size-0,
ablock-store-refsize-cons/group-store/size-rem is used by size-0,

Used from specification address-data

Used from specification oelem

oelem/nat-set/irreflexivity is used by valid-group-nodes-ls, valid-group-nodes-le, valid-group-nodes-entire, valid-group-nodes-drop, valid-group-nodes-app-transaction-prefix, nodes-append-subseteq, induction-rev-list, adr-in-index-node-key,
oelem/nat-set/transitivity is used by valid-group-nodes-ls, nodes-append-subseteq, adr-in-index-node-key,

Used from specification gjournal-abs

gjournal-abs/in-keys-elim is used by keys-remove-leb, keys-nodes-in-ri,
gjournal-abs/in-ri is used by size-0, range-rem-in, lebs-dom-remove-refsize0,
gjournal-abs/index-update-one is used by index-update-one,
gjournal-abs/key-in-update-index is used by key-in-update-index,
gjournal-abs/keys-append is used by keys-append,
gjournal-abs/keys-one is used by keys-one,
gjournal-abs/keys-size is used by keys-size,

Used from specification list-del

list-del/address-list-set/app-05-neg is used by nodes-transaction,
list-del/laddress-list/app-05-neg is used by nodes-append-subseteq,
list-del/group-store/get-append-grt is used by nodes-append-subseteq, adr-in-index-node-key,
list-del/key-list-set/get-append-grt is used by keys-at,
list-del/address-list-set/app-05 is used by nodes-transaction,
list-del/laddress-list/app-05 is used by nodes-append-subseteq-nodown, nodes-append-subseteq,
list-del/laddress-list/app-05-neg is used by nodes-transaction, nodes-append-subseteq, adr-in-index-node-key,
list-del/address-list-set/elim-firstn-restn is used by prefixn-toset-restr-empty, prefixn-toset-inter-empty, new-prefixn,
list-del/group-store/first-append is used by valid-group-nodes-prefixn-append-nonend,
list-del/group-store/first-length is used by valid-group-nodes-drop,
list-del/group-store/firstn-app is used by valid-group-nodes-prefixn-append-nonend,
list-del/group-store/firstn-length-04 is used by valid-group-nodes-drop,
list-del/group-store/firstn-one-02 is used by valid-group-nodes-prefixn-append-nonend,
list-del/laddress-list/get-app is used by size-0,
list-del/group-store/get-append-grt is used by nodes-append-subseteq-nodown,
list-del/group-store/get-append-grt-02 is used by nodes-transaction,
list-del/group-store/get-append-less is used by nodes-append-subseteq-nodown, adr-in-index-node-key,
list-del/key-list-set/get-append-less is used by keys-at,
list-del/group-store/get-butlast is used by nodes-append-subseteq,
list-del/address-list-set/get-succ is used by keys-at,
list-del/group-store/get-zero-01 is used by adr-in-index-node-key,
list-del/address-list-set/get-zero-01 is used by keys-at,
list-del/laddress-list/inl is used by nodes-append-subseteq,
list-del/laddress-list/inl-01 is used by nodes-append-subseteq-nodown, nodes-append-subseteq,
list-del/laddress-list/notin-03 is used by nodes-append-subseteq-nodown, nodes-append-subseteq,
list-del/group-store/one-03 is used by nodes-transaction,
list-del/key-list-set/one-03 is used by keys-at,
list-del/laddress-list/pos-y is used by nodes-transaction, adr-in-index-node-key,
list-del/address-list-set/pos-y is used by nodes-transaction,

Used from specification groupnode