[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 referenced-adrs-lookup-keys-nodups, referenced-adrs-lookup-keys-lookup, referenced-adrs-lookup-keys-in-dom, referenced-adrs-lookup-key-cons, range-write-in, range-del-in, lebs-write, in-rem-keys-in-data,
store+set/node-index/Data-notin-other is used by lebs-write-subseteq0, lebs-write-subseteq,
store+set/node-index/Data-in-del is used by lebs-del-subseteq,
store+set/node-index/Data-in-other is used by range-write-notin, lebs-write,
store+set/node-index/Data-in-putsame is used by lebs-write,
store+set/node-index/Data-notin-other is used by range-write-notin,
store+set/node-index/Diff-ext is used by inos-greater-rem, in-rem-keys-in-data,
store+set/node-index/Diff-get is used by in-rem-keys-in-data,
store+set/node-store/Dom is used by new-inter-empty,
store+set/node-index/Dom is used by referenced-adrs-lookup-keys-in-dom, inos-dom, index-update-range,
store+set/group-store-ablock-store-nat-store/Dom is used by refsize-cons-crash, lebs-write-subseteq0, lebs-write-subseteq, lebs-in-ri-in-gstore-explicit, lebs-in-ri-in-gstore,
store+set/node-index/In-data-in is used by ri-inj-index-update, range-add-explicit, in-rem-keys-in-data, in-index-in-range, in-data-explicit,

Used from specification ablock

ablock/group-store/elim is used by refsize-cons-in-ri-0, refsize-cons-crash, nodes-cons-write-other, nodes-cons-write-app, except-refsizeeq-valid-head,
ablock/group-store/inj is used by refsize-cons-crash, nodes-cons-write-other, nodes-cons-write-app,
ablock/group-store/sel-01 is used by nodes-cons-write-other, nodes-cons-write-app, except-refsizeeq-valid-head,
ablock/group-store/sel-02 is used by nodes-cons-write-other, nodes-cons-write-app, except-refsizeeq-valid-head,
ablock/group-store/sel-03 is used by refsize-cons-in-ri-0,

Used from specification nat-basic

Used from specification list+set

list+set/key-list-set/toSet-app is used by referenced-adrs-lookup-keys-in-dom, index-update-range, index-update-dom,
list+set/address-list-set/toSet-app is used by ri-inj-index-update, index-update-range,
list+set/key-list-set/toSet-empty is used by referenced-adrs-lookup-keys-in-dom, index-update-range, index-update-dom,
list+set/address-list-set/toSet-empty is used by ri-inj-index-update, index-update-range,
list+set/key-list-set/toSet-ext is used by referenced-adrs-lookup-keys-in-dom,
list+set/address-list-set/toSet-ext is used by referenced-adrs-subseteq-range, referenced-adrs-inter-empty, new-inter-empty,
list+set/key-list-set/toSet-one is used by referenced-adrs-lookup-keys-in-dom, index-update-range, index-update-dom,
list+set/address-list-set/toSet-one is used by ri-inj-index-update, index-update-range,

Used from specification aubifs-inv

aubifs-inv/inodes-put is used by keys-inodekeys,
aubifs-inv/ri-inj is used by range-write-in, range-del-in,
aubifs-inv/empty-inodes is used by keys-inodekeys,
aubifs-inv/inodes-nodata is used by keys-in,
aubifs-inv/inodes-nodentry is used by keys-in,
aubifs-inv/ri-cons-key is used by referenced-adrs-lookup-keys-nodups, referenced-adrs-lookup-keys-lookup, referenced-adrs-lookup-keys-in-dom, referenced-adrs-lookup-key-cons,
aubifs-inv/ri-inj-variant1-01 is used by ri-inj-index-update,
aubifs-inv/ri-key-cons is used by referenced-adrs-lookup-key-cons,

Used from specification aubifs-base

aubifs-base/keys-at-other is used by ri-inj-index-update,
aubifs-base/read-split is used by referenced-adrs-lookup-keys-nodups,
aubifs-base/data-in-empty is used by lebs-empty,
aubifs-base/index-lookup-app is used by referenced-adrs-lookup-keys-lookup, index-update-range,
aubifs-base/index-lookup-base is used by referenced-adrs-lookup-keys-lookup, index-update-range,
aubifs-base/index-lookup-one is used by referenced-adrs-lookup-keys-lookup, index-update-range,
aubifs-base/index-update-at-last-oc is used by ri-inj-index-update,
aubifs-base/index-update-in is used by ri-inj-index-update, index-update-range,
aubifs-base/index-update-key-base is used by ri-inj-index-update, index-update-range,
aubifs-base/index-update-key-rec is used by ri-inj-index-update,
aubifs-base/keys-at-other is used by ri-inj-index-update, index-update-range,
aubifs-base/new-not-new is used by new-inter-empty,
aubifs-base/range is used by ri-inj-index-update, restrict-range-notin-lebs, restrict-in-empty, refsize-cons-in-ri-0, referenced-adrs-subseteq-range, range-write-notin, range-write-in, range-del-in, range-add-explicit, lebs-range, index-update-range, in-index-in-range,
aubifs-base/range-inter-empty-in is used by index-update-range,
aubifs-base/read-app is used by referenced-adrs-lookup-keys-nodups, referenced-adrs-lookup-keys-lookup, referenced-adrs-lookup-keys-in-dom, referenced-adrs-lookup-key-cons,
aubifs-base/read-base is used by referenced-adrs-lookup-keys-nodups, referenced-adrs-lookup-keys-lookup, referenced-adrs-lookup-keys-in-dom, referenced-adrs-lookup-key-cons,
aubifs-base/read-eq-one is used by referenced-adrs-lookup-keys-nodups, referenced-adrs-eq-one-lookup,
aubifs-base/read-one is used by referenced-adrs-lookup-keys-nodups, referenced-adrs-lookup-keys-lookup, referenced-adrs-lookup-keys-in-dom, referenced-adrs-lookup-key-cons,
aubifs-base/toSet-subseteq-domri-notin is used by referenced-adrs-lookup-keys-in-dom,
aubifs-base/update-index-app is used by ri-inj-index-update, index-update-range,
aubifs-base/update-index-append is used by ri-inj-index-update,
aubifs-base/write-rec is used by at-write-at,

Used from specification key

key/inj-03 is used by keys-rem, keys-inodekey-in, keys-in, keys-empty,
key/inodekey-id is used by inos-write,
key/sel-04 is used by inos-write,
key/test-02 is used by keys-inodekeys, inos-write,

Used from specification ablock-store-inv

ablock-store-inv/group-store/at is used by nodes-cons-write-other, nodes-cons-write-app,
ablock-store-inv/group-store/except-refsize-eq is used by except-refsizeeq-valid-head,
ablock-store-inv/group-store/in is used by nodes-cons-write-other, nodes-cons-write-app,
ablock-store-inv/group-store/addresslist-in-lnum-simp is used by nodes-cons-write-app,
ablock-store-inv/group-store/addresslist-length is used by nodes-cons-write-app,
ablock-store-inv/group-store/adrs-rec is used by nodes-cons-write-app, ladrlist-to-adr-split,
ablock-store-inv/group-store/at-explicit-other is used by nodes-cons-write-other,
ablock-store-inv/group-store/in-adr-in is used by nodes-cons-write-other,
ablock-store-inv/group-store/in-write-app is used by nodes-cons-write-app,
ablock-store-inv/group-store/in-write-explicit is used by nodes-cons-write-other, nodes-cons-write-app,
ablock-store-inv/group-store/notin-notin is used by nodes-cons-write-other,
ablock-store-inv/group-store/to-adrs-append is used by nodes-cons-write-app, ladrlist-to-adr-split,

Used from specification apersistence-base

apersistence-base/crash-group-in is used by refsize-cons-crash,
apersistence-base/crash-group-at is used by refsize-cons-crash,
apersistence-base/elems-def is used by refsize-cons-crash,

Used from specification nat

nat/add-01 is used by transaction-prefix-app-nonlast,
nat/add-num-01 is used by at-write-at,
nat/anti is used by transaction-prefix-app-nonlast, transaction-prefix-app-last,
nat/elim-pred-c is used by transaction-prefix-last-nonend, transaction-prefix-is-transaction-prefix, transaction-prefix-app-nonlast, transaction-prefix-app-last, nodes-cons-write-app, nodes-cons-rec, ladrlist-to-adr-split, key-cons-ext,
nat/eq-01 is used by nodes-cons-write-app,
nat/eqle-one is used by nodes-cons-write-app,
nat/fle is used by transaction-prefix-is-transaction-prefix, transaction-prefix-app, natset-ls-add-max-ls,
nat/fle-01 is used by transaction-prefix-is-transaction-prefix, natset-ls-max-ls,
nat/le-def is used by transaction-prefix-is-transaction-prefix, ri-inj-index-update,
nat/le-ls-simp is used by transaction-prefix-is-transaction-prefix, transaction-prefix-app-last, transaction-prefix-app, natset-ls-add-max-ls, inos-greater-rem, inos-greater-del,
nat/le-one is used by natset-ls-add-max-ls,
nat/lels is used by transaction-prefix-is-transaction-prefix, transaction-prefix-app-nonlast, transaction-prefix-app-last, transaction-prefix-app, ri-inj-index-update, nodes-cons-write-app, nodes-cons-rec, natset-ls-max-ls, natset-ls-add-max-ls, ladrlist-to-adr-split, key-cons-ext, inos-greater-rem, inos-greater-del,
nat/lels-02 is used by transaction-prefix-is-transaction-prefix,
nat/lels-03 is used by transaction-prefix-is-transaction-prefix, transaction-prefix-app-nonlast, transaction-prefix-app-last,
nat/lep is used by transaction-prefix-is-transaction-prefix, transaction-prefix-app-nonlast, nodes-cons-write-app,
nat/ler is used by transaction-prefix-app-nonlast, transaction-prefix-app-last, nodes-cons-write-app,
nat/let is used by transaction-prefix-is-transaction-prefix, transaction-prefix-app-nonlast,
nat/lez is used by transaction-prefix-app-nonlast, transaction-prefix-app-last, nodes-cons-write-app, nodes-cons-rec, ladrlist-to-adr-split, key-cons-ext,
nat/lez-01 is used by transaction-prefix-app-nonlast, transaction-prefix-app-last,
nat/ls-le-simp is used by nodes-cons-write-app,
nat/not-zero is used by transaction-prefix-is-transaction-prefix,
nat/one-02 is used by transaction-prefix-is-transaction-prefix,
nat/succ-01 is used by transaction-prefix-is-transaction-prefix, transaction-prefix-app-nonlast, transaction-prefix-app-last, nodes-cons-write-app, nodes-cons-rec, natset-ls-add-max-ls, ladrlist-to-adr-split, key-cons-ext,
nat/zero is used by transaction-prefix-app-nonlast, transaction-prefix-app-last, ri-inj-index-update, nodes-cons-write-app,

Used from specification store

store/node-index/At-other is used by ri-inj-index-update, range-write-in,
store/group-store-ablock-store-nat-store/At-other is used by nodes-cons-write-other,
store/node-index/At-other is used by ri-inj-index-update,
store/node-store/At-same is used by at-write-at,
store/node-index/At-same is used by ri-inj-index-update, range-write-in,
store/group-store-ablock-store-nat-store/At-same is used by nodes-cons-write-other, nodes-cons-write-app,
store/node-index/Del-at is used by range-del-in,
store/node-index/Del-in is used by range-del-in, inos-greater-del,
store/node-index/In-empty is used by inos-empty,
store/node-index/In-insert is used by range-write-in, inos-write,
store/group-store-ablock-store-nat-store/In-insert is used by nodes-cons-write-other,
store/node-index/in-neq is used by ri-inj-index-update, range-write-in,
store/group-store-ablock-store-nat-store/in-neq is used by nodes-cons-write-other,
store/node-index/insin is used by ri-inj-index-update, range-write-in,
store/group-store-ablock-store-nat-store/insin is used by nodes-cons-write-other,
store/group-store-ablock-store-nat-store/notmemlookup is used by refsize-cons-crash,

Used from specification set-union

set-union/node-store/del-in is used by index-update-range,
set-union/node-store/subdef is used by referenced-adrs-subseteq-range,
set-union/nat-set/subdef is used by lebs-write-subseteq0, lebs-write-subseteq, lebs-rem-subseteq, lebs-lookup-subseteq, lebs-in-ri-in-gstore-explicit, lebs-in-ri-in-gstore, lebs-del-subseteq-set, lebs-del-subseteq,
set-union/nat-set/unrax is used by refsize-cons-crash,
set-union/nat-set/Delete is used by keys-rem,
set-union/node-store/Delete is used by range-write-in, range-del-in, lebs-del-subseteq-set,
set-union/node-index/Delete is used by keys-rem,
set-union/node-store/Intersect is used by referenced-adrs-inter-empty, new-inter-empty,
set-union/node-store/diff-add-del is used by index-update-range,
set-union/node-store/diff-e is used by index-update-range,
set-union/node-store/int-a is used by ri-inj-index-update, referenced-adrs-inter-empty, new-inter-empty, index-update-range,
set-union/node-store/int-c is used by ri-inj-index-update, referenced-adrs-inter-empty, new-inter-empty, index-update-range,
set-union/node-store/int-e is used by ri-inj-index-update, index-update-range,
set-union/node-store/int-ins is used by ri-inj-index-update, index-update-range,
set-union/node-store/intu-empty is used by ri-inj-index-update,
set-union/nat-set/una is used by refsize-cons-crash, inos-write,
set-union/node-index/una is used by referenced-adrs-lookup-keys-in-dom, index-update-range, index-update-dom,
set-union/node-store/una is used by ri-inj-index-update, index-update-range,
set-union/node-index/unadd is used by index-update-range, index-update-dom,
set-union/nat-set/unadd is used by inos-write,
set-union/node-store/unadd is used by ri-inj-index-update, index-update-range,
set-union/node-index/unc is used by referenced-adrs-lookup-keys-in-dom, index-update-range, index-update-dom,
set-union/nat-set/unc is used by refsize-cons-crash, inos-write,
set-union/node-store/unc is used by ri-inj-index-update, index-update-range,
set-union/node-store/undel is used by index-update-range,
set-union/node-store/undel-02 is used by index-update-range,
set-union/node-index/une is used by index-update-range, index-update-dom,
set-union/nat-set/une is used by inos-write,
set-union/node-store/une is used by ri-inj-index-update, index-update-range,
set-union/nat-set/unin-01 is used by refsize-cons-crash, inos-write,
set-union/node-index/unsub-union-01 is used by referenced-adrs-lookup-keys-in-dom,

Used from specification min-max

min-max/max is used by natset-ls-add-max-ls,
min-max/max-notls2 is used by natset-ls-max-ls,

Used from specification set-basic

set-basic/node-index/Extension is used by keys-rem, keys-empty, inos-dom,
set-basic/node-store/Extension is used by restrict-range-notin-lebs, restrict-in-empty, referenced-adrs-inter-empty, range-write-notin, range-write-in, range-del-in, new-inter-empty,
set-basic/nat-set/Extension is used by refsize-cons-crash, lebs-write, lebs-range, lebs-empty, keys-inodekeys, keys-inodekey-in, keys-empty, inos-write, inos-empty, inos-dom,
set-basic/node-store/indef is used by refsize-cons-in-ri-0,
set-basic/nat-set/indef is used by keys-inodekeys, keys-inodekey-in,
set-basic/nat-set/In-empty is used by lebs-empty, keys-inodekeys, keys-inodekey-in, keys-empty, inos-empty,
set-basic/node-store/In-empty is used by restrict-range-notin-lebs, restrict-in-empty, referenced-adrs-inter-empty, new-inter-empty,
set-basic/node-index/In-empty is used by keys-inodekey-in, keys-empty,
set-basic/node-store/In-insert is used by range-write-notin, range-write-in,
set-basic/nat-set/In-insert is used by natset-ls-add-max-ls, lebs-write, keys-inodekey-in, inos-write,
set-basic/node-index/In-insert is used by keys-inodekey-in,
set-basic/nat-set/Size-insert is used by keys-inodekeys, keys-inodekey-in,
set-basic/nat-set/add is used by lebs-write-subseteq,
set-basic/nat-set/eq is used by keys-rec-full,
set-basic/node-store/eq-03 is used by range-add-explicit,
set-basic/node-index/eq-03 is used by keys-rec-full,
set-basic/nat-set/in-04 is used by inos-write,
set-basic/nat-set/ne is used by inos-write,
set-basic/node-store/ne-01 is used by referenced-adrs-inter-empty, new-inter-empty, lebs-lookup-subseteq, lebs-del-subseteq-set,
set-basic/nat-set/ne-01 is used by refsize-cons-crash, natset-ls-max-ls, natset-ls-add-max-ls, keys-rec-full, inos-write,
set-basic/node-index/ne-01 is used by keys-in,
set-basic/nat-set/size-zero is used by lebs-empty, keys-inodekeys, keys-inodekey-in, keys-empty, inos-write, inos-empty,
set-basic/node-store/size-zero is used by restrict-range-notin-lebs, referenced-adrs-inter-empty, new-inter-empty,
set-basic/nat-set/size-zero-01 is used by refsize-cons-crash, natset-ls-max-ls, natset-ls-add-max-ls, lebs-empty, keys-inodekeys, keys-inodekey-in, keys-empty, inos-write, inos-empty,
set-basic/node-store/size-zero-01 is used by restrict-range-notin-lebs, referenced-adrs-inter-empty, new-inter-empty, lebs-lookup-subseteq, lebs-del-subseteq-set,
set-basic/node-index/size-zero-01 is used by keys-in,
set-basic/node-index/sub-add-03 is used by index-update-range,
set-basic/node-index/sub-e is used by referenced-adrs-lookup-keys-in-dom, index-update-range,
set-basic/node-store/sub-in is used by new-inter-empty,
set-basic/node-index/sub-ntrans-01 is used by referenced-adrs-lookup-keys-in-dom,
set-basic/nat-set/sub-ntrans-01 is used by lebs-write-subseteq0, lebs-rem-subseteq, lebs-lookup-subseteq, lebs-del-subseteq-set, lebs-del-subseteq,
set-basic/node-index/sub-one-02 is used by referenced-adrs-lookup-keys-in-dom,

Used from specification list-last

list-last/group-store/l-02 is used by transaction-prefix-is-transaction-prefix, nodes-cons-write-app,
list-last/group-store/lapp-04 is used by transaction-prefix-app-nonlast,
list-last/group-store/last-def is used by transaction-prefix-app-last, transaction-last-nend,

Used from specification gjournal-base

gjournal-base/at-write-other is used by at-write-other, at-write-at,
gjournal-base/in-write is used by in-write,
gjournal-base/index-update-dom is used by index-update-dom,
gjournal-base/range-empty is used by range-empty,

Used from specification list-prefixn

list-prefixn/group-store/in-prefixn-at-smaller is used by transaction-prefix-is-transaction-prefix,
list-prefixn/group-store/prefixn-shift-right is used by transaction-prefix-is-transaction-prefix,
list-prefixn/group-store/prefixn-append-left is used by transaction-prefix-is-transaction-prefix,
list-prefixn/group-store/prefixn-eq-empty is used by transaction-prefix-is-transaction-prefix,
list-prefixn/group-store/prefixn-fulln is used by transaction-prefix-is-transaction-prefix,
list-prefixn/group-store/prefixn-len-n is used by transaction-prefix-is-transaction-prefix,

Used from specification list-data

list-data/node-list/elim-list-c is used by transaction-prefix-app-last,
list-data/group-store/elim-list-c is used by transaction-prefix-last-nonend, transaction-prefix-is-transaction-prefix, transaction-prefix-app-nonlast, transaction-prefix-app-last, transaction-prefix-app, nodes-cons-write-app,
list-data/group-store/l is used by transaction-prefix-last-nonend, transaction-prefix-is-transaction-prefix, transaction-prefix-app-nonlast, transaction-prefix-app-last, transaction-prefix-app, transaction-empty, nodes-cons-write-app,
list-data/node-list/l is used by transaction-prefix-last-nonend, transaction-prefix-is-transaction-prefix, transaction-prefix-empty, transaction-prefix-app-nonlast, transaction-prefix-app-last, transaction-prefix-app, transaction-empty-right, nodes-cons-write-other, nodes-cons-rec, key-cons-ext, in-write,
list-data/laddress-list/l is used by nodes-cons-write-app, ladrlist-to-adr-split,
list-data/address-list-set/l is used by ri-inj-index-update, index-update-range, index-update-dom,
list-data/key-list-set/l is used by ri-inj-index-update, index-update-range,
list-data/address-list-set/size-01 is used by ri-inj-index-update, index-update-range, index-update-dom, in-write, at-write-at,
list-data/group-store/size-01 is used by transaction-prefix-last-nonend, transaction-prefix-is-transaction-prefix, transaction-prefix-empty, transaction-prefix-app-nonlast, transaction-prefix-app-last, transaction-empty-right, nodes-cons-write-app, nds-length,
list-data/node-list/size-01 is used by transaction-prefix-empty, transaction-prefix-app-last, transaction-empty-right, transaction-empty, nds-length, keys-len, key-cons-ext, in-write, at-write-at,
list-data/laddress-list/size-01 is used by nodes-cons-write-app, ladrlist-to-adr-split,
list-data/key-list-set/size-01 is used by ri-inj-index-update, keys-len, index-update-range, index-update-dom,

Used from specification laddress

laddress/elim is used by ladrlist-to-adr-split,
laddress/inj is used by ladrlist-to-adr-split,
laddress/sel-01 is used by nodes-cons-write-app, ladrlist-to-adr-split,
laddress/sel-02 is used by nodes-cons-write-app, ladrlist-to-adr-split,

Used from specification list

list/node-list/One is used by keys-one, key-cons-one, flashsize-one,
list/address-list-set/One is used by referenced-adrs-one,
list/group-store/One is used by nds-one,
list/address-list-set/c is used by referenced-adrs-one,
list/node-list/c is used by keys-one, key-cons-one, flashsize-one,
list/address-list-set/in-def is used by at-write-at,
list/key-list-set/in-def is used by referenced-adrs-lookup-keys-nodups,
list/group-store/lastdiv-rew is used by transaction-prefix-last-nonend,
list/key-list-set/lastdiv-rew is used by ri-inj-index-update, index-update-range,
list/address-list-set/lastdiv-rew is used by ri-inj-index-update, index-update-range,
list/key-list-set/lastoc-rew is used by ri-inj-index-update,
list/address-list-set/split-first is used by ri-inj-index-update,
list/address-list-set/Nil is used by referenced-adrs-split-one, referenced-adrs-split, referenced-adrs-nodups, referenced-adrs-app, at-write-at,
list/group-store/Nil is used by transaction-prefix-app-nonlast, transaction-prefix-app-last, nds-app,
list/node-list/Nil is used by nds-app, keys-split, keys-app, key-cons-app, flashsize-app,
list/laddress-list/Nil is used by nodes-cons-write-app, ladrlist-to-adr-split,
list/key-list-set/Nil is used by referenced-adrs-lookup-keys-nodups, keys-split, keys-app,
list/address-list-set/a is used by ri-inj-index-update, referenced-adrs-split-one, referenced-adrs-split, referenced-adrs-one, referenced-adrs-nodups, referenced-adrs-lookup-keys-nodups, referenced-adrs-lookup-keys-lookup, referenced-adrs-lookup-keys-in-dom, referenced-adrs-lookup-key-cons, referenced-adrs-in, referenced-adrs-eq-one-lookup, referenced-adrs-app, nodes-cons-write-app, nodes-cons-rec, ladrlist-to-adr-split, index-update-range, in-write, at-write-at,
list/node-list/a is used by transaction-prefix-app-nonlast, transaction-prefix-app-last, referenced-adrs-lookup-keys-nodups, referenced-adrs-lookup-keys-lookup, referenced-adrs-lookup-keys-in-dom, referenced-adrs-lookup-key-cons, nodes-cons-rec, nds-length, nds-eq-one, nds-eq-empty, nds-app, keys-split, keys-len, keys-eq-one, keys-app, key-cons-ext, key-cons-app, flashsize-app, at-write-at,
list/group-store/a is used by transaction-prefix-last-nonend, transaction-prefix-is-transaction-prefix, transaction-prefix-app-nonlast, transaction-prefix-app-last, transaction-prefix-app, transaction-last-nend, nodes-cons-write-app, nds-one, nds-length, nds-eq-one, nds-eq-empty, nds-app,
list/key-list-set/a is used by ri-inj-index-update, referenced-adrs-lookup-keys-nodups, referenced-adrs-lookup-keys-lookup, referenced-adrs-lookup-keys-in-dom, keys-split, keys-one, keys-len, keys-eq-one, keys-app, index-update-range, index-update-dom,
list/laddress-list/a is used by nodes-cons-write-app, ladrlist-to-adr-split,
list/address-list-set/app is used by referenced-adrs-one,
list/node-list/app is used by nds-eq-one, keys-eq-one,
list/key-list-set/app is used by keys-one,
list/laddress-list/app is used by nodes-cons-write-app,
list/group-store/app is used by transaction-prefix-last-nonend, transaction-prefix-app-nonlast, nds-one,
list/address-list-set/app-01 is used by referenced-adrs-split, referenced-adrs-app,
list/key-list-set/app-01 is used by keys-split,
list/group-store/app-02 is used by transaction-prefix-last-nonend, transaction-prefix-app-nonlast, transaction-prefix-app-last, transaction-prefix-app,
list/key-list-set/app-02 is used by keys-split, keys-eq-one,
list/address-list-set/app-02 is used by referenced-adrs-split,
list/node-list/app-02 is used by nds-eq-empty,
list/address-list-set/app-03 is used by referenced-adrs-lookup-keys-lookup,
list/group-store/app-06 is used by transaction-prefix-last-nonend,
list/address-list-set/app-08 is used by referenced-adrs-split-one, referenced-adrs-split,
list/key-list-set/app-08 is used by keys-split, keys-app,
list/laddress-list/app-08 is used by ladrlist-to-adr-split,
list/node-list/app-08 is used by nds-app, keys-split,
list/address-list-set/c is used by ri-inj-index-update, referenced-adrs-split-one, referenced-adrs-split, referenced-adrs-nodups, referenced-adrs-lookup-keys-nodups, referenced-adrs-lookup-keys-lookup, referenced-adrs-lookup-keys-in-dom, referenced-adrs-lookup-key-cons, referenced-adrs-in, referenced-adrs-app, nodes-cons-write-app, ladrlist-to-adr-split, in-write, at-write-at,
list/node-list/c is used by transaction-prefix-app-last, nds-length, nds-eq-one, nds-eq-empty, nds-app, keys-split, keys-len, keys-eq-one, keys-app, key-cons-ext, key-cons-app, flashsize-app, at-write-at,
list/group-store/c is used by transaction-prefix-last-nonend, transaction-prefix-is-transaction-prefix, transaction-prefix-app-nonlast, transaction-prefix-app-last, transaction-prefix-app, nodes-cons-write-app, nds-one, nds-length, nds-eq-one, nds-eq-empty, nds-app,
list/key-list-set/c is used by referenced-adrs-lookup-keys-nodups, keys-split, keys-one, keys-len, keys-eq-one, keys-app, index-update-dom,
list/laddress-list/c is used by ladrlist-to-adr-split,
list/address-list-set/c-03 is used by referenced-adrs-split-one,
list/node-list/c-03 is used by nds-eq-one,
list/key-list-set/c-03 is used by keys-eq-one,
list/group-store/c-03 is used by transaction-prefix-app-nonlast, transaction-prefix-app-last, nds-eq-one,
list/key-list-set/c-04 is used by keys-one, keys-eq-one,
list/address-list-set/c-04 is used by referenced-adrs-lookup-keys-lookup,
list/node-list/c-04 is used by nds-eq-one, keys-eq-one,
list/group-store/c-04 is used by nds-one,
list/group-store/c-05 is used by transaction-prefix-last-nonend,
list/key-list-set/c-06 is used by keys-split,
list/group-store/c-06 is used by transaction-prefix-app-nonlast, transaction-prefix-app-last,
list/laddress-list/c-06 is used by ladrlist-to-adr-split,
list/address-list-set/c-06 is used by referenced-adrs-split,
list/group-store/c-08 is used by transaction-prefix-is-transaction-prefix,
list/key-list-set/e is used by keys-eq-one,
list/node-list/e is used by nds-eq-one, nds-eq-empty,
list/address-list-set/e is used by referenced-adrs-split-one,
list/group-store/e is used by transaction-prefix-last-nonend, transaction-prefix-app-nonlast, transaction-prefix-app-last, nds-eq-one,
list/node-list/e-01 is used by transaction-prefix-app-last,
list/laddress-list/e-01 is used by ladrlist-to-adr-split,
list/group-store/e-01 is used by transaction-prefix-is-transaction-prefix, transaction-prefix-app-nonlast, transaction-prefix-app-last, transaction-prefix-app, nodes-cons-write-app,
list/group-store/e-02 is used by transaction-prefix-last-nonend, transaction-prefix-app-nonlast, transaction-prefix-app-last, transaction-last-nend,
list/laddress-list/e-03 is used by nodes-cons-write-app, ladrlist-to-adr-split,
list/address-list-set/eq-04 is used by referenced-adrs-split-one,
list/group-store/first is used by transaction-prefix-is-transaction-prefix,
list/group-store/first-01 is used by transaction-prefix-app,
list/group-store/in-01 is used by transaction-prefix-app-nonlast,
list/address-list-set/in-06 is used by ri-inj-index-update, at-write-at,
list/laddress-list/in-10 is used by nodes-cons-write-app,
list/group-store/in-11 is used by transaction-prefix-app-nonlast,
list/address-list-set/in-13 is used by referenced-adrs-lookup-keys-nodups,
list/key-list-set/in-14 is used by keys-split,
list/laddress-list/in-14 is used by ladrlist-to-adr-split,
list/group-store/in-14 is used by transaction-prefix-last-nonend, transaction-prefix-app-nonlast, transaction-prefix-app-last,
list/node-list/in-14 is used by referenced-adrs-lookup-keys-nodups,
list/address-list-set/in-14 is used by referenced-adrs-split-one, referenced-adrs-split, referenced-adrs-lookup-keys-nodups,
list/group-store/in-15 is used by transaction-prefix-last-nonend, transaction-prefix-app-nonlast, transaction-prefix-app-last,
list/address-list-set/in-17 is used by referenced-adrs-in,
list/group-store/in-17 is used by transaction-prefix-last-nonend, transaction-prefix-app-nonlast, transaction-prefix-app-last,
list/node-list/in-17 is used by referenced-adrs-lookup-keys-nodups,
list/address-list-set/in-append is used by ri-inj-index-update, referenced-adrs-split-one, referenced-adrs-split, referenced-adrs-lookup-keys-nodups, referenced-adrs-in, nodes-cons-write-app, at-write-at,
list/group-store/in-append is used by transaction-prefix-last-nonend, transaction-prefix-app-nonlast, transaction-prefix-app-last,
list/key-list-set/in-append is used by keys-split,
list/laddress-list/in-append is used by nodes-cons-write-app, ladrlist-to-adr-split,
list/node-list/in-append is used by referenced-adrs-lookup-keys-nodups,
list/group-store/in-append0-not-left is used by transaction-prefix-app-nonlast, transaction-prefix-app-last,
list/address-list-set/in-empty is used by referenced-adrs-split, referenced-adrs-in, in-write, at-write-at,
list/group-store/in-empty is used by transaction-prefix-app-nonlast,
list/laddress-list/in-empty is used by nodes-cons-write-app,
list/key-list-set/in-empty is used by keys-split,
list/address-list-set/in-rec is used by referenced-adrs-split, referenced-adrs-lookup-keys-nodups, referenced-adrs-in, nodes-cons-write-app, in-write,
list/group-store/in-rec is used by transaction-prefix-last-nonend, transaction-prefix-app-nonlast, transaction-prefix-app-last,
list/key-list-set/in-rec is used by keys-split,
list/node-list/in-rec is used by referenced-adrs-lookup-keys-nodups,
list/laddress-list/in-rec is used by ladrlist-to-adr-split,
list/group-store/inapp-07 is used by transaction-prefix-last-nonend,
list/group-store/inapp-08 is used by transaction-prefix-app-nonlast, transaction-prefix-app-last,
list/group-store/inapp-10 is used by transaction-prefix-app-nonlast,
list/address-list-set/len is used by ri-inj-index-update, index-update-range, at-write-at,
list/node-list/len is used by transaction-prefix-app-nonlast, transaction-prefix-app-last,
list/group-store/len is used by transaction-prefix-last-nonend, transaction-prefix-app-nonlast, transaction-prefix-app-last, transaction-prefix-app, transaction-last-nend,
list/key-list-set/len is used by ri-inj-index-update, index-update-range,
list/laddress-list/len is used by nodes-cons-write-app, ladrlist-to-adr-split,
list/address-list-set/len-02 is used by ri-inj-index-update, nodes-cons-rec, ladrlist-to-adr-split, index-update-range,
list/group-store/len-02 is used by transaction-prefix-last-nonend, transaction-prefix-is-transaction-prefix, transaction-prefix-app-nonlast, transaction-prefix-app-last, transaction-last-nend, nodes-cons-write-app,
list/key-list-set/len-02 is used by ri-inj-index-update, index-update-range,
list/node-list/len-02 is used by transaction-prefix-app-last, key-cons-ext,
list/address-list-set/len-05 is used by ri-inj-index-update, nodes-cons-rec, in-write, at-write-at,
list/group-store/len-05 is used by transaction-prefix-last-nonend, transaction-prefix-is-transaction-prefix, transaction-prefix-app-nonlast, transaction-prefix-app-last, transaction-prefix-app, nodes-cons-write-app, nds-length,
list/node-list/len-05 is used by transaction-prefix-app-nonlast, transaction-prefix-app-last, nodes-cons-rec, nds-length, keys-len, key-cons-ext, at-write-at,
list/laddress-list/len-05 is used by nodes-cons-write-app, ladrlist-to-adr-split,
list/key-list-set/len-05 is used by ri-inj-index-update, keys-len, index-update-dom,
list/group-store/ni is used by transaction-prefix-app-nonlast, transaction-prefix-app-last,

Used from specification list-dup

list-dup/key-list-set/a is used by referenced-adrs-lookup-keys-nodups,
list-dup/address-list-set/a is used by ri-inj-index-update, referenced-adrs-lookup-keys-nodups, at-write-at,
list-dup/laddress-list/a is used by nodes-cons-write-app,
list-dup/key-list-set/c is used by referenced-adrs-lookup-keys-nodups,
list-dup/address-list-set/c-02 is used by at-write-at,
list-dup/key-list-set/c-03 is used by referenced-adrs-lookup-keys-nodups,
list-dup/key-list-set/d is used by referenced-adrs-lookup-keys-nodups,
list-dup/laddress-list/d is used by nodes-cons-write-app,
list-dup/address-list-set/dups-cons is used by ri-inj-index-update, referenced-adrs-nodups, referenced-adrs-lookup-keys-nodups, at-write-at,
list-dup/key-list-set/dups-cons is used by referenced-adrs-lookup-keys-nodups,
list-dup/address-list-set/e-01 is used by ri-inj-index-update, referenced-adrs-nodups, at-write-at,
list-dup/laddress-list/e-01 is used by nodes-cons-write-app,
list-dup/key-list-set/e-01 is used by referenced-adrs-lookup-keys-nodups, index-update-range,
list-dup/address-list-set/f is used by ri-inj-index-update, index-update-range,
list-dup/key-list-set/f is used by referenced-adrs-lookup-keys-nodups, index-update-range,
list-dup/address-list-set/f-01 is used by ri-inj-index-update, referenced-adrs-lookup-keys-nodups, at-write-at,
list-dup/laddress-list/f-01 is used by nodes-cons-write-app,

Used from specification address-data

Used from specification ablock-store-refsize-cons

ablock-store-refsize-cons/group-store/refsize-cons-def is used by refsize-cons-in-ri-0, refsize-cons-crash,
ablock-store-refsize-cons/group-store/restrict-add is used by refsize-cons-in-ri-0,
ablock-store-refsize-cons/group-store/restrict-in is used by restrict-in-empty, refsize-cons-in-ri-0,
ablock-store-refsize-cons/group-store/restrict-leb is used by restrict-range-notin-lebs,
ablock-store-refsize-cons/group-store/size-emp is used by refsize-cons-crash,
ablock-store-refsize-cons/group-store/size-rec-simp is used by refsize-cons-in-ri-0,

Used from specification oelem

oelem/nat-set/irreflexivity is used by transaction-prefix-last-nonend, transaction-prefix-app-nonlast, ri-inj-index-update, nodes-cons-write-app, natset-ls-add-max-ls, keys-inodekeys, keys-inodekey-in, inos-greater-notin, index-update-range,
oelem/nat-set/ls-le is used by transaction-prefix-is-transaction-prefix,
oelem/nat-set/transitivity is used by transaction-prefix-is-transaction-prefix, transaction-prefix-app,

Used from specification list-del

list-del/group-store/get-append-grt is used by transaction-prefix-last-nonend, transaction-prefix-is-transaction-prefix, transaction-prefix-app-nonlast, transaction-prefix-app-last, transaction-prefix-app, nodes-cons-write-app,
list-del/node-list/get-append-grt is used by transaction-prefix-app-nonlast, transaction-prefix-app-last, key-cons-ext,
list-del/address-list-set/get-append-grt is used by ri-inj-index-update, nodes-cons-write-app, nodes-cons-rec, ladrlist-to-adr-split,
list-del/address-list-set/app-05-neg is used by at-write-at,
list-del/laddress-list/app-05-neg is used by nodes-cons-write-app,
list-del/group-store/get-append-grt is used by transaction-prefix-is-transaction-prefix, transaction-prefix-app-nonlast, transaction-prefix-app-last,
list-del/node-list/get-append-less is used by transaction-prefix-app-nonlast,
list-del/address-list-set/get-append-less is used by ri-inj-index-update, nodes-cons-write-app, nodes-cons-rec, ladrlist-to-adr-split,
list-del/group-store/get-append-less is used by transaction-prefix-last-nonend, transaction-prefix-is-transaction-prefix, transaction-prefix-app-nonlast, transaction-prefix-app-last, transaction-prefix-app, nodes-cons-write-app,
list-del/group-store/get-butlast is used by transaction-prefix-app-nonlast, transaction-prefix-app-last,
list-del/node-list/get-butlast is used by transaction-prefix-app-last,
list-del/address-list-set/get-in is used by ri-inj-index-update,
list-del/group-store/get-last is used by transaction-prefix-last-nonend,
list-del/node-list/get-last is used by transaction-prefix-app-last,
list-del/group-store/get-last-03 is used by transaction-prefix-app-nonlast,
list-del/node-list/get-succ is used by nodes-cons-rec, key-cons-ext, at-write-at,
list-del/group-store/get-succ is used by transaction-prefix-app-nonlast, transaction-prefix-app-last, nodes-cons-write-app,
list-del/address-list-set/get-succ is used by nodes-cons-rec, ladrlist-to-adr-split,
list-del/node-list/get-zero is used by transaction-prefix-app-last,
list-del/group-store/get-zero is used by transaction-prefix-app-nonlast, transaction-prefix-app-last,
list-del/node-list/get-zero-01 is used by transaction-prefix-app-nonlast, transaction-prefix-app-last, nodes-cons-rec, key-cons-ext, at-write-at,
list-del/address-list-set/get-zero-01 is used by ri-inj-index-update, nodes-cons-write-app, nodes-cons-rec, ladrlist-to-adr-split,
list-del/group-store/get-zero-01 is used by transaction-prefix-is-transaction-prefix, nodes-cons-write-app,
list-del/node-list/one-03 is used by transaction-prefix-app-last,
list-del/address-list-set/one-03 is used by nodes-cons-rec, ladrlist-to-adr-split,
list-del/group-store/one-03 is used by transaction-prefix-last-nonend, transaction-prefix-app-nonlast, transaction-prefix-app-last, nodes-cons-write-app,
list-del/address-list-set/pos-y is used by at-write-at,
list-del/laddress-list/pos-y is used by nodes-cons-write-app,

Used from specification groupnode

Used from specification index-base

index-base/lookup-keys is used by lebs-lookup-subseteq,

Used from specification oset

oset/nat-set/Greater is used by natset-ls-max-ls, natset-ls-add-max-ls, inos-greater-rem, inos-greater-notin, inos-greater-del,