Used simplifier rules/spec theorems by specification

Used from specification store+set

• store+set/ablock-store-nat-store/Diff-ext is used by in-diff,
• store+set/ablock-store-nat-store/Diff-get is used by prefix-rem-alloc,
• store+set/ablock-store-nat-store/rem-write is used by inv-alloc,
• store+set/ablock-store-nat-store/Diff-ext is used by prefix-rem-left, prefix-rem-alloc, prefix-rem, inv-remove-refsize0-diff, inv-reduce-rem, inv-reduce, inv-diff-n, inv-alloc, at-explicit-diff,
• store+set/ablock-store-nat-store/Diff-get is used by prefix-rem-left, prefix-rem-alloc, prefix-rem, inv-remove-refsize0-diff, inv-reduce-rem, inv-reduce, inv-diff-n, inv-alloc, in-diff, at-explicit-diff, at-diff,
• store+set/ablock-store-nat-store/Diff-mems-get is used by prefix-rem-alloc, inv-alloc,
• store+set/ablock-store-nat-store/Dom is used by prefix-trans, prefix-rem-alloc, prefix-rem, prefix-notin-fwd, prefix-just-alloc, prefix-in, prefix-fwd-in, prefix-del-right, prefix-at, prefix-append-notin, inv-remove-refsize0-diff, dom-remove-refsize0,
• store+set/ablock-store-nat-store/diff-get-add is used by prefix-rem-alloc, inv-reduce-rem,
• store+set/ablock-store-nat-store/dom-add-in is used by prefix-set-flags, prefix-append-in,
• store+set/ablock-store-nat-store/dom-del is used by prefix-rem-left, prefix-rem, prefix-del-right,
• store+set/ablock-store-nat-store/dom-emp is used by prefix-empty-right, prefix-empty-left,
• store+set/ablock-store-nat-store/dom-ins is used by prefix-set-flags, prefix-rem-alloc, prefix-just-alloc, prefix-append-notin, prefix-append-in, prefix-alloc,
• store+set/ablock-store-nat-store/dom-isemp is used by prefix-empty-right,
• store+set/ablock-store-nat-store/dom-rem is used by prefix-rem-left, prefix-rem-alloc, prefix-rem,
• store+set/ablock-store-nat-store/rem-write-other is used by inv-alloc,

Used from specification nat-basic

• nat-basic/a is used by to-adrs-sublist, to-adrs-drop, size-one, size-append, prefixn-to-adrs, prefix-at, prefix-append-in, list-split, inv-flashsize-prepend, inv-flashsize-append, inv-flashsize-app, inv-append, inv-add-node, at-explicit-diff, at-explicit, addresslist-length,
• nat-basic/add-base is used by to-adrs-sublist, to-adrs-drop, size-one, size-append, prefix-at, at-explicit-diff, at-explicit,
• nat-basic/c is used by to-adrs-sublist, to-adrs-drop, size-one, size-append, prefixn-to-adrs, prefix-at, prefix-append-in, list-split, inv-flashsize-prepend, inv-flashsize-append, inv-flashsize-app, inv-append, inv-add-node, at-explicit-diff, at-explicit, addresslist-length,
• nat-basic/eq-01 is used by size-append, prefix-at, prefix-append-in, inv-flashsize-prepend, inv-flashsize-append, inv-append, inv-add-node, at-explicit-diff, at-explicit, addresslist-length,
• nat-basic/eq-02 is used by prefix-at,
• nat-basic/f is used by inv-listlen-ls2, inv-listlen-ls1, inv-flashsize-prepend, inv-flashsize-prefix, inv-flashsize-append, inv-flashsize-app, at-explicit-diff, at-explicit,
• nat-basic/l is used by inv-flashsize-app,
• nat-basic/l-01 is used by inv-flashsize-app,
• nat-basic/lf-01 is used by inv-listlen-ls2, inv-listlen-ls1, inv-flashsize-prepend, inv-flashsize-prefix, inv-flashsize-append, inv-flashsize-app, at-explicit-diff, at-explicit,
• nat-basic/lf-02 is used by inv-listlen-ls2, inv-listlen-ls1, at-explicit-diff, at-explicit,
• nat-basic/ls-02 is used by inv-listlen-ls2, inv-listlen-ls1, inv-flashsize-append, at-explicit-diff, at-explicit,
• nat-basic/nls-fst is used by to-adrs-sublist,
• nat-basic/one-01 is used by to-adrs-sublist, inv-flashsize-prepend,
• nat-basic/oz is used by to-adrs-sublist, to-adrs-drop, prefix-at, inv-flashsize-prepend,
• nat-basic/s-04 is used by inv-flashsize-prepend, inv-flashsize-append,
• nat-basic/succ is used by to-adrs-sublist, prefix-at, list-split, inv-flashsize-prepend, at-explicit-diff, at-explicit, addresslist-length,
• nat-basic/z-01 is used by to-adrs-sublist, to-adrs-drop, prefix-at,
• nat-basic/zero-01 is used by inv-flashsize-prepend, inv-flashsize-empty,

