Used simplifier rules/spec theorems by specification

Used from specification array-splice

• array-splice/buffer/append-a is used by abs-padding-abs-nodes-h, abs-nodes-one-abs-node, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,
• array-splice/buffer/append-inj is used by abs-padding-abs-nodes-h, abs-nodes-one-abs-node, abs-nodes-add-crash-aligned-h,
• array-splice/buffer/range-eq-subarrays is used by abs-nodes-notrailer-h,
• array-splice/buffer/subarray-append-elim-left is used by abs-nodes-notrailer-h,
• array-splice/buffer/subarray-append-shift-right is used by abs-nodes-subarray-failed, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,
• array-splice/buffer/subarray-elim-right is used by abs-nodes-notrailer-h,
• array-splice/buffer/append-a is used by ls-abs-node-buf-size, abs-split-by-address-h, abs-split-by-address, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-prefix-elim, abs-nodes-padding-prefix, abs-nodes-one-h, abs-nodes-one-abs-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nospace-h, abs-nodes-nodups-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-one, abs-nodes-no-padding-last, abs-nodes-mkbuf0-empty-h, abs-nodes-first-adr-explicit, abs-nodes-emptyheader-h, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-case-distinction-h, abs-nodes-bothcrash-prefix, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-append-empty, abs-nodes-append, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-nodes, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned, abs-failed-abs-nodes-h,
• array-splice/buffer/append-eq-emptyar is used by abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-mkbuf0-empty-h, abs-nodes-append-h, abs-nodes-add-crash-aligned-h, abs-failed-abs-nodes-h,
• array-splice/buffer/append-eq-left is used by abs-split-by-address-h, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-padding-prefix, abs-nodes-one-h, abs-nodes-one-abs-node, abs-nodes-no-padding-rec, abs-nodes-no-padding-last, abs-nodes-case-distinction-h, abs-nodes-bothcrash-prefix, abs-nodes-append-h, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,
• array-splice/buffer/append-inj is used by abs-padding-abs-nodes-h, abs-nodes-append-h,
• array-splice/buffer/append-len is used by ls-abs-node-buf-size, abs-split-by-address-h, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-padding-prefix, abs-nodes-one-abs-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nospace-h, abs-nodes-nodups-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-one, abs-nodes-no-padding-last, abs-nodes-first-adr-explicit, abs-nodes-emptyheader-h, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-bothcrash-prefix, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-nodes, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,
• array-splice/buffer/append-prefix-left is used by abs-padding-abs-nodes-h,
• array-splice/buffer/append-zero-left is used by abs-split-by-address-h, abs-nodes-split-h, abs-nodes-no-padding-last, abs-nodes-append-h, abs-nodes-add-crash-aligned-h,
• array-splice/buffer/append-zero-right is used by abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-subarray-failed, abs-nodes-one-abs-node, abs-nodes-nospace-header-h, abs-nodes-no-padding-one, abs-nodes-add-crash-aligned,
• array-splice/buffer/emparray-len is used by abs-nodes-emptyheader-h,
• array-splice/buffer/subarray-append-elim-left is used by abs-nodes-notrailer-h, abs-nodes-add-crash-aligned-h,
• array-splice/buffer/subarray-append-left is used by abs-nodes-valid-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-add-crash-aligned-h,
• array-splice/buffer/subarray-append-shift-right-simp-0 is used by abs-nodes-bothcrash-prefix,
• array-splice/buffer/subarray-elim-right is used by abs-nodes-valid-node, abs-nodes-subarray-failed, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,

Used from specification nat-basic

