[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/group-store-ablock-store-nat-store/Diff-get is used by store-diff-union-elems-notin,
store+set/group-store-ablock-store-nat-store/Diff-ext is used by fwd-inv-loghead, fwd-inv-gblock-rem-del, crash-gstore-inv,
store+set/group-store-ablock-store-nat-store/Diff-get is used by fwd-inv-loghead, fwd-inv-gblock-rem-del, crash-gstore-inv,
store+set/group-store-ablock-store-nat-store/Diff-mems-get is used by store-diff-union-elems-notin,
store+set/group-store-ablock-store-nat-store/Dom is used by notin-gstore-ginval-notin-gstore0, fwd-inv-loghead, fwd-in-log-in-gstore, fwd-in-gstore0, fwd-in-gstore-loghead, elems-log-subset-gstore-union-ginval, dom-gstore-crash,
store+set/index-store-ablock-store-nat-store/Dom is used by dom-istore-crash-refm-refsize0, dom-istore-crash, dom-disj-in-r,
store+set/group-store-ablock-store-nat-store/in-dom-inter is used by dom-gstore-intersect-in-gstore, dom-disj-in-r,

Used from specification ablock

ablock/group-store/elim is used by in-crash-in-gstore, in-crash-at-gstore, crash-gstore-inv,
ablock/index-store/elim is used by inv-crash, icrash-remove-refsize0-prefix, icrash-refsize-cons, icrash-inv, dom-istore-crash-refm-refsize0,
ablock/group-store/inj is used by in-crash-in-gstore, in-crash-at-gstore, crash-gstore-inv,
ablock/index-store/inj is used by icrash-remove-refsize0-prefix, icrash-refsize-cons, icrash-inv, dom-istore-crash-refm-refsize0,
ablock/index-store/sel-01 is used by icrash-remove-refsize0-prefix,
ablock/group-store/sel-01 is used by in-crash-at-gstore, crash-update-reverted,
ablock/index-store/sel-02 is used by icrash-remove-refsize0-prefix,
ablock/group-store/sel-02 is used by in-crash-in-gstore, in-crash-at-gstore, crash-update-reverted,
ablock/index-store/sel-03 is used by icrash-remove-refsize0-prefix, icrash-refsize-cons, icrash-inv,

Used from specification set-union

set-union/nat-set/Difference is used by elems-subseteq-add-diff-notin, elems-in-diff,
set-union/nat-set/subdef is used by elems-log-subset-gstore-union-ginval, elems-in-fwd,
set-union/nat-set/unrax is used by fwd-in-gstore0,
set-union/nat-set/Delete is used by fwd-inv-gblock-rem-del, elems-minus,
set-union/nat-set/Intersect is used by elems-in-notin-ginval,
set-union/nat-set/int-a is used by fwd-inv-loghead, fwd-in-log-in-gstore, fwd-in-gstore-loghead, elems-in-notin-ginval, dom-gstore-intersect-in-gstore, dom-disj-in-r, dom-disj-in-l,
set-union/nat-set/int-c is used by fwd-inv-loghead, fwd-in-log-in-gstore, fwd-in-gstore-loghead, elems-in-notin-ginval, dom-gstore-intersect-in-gstore, dom-disj-in-r, dom-disj-in-l,
set-union/nat-set/int-ins is used by fwd-inv-loghead, fwd-in-gstore-loghead,
set-union/nat-set/una is used by store-diff-union-elems-notin, notin-gstore-ginval-notin-gstore0, fwd-inv-loghead, fwd-in-log-in-gstore, fwd-in-gstore0, fwd-in-gstore-loghead, elems-log-subset-gstore-union-ginval, dom-gstore-crash,
set-union/nat-set/unadd is used by fwd-inv-loghead, fwd-in-gstore-loghead,
set-union/nat-set/unc is used by store-diff-union-elems-notin, notin-gstore-ginval-notin-gstore0, fwd-inv-loghead, fwd-in-log-in-gstore, fwd-in-gstore0, fwd-in-gstore-loghead, elems-log-subset-gstore-union-ginval, dom-gstore-crash,
set-union/nat-set/unin is used by store-diff-union-elems-notin, notin-gstore-ginval-notin-gstore0, fwd-inv-loghead, fwd-in-log-in-gstore, fwd-in-gstore-loghead, elems-log-subset-gstore-union-ginval, dom-gstore-crash,
set-union/nat-set/unin-01 is used by notin-gstore-ginval-notin-gstore0, fwd-in-log-in-gstore, fwd-in-gstore0, elems-log-subset-gstore-union-ginval, dom-gstore-crash,

Used from specification store

store/index-store-ablock-store-nat-store/Extension is used by icrash-remove-refsize0-prefix,
store/group-store-ablock-store-nat-store/In-insert is used by crash-update-reverted,
store/group-store-ablock-store-nat-store/k-Extension is used by crash-update-reverted,
store/group-store-ablock-store-nat-store/At-other is used by crash-update-reverted,
store/group-store-ablock-store-nat-store/At-same is used by crash-update-reverted,
store/group-store-ablock-store-nat-store/notmemlookup is used by in-crash-in-gstore, in-crash-at-gstore, fwd-inv-loghead, crash-update-reverted, crash-gstore-inv,

Used from specification ablock-store-inv

ablock-store-inv/group-store/at is used by in-crash-at-gstore,
ablock-store-inv/index-store/at-remove-refsize0 is used by icrash-remove-refsize0-prefix, icrash-inv,
ablock-store-inv/index-store/blockstore-prefix is used by icrash-remove-refsize0-prefix,
ablock-store-inv/group-store/in is used by in-crash-in-gstore,
ablock-store-inv/index-store/in-remove-refsize0 is used by dom-istore-crash-refm-refsize0,
ablock-store-inv/group-store/inv-block is used by crash-gstore-inv,
ablock-store-inv/group-store/inv-store is used by fwd-inv-loghead, fwd-inv-gblock-rem-del, crash-gstore-inv,
ablock-store-inv/index-store/inv-store is used by inv-crash, icrash-inv,
ablock-store-inv/index-store/in-remove-refsize0 is used by icrash-remove-refsize0-prefix, icrash-inv,
ablock-store-inv/group-store/in-store-inv is used by fwd-inv-gblock,
ablock-store-inv/index-store/in-store-inv is used by fwd-inv-iblock,
ablock-store-inv/group-store/inv-diff-n is used by fwd-inv-gblock-rem,
ablock-store-inv/group-store/inv-flashsize-size is used by crash-gstore-inv,
ablock-store-inv/index-store/inv-set-sizes is used by inv-crash, icrash-inv,
ablock-store-inv/group-store/notin-notin is used by in-crash-at-gstore,
ablock-store-inv/index-store/prefix-fwd-in is used by inv-crash, icrash-remove-refsize0-prefix, icrash-inv,
ablock-store-inv/index-store/remove-refsize0-eq-nonzero is used by dom-istore-crash-refm-refsize0,

Used from specification list-last

list-last/nat-list-set/last-def is used by fwd-inv-loghead, fwd-in-gstore-loghead,

Used from specification set-basic

set-basic/nat-set/Extension is used by notin-gstore-ginval-notin-gstore0, fwd-inv-loghead, fwd-in-log-in-gstore, fwd-in-gstore0, fwd-in-gstore-loghead, elems-subseteq-add-diff-notin, elems-prepend, elems-minus, elems-log-subset-gstore-union-ginval, elems-in-notin-ginval, elems-empty, elems-append, dom-istore-crash-refm-refsize0, dom-istore-crash, dom-gstore-intersect-in-gstore, dom-gstore-crash, dom-disj-in-r,
set-basic/nat-set/In-empty is used by elems-in-notin-ginval, elems-empty, dom-gstore-intersect-in-gstore, dom-disj-in-r,
set-basic/nat-set/In-insert is used by fwd-inv-loghead, fwd-in-gstore-loghead, elems-subseteq-add-diff-notin, elems-prepend, elems-append,
set-basic/nat-set/in-02 is used by elems-subseteq-add-diff-notin,
set-basic/nat-set/ne-01 is used by fwd-in-gstore0, elems-in-notin-ginval, dom-gstore-intersect-in-gstore,
set-basic/nat-set/size-zero is used by elems-empty,
set-basic/nat-set/size-zero-01 is used by fwd-in-gstore0, elems-in-notin-ginval, elems-empty, dom-gstore-intersect-in-gstore,
set-basic/nat-set/sub-idem is used by icrash-remove-refsize0-prefix,

Used from specification list

list/nat-list-set/lastdiv-rew is used by fwd-inv-loghead, fwd-in-gstore-loghead,
list/nat-list-set/a is used by fwd-inv-loghead, fwd-in-gstore-loghead, elems-prepend, elems-append,
list/nat-list-set/in-17 is used by elems-append,
list/nat-list-set/in-append is used by elems-append,
list/nat-list-set/in-empty is used by elems-empty,
list/nat-list-set/in-rec is used by elems-prepend,

Used from specification address-data

address-data/sel-03 is used by in-crash-in-gstore, in-crash-at-gstore,
address-data/sel-04 is used by in-crash-in-gstore, in-crash-at-gstore,
address-data/sel-05 is used by in-crash-in-gstore, in-crash-at-gstore,

Used from specification list-del

list-del/nat-list-set/in-del-new is used by elems-minus,

Used from specification ablock-store-refsize-cons

ablock-store-refsize-cons/index-store/refsize-cons-def is used by icrash-refsize-cons,