Used from specification ablock

• ablock/elim is used by remove-refsize0-one, prefix-trans, prefix-set-flags, prefix-remove-refsize0, prefix-rem-left, prefix-rem-alloc, prefix-rem, prefix-refl, prefix-notin-fwd, prefix-just-alloc, prefix-in, prefix-del-right, prefix-at, prefix-append-notin, prefix-append-in, prefix-alloc, inv-remove-refsize0-diff, inv-remove-refsize0, inv-reduce-rem, inv-reduce, inv-diff-n, inv-alloc, in-write-same, in-write-refsize, in-write-explicit, in-write-app, in-store-inv, in-diff, in-dealloc, in-alloc, except-refsizeeq-write-left, except-refsizeeq-trans, except-refsizeeq-comm, at-write-same, at-write-refsize, at-write-app, at-store-inv, at-explicit-other, at-diff, at-dealloc, at-alloc,
• ablock/inj is used by remove-refsize0-one, prefix-set-flags, prefix-append-in, inv-reduce, inv-alloc, in-write-same, in-write-refsize, in-diff, except-refsizeeq-write-left, except-refsizeeq-trans, at-write-same, at-write-refsize, at-write-app, at-store-inv,
• ablock/sel-01 is used by prefix-trans, prefix-set-flags, prefix-remove-refsize0, prefix-rem-left, prefix-rem-alloc, prefix-rem, prefix-refl, prefix-notin-fwd, prefix-just-alloc, prefix-in, prefix-del-right, prefix-at, prefix-append-notin, prefix-append-in, prefix-alloc, inv-set-sizes, inv-remove-refsize0-diff, inv-remove-refsize0, inv-reduce-rem, inv-reduce, inv-nodups-app-left, inv-nodups, inv-listlen-ls2, inv-listlen-ls1, inv-eq-list-size, inv-diff-n, inv-block-empty, inv-append, inv-alloc, inv-add-node, in-store-inv, except-refsizeeq-write-left, except-refsizeeq-trans, except-refsizeeq-comm, at-write-same, at-write-app, at-store-inv, at-explicit-other, at-explicit-diff, at-explicit, at-diff, at-dealloc, at-alloc,
• ablock/sel-02 is used by prefix-trans, prefix-set-flags, prefix-remove-refsize0, prefix-rem-left, prefix-rem-alloc, prefix-rem, prefix-refl, prefix-notin-fwd, prefix-just-alloc, prefix-in, prefix-del-right, prefix-at, prefix-append-notin, prefix-append-in, prefix-alloc, inv-set-sizes, inv-remove-refsize0-diff, inv-remove-refsize0, inv-reduce-rem, inv-reduce, inv-nodups-app-left, inv-nodups, inv-listlen-ls2, inv-listlen-ls1, inv-eq-list-size, inv-diff-n, inv-block-empty, inv-append, inv-alloc, inv-add-node, in-write-explicit, in-write-app, in-store-inv, in-in-adr, in-alloc, in-adr-in, except-refsizeeq-write-left, except-refsizeeq-trans, except-refsizeeq-comm, at-write-same, at-write-refsize, at-write-app, at-store-inv, at-explicit-other, at-explicit-diff, at-explicit, at-diff, at-dealloc, at-alloc,
• ablock/sel-03 is used by remove-refsize0-eq-nonzero, inv-remove-refsize0-diff,
• ablock/upd-03 is used by in-write-refsize, at-write-refsize,
• ablock/updsel-10 is used by inv-set-refsize,
• ablock/updsel-11 is used by inv-set-refsize,