• nat-basic/a is used by ls-abs-node-buf-size, flashsize-one, flashsize-eq-0, add-failed-is-aligned, abs-split-by-address-h, abs-split-by-address, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-split, abs-nodes-prefix-h, abs-nodes-prefix-elim, abs-nodes-padding-prefix, abs-nodes-one-abs-node, abs-nodes-one, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nospace-h, abs-nodes-nodups-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-one, abs-nodes-no-padding-last, abs-nodes-headerspace, abs-nodes-first-adr-explicit, abs-nodes-emptyheader-h, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-bothcrash-prefix, abs-nodes-beyond-no-address-h, abs-nodes-beyond-no-address, abs-nodes-before-no-address-h, abs-nodes-atend-no-address, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-nodes, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,
• nat-basic/add-base is used by flashsize-one, abs-split-by-address-h, abs-split-by-address, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-split, abs-nodes-prefix-h, abs-nodes-prefix-elim, abs-nodes-one, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nodups-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-last, abs-nodes-first-adr-explicit, abs-nodes-emptyheader-h, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-beyond-no-address-h, abs-nodes-beyond-no-address, abs-nodes-before-no-address-h, abs-nodes-atend-no-address, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-nodes, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,
• nat-basic/c is used by ls-abs-node-buf-size, flashsize-one, flashsize-eq-0, add-failed-is-aligned, abs-split-by-address-h, abs-split-by-address, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-split, abs-nodes-prefix-h, abs-nodes-prefix-elim, abs-nodes-padding-prefix, abs-nodes-one-h, abs-nodes-one-abs-node, abs-nodes-one, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nospace-h, abs-nodes-nodups-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-one, abs-nodes-no-padding-last, abs-nodes-headerspace, abs-nodes-first-adr-explicit, abs-nodes-emptyheader-h, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-case-distinction-h, abs-nodes-bothcrash-prefix, abs-nodes-beyond-no-address-h, abs-nodes-beyond-no-address, abs-nodes-before-no-address-h, abs-nodes-atend-no-address, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-nodes, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,
• nat-basic/eq-01 is used by ls-abs-node-buf-size, flashsize-one, abs-split-by-address-h, abs-padding-abs-nodes-h, abs-nodes-subarray-failed, abs-nodes-one-abs-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-last, abs-nodes-emptyheader-h, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,
• nat-basic/eq-02 is used by abs-nodes-no-padding-one, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,
• nat-basic/f is used by abs-nodes-valid-node, abs-nodes-subarray-failed, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nospace-h, abs-nodes-headerspace, abs-nodes-crash-prefix, abs-nodes-crash-h, abs-nodes-bothcrash-prefix, abs-nodes-before-no-address-h, abs-nodes-at-least-flashsize, abs-nodes-add-crash-aligned-h,
• nat-basic/l is used by abs-nodes-subarray-failed, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-crash-h, abs-nodes-at-least-flashsize, abs-nodes-add-crash-aligned-h,
• nat-basic/l-01 is used by abs-nodes-subarray-failed, abs-nodes-nodups-h, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,
• nat-basic/l-02 is used by abs-nodes-nospace-header-h, abs-nodes-nospace-h, abs-nodes-headerspace, abs-nodes-before-no-address-h, abs-nodes-add-crash-aligned-h,
• nat-basic/l-05 is used by abs-nodes-nospace-header-h, abs-nodes-add-crash-aligned-h,
• nat-basic/l-08 is used by abs-nodes-add-crash-aligned-h,
• nat-basic/lf is used by abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,
• nat-basic/lf-01 is used by abs-nodes-subarray-failed, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-before-no-address-h, abs-nodes-add-crash-aligned-h,
• nat-basic/lf-02 is used by abs-nodes-valid-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-crash-h, abs-nodes-before-no-address-h, abs-nodes-add-crash-aligned-h,
• nat-basic/nls-fst is used by abs-nodes-at-least-flashsize,
• nat-basic/one is used by abs-nodes-crash-h,
• nat-basic/one-01 is used by abs-nodes-subarray-failed,
• nat-basic/oz is used by abs-nodes-no-padding-last, abs-nodes-add-crash-aligned-nodes,
• nat-basic/ref is used by abs-nodes-notrailer-h, abs-nodes-before-no-address-h,
• nat-basic/s-04 is used by abs-nodes-subarray-failed,
• nat-basic/succ is used by abs-split-by-address-h, abs-nodes-subarray-failed, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,
• nat-basic/trans is used by abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,
• nat-basic/z-01 is used by flashsize-eq-0, abs-split-by-address-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-padding-prefix, abs-nodes-notrailer-h, abs-nodes-nodups-h, abs-nodes-no-padding-last, abs-nodes-elems-adr-length-h, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-h,
• nat-basic/zero is used by abs-padding-abs-nodes-h, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-prefix-h, abs-nodes-nospace-h, abs-nodes-no-padding-one, abs-nodes-mkbuf0-empty-h, abs-nodes-crash-h, abs-nodes-beyond-no-address-h, abs-nodes-add-crash-aligned-h,
• nat-basic/zero-01 is used by abs-nodes-subarray-failed,

Used from specification node-header-size

