Used simplifier rules/spec theorems by specification

Used from specification store+set

• store+set/node-index/Data-in is used by notin-dels, notin-del, data-in-empty,
• store+set/node-index/Diff-get is used by inode-at-del-datakeys, dentry-at-del-datakeys, data-at-del-datakeys,
• store+set/node-index/Data-notin-other is used by update-index-data-notin,
• store+set/node-index/Diff-base is used by del-with-emp,
• store+set/node-index/Diff-del-rw is used by in-del-ro, at-del-ro-nodata, at-del-ro-data,
• store+set/node-index/Diff-ext is used by in-dels-ro, in-del-ro,
• store+set/node-index/Diff-get is used by at-dels-ro-nodata, at-dels-ro-data, at-del-ro-nodata, at-del-ro-data,
• store+set/node-index/Diff-mems-get is used by inode-at-del-datakeys, dentry-at-del-datakeys, data-at-del-datakeys, at-dels-ro-nodata, at-dels-ro-data, at-del-ro-nodata, at-del-ro-data,
• store+set/node-index/Dom is used by toSet-subseteq-domri-notin, in-read-in-dom,
• store+set/node-index/In-data-in is used by range-inter-empty-in, notin-dels, notin-del, in-read-in-dom,
• store+set/node-store/dom-ins is used by write-dom,
• store+set/node-index/dom-ins is used by index-update-dom,

Used from specification nat-basic

• nat-basic/a is used by write-shift, write-dom, write-app, update-index-shift, update-index-data-notin, update-index-append, read-length, new-inode-exists, new-butlastn, keys-length, keys-firstn, keys-at-other, index-update-in, index-update-dom, index-update-at-last-oc, index-lookup-length, in-write, at-write-other, at-write-at,
• nat-basic/c is used by write-shift, write-dom, write-app, update-index-shift, update-index-data-notin, update-index-append, read-length, new-inode-exists, new-butlastn, keys-length, keys-firstn, keys-at-other, index-update-in, index-update-dom, index-update-at-last-oc, index-lookup-length, in-write, at-write-other, at-write-at,
• nat-basic/eq-01 is used by write-shift, write-dom, write-app, update-index-shift, update-index-data-notin, update-index-append, read-length, keys-length, keys-at-other, index-update-in, index-update-dom, index-update-at-last-oc, index-lookup-length, in-write, at-write-other, at-write-at,
• nat-basic/f is used by new-inode-exists,
• nat-basic/l-02 is used by new-inode-exists,
• nat-basic/l-05 is used by new-inode-exists,
• nat-basic/lf is used by new-inode-exists,
• nat-basic/oz is used by new-inode-exists,
• nat-basic/ref is used by new-inode-exists,
• nat-basic/s-04 is used by new-inode-exists,
• nat-basic/succ is used by write-shift, write-dom, write-app, update-index-shift, update-index-data-notin, update-index-append, update-index-app, read-length, new-inode-exists, keys-length, keys-firstn, keys-at-other, index-update-in, index-update-dom, index-update-at-last-oc, index-lookup-length, in-write, at-write-other, at-write-at,
• nat-basic/trans is used by new-inode-exists,
• nat-basic/z-01 is used by write-shift, write-dom, write-app, update-index-shift, update-index-data-notin, update-index-append, keys-at-other, index-update-in, index-update-dom, index-update-at-last-oc, in-write, at-write-other, at-write-at,

Used from specification list+set

• list+set/address-list-set/toSet-app is used by write-dom,
• list+set/key-list-set/toSet-app is used by index-update-dom, in-read-in-dom,
• list+set/key-list-set/toSet-empty is used by index-update-dom, in-read-in-dom,
• list+set/address-list-set/toSet-empty is used by write-dom,
• list+set/key-list-set/toSet-ext is used by toSet-subseteq-domri-notin,
• list+set/address-list-set/toSet-one is used by write-dom,
• list+set/key-list-set/toSet-one is used by index-update-dom, in-read-in-dom,

Used from specification key