Used from specification store

• store/ablock-store-nat-store/At-other is used by prefix-append-in, in-write-refsize, in-write-app, at-write-refsize,
• store/ablock-store-nat-store/Extension is used by remove-refsize0-eq-nonzero, remove-refsize0-empty,
• store/ablock-store-nat-store/k-Extension is used by remove-refsize0-one, remove-refsize0-idem,
• store/ablock-store-nat-store/At-in-out is used by prefix-rem-alloc, prefix-just-alloc, prefix-alloc, in-alloc, at-alloc,
• store/ablock-store-nat-store/At-other is used by remove-refsize0-one, prefix-set-flags, prefix-append-notin, inv-reduce, inv-alloc, in-write-same, except-refsizeeq-write-left, at-write-same, at-write-app, at-store-inv, at-explicit-other,
• store/ablock-store-nat-store/At-same is used by remove-refsize0-one, prefix-set-flags, prefix-append-notin, prefix-append-in, inv-reduce, inv-alloc, in-write-same, in-write-refsize, in-write-explicit, in-write-app, except-refsizeeq-write-left, at-write-same, at-write-refsize, at-write-app, at-store-inv,
• store/ablock-store-nat-store/Del-at is used by store-inv-rem, prefix-rem-left, prefix-rem, prefix-del-right, in-dealloc, at-dealloc,
• store/ablock-store-nat-store/Del-in is used by store-inv-rem, prefix-rem-left, prefix-rem, prefix-del-right, in-dealloc, at-dealloc,
• store/ablock-store-nat-store/In-empty is used by remove-refsize0-one, remove-refsize0-empty, prefix-empty-right, prefix-empty-left, inv-store-empty, in-empty,
• store/ablock-store-nat-store/In-insert is used by prefix-just-alloc, prefix-append-notin, inv-alloc, in-alloc, at-alloc,
• store/ablock-store-nat-store/in-neq is used by remove-refsize0-one, prefix-set-flags, prefix-rem-alloc, prefix-append-notin, prefix-append-in, inv-reduce, inv-alloc, in-write-same, in-write-refsize, in-write-app, except-refsizeeq-write-left, at-store-inv, at-explicit-other,
• store/ablock-store-nat-store/insin is used by remove-refsize0-one, prefix-set-flags, prefix-append-in, inv-reduce, inv-alloc, in-write-same, in-write-refsize, in-write-explicit, in-write-app, except-refsizeeq-write-left, at-store-inv,
• store/ablock-store-nat-store/notmemlookup is used by remove-refsize0-eq-nonzero, remove-refsize0-empty, except-refsizeeq-trans, dom-remove-refsize0,

Used from specification nat

• nat/add-01 is used by to-adrs-sublist, to-adrs-drop,
• nat/anti is used by inv-flashsize-append,
• nat/elim-pred-c is used by to-adrs-sublist, to-adrs-drop, inv-flashsize-prepend,
• nat/elim-sub is used by prefix-at, inv-flashsize-app,
• nat/fle is used by inv-flashsize-prefix, inv-flashsize-append,
• nat/fle-01 is used by inv-flashsize-append, inv-flashsize-app,
• nat/le-def is used by to-adrs-sublist, prefixn-to-adrs, inv-prefixn-lax, inv-flashsize-prefix,
• nat/le-ls-simp is used by inv-flashsize-prefix,
• nat/le-sum is used by to-adrs-sublist,
• nat/lels is used by prefix-at, inv-flashsize-prepend, inv-flashsize-append, inv-flashsize-app, at-write-app, at-explicit-diff, at-explicit,
• nat/lels-03 is used by inv-flashsize-append,
• nat/lep is used by to-adrs-sublist, prefixn-to-adrs, list-split, inv-flashsize-app,
• nat/lep-02 is used by to-adrs-sublist, list-split,
• nat/ler is used by prefixn-to-adrs, inv-flashsize-append,
• nat/let is used by to-adrs-sublist, inv-flashsize-append,
• nat/lez is used by list-split,
• nat/lez-01 is used by to-adrs-sublist, list-split,
• nat/not-zero is used by to-adrs-sublist,
• nat/succ-01 is used by inv-flashsize-prepend,
• nat/zero is used by inv-flashsize-append, at-explicit-diff, at-explicit,