• node-header-size/is-aligned-pagesize-imp-headersize is used by abs-nodes-crash, abs-nodes-add-crash-aligned,
• node-header-size/2-node-header-size-add-eq-0 is used by abs-nodes-nospace-header-h, abs-nodes-crash-h, abs-nodes-at-least-flashsize, abs-nodes-add-crash-aligned-h,
• node-header-size/is-aligned-pagesize-imp-headersize is used by add-failed-is-aligned,
• node-header-size/node-header-size-add-eq-0 is used by abs-padding-abs-nodes-h, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,
• node-header-size/nodeheader-notzero is used by flashsize-eq-0, add-failed-is-aligned, abs-split-by-address-h, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nospace-h, abs-nodes-nodups-h, abs-nodes-no-padding-one, abs-nodes-no-padding-last, abs-nodes-mkbuf0-empty-h, abs-nodes-headerspace, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-mod, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned, abs-failed-abs-nodes-h,
• node-header-size/nodeheader-pagesize is used by abs-nodes-aligned-2headersize-mod,
• node-header-size/validtrailer-neq-0 is used by abs-nodes-add-crash-aligned-h,
• node-header-size/validtrailer-size is used by ls-abs-node-buf-size, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-one-abs-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nospace-h, abs-nodes-emptyheader-h, abs-nodes-crash-h, abs-nodes-aligned-headersize-h, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,

Used from specification encoding-node-base

• encoding-node-base/alignedsize is used by abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-crash-h,
• encoding-node-base/is-aligned-2-alignedsize is used by abs-nodes-notrailer-h,
• encoding-node-base/is-aligned-alignedsize is used by abs-nodes-crash-h,
• encoding-node-base/is-encoded-empbuf is used by abs-nodes-emptyheader-h,
• encoding-node-base/node-flash-size is used by flashsize-one, flashsize-eq-0, abs-split-by-address-h, abs-split-by-address, abs-nodes-valid-node, abs-nodes-subarray-failed, abs-nodes-one-h, abs-nodes-one-abs-node, abs-nodes-one, abs-nodes-no-padding-rec, abs-nodes-no-padding-one, abs-nodes-no-padding-last, abs-nodes-case-distinction-h, abs-nodes-at-least-flashsize, abs-nodes-add-crash-aligned-nodes, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,

Used from specification nat

• nat/anti is used by abs-nodes-notrailer-h,
• nat/elim-sub is used by abs-nodes-subarray-failed, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,
• nat/eq-01 is used by abs-nodes-notrailer-h,
• nat/fle is used by abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-headerspace, abs-nodes-crash-h,
• nat/fle-01 is used by abs-nodes-subarray-failed, abs-nodes-nospace-header-h, abs-nodes-crash-h, abs-nodes-before-no-address-h, abs-nodes-add-crash-aligned-h,
• nat/ge is used by abs-nodes-valid-node, abs-nodes-no-padding-rec, abs-nodes-crash-h, abs-nodes-at-least-flashsize, abs-failed-abs-nodes-h,
• nat/le-add is used by abs-split-by-address-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-nodups-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-last, abs-nodes-first-adr-explicit, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-h,
• nat/le-def is used by abs-nodes-valid-node, abs-nodes-subarray-failed, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-headerspace, abs-nodes-emptyheader-h, abs-nodes-crash-h, abs-nodes-at-least-flashsize, abs-nodes-add-crash-aligned-h,
• nat/le-ls-simp is used by abs-nodes-notrailer-h,
• nat/lels is used by add-failed-is-aligned, abs-split-by-address-h, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-prefix-elim, abs-nodes-nospace, abs-nodes-nodups-h, abs-nodes-no-padding-last, abs-nodes-headerspace, abs-nodes-first-adr-explicit, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-h,
• nat/lels-02 is used by abs-nodes-notrailer-h, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,
• nat/lels-03 is used by abs-nodes-subarray-failed, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,
• nat/lep is used by abs-nodes-valid-node, abs-nodes-subarray-failed, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,
• nat/lep-02 is used by abs-nodes-valid-node, abs-nodes-notrailer-h, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,
• nat/ler is used by abs-nodes-notrailer-h, abs-nodes-atend-no-address,
• nat/let is used by abs-nodes-valid-node, abs-nodes-subarray-failed, abs-nodes-notrailer-h, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,
• nat/lez is used by abs-nodes-add-crash-aligned-h,
• nat/lez-01 is used by abs-nodes-valid-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h, abs-failed-abs-nodes-h,
• nat/ls-03 is used by abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,
• nat/ls-le-simp is used by abs-nodes-nospace,
• nat/zero is used by abs-nodes-notrailer-h,

Used from specification list-last