• key/ex-02 is used by new-inode-exists,
• key/disj-01 is used by del-put-again, del-del-again,
• key/elim-02 is used by notin-dels, notin-del, dels-ignore-data, del-this, del-put-again, del-merge-dels, del-del-again, del-commute-dels,
• key/inj-03 is used by new-inode-exists, del-del-again,
• key/inodekey-id is used by in-del-ro, datakeys-set-del, datakeys-set-add, at-del-ro-data,
• key/sel-03 is used by dels-ignore-data, del-merge-dels, del-del-again, del-commute-dels, data-at-del-datakeys, at-dels-ro-data, at-del-ro-data,
• key/sel-04 is used by in-del-ro, datakeys-set-del, datakeys-set-add, data-at-del-datakeys,
• key/test-02 is used by new-inode-exists, in-del-ro, datakeys-set-del, datakeys-set-add, data-at-del-datakeys,
• key/test-07 is used by dentry-at-del-datakeys, datakeys-put-dentry, datakeys-del-dentry,
• key/test-08 is used by inode-at-del-datakeys, in-dels-inode, datakeys-put-inode-01, datakeys-put-inode,
• key/test-09 is used by notin-dels, notin-del, dels-ignore-data, del-this, del-put-again, del-merge-dels, del-del-again, del-commute-dels, data-at-del-datakeys, at-dels-ro-data, at-del-ro-data,

Used from specification store

• store/node-index/At-other is used by del-put-again,
• store/node-index/In-insert is used by del-put-again,
• store/node-index/k-Extension is used by dels-ignore-data, del-this, del-put-again, del-merge-dels, del-del-again, del-commute-dels,
• store/node-store/rew is used by write-shift,
• store/node-index/rew is used by update-index-shift,
• store/node-store/At-other is used by read-write-other-fs, keys-drop-fs, at-write-other,
• store/node-index/At-other is used by read-write-other, keys-at-other, del-this,
• store/node-index/At-same is used by index-update-at-last-oc,
• store/node-store/At-same is used by at-write-at,
• store/node-index/Del-at is used by dels-ignore-data, at-del-ro-nodata, at-del-ro-data,
• store/node-index/Del-in is used by in-del-ro, dels-ignore-data, datakeys-del-dentry,
• store/node-index/In-empty is used by data-in-empty,
• store/node-index/In-insert is used by index-update-in, datakeys-put-inode-01, datakeys-put-inode, datakeys-put-dentry,
• store/node-index/in-neq is used by keys-at-other, index-update-in, del-this,
• store/node-index/insin is used by index-update-in, index-update-at-last-oc,

Used from specification nat

• nat/add-num-01 is used by index-update-at-last-oc,
• nat/le-ls-simp is used by new-inode-exists,
• nat/lels is used by new-inode-exists,
• nat/lep is used by new-butlastn, keys-firstn,
• nat/lez is used by datakeys-0,

Used from specification set-union

• set-union/node-index/Difference is used by datakeys-set-del,
• set-union/node-index/subdef is used by toSet-subseteq-domri-notin,
• set-union/node-index/unrax is used by datakeys-set-add,
• set-union/node-index/Delete is used by datakeys-set-del,
• set-union/node-store/Intersect is used by range-inter-empty-in,
• set-union/node-store/int-a is used by range-inter-empty-in,
• set-union/node-store/int-c is used by range-inter-empty-in,
• set-union/node-store/una is used by write-dom,
• set-union/node-index/una is used by index-update-dom, in-read-in-dom,
• set-union/node-store/unadd is used by write-dom,
• set-union/node-index/unadd is used by index-update-dom, in-read-in-dom,
• set-union/node-store/unc is used by write-dom,
• set-union/node-index/unc is used by index-update-dom, in-read-in-dom,
• set-union/node-store/une is used by write-dom,
• set-union/node-index/une is used by index-update-dom, in-read-in-dom,

Used from specification set-basic

• set-basic/node-store/Extension is used by range-inter-empty-in, range-empty,
• set-basic/node-index/Extension is used by new-inode-exists, datakeys-set-empty, datakeys-set-del, datakeys-set-add, datakeys-put-inode-01, datakeys-put-inode, datakeys-put-dentry, datakeys-del-dentry, datakeys-0,
• set-basic/node-index/indef is used by new-inode-exists,
• set-basic/node-store/In-empty is used by range-inter-empty-in, range-empty,
• set-basic/node-index/In-empty is used by new-inode-exists, datakeys-set-empty,
• set-basic/node-index/In-insert is used by new-inode-exists, datakeys-set-add,
• set-basic/node-index/Size-insert is used by new-inode-exists,
• set-basic/node-store/ne-01 is used by range-inter-empty-in,
• set-basic/node-index/ne-01 is used by new-inode-exists, dels-ignore-data, del-put-again, del-merge-dels, del-del-again, datakeys-set-del,
• set-basic/node-index/size-zero is used by new-inode-exists, datakeys-set-empty,
• set-basic/node-store/size-zero is used by range-empty,
• set-basic/node-store/size-zero-01 is used by range-inter-empty-in, range-empty,
• set-basic/node-index/size-zero-01 is used by new-inode-exists, dels-ignore-data, del-put-again, del-merge-dels, del-del-again, datakeys-set-empty,
• set-basic/node-index/sub-add-03 is used by in-read-in-dom,
• set-basic/node-index/sub-e is used by in-read-in-dom,