Used from specification set-union

• set-union/nat-set/Difference is used by prefix-rem-alloc,
• set-union/nat-set/subdef is used by prefix-trans, prefix-rem-alloc, prefix-rem, prefix-notin-fwd, prefix-in, prefix-fwd-in, prefix-at, prefix-append-notin, dom-remove-refsize0,
• set-union/nat-set/Delete is used by prefix-rem-alloc, inv-alloc,
• set-union/nat-set/Difference is used by prefix-rem-alloc, prefix-rem,
• set-union/nat-set/Intersect is used by inv-remove-refsize0-diff,
• set-union/nat-set/diff-add-del is used by prefix-rem-alloc,
• set-union/nat-set/int-a is used by inv-remove-refsize0-diff,
• set-union/nat-set/int-c is used by inv-remove-refsize0-diff,
• set-union/nat-set/sub-del is used by prefix-rem,
• set-union/nat-set/sub-del-03 is used by prefix-rem-left,
• set-union/nat-set/sub-del-04 is used by prefix-del-right,

Used from specification set-basic

• set-basic/nat-set/Extension is used by inv-remove-refsize0-diff,
• set-basic/nat-set/In-empty is used by inv-remove-refsize0-diff,
• set-basic/nat-set/In-insert is used by prefix-rem-alloc, inv-reduce-rem,
• set-basic/nat-set/ne-01 is used by inv-remove-refsize0-diff,
• set-basic/nat-set/sub-add-01 is used by prefix-alloc,
• set-basic/nat-set/sub-add-03 is used by prefix-just-alloc,
• set-basic/nat-set/sub-e is used by prefix-empty-right, prefix-empty-left,
• set-basic/nat-set/sub-idem is used by prefix-refl,
• set-basic/nat-set/sub-insert-01 is used by prefix-append-notin,
• set-basic/nat-set/sub-trans is used by prefix-trans,
• set-basic/nat-set/subset-empty is used by prefix-empty-right,

Used from specification list-last

• list-last/prefix is used by prefix-at,
• list-last/laddress-list/prefix is used by prefix-at,
• list-last/prefix-rec is used by list-split,
• list-last/laddress-list/prefix-app is used by prefix-append-in,
• list-last/prefix-app is used by prefix-append-in,
• list-last/prefix-app-05 is used by list-split,
• list-last/laddress-list/prefix-in-01 is used by prefix-at,
• list-last/laddress-list/prefix-in-02 is used by prefix-notin-fwd, prefix-in,
• list-last/prefix-nil is used by list-split,
• list-last/prefix-self is used by prefix-remove-refsize0, prefix-refl, prefix-alloc,
• list-last/laddress-list/prefix-self is used by prefix-remove-refsize0, prefix-refl, prefix-alloc,
• list-last/prefix-trans is used by prefix-trans,
• list-last/laddress-list/prefix-trans is used by prefix-trans,

Used from specification list-prefixn

• list-prefixn/laddress-list/dropn-first is used by to-adrs-drop,
• list-prefixn/address-list-set/dropn-first is used by to-adrs-drop,
• list-prefixn/address-list-set/prefixn is used by prefixn-to-adrs,
• list-prefixn/laddress-list/prefixn is used by prefixn-to-adrs,
• list-prefixn/laddress-list/dropn-0 is used by to-adrs-drop,
• list-prefixn/address-list-set/dropn-0 is used by to-adrs-drop,
• list-prefixn/address-list-set/dropn-empty is used by to-adrs-drop,
• list-prefixn/laddress-list/dropn-empty is used by to-adrs-drop,
• list-prefixn/in-prefixn-at-smaller is used by inv-flashsize-prefix,
• list-prefixn/laddress-list/in-prefixn-at-smaller is used by inv-flashsize-prefix,
• list-prefixn/laddress-list/prefixn-fulln is used by inv-prefixn-lax,
• list-prefixn/laddress-list/prefixn-len-n is used by inv-flashsize-prefix,
• list-prefixn/prefixn-len-n is used by inv-flashsize-prefix,