• list-last/laddress-list/prefix is used by abs-nodes-prefix-elim,
• list-last/prefix is used by abs-nodes-prefix-elim,
• list-last/prefix-empty is used by abs-nodes-prefix-h, abs-nodes-crash-h,
• list-last/laddress-list/prefix-empty is used by abs-nodes-crash-h,
• list-last/prefix-nil is used by abs-nodes-prefix-h, abs-nodes-crash-h,
• list-last/laddress-list/prefix-nil is used by abs-nodes-prefix-h, abs-nodes-crash-h,
• list-last/laddress-list/prefix-rec-02 is used by abs-nodes-prefix-h, abs-nodes-crash-h,
• list-last/prefix-rec-03 is used by abs-nodes-prefix-h, abs-nodes-crash-h,

Used from specification list-prefixn

• list-prefixn/laddress-list/prefixn-0 is used by abs-nodes-subarray-failed,
• list-prefixn/prefixn-0 is used by abs-nodes-subarray-failed,
• list-prefixn/prefixn-append-left is used by abs-nodes-subarray-failed,
• list-prefixn/laddress-list/prefixn-append-left is used by abs-nodes-subarray-failed,
• list-prefixn/prefixn-prepend-one is used by abs-nodes-subarray-failed,
• list-prefixn/laddress-list/prefixn-prepend-one is used by abs-nodes-subarray-failed,
• list-prefixn/laddress-list/prefixn-single-1 is used by abs-nodes-subarray-failed,
• list-prefixn/prefixn-single-1 is used by abs-nodes-subarray-failed,

Used from specification list-data

• list-data/laddress-list/elim-list-c is used by abs-split-by-address-h, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-padding-prefix, abs-nodes-one-h, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nodups-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-one, abs-nodes-no-padding-last, abs-nodes-first-adr-explicit, abs-nodes-emptyheader-h, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-case-distinction-h, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-h,
• list-data/l is used by abs-split-by-address-h,
• list-data/laddress-list/l is used by abs-nodes-subarray-failed, abs-nodes-elems-empty-adr-empty-h, abs-nodes-elems-adr-length-h,
• list-data/laddress-list/size-01 is used by abs-split-by-address-h, abs-nodes-no-padding-last, abs-nodes-add-crash-aligned-nodes,
• list-data/size-01 is used by abs-nodes-elems-empty-adr-empty-h, abs-nodes-elems-adr-length-h,

Used from specification laddress

• laddress/elim is used by abs-split-by-address-h, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-padding-prefix, abs-nodes-one-h, abs-nodes-one-abs-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nospace-h, abs-nodes-nodups-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-one, abs-nodes-no-padding-last, abs-nodes-first-adr-explicit, abs-nodes-emptyheader-h, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-case-distinction-h, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-h, abs-failed-abs-nodes-h,
• laddress/inj is used by inj-adr, abs-split-by-address-h, abs-split-by-address, abs-nodes-valid-node, abs-nodes-unique-strong-h, abs-nodes-split-h, abs-nodes-one-h, abs-nodes-one-abs-node, abs-nodes-first-adr-explicit, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h, abs-nodes-append-h, abs-nodes-add-crash-aligned-h,
• laddress/sel-01 is used by abs-split-by-address-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-one, abs-nodes-no-padding-last, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,
• laddress/sel-02 is used by abs-split-by-address-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-one, abs-nodes-no-padding-last, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,

Used from specification encoding-fixed-size-nonempty

• encoding-fixed-size-nonempty/encoding-node-header/is-encoded-not-garbage-nonempty is used by abs-nodes-valid-node, abs-nodes-crash-h,
• encoding-fixed-size-nonempty/encoding-node-header/is-encoded-unique is used by abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-one-abs-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,

Used from specification align

• align/between-is-aligned is used by abs-nodes-crash-h,
• align/is-aligned-add is used by abs-nodes-crash-h, abs-nodes-aligned-2headersize-mod,
• align/is-aligned-intro is used by abs-nodes-aligned-2headersize-mod,
• align/is-aligned-of-mod is used by abs-nodes-aligned-2headersize-mod,
• align/aligndown-is-aligned is used by abs-nodes-crash, abs-nodes-add-crash-aligned,
• align/aligndown-is-aligned-add is used by abs-nodes-bothcrash-prefix,
• align/aligndown-is-smaller-01 is used by abs-nodes-crash, abs-nodes-bothcrash-prefix, abs-nodes-add-crash-aligned,
• align/aligndown-same-equiv is used by abs-nodes-add-crash-aligned,
• align/alignup-isnot-smaller is used by abs-nodes-notrailer-h,
• align/alignup-le-is-aligned is used by abs-nodes-notrailer-h,
• align/alignup-same is used by abs-nodes-valid-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-crash-h,
• align/is-aligned-add is used by add-failed-is-aligned, abs-nodes-valid-node, abs-nodes-subarray-failed, abs-nodes-crash-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-h,
• align/is-aligned-align-up-multiple is used by abs-nodes-crash-h,
• align/is-aligned-le-eq-zero is used by add-failed-is-aligned, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,
• align/is-aligned-ls-eq-zero is used by abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,
• align/is-aligned-mod is used by abs-nodes-valid-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-crash-h,
• align/is-aligned-multiple-1 is used by abs-nodes-crash-h, abs-nodes-aligned-headersize-h, abs-nodes-add-crash-aligned-h,
• align/is-aligned-multiplier is used by abs-nodes-crash-h,
• align/is-aligned-same is used by abs-nodes-valid-node, abs-nodes-crash-h, abs-nodes-aligned-headersize-h, abs-nodes-add-crash-aligned-h,
• align/is-aligned-zero is used by add-failed-is-aligned, abs-nodes-subarray-failed, abs-nodes-crash-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,

