[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 ubifs-adr-in-ri, ri-cons-range-ri, ri-closed-drop, index-update-dom, in-ri-update-in-ri,
store+set/node-store/Diff-get is used by ri-cons-drop, ri-closed-drop,
store+set/node-index/Diff-ext is used by ri-inj-rem,
store+set/node-store/Diff-ext is used by ri-cons-drop, ri-closed-drop, log-cons-drop,
store+set/node-index/Diff-get is used by ri-inj-rem,
store+set/node-store/Diff-get is used by log-cons-drop,
store+set/node-store/Diff-mems-get is used by ri-cons-drop, ri-closed-drop, log-cons-drop,
store+set/node-index/Dom is used by ubifs-ro-subset, ubifs-fo-subset, ri-cons-copy-new, read-lookup-copy, log-cons-copy-new, index-update-dom,
store+set/node-store/Dom is used by ri-cons-range-ri,
store+set/node-index/In-data-in is used by ubifs-dir-data, ri-inj-write, ri-cons-drop,

Used from specification nat-basic

nat-basic/a is used by ri-cons-copy-new, read-lookup-copy, read-get, log-cons-copy-new, in-ri-update-in-ri,
nat-basic/c is used by ri-cons-copy-new, read-lookup-copy, read-get, log-cons-copy-new, in-ri-update-in-ri,
nat-basic/eq-01 is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new, in-ri-update-in-ri,
nat-basic/f is used by ri-cons-copy-new, read-lookup-copy, read-get, log-cons-copy-new,
nat-basic/l-02 is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new,
nat-basic/lf-01 is used by ri-cons-copy-new,
nat-basic/lf-02 is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new,
nat-basic/ls-02 is used by ri-cons-copy-new,
nat-basic/one-01 is used by read-get,
nat-basic/oz is used by read-get,
nat-basic/s-04 is used by read-get,
nat-basic/succ is used by ri-cons-copy-new, read-lookup-copy, read-get, log-cons-copy-new, in-ri-update-in-ri,
nat-basic/z-01 is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new, in-ri-update-in-ri,

Used from specification node

node/elim-02 is used by ubifs-parent-in, ubifs-parent-dir, ri-closed-gc-one, key-node-cons,
node/elim-03 is used by ubifs-parent-dir, key-node-cons,
node/elim-05 is used by ubifs-file-notdir, ubifs-file-in, ri-closed-gc-one, key-node-cons,
node/sel-01 is used by dentrynode-closed,
node/sel-03 is used by datanode-closed,
node/sel-04 is used by ri-cons-truncnode,
node/sel-09 is used by datanode-closed,
node/sel-11 is used by ubifs-parent-dir,
node/sel-14 is used by dentrynode-closed,
node/test-01 is used by key-node-cons, dentrynode-cons,
node/test-02 is used by ubifs-parent-in, ubifs-parent-dir, ri-closed-gc-one, key-node-cons, dentrynode-cons, dentrynode-closed,
node/test-03 is used by ri-closed-gc-one, key-node-cons, dentrynode-cons, dentrynode-closed,
node/test-06 is used by ubifs-parent-dir, key-node-cons, inodenode-cons,
node/test-08 is used by key-node-cons, inodenode-cons, inodenode-closed,
node/test-09 is used by key-node-cons, inodenode-cons, inodenode-closed,
node/test-11 is used by inodenode-cons,
node/test-12 is used by key-node-cons, datanode-cons,
node/test-13 is used by ri-closed-gc-one, key-node-cons, datanode-cons, datanode-closed,
node/test-14 is used by key-node-cons, dentrynode-cons,
node/test-15 is used by truncnode-cons, ri-cons-truncnode,
node/test-16 is used by truncnode-cons, ri-cons-truncnode,
node/test-17 is used by truncnode-cons, ri-cons-truncnode,
node/test-18 is used by truncnode-cons,
node/test-19 is used by key-node-cons, datanode-cons,
node/test-22 is used by ubifs-file-notdir, ubifs-file-in, ri-closed-gc-one, key-node-cons, datanode-cons, datanode-closed,

Used from specification list+set

list+set/key-list-set/toSet-app is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new,
list+set/address-list-set/toSet-app is used by in-ri-update-in-ri,
list+set/address-list-set/toSet-empty is used by in-ri-update-in-ri,
list+set/key-list-set/toSet-ext is used by index-update-dom,
list+set/address-list-set/toSet-ext is used by log-cons-drop, index-update-dom,
list+set/key-list-set/toSet-one is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new,
list+set/address-list-set/toSet-one is used by in-ri-update-in-ri,

Used from specification key

key/elim-01 is used by datalkeys-drop-orphans,
key/elim-02 is used by ubifs-dir-data, ri-cons-del-orphans, datalkeys-drop-orphans,
key/inj-03 is used by ri-closed-gc-one,
key/inodekey-id is used by datalkeys-drop-orphans-in,
key/sel-02 is used by ubifs-parent-in, ubifs-parent-dir,
key/sel-03 is used by ubifs-file-notdir, ubifs-file-in, datalkeys-drop-orphans,
key/sel-04 is used by ubifs-dir-data, key-node-cons, inodekey-cons,
key/test-01 is used by ri-cons-truncnode, key-node-cons, dentrykey-cons,
key/test-02 is used by ubifs-dir-data, ri-cons-truncnode, key-node-cons, inodekey-cons, datalkeys-drop-orphans,
key/test-03 is used by ri-cons-truncnode, key-node-cons, datakey-cons,
key/test-04 is used by ri-cons-truncnode, key-node-cons, inodes-nodata, datakey-cons,
key/test-05 is used by key-node-cons, inodekey-cons,
key/test-06 is used by ri-cons-truncnode, key-node-cons, inodes-nodentry, dentrykey-cons,
key/test-07 is used by key-node-cons, dentrykey-cons,
key/test-08 is used by key-node-cons, inodekey-cons,
key/test-09 is used by ubifs-dir-data, ri-cons-truncnode, ri-cons-del-orphans, key-node-cons, datalkeys-drop-orphans, datakey-cons,

Used from specification aubifs-base

aubifs-base/at-dels-ro-nodata is used by ri-cons-del-orphans,
aubifs-base/at-write-other is used by ri-cons-copy-new, ri-cons-copy, log-cons-copy-old, log-cons-copy-new,
aubifs-base/in-dels-ro is used by datalkeys-drop-orphans,
aubifs-base/index-update-in is used by ri-cons-copy-new, in-ri-update-in-ri,
aubifs-base/keys-at-other is used by read-lookup-copy,
aubifs-base/keys-in-elim is used by index-update-dom,
aubifs-base/notin-del is used by ubifs-cons-notin-del,
aubifs-base/notin-dels is used by ubifs-cons-notin-dels,
aubifs-base/update-index-shift is used by read-lookup-copy,
aubifs-base/write-shift is used by read-lookup-copy,
aubifs-base/at-dels-ro-data is used by ri-cons-del-orphans,
aubifs-base/datakeys is used by ubifs-dir-data, datalkeys-drop-orphans-in, datalkeys-drop-orphans,
aubifs-base/datakeys-ge is used by datalkeys-drop-orphans-in, datalkeys-drop-orphans,
aubifs-base/in-dels-ro is used by ri-cons-del-orphans, datalkeys-drop-orphans-in,
aubifs-base/in-write is used by ri-cons-copy-new, ri-cons-copy, log-cons-copy-old, log-cons-copy-new,
aubifs-base/index-lookup-app is used by ri-cons-copy-new, log-cons-copy-new,
aubifs-base/index-lookup-base is used by read-lookup-copy,
aubifs-base/index-lookup-length is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new,
aubifs-base/index-lookup-rec is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new,
aubifs-base/index-update-at-last-oc is used by ri-cons-copy-new, read-lookup-copy,
aubifs-base/index-update-dom is used by index-update-dom,
aubifs-base/index-update-key-base is used by read-lookup-copy, in-ri-update-in-ri,
aubifs-base/index-update-key-rec is used by read-lookup-copy, in-ri-update-in-ri,
aubifs-base/keys-at-other is used by ri-cons-copy-new,
aubifs-base/keys-base is used by in-ri-update-in-ri,
aubifs-base/keys-length is used by index-update-dom, in-ri-update-in-ri,
aubifs-base/keys-rec is used by in-ri-update-in-ri,
aubifs-base/new-append is used by ri-cons-copy-new, read-lookup-copy,
aubifs-base/new-base is used by read-lookup-copy,
aubifs-base/new-in-fs is used by ri-cons-copy, nodups-new-nodups,
aubifs-base/new-not-new is used by ri-cons-copy-new, log-cons-copy-old,
aubifs-base/new-rec is used by ri-cons-copy-new, read-lookup-copy,
aubifs-base/range is used by ri-cons-range-ri, ri-cons-drop, ri-closed-drop, index-update-dom, in-ri-update-in-ri,
aubifs-base/range-inter-empty-in is used by ri-cons-drop, ri-closed-drop,
aubifs-base/read-app is used by ri-cons-copy-new, log-cons-copy-new,
aubifs-base/read-base is used by read-lookup-copy,
aubifs-base/read-length is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new,
aubifs-base/read-rec is used by ri-cons-copy-new, read-lookup-copy, read-get, log-cons-copy-new,
aubifs-base/toSet-subseteq-domri-notin is used by ri-cons-copy-new,
aubifs-base/write-app is used by ri-cons-copy-new, log-cons-copy-new,
aubifs-base/write-base is used by read-lookup-copy,
aubifs-base/write-rec is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new,

Used from specification set-union

set-union/node-store/subdef is used by ri-cons-range-ri, index-update-dom,
set-union/node-index/subdef is used by index-update-dom,
set-union/node-index/Delete is used by inodes-del,
set-union/node-store/Intersect is used by ri-cons-drop, ri-closed-drop, log-cons-drop,
set-union/node-store/int-a is used by ri-cons-drop, ri-closed-drop, log-cons-drop,
set-union/node-store/int-c is used by ri-cons-drop, ri-closed-drop, log-cons-drop,
set-union/node-store/una is used by in-ri-update-in-ri,
set-union/node-index/una is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new, index-update-dom,
set-union/node-index/unadd is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new,
set-union/node-store/unadd is used by in-ri-update-in-ri,
set-union/node-store/unc is used by in-ri-update-in-ri,
set-union/node-index/unc is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new, index-update-dom,
set-union/node-index/une is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new,
set-union/node-store/une is used by in-ri-update-in-ri,
set-union/node-index/uneq is used by index-update-dom,
set-union/node-index/unsub-union-01 is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new,

Used from specification nat

nat/elim-pred-c is used by read-get,
nat/le-def is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new,
nat/lels is used by ri-cons-copy-new, read-lookup-copy, read-get,
nat/ler is used by ri-cons-copy-new,
nat/succ-01 is used by read-get,
nat/zero is used by ri-cons-copy-new, read-lookup-copy,

Used from specification store

store/node-store/At-other is used by read-lookup-copy,
store/node-index/At-other is used by read-lookup-copy,
store/node-index/In-insert is used by in-ri-update-in-ri,
store/node-store/At-in-out is used by ri-cons-gc-one, ri-closed-gc-one,
store/node-index/At-other is used by ri-inj-write, ri-cons-gc-one, ri-closed-gc-one,
store/node-store/At-other is used by ri-closed-gc-one,
store/node-store/At-same is used by ri-cons-gc-one, ri-cons-copy-new, ri-closed-gc-one, read-lookup-copy, log-cons-copy-new,
store/node-index/At-same is used by ri-inj-write, ri-cons-gc-one, ri-closed-gc-one, read-lookup-copy,
store/node-index/Del-at is used by ri-inj-del,
store/node-index/Del-in is used by ri-inj-del,
store/node-index/In-empty is used by ri-inj-empty, ri-cons-empty-2,
store/node-index/In-insert is used by ri-closed-gc-one,
store/node-index/in-neq is used by ri-inj-write, ri-cons-gc-one, ri-closed-gc-one,
store/node-index/insin is used by ri-inj-write, ri-cons-gc-one, ri-closed-gc-one,
store/node-store/k-At-same is used by ri-closed-gc-one,
store/node-index/k-At-same is used by ri-closed-gc-one,
store/node-store/notmemlookup is used by ri-closed-gc-one, read-lookup-copy,
store/node-index/notmemlookup is used by ubifs-file-in, ubifs-dir-data, ri-closed-drop,

Used from specification set-basic

set-basic/node-store/Extension is used by ri-cons-drop, ri-closed-drop, log-cons-drop,
set-basic/node-index/Extension is used by ubifs-dir-data, datalkeys-drop-orphans-in, datalkeys-drop-orphans,
set-basic/node-store/In-empty is used by ri-cons-drop, ri-closed-drop, log-cons-drop,
set-basic/node-index/In-empty is used by ubifs-dir-data, empty-inodes, datalkeys-drop-orphans-in,
set-basic/node-index/In-insert is used by inodes-put,
set-basic/node-index/ne-01 is used by ubifs-ro-subset, ubifs-ro-dentry, ubifs-ro-data, ubifs-fo-subset, inodes-nodentry, inodes-nodata, inodes-in, datalkeys-drop-orphans-in,
set-basic/node-store/ne-01 is used by ri-cons-drop, ri-closed-drop, log-cons-drop,
set-basic/node-index/size-zero is used by ubifs-dir-data, datalkeys-drop-orphans-in,
set-basic/node-store/size-zero-01 is used by ri-cons-drop, ri-closed-drop, log-cons-drop,
set-basic/node-index/size-zero-01 is used by ubifs-ro-dentry, ubifs-ro-data, ubifs-dir-data, inodes-nodentry, inodes-nodata, inodes-in, datalkeys-drop-orphans-in,
set-basic/node-index/sub-add-03 is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new,
set-basic/node-store/sub-add-03 is used by in-ri-update-in-ri,
set-basic/node-store/sub-e is used by in-ri-update-in-ri,
set-basic/node-index/sub-in is used by ubifs-ro-subset, ubifs-fo-subset,

Used from specification list-data

list-data/key-list-set/l is used by ri-cons-copy-new, read-lookup-copy,
list-data/address-list-set/l is used by read-lookup-copy, read-get, log-cons-copy-new, in-ri-update-in-ri,
list-data/address-list-set/size-01 is used by ri-cons-copy-new, read-lookup-copy, in-ri-update-in-ri,
list-data/key-list-set/size-01 is used by read-lookup-copy, log-cons-copy-new,

Used from specification list

list/address-list-set/in-def is used by log-cons-copy-new,
list/key-list-set/in-def is used by ri-cons-copy-new, read-lookup-copy,
list/address-list-set/split-first is used by ri-cons-copy-new, read-lookup-copy,
list/key-list-set/split-first is used by log-cons-copy-new,
list/address-list-set/Nil is used by nodups-new-nodups,
list/key-list-set/a is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new, in-ri-update-in-ri,
list/node-list/a is used by ri-cons-copy-new, read-lookup-copy, read-get, log-cons-copy-new,
list/address-list-set/a is used by ubifs-log-nodups-add5, ubifs-log-nodups-add4, ubifs-log-nodups-add3, ubifs-log-nodups-add2, ubifs-log-nodups-add1, ri-cons-copy-new, read-lookup-copy, read-get, nodups-new-nodups, log-cons-copy-new, log-cons-app, in-ri-update-in-ri,
list/key-list-set/c is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new, in-ri-update-in-ri,
list/address-list-set/c is used by ri-cons-copy-new, read-lookup-copy, read-get, nodups-new-nodups, log-cons-copy-new, in-ri-update-in-ri,
list/node-list/c is used by ri-cons-copy-new, read-lookup-copy, read-get, log-cons-copy-new,
list/address-list-set/e-01 is used by read-get,
list/address-list-set/in-01 is used by ubifs-log-nodups-add5, ubifs-log-nodups-add4,
list/address-list-set/in-06 is used by read-lookup-copy,
list/address-list-set/in-17 is used by ubifs-log-nodups-add5, ubifs-log-nodups-add4, log-cons-one,
list/address-list-set/in-append is used by ubifs-log-nodups-add5, ubifs-log-nodups-add4, ri-cons-copy-new, read-lookup-copy, nodups-new-nodups, log-cons-app,
list/key-list-set/in-append is used by read-lookup-copy,
list/address-list-set/in-empty is used by nodups-new-nodups, log-cons-emp,
list/key-list-set/in-rec is used by read-lookup-copy,
list/address-list-set/in-rec is used by ri-cons-copy-new, nodups-new-nodups,
list/address-list-set/len is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new,
list/key-list-set/len is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new,
list/node-list/len-02 is used by read-get,
list/address-list-set/len-05 is used by ri-cons-copy-new, read-lookup-copy, read-get, log-cons-copy-new, in-ri-update-in-ri,
list/node-list/len-05 is used by ri-cons-copy-new,
list/key-list-set/len-05 is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new,

Used from specification node-store

node-store/in-insert is used by ri-cons-gc-one, ri-closed-gc-one,

Used from specification list-dup

list-dup/address-list-set/l-03 is used by ubifs-log-nodups-add5, ubifs-log-nodups-add4,
list-dup/address-list-set/a is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new,
list-dup/key-list-set/a is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new,
list-dup/key-list-set/c-02 is used by log-cons-copy-new,
list-dup/key-list-set/dups-cons is used by read-lookup-copy,
list-dup/address-list-set/dups-cons is used by ri-cons-copy-new, read-lookup-copy, nodups-new-nodups,
list-dup/address-list-set/e-01 is used by read-lookup-copy, nodups-new-nodups,
list-dup/address-list-set/f is used by ubifs-log-nodups-add5, ubifs-log-nodups-add4, ubifs-log-nodups-add3, ubifs-log-nodups-add2, ubifs-log-nodups-add1,
list-dup/address-list-set/f-01 is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new,
list-dup/key-list-set/f-01 is used by ri-cons-copy-new, read-lookup-copy, log-cons-copy-new,
list-dup/address-list-set/l-01 is used by ubifs-log-nodups-add3, ubifs-log-nodups-add2,
list-dup/address-list-set/n is used by ubifs-log-nodups-add4, ubifs-log-nodups-add3,
list-dup/address-list-set/rec is used by nodups-new-nodups,

Used from specification list-del

list-del/address-list-set/get-append-grt is used by ri-cons-copy-new, read-lookup-copy,
list-del/node-list/get-append-grt is used by read-get,
list-del/node-list/get-append-less is used by read-get,
list-del/address-list-set/get-append-less is used by ri-cons-copy-new, read-lookup-copy,
list-del/address-list-set/get-in is used by ri-cons-copy-new, read-lookup-copy,
list-del/address-list-set/get-succ is used by read-get,
list-del/address-list-set/get-zero-01 is used by ri-cons-copy-new, read-lookup-copy, read-get,
list-del/node-list/one-03 is used by read-get,