Used from specification list-data

• list-data/elim-list-c is used by list-split,
• list-data/l is used by list-split,
• list-data/laddress-list/l is used by inv-listlen-ls2, inv-listlen-ls1, inv-flashsize-prepend, inv-flashsize-prefix, inv-flashsize-empty, inv-flashsize-append, inv-flashsize-app, at-explicit-diff, at-explicit,
• list-data/address-list-set/size-01 is used by addresslist-length,
• list-data/size-01 is used by list-split, inv-flashsize-empty, inv-block-empty,
• list-data/laddress-list/size-01 is used by to-adrs-sublist, inv-flashsize-empty, inv-block-empty, addresslist-length,

Used from specification laddress

• laddress/elim is used by to-ards-no-dups, to-adrs-sublist, to-adrs-in, to-adrs-eq-one, to-adrs-eq-app, to-adrs-eq, to-adrs-drop, inv-flashsize-prepend, inv-flashsize-prefix, inv-flashsize-append, inv-flashsize-app,
• laddress/inj is used by to-adrs-in, to-adrs-eq-app, inv-flashsize-prepend, inv-flashsize-append,
• laddress/sel-01 is used by to-adrs-sublist, to-adrs-eq-one, to-adrs-eq-app, to-adrs-drop, inv-flashsize-prepend, inv-flashsize-prefix, inv-flashsize-append, inv-flashsize-app,
• laddress/sel-02 is used by to-adrs-sublist, to-adrs-eq-one, to-adrs-eq-app, to-adrs-drop,

Used from specification list