Used from specification list

• list/One is used by flashsize-one, abs-nodes-one-h, abs-nodes-one-abs-node, abs-nodes-no-padding-one, abs-nodes-add-crash-aligned,
• list/c is used by flashsize-one, abs-nodes-one-h, abs-nodes-one-abs-node, abs-nodes-no-padding-one, abs-nodes-add-crash-aligned,
• list/elim-first is used by abs-nodes-subarray-failed,
• list/lastdiv-rew is used by abs-nodes-add-crash-aligned-nodes,
• list/laddress-list/lastdiv-rew is used by abs-nodes-add-crash-aligned-nodes,
• list/Nil is used by abs-split-by-address-h, abs-nodes-split-h, abs-nodes-no-padding-last, abs-nodes-append-h, abs-nodes-add-crash-aligned-h,
• list/laddress-list/Nil is used by abs-split-by-address-h, abs-nodes-split-h, abs-nodes-no-padding-last, abs-nodes-append-h, abs-nodes-add-crash-aligned-h,
• list/a is used by flashsize-eq-0, abs-split-by-address-h, abs-split-by-address, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-prefix-elim, abs-nodes-one-h, abs-nodes-one-abs-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nospace-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-one, abs-nodes-no-padding-last, abs-nodes-mkbuf0-empty-h, abs-nodes-emptyheader-h, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-case-distinction-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-append-empty-h, abs-nodes-append-empty, abs-nodes-append, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-nodes, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned, abs-failed-abs-nodes-h,
• list/laddress-list/a is used by abs-split-by-address-h, abs-split-by-address, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-prefix-elim, abs-nodes-padding-prefix, abs-nodes-one-h, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nodups-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-one, abs-nodes-no-padding-last, abs-nodes-first-adr-explicit, abs-nodes-emptyheader-h, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-case-distinction-h, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-append-empty-h, abs-nodes-append-empty, abs-nodes-append, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-nodes, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,
• list/app is used by abs-nodes-one-h, abs-nodes-one-abs-node, abs-nodes-no-padding-one, abs-nodes-append-empty-h, abs-nodes-add-crash-aligned,
• list/laddress-list/app is used by abs-nodes-one-h, abs-nodes-no-padding-one, abs-nodes-append-empty-h, abs-nodes-add-crash-aligned-nodes,
• list/app-01 is used by abs-nodes-prefix-elim, abs-nodes-append,
• list/laddress-list/app-01 is used by abs-nodes-prefix-elim, abs-nodes-append,
• list/laddress-list/app-02 is used by abs-split-by-address-h, abs-nodes-unique-weak-h, abs-nodes-no-padding-last,
• list/app-02 is used by abs-nodes-at-least-flashsize,
• list/app-04 is used by abs-nodes-append-empty, abs-nodes-add-crash-aligned-h,
• list/laddress-list/app-04 is used by abs-nodes-append-empty,
• list/laddress-list/app-07 is used by abs-nodes-split-h,
• list/app-08 is used by abs-nodes-unique-strong-h, abs-nodes-add-crash-aligned-h,
• list/laddress-list/app-08 is used by abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-first-adr-explicit, abs-nodes-case-distinction-h,
• list/c is used by flashsize-eq-0, abs-split-by-address-h, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-padding-prefix, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nospace-h, abs-nodes-nodups-h, abs-nodes-no-padding-last, abs-nodes-mkbuf0-empty-h, abs-nodes-emptyheader-h, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-case-distinction-h, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-h, abs-failed-abs-nodes-h,
• list/laddress-list/c is used by abs-split-by-address-h, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-padding-prefix, abs-nodes-one-h, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nospace-h, abs-nodes-nodups-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-one, abs-nodes-no-padding-last, abs-nodes-first-adr-explicit, abs-nodes-emptyheader-h, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-case-distinction-h, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-h, abs-failed-abs-nodes-h,
• list/laddress-list/c-03 is used by abs-split-by-address-h, abs-nodes-one-h, abs-nodes-no-padding-last,
• list/laddress-list/c-04 is used by abs-nodes-subarray-failed, abs-nodes-one-h, abs-nodes-no-padding-one, abs-nodes-add-crash-aligned-h,
• list/laddress-list/c-05 is used by abs-nodes-no-padding-last,
• list/c-06 is used by abs-split-by-address-h, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h,
• list/laddress-list/c-06 is used by abs-split-by-address-h, abs-nodes-unique-strong-h, abs-nodes-no-padding-last,
• list/laddress-list/c-07 is used by abs-split-by-address-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-last, abs-nodes-crash-h, abs-nodes-case-distinction-h, abs-nodes-append-h, abs-nodes-add-crash-aligned-h,
• list/c-07 is used by abs-nodes-valid-node, abs-nodes-case-distinction-h,
• list/c-08 is used by abs-nodes-valid-node, abs-nodes-case-distinction-h,
• list/laddress-list/c-08 is used by abs-split-by-address-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-last, abs-nodes-first-adr-explicit, abs-nodes-crash-h, abs-nodes-append-h, abs-nodes-add-crash-aligned-h,
• list/laddress-list/e is used by abs-split-by-address-h, abs-nodes-unique-weak-h, abs-nodes-one-h, abs-nodes-one-abs-node, abs-nodes-no-padding-one, abs-nodes-no-padding-last, abs-nodes-add-crash-aligned,
• list/e is used by abs-nodes-subarray-failed, abs-nodes-one-abs-node, abs-nodes-at-least-flashsize, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,
• list/e-01 is used by abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-prefix-h, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nospace-h, abs-nodes-mkbuf0-empty-h, abs-nodes-emptyheader-h, abs-nodes-crash-h, abs-nodes-case-distinction-h, abs-nodes-at-least-flashsize, abs-failed-abs-nodes-h,
• list/laddress-list/e-01 is used by abs-split-by-address-h, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-padding-prefix, abs-nodes-one-h, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nodups-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-last, abs-nodes-first-adr-explicit, abs-nodes-emptyheader-h, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-case-distinction-h, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-h,
• list/laddress-list/e-02 is used by abs-split-by-address-h, abs-nodes-no-padding-last,
• list/laddress-list/e-03 is used by abs-split-by-address-h,
• list/e-03 is used by abs-split-by-address-h,
• list/laddress-list/first is used by abs-nodes-one-abs-node, abs-nodes-no-padding-one, abs-nodes-add-crash-aligned,
• list/laddress-list/first-01 is used by abs-nodes-append-h,
• list/laddress-list/first-02 is used by abs-split-by-address-h,
• list/laddress-list/first-app is used by abs-nodes-append-h,
• list/laddress-list/in-12 is used by abs-nodes-before-no-address-h,
• list/in-14 is used by abs-split-by-address-h,
• list/laddress-list/in-14 is used by abs-split-by-address-h, abs-padding-abs-nodes-h, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-no-padding-last, abs-nodes-first-adr-explicit, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-case-distinction-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-h,
• list/laddress-list/in-15 is used by abs-split-by-address-h, abs-nodes-no-padding-last,
• list/laddress-list/in-17 is used by abs-split-by-address-h, abs-nodes-no-padding-last,
• list/in-append is used by abs-split-by-address-h,
• list/laddress-list/in-append is used by abs-split-by-address-h, abs-nodes-split-h, abs-nodes-no-padding-last,
• list/laddress-list/in-empty is used by abs-split-by-address-h, abs-nodes-no-padding-last, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h,
• list/laddress-list/in-rec is used by abs-split-by-address-h, abs-padding-abs-nodes-h, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-no-padding-last, abs-nodes-first-adr-explicit, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-case-distinction-h, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-h,
• list/in-rec is used by abs-split-by-address-h,
• list/len is used by abs-nodes-no-padding-last, abs-nodes-add-crash-aligned-nodes,
• list/laddress-list/len-02 is used by abs-nodes-subarray-failed,
• list/len-02 is used by abs-nodes-subarray-failed, abs-nodes-no-padding-last, abs-nodes-add-crash-aligned-nodes,
• list/laddress-list/len-05 is used by abs-split-by-address-h, abs-nodes-subarray-failed, abs-nodes-elems-adr-length-h,
• list/len-05 is used by abs-split-by-address-h, abs-nodes-elems-adr-length-h,
• list/laddress-list/rest is used by abs-nodes-one-abs-node, abs-nodes-no-padding-one, abs-nodes-add-crash-aligned,
• list/laddress-list/rest-01 is used by abs-nodes-append-h,