Used from specification list-data

• list-data/key-list-set/l is used by update-index-shift, update-index-data-notin, update-index-append, keys-at-other, index-update-in, index-update-dom,
• list-data/address-list-set/l is used by write-shift, write-dom, write-app, update-index-shift, update-index-data-notin, update-index-append, update-index-app, keys-at-other, index-update-in, index-update-dom, in-write, at-write-other, at-write-at,
• list-data/node-list/l is used by write-shift, write-dom, write-app, in-write, at-write-other, at-write-at,
• list-data/address-list-set/size-01 is used by write-shift, write-dom, write-app, update-index-shift, update-index-data-notin, update-index-append, read-length, keys-length, keys-firstn, keys-at-other, index-update-in, index-update-dom, index-update-at-last-oc, index-lookup-length, in-write, at-write-other, at-write-at,
• list-data/key-list-set/size-01 is used by update-index-shift, update-index-data-notin, update-index-append, update-index-app, keys-length, keys-at-other, index-update-in, index-update-dom, index-update-at-last-oc, index-lookup-length,
• list-data/node-list/size-01 is used by write-shift, write-dom, write-app, read-length, in-write, at-write-other, at-write-at,

Used from specification list

• list/key-list-set/One is used by update-index-one, index-lookup-one,
• list/node-list/One is used by write-one,
• list/address-list-set/One is used by write-one, update-index-one, read-one, keys-one,
• list/node-list/c is used by write-one,
• list/key-list-set/c is used by update-index-one, index-lookup-one,
• list/address-list-set/c is used by write-one, update-index-one, read-one, keys-one,
• list/node-list/Nil is used by write-app, read-split, read-app,
• list/key-list-set/Nil is used by update-index-append, update-index-app, keys-firstn, keys-append, index-update-at-last-oc, index-lookup-app,
• list/address-list-set/Nil is used by write-app, update-index-append, update-index-app, read-split, read-app, new-append, keys-in-elim-last-oc, keys-append, index-lookup-app,
• list/address-list-set/a is used by write-shift, write-new-app, write-dom, write-app, update-index-shift, update-index-data-notin, update-index-append, update-index-app, read-write-other-fs, read-write-other, read-split, read-length, read-eq-one, read-eq-empty, read-app, nodups-new, new-write, new-one, new-not-new, new-ext, new-butlastn, new-append, keys-length, keys-in-elim-last-oc, keys-in-elim, keys-firstn, keys-drop-fs, keys-at-other, keys-append, index-update-in, index-update-dom, index-update-at-last-oc, index-lookup-one, index-lookup-length, index-lookup-app, in-write, in-read-in-dom, at-write-other, at-write-at,
• list/node-list/a is used by write-shift, write-dom, write-app, read-write-other-fs, read-split, read-one, read-length, read-eq-one, read-eq-empty, read-app, in-write, at-write-other, at-write-at,
• list/key-list-set/a is used by update-index-shift, update-index-data-notin, update-index-append, update-index-app, read-write-other, keys-one, keys-length, keys-in-elim-last-oc, keys-in-elim, keys-firstn, keys-drop-fs, keys-at-other, keys-append, index-update-in, index-update-dom, index-update-at-last-oc, index-lookup-length, index-lookup-app, in-read-in-dom,
• list/node-list/app is used by read-one,
• list/address-list-set/app is used by new-one, index-lookup-one,
• list/key-list-set/app is used by keys-one,
• list/node-list/app-01 is used by read-split,
• list/node-list/app-02 is used by read-split, read-eq-empty,
• list/address-list-set/app-08 is used by read-write-other, keys-in-elim-last-oc, index-lookup-app,
• list/node-list/app-08 is used by read-write-other-fs, read-split, read-app,
• list/key-list-set/app-08 is used by keys-firstn, keys-drop-fs, keys-append,
• list/address-list-set/c is used by write-shift, write-new-app, write-dom, write-app, update-index-shift, update-index-data-notin, update-index-append, read-write-other-fs, read-write-other, read-split, read-length, read-eq-one, read-eq-empty, read-app, new-write, new-not-new, new-ext, new-append, keys-length, keys-in-elim-last-oc, keys-in-elim, keys-firstn, keys-drop-fs, keys-at-other, keys-append, index-update-in, index-update-dom, index-update-at-last-oc, index-lookup-one, index-lookup-length, index-lookup-app, in-write, in-read-in-dom, at-write-other, at-write-at,
• list/node-list/c is used by write-shift, write-dom, write-app, read-write-other-fs, read-split, read-one, read-length, read-eq-one, read-eq-empty, read-app, in-write, at-write-other, at-write-at,
• list/key-list-set/c is used by update-index-shift, update-index-data-notin, update-index-append, update-index-app, read-write-other, keys-one, keys-length, keys-in-elim-last-oc, keys-in-elim, keys-firstn, keys-drop-fs, keys-at-other, keys-append, index-update-in, index-update-dom, index-update-at-last-oc, index-lookup-length, index-lookup-app, in-read-in-dom,
• list/address-list-set/c-03 is used by read-eq-one,
• list/node-list/c-03 is used by read-eq-one,
• list/address-list-set/c-04 is used by index-lookup-one,
• list/node-list/c-04 is used by read-one, read-eq-one,
• list/key-list-set/c-04 is used by keys-one,
• list/node-list/c-06 is used by read-split,
• list/node-list/e is used by read-eq-one, read-eq-empty,
• list/address-list-set/in-06 is used by write-shift, update-index-data-notin, read-write-other-fs, keys-drop-fs, at-write-other,
• list/key-list-set/in-06 is used by update-index-shift, read-write-other, keys-at-other,
• list/key-list-set/in-10 is used by keys-in-elim-last-oc,
• list/node-list/in-14 is used by read-split,
• list/key-list-set/in-append is used by keys-in-elim-last-oc,
• list/node-list/in-append is used by read-split,
• list/node-list/in-append0-not-left is used by read-split,
• list/address-list-set/in-empty is used by write-shift, update-index-data-notin, new-write, new-not-new, keys-in-elim, in-write, in-read-in-dom, at-write-other, at-write-at,
• list/key-list-set/in-empty is used by update-index-shift, keys-in-elim-last-oc, keys-in-elim, keys-at-other, index-update-in,
• list/node-list/in-empty is used by read-split,
• list/node-list/in-rec is used by read-split,
• list/address-list-set/in-rec is used by new-write, new-not-new, new-ext, keys-in-elim, in-write, in-read-in-dom, at-write-at,
• list/key-list-set/in-rec is used by keys-in-elim-last-oc, keys-in-elim, index-update-in,
• list/address-list-set/len is used by new-butlastn, keys-firstn,
• list/address-list-set/len-02 is used by update-index-app,
• list/key-list-set/len-02 is used by update-index-app,
• list/address-list-set/len-05 is used by write-shift, write-dom, write-app, update-index-shift, update-index-data-notin, update-index-append, read-length, keys-length, keys-firstn, keys-at-other, index-update-in, index-update-dom, index-update-at-last-oc, index-lookup-length, in-write, at-write-other, at-write-at,
• list/key-list-set/len-05 is used by update-index-shift, update-index-data-notin, update-index-append, update-index-app, keys-length, keys-at-other, index-update-in, index-update-dom, index-update-at-last-oc, index-lookup-length,
• list/node-list/len-05 is used by write-shift, write-dom, write-app, read-length, in-write, at-write-other, at-write-at,

Used from specification node-store

• node-store/in-insert is used by new-write, in-write,

Used from specification list-dup

• list-dup/address-list-set/dups-appex is used by write-new-app-nodups,
• list-dup/address-list-set/dups-cons is used by at-write-at,

Used from specification list-del

• list-del/address-list-set/elim-firstn-restn is used by keys-firstn,
• list-del/address-list-set/elim-lastn-butlastn is used by new-butlastn,
• list-del/key-list-set/firstN-zero is used by keys-firstn,
• list-del/node-list/get-succ is used by at-write-at,
• list-del/address-list-set/get-succ is used by index-update-at-last-oc,
• list-del/node-list/get-zero-01 is used by at-write-at,
• list-del/address-list-set/get-zero-01 is used by index-update-at-last-oc,
• list-del/address-list-set/pos-e is used by at-write-at,
• list-del/address-list-set/pos-n is used by at-write-at,
• list-del/address-list-set/pos-y is used by at-write-at,
• list-del/key-list-set/weak-firstN-rec is used by keys-firstn,