• list/One is used by size-one,
• list/laddress-list/One is used by to-adrs-one,
• list/laddress-list/c is used by to-adrs-one,
• list/c is used by size-one,
• list/laddress-list/firstoc-rew is used by prefix-at,
• list/laddress-list/Last is used by to-adrs-eq-app,
• list/Nil is used by size-append, list-split,
• list/address-list-set/Nil is used by to-adrs-eq-app, to-adrs-append,
• list/laddress-list/Nil is used by to-adrs-eq-app, to-adrs-append,
• list/address-list-set/a is used by to-ards-no-dups, to-adrs-sublist, to-adrs-one, to-adrs-in, to-adrs-eq-one, to-adrs-eq-empty, to-adrs-eq-app, to-adrs-eq, to-adrs-drop, to-adrs-append, addresslist-length,
• list/laddress-list/a is used by to-ards-no-dups, to-adrs-sublist, to-adrs-in, to-adrs-eq-one, to-adrs-eq-empty, to-adrs-eq-app, to-adrs-eq, to-adrs-drop, to-adrs-append, prefixn-to-adrs, prefix-at, prefix-append-in, inv-nodups-app-left, inv-flashsize-prepend, inv-flashsize-append, inv-flashsize-app, inv-append, inv-add-node, in-write-app, at-write-app, at-explicit-diff, at-explicit, addresslist-length,
• list/a is used by size-append, prefix-at, prefix-append-in, list-split, inv-flashsize-prepend, inv-flashsize-append, inv-flashsize-app, inv-append, inv-add-node, at-write-app, at-explicit-diff, at-explicit,
• list/address-list-set/app is used by to-adrs-one,
• list/address-list-set/app-01 is used by to-adrs-eq-app,
• list/app-01 is used by list-split,
• list/address-list-set/app-02 is used by to-adrs-eq-empty, to-adrs-eq-app, to-adrs-eq,
• list/app-08 is used by list-split,
• list/laddress-list/app-08 is used by to-adrs-eq-app, to-adrs-eq,
• list/address-list-set/app-08 is used by to-adrs-sublist, to-adrs-drop, to-adrs-append,
• list/address-list-set/c is used by to-ards-no-dups, to-adrs-sublist, to-adrs-one, to-adrs-in, to-adrs-eq-one, to-adrs-eq-empty, to-adrs-eq-app, to-adrs-eq, to-adrs-drop, to-adrs-append, addresslist-length,
• list/laddress-list/c is used by to-ards-no-dups, to-adrs-sublist, to-adrs-in, to-adrs-eq-one, to-adrs-eq-empty, to-adrs-eq-app, to-adrs-eq, to-adrs-drop, to-adrs-append, addresslist-length,
• list/c is used by size-append, list-split,
• list/laddress-list/c-03 is used by to-adrs-eq-one, to-adrs-eq-app,
• list/address-list-set/c-03 is used by to-adrs-eq-one, to-adrs-eq-app,
• list/address-list-set/c-04 is used by to-adrs-one, to-adrs-eq-one,
• list/address-list-set/c-06 is used by to-adrs-eq-app, to-adrs-eq,
• list/address-list-set/c-07 is used by to-adrs-drop,
• list/laddress-list/c-07 is used by to-adrs-drop,
• list/address-list-set/e is used by to-adrs-eq-one, to-adrs-eq-empty, to-adrs-eq-app, to-adrs-eq,
• list/e-01 is used by list-split,
• list/laddress-list/e-01 is used by to-adrs-drop,
• list/address-list-set/e-01 is used by to-adrs-drop,
• list/laddress-list/in-10 is used by at-explicit-diff, at-explicit,
• list/address-list-set/in-14 is used by to-adrs-eq-app, to-adrs-eq,
• list/address-list-set/in-15 is used by to-adrs-eq-app,
• list/address-list-set/in-17 is used by to-adrs-eq-app,
• list/laddress-list/in-append is used by prefix-at, in-write-app, at-explicit-diff, at-explicit,
• list/address-list-set/in-append is used by to-adrs-eq-app,
• list/laddress-list/in-empty is used by to-adrs-in,
• list/address-list-set/in-empty is used by to-adrs-in,
• list/laddress-list/in-rec is used by to-adrs-in, to-adrs-eq-app, to-adrs-eq, prefix-at,
• list/address-list-set/in-rec is used by to-adrs-in, to-adrs-eq-app,
• list/laddress-list/len is used by prefixn-to-adrs, prefix-at, prefix-append-in, inv-nodups-app-left, inv-flashsize-append, inv-flashsize-app, inv-append, inv-add-node, at-explicit-diff, at-explicit,
• list/len is used by prefix-at, prefix-append-in, list-split, inv-flashsize-append, inv-flashsize-app, inv-append, inv-add-node, at-explicit-diff, at-explicit,
• list/address-list-set/len-02 is used by to-adrs-sublist,
• list/len-02 is used by inv-flashsize-prepend, inv-flashsize-append, inv-append, inv-add-node,
• list/laddress-list/len-02 is used by to-adrs-sublist, inv-flashsize-append, inv-append, inv-add-node,
• list/laddress-list/len-05 is used by to-adrs-sublist, prefix-at, inv-flashsize-prepend, at-explicit-diff, at-explicit, addresslist-length,
• list/len-05 is used by list-split, inv-flashsize-prepend, at-explicit-diff, at-explicit,
• list/address-list-set/len-05 is used by addresslist-length,

Used from specification list-dup

• list-dup/laddress-list/a is used by at-write-app, at-explicit-diff, at-explicit,
• list-dup/laddress-list/app-05 is used by inv-nodups-app-left,
• list-dup/address-list-set/e-01 is used by to-ards-no-dups,
• list-dup/laddress-list/e-01 is used by to-ards-no-dups, inv-block-empty,
• list-dup/laddress-list/f-01 is used by at-explicit-diff, at-explicit,
• list-dup/laddress-list/l-03 is used by inv-append, inv-add-node,
• list-dup/address-list-set/rec is used by to-ards-no-dups,
• list-dup/laddress-list/rec is used by to-ards-no-dups,

Used from specification address-data