Used from specification array-copy

• array-copy/buffer/size-subarray is used by abs-nodes-valid-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-crash-h, abs-nodes-crash, abs-nodes-add-crash-aligned-h,
• array-copy/buffer/subarray-at is used by abs-nodes-add-crash-aligned-h,
• array-copy/buffer/subarray-elim is used by abs-nodes-valid-node, abs-nodes-one-abs-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nospace-h, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,
• array-copy/buffer/subarray-zero is used by abs-nodes-subarray-failed, abs-nodes-add-crash-aligned-h,

Used from specification list-dup

• list-dup/laddress-list/e-01 is used by abs-nodes-nodups-h,
• list-dup/laddress-list/rec is used by abs-nodes-nodups-h,

Used from specification abs-node

• abs-node/abs-failed is used by abs-nodes-valid-node, abs-nodes-crash-h, abs-failed-abs-nodes-h,
• abs-node/abs-node is used by ls-abs-node-buf-size, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-one-abs-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nospace-h, abs-nodes-emptyheader-h, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,
• abs-node/abs-node-no-abs-padding is used by abs-nodes-prefix-h, abs-nodes-append-h,
• abs-node/abs-padding is used by abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-one-abs-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nospace-h, abs-nodes-emptyheader-h, abs-nodes-crash-h, abs-nodes-aligned-headersize-h, abs-nodes-add-crash-aligned-h,
• abs-node/abs-failed-aligned-headersize is used by abs-nodes-aligned-headersize-h,
• abs-node/abs-failed-nospace is used by abs-nodes-nospace-h,
• abs-node/abs-node-abs-failed is used by abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-prefix-h, abs-failed-abs-nodes-h,
• abs-node/abs-node-abs-node is used by abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-one-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-last, abs-nodes-case-distinction-h, abs-nodes-add-crash-aligned-h,
• abs-node/abs-node-aligned-2headersize is used by abs-nodes-aligned-2headersize-h,
• abs-node/abs-node-aligned-headersize is used by abs-nodes-subarray-failed, abs-nodes-aligned-headersize-h, abs-nodes-add-crash-aligned-h,
• abs-node/abs-node-emptybuf is used by abs-nodes-add-crash-aligned-h,
• abs-node/abs-node-full is used by abs-nodes-one-abs-node, abs-nodes-crash-h, abs-nodes-add-crash-aligned,
• abs-node/abs-node-no-abs-padding is used by abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-padding-prefix, abs-nodes-one-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-last, abs-nodes-case-distinction-h, abs-nodes-append-h, abs-nodes-add-crash-aligned-h,
• abs-node/abs-node-subarray-failed is used by abs-nodes-subarray-failed,
• abs-node/abs-node-unique is used by abs-split-by-address-h, abs-split-by-address, abs-nodes-subarray-failed, abs-nodes-prefix-h, abs-nodes-no-padding-one, abs-nodes-no-padding-last, abs-nodes-append-h, abs-nodes-add-crash-aligned-nodes, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,
• abs-node/abs-padding-abs-failed-append is used by abs-nodes-unique-weak-h, abs-nodes-padding-prefix, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-emptyheader-h, abs-failed-abs-nodes-h,
• abs-node/abs-padding-aligned-2headersize is used by abs-nodes-aligned-2headersize-h,
• abs-node/abs-padding-alignup is used by abs-nodes-valid-node,
• abs-node/abs-padding-eq is used by abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-padding-prefix, abs-nodes-one-h, abs-nodes-case-distinction-h, abs-nodes-append-h,
• abs-node/abs-padding-full is used by abs-padding-abs-nodes-h, abs-nodes-crash-h,
• abs-node/abs-padding-isempty is used by abs-nodes-emptyheader-h,
• abs-node/abs-padding-mkbuf0 is used by abs-split-by-address-h, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-padding-prefix, abs-nodes-nodups-h, abs-nodes-no-padding-rec, abs-nodes-first-adr-explicit, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-h,
• abs-node/abs-padding-nospace is used by abs-nodes-valid-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-emptyheader-h,
• abs-node/abs-padding-size is used by abs-nodes-valid-node,
• abs-node/buf-size-zero is used by add-failed-is-aligned, abs-split-by-address-h, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-padding-prefix, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nospace-h, abs-nodes-nodups-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-one, abs-nodes-no-padding-last, abs-nodes-headerspace, abs-nodes-first-adr-explicit, abs-nodes-emptyheader-h, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-case-distinction-h, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned, abs-failed-abs-nodes-h,
• abs-node/lfw-is-encoded-nodeheader-size is used by ls-abs-node-buf-size, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-one-abs-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-emptyheader-h, abs-nodes-crash-h, abs-nodes-aligned-headersize-h, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,

Used from specification node-header

• node-header/elim is used by abs-nodes-crash-h,
• node-header/inj is used by abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-one-abs-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-add-crash-aligned-h,
• node-header/sel is used by abs-nodes-valid-node, abs-nodes-crash-h,

Used from specification eraseblock

• eraseblock/isempty-elim-right is used by abs-nodes-emptyheader-h,
• eraseblock/isempty-elim-right0 is used by abs-nodes-emptyheader-h,
• eraseblock/isempty-empbuf is used by abs-nodes-emptyheader-h,
• eraseblock/page-size is used by add-failed-is-aligned, abs-nodes-crash-prefix, abs-nodes-crash, abs-nodes-bothcrash-prefix, abs-nodes-aligned-2headersize-mod, abs-nodes-add-crash-aligned,

Used from specification nat-mult

• nat-mult/ls-08 is used by abs-nodes-valid-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h,
• nat-mult/mult-a is used by ls-abs-node-buf-size, flashsize-eq-0, abs-split-by-address-h, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-one-abs-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nodups-h, abs-nodes-no-padding-last, abs-nodes-emptyheader-h, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-mod, abs-nodes-aligned-2headersize-h, abs-nodes-aligned-2headersize, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,
• nat-mult/mult-c is used by ls-abs-node-buf-size, flashsize-eq-0, abs-split-by-address-h, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-one-abs-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nodups-h, abs-nodes-no-padding-last, abs-nodes-emptyheader-h, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-mod, abs-nodes-aligned-2headersize-h, abs-nodes-aligned-2headersize, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,
• nat-mult/numeral-19 is used by ls-abs-node-buf-size, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-one-abs-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-emptyheader-h, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,
• nat-mult/numeral-20 is used by abs-nodes-valid-node, abs-nodes-notrailer-h,
• nat-mult/numeral-23 is used by abs-nodes-crash-h,
• nat-mult/numeral-24 is used by abs-nodes-nospace-header-h, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,
• nat-mult/numeral-26 is used by abs-nodes-notrailer-h,
• nat-mult/numeral-29 is used by abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,
• nat-mult/numeral-30 is used by abs-nodes-nospace-header-h, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h,
• nat-mult/one is used by ls-abs-node-buf-size, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-one-abs-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-emptyheader-h, abs-nodes-crash-h, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,
• nat-mult/two-02 is used by abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-one-abs-node, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-crash-h, abs-nodes-aligned-headersize-h, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned,
• nat-mult/two-zero-01 is used by flashsize-eq-0, abs-split-by-address-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nodups-h, abs-nodes-no-padding-last, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-mod, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-h,