• address-data/elim is used by to-adrs-eq-one, prefix-notin-fwd, prefix-in, prefix-at, in-write-same, in-write-refsize, in-write-app, in-diff, in-dealloc, in-alloc, at-write-same, at-write-refsize, at-write-app, at-alloc, addresslist-in,
• address-data/inj is used by to-adrs-in, to-adrs-eq-one, to-adrs-eq-app, to-adrs-eq,
• address-data/sel-03 is used by prefix-notin-fwd, prefix-in, prefix-at, notin-notin, in-write-refsize, in-write-explicit, in-write-app, in-in-adr, in-diff-explicit, in-diff, in-dealloc, in-alloc, in-adr-in, at-write-same, at-write-refsize, at-write-app, at-explicit-other, at-explicit-diff, at-explicit, at-diff, at-dealloc, at-alloc,
• address-data/sel-04 is used by prefix-notin-fwd, prefix-in, prefix-at, in-write-refsize, in-write-explicit, in-write-app, in-in-adr, in-diff, in-dealloc, in-alloc, in-adr-in, at-write-same, at-write-refsize, at-write-app, at-explicit-other, at-explicit-diff, at-explicit, at-diff, at-dealloc, at-alloc,
• address-data/sel-05 is used by prefix-notin-fwd, prefix-in, prefix-at, in-write-refsize, in-write-explicit, in-write-app, in-in-adr, in-diff, in-dealloc, in-alloc, in-adr-in, at-write-same, at-write-refsize, at-write-app, at-explicit-other, at-explicit-diff, at-explicit, at-diff, at-dealloc, at-alloc,

Used from specification oelem

• oelem/nat-set/irreflexivity is used by prefixn-to-adrs, inv-flashsize-append,

Used from specification list-del

• list-del/address-list-set/first-all-01 is used by prefixn-to-adrs,
• list-del/address-list-set/first-append is used by prefixn-to-adrs,
• list-del/get-append-grt is used by inv-flashsize-prepend, inv-flashsize-append, inv-flashsize-app, at-write-app, at-explicit-diff, at-explicit,
• list-del/get-append-less is used by prefix-at,
• list-del/laddress-list/sublist-append-01-01 is used by to-adrs-sublist,
• list-del/address-list-set/sublist-append-01-01 is used by to-adrs-sublist,
• list-del/address-list-set/sublist-append-02 is used by to-adrs-sublist,
• list-del/laddress-list/sublist-append-02 is used by to-adrs-sublist,
• list-del/laddress-list/app-05 is used by at-write-app,
• list-del/laddress-list/app-05-neg is used by prefix-at, at-explicit-diff, at-explicit,
• list-del/laddress-list/elim-firstn-restn is used by prefixn-to-adrs,
• list-del/get-append-grt is used by prefix-at,
• list-del/laddress-list/get-append-grt-02 is used by inv-flashsize-app,
• list-del/get-append-less is used by inv-flashsize-prepend, inv-flashsize-app, at-write-app, at-explicit-diff, at-explicit,
• list-del/laddress-list/get-append-less is used by inv-flashsize-app,
• list-del/get-butlast is used by inv-flashsize-append,
• list-del/laddress-list/get-butlast is used by inv-flashsize-append,
• list-del/get-last is used by inv-flashsize-append,
• list-del/laddress-list/get-last is used by inv-flashsize-append,
• list-del/laddress-list/get-last-03 is used by inv-flashsize-append,
• list-del/laddress-list/get-succ is used by inv-flashsize-prepend,
• list-del/get-succ is used by inv-flashsize-prepend,
• list-del/get-zero-01 is used by inv-flashsize-prepend, at-explicit-diff, at-explicit,
• list-del/laddress-list/get-zero-01 is used by inv-flashsize-prepend,
• list-del/laddress-list/inl-01 is used by at-write-app,
• list-del/one-03 is used by inv-flashsize-prepend, inv-flashsize-append,
• list-del/laddress-list/pos-y is used by prefix-at, at-explicit-diff, at-explicit,
• list-del/laddress-list/sub-zerozero is used by to-adrs-sublist,
• list-del/address-list-set/sub-zerozero is used by to-adrs-sublist,