Used from specification awbuf-inv

• awbuf-inv/align-down-is-aligned is used by abs-nodes-add-crash-aligned,
• awbuf-inv/down-arrow-buf is used by abs-nodes-crash, abs-nodes-bothcrash-prefix, abs-nodes-add-crash-aligned,
• awbuf-inv/align-down-elim is used by abs-nodes-crash-prefix, abs-nodes-bothcrash-prefix,

Used from specification array

• array/buffer/Extension is used by abs-nodes-add-crash-aligned-h,
• array/buffer/Size-mkarray is used by add-failed-is-aligned, abs-split-by-address-h, abs-padding-abs-nodes-h, abs-nodes-valid-node, abs-nodes-unique-weak-h, abs-nodes-unique-strong-h, abs-nodes-subarray-failed, abs-nodes-split-h, abs-nodes-prefix-h, abs-nodes-notrailer-h, abs-nodes-nospace-header-h, abs-nodes-nospace-h, abs-nodes-nodups-h, abs-nodes-no-padding-rec, abs-nodes-no-padding-one, abs-nodes-no-padding-last, abs-nodes-mkbuf0-empty-h, abs-nodes-first-adr-explicit, abs-nodes-elems-adr-length-h, abs-nodes-crash-h, abs-nodes-beyond-no-address-h, abs-nodes-before-no-address-h, abs-nodes-at-least-flashsize, abs-nodes-append-h, abs-nodes-aligned-headersize-h, abs-nodes-aligned-2headersize-h, abs-nodes-add-crash-aligned-h, abs-nodes-add-crash-aligned, abs-failed-abs-nodes-h,