Used simplifier rules/spec theorems by specification

Used from specification nat-basic

• nat-basic/a is used by encode-node, decode-node, abs-padding-subarray-failed, abs-padding-size, abs-padding-nospace, abs-padding-aligned-2headersize, abs-padding-abs-failed-append, abs-node-subarray-failed, abs-node-aligned-headersize, abs-node-aligned-2headersize, abs-node-abs-node-append-subarray, abs-node-abs-failed, abs-failed-size0,
• nat-basic/add-base is used by encode-node, decode-node, abs-padding-subarray-failed, abs-node-subarray-failed,
• nat-basic/c is used by encode-node, decode-node, abs-padding-subarray-failed, abs-padding-size, abs-padding-nospace, abs-padding-aligned-2headersize, abs-padding-abs-failed-append, abs-node-subarray-failed, abs-node-aligned-headersize, abs-node-aligned-2headersize, abs-node-abs-node-append-subarray, abs-node-abs-failed, abs-failed-size0,
• nat-basic/eq-01 is used by encode-node, decode-node, abs-node-abs-node-append-subarray,
• nat-basic/eq-02 is used by encode-node,
• nat-basic/eqs is used by encode-node,
• nat-basic/f is used by encode-node, decode-node, abs-padding-subarray-failed, abs-padding-nospace, abs-node-subarray-failed, abs-failed-size0,
• nat-basic/l is used by encode-node, decode-node, abs-padding-subarray-failed, abs-node-subarray-failed,
• nat-basic/l-01 is used by encode-node, abs-padding-subarray-failed, abs-node-subarray-failed,
• nat-basic/l-02 is used by encode-node, decode-node, abs-padding-nospace, abs-node-subarray-failed, abs-node-abs-node-append-subarray, abs-failed-size0,
• nat-basic/l-05 is used by encode-node, decode-node,
• nat-basic/l-06 is used by encode-node,
• nat-basic/l-08 is used by encode-node, abs-node-subarray-failed,
• nat-basic/lf is used by encode-node, abs-node-subarray-failed,
• nat-basic/lf-01 is used by encode-node, abs-node-subarray-failed, abs-failed-size0,
• nat-basic/lf-02 is used by encode-node, decode-node,
• nat-basic/ls-02 is used by encode-node, abs-node-subarray-failed,
• nat-basic/one is used by encode-node,
• nat-basic/ref is used by encode-node, abs-node-subarray-failed,
• nat-basic/succ is used by encode-node, abs-node-subarray-failed,
• nat-basic/trans is used by encode-node, abs-node-subarray-failed,
• nat-basic/z-01 is used by encode-node, abs-padding-abs-failed-append, abs-node-abs-failed,

Used from specification array-splice

• array-splice/buffer/append-a is used by abs-padding-eq, abs-padding-abs-failed-append, abs-node-no-abs-padding, abs-node-abs-node-append-subarray, abs-node-abs-node, abs-node-abs-failed,
• array-splice/buffer/append-at is used by encode-node,
• array-splice/buffer/append-inj is used by abs-padding-eq, abs-padding-abs-failed-append, abs-node-unique, abs-node-no-abs-padding, abs-node-abs-node-append-subarray, abs-node-abs-node, abs-node-abs-failed,
• array-splice/buffer/array-split1 is used by decode-node,
• array-splice/buffer/copy2append0 is used by encode-node,
• array-splice/buffer/fill2append is used by encode-node,
• array-splice/buffer/range-eq-subarrays is used by decode-node,
• array-splice/buffer/subarray-append-elim-left0 is used by decode-node,
• array-splice/buffer/subarray-append-shift-right is used by decode-node, abs-padding-subarray-failed, abs-node-subarray-failed, abs-node-abs-node-append-subarray,
• array-splice/buffer/subarray-elim is used by decode-node,
• array-splice/buffer/subarray-elim-right is used by decode-node,
• array-splice/buffer/append-a is used by encode-node, decode-node, buf-elim-2, buf-elim, abs-padding-subarray-failed, abs-padding-size, abs-padding-nospace, abs-padding-mkbuf0, abs-padding-isempty, abs-padding-full, abs-padding-eq, abs-padding-alignup, abs-padding-aligned-2headersize, abs-padding-abs-failed-append, abs-node-unique, abs-node-subarray-failed, abs-node-isempty, abs-node-full, abs-node-emptybuf, abs-node-aligned-headersize, abs-node-aligned-2headersize, abs-node-abs-node-append-subarray, abs-node-abs-node, abs-node-abs-failed, abs-failed-size0,
• array-splice/buffer/append-eq-emptyar is used by abs-padding-mkbuf0, abs-node-emptybuf,
• array-splice/buffer/append-eq-left is used by abs-padding-eq, abs-node-abs-node,
• array-splice/buffer/append-eq-right is used by decode-node, abs-padding-full, abs-padding-eq, abs-node-unique, abs-node-full, abs-node-abs-node-append-subarray, abs-node-abs-node,
• array-splice/buffer/append-inj is used by abs-padding-eq, abs-node-abs-node-append-subarray,
• array-splice/buffer/append-len is used by encode-node, decode-node, abs-padding-subarray-failed, abs-padding-size, abs-padding-nospace, abs-padding-aligned-2headersize, abs-padding-abs-failed-append, abs-node-subarray-failed, abs-node-aligned-headersize, abs-node-aligned-2headersize, abs-node-abs-node-append-subarray, abs-node-abs-failed, abs-failed-size0,
• array-splice/buffer/append-prefix-left is used by buf-elim-2,
• array-splice/buffer/append-zero-left is used by decode-node, buf-elim,
• array-splice/buffer/append-zero-right is used by abs-padding-subarray-failed, abs-node-subarray-failed,
• array-splice/buffer/emparray-at is used by encode-node,
• array-splice/buffer/emparray-len is used by encode-node, abs-padding-isempty, abs-node-isempty,
• array-splice/buffer/mkemparray0-append-right is used by encode-node,
• array-splice/buffer/range-eq-shift-right is used by decode-node,
• array-splice/buffer/subarray-append-elim-left is used by encode-node, decode-node,
• array-splice/buffer/subarray-append-elim-left0-simp is used by decode-node,
• array-splice/buffer/subarray-append-left is used by encode-node, decode-node, abs-padding-size, abs-padding-alignup, abs-node-abs-node-append-subarray,
• array-splice/buffer/subarray-append-shift-right-simp-0 is used by decode-node, abs-node-abs-node-append-subarray,
• array-splice/buffer/subarray-elim-right is used by encode-node, abs-padding-subarray-failed, abs-node-subarray-failed,

Used from specification node-header-size

• node-header-size/2-node-header-size-add-eq-0 is used by encode-node, abs-padding-subarray-failed, abs-node-subarray-failed,
• node-header-size/node-header-size-add-eq-0 is used by encode-node, decode-node, abs-padding-subarray-failed, abs-padding-abs-failed-append, abs-node-subarray-failed, abs-node-abs-failed,
• node-header-size/node-header-size-ls-2-node-header-size is used by encode-node,
• node-header-size/nodeheader-notzero is used by encode-node, decode-node, abs-padding-subarray-failed, abs-padding-nospace, abs-padding-alignup, abs-padding-aligned-2headersize, abs-padding-abs-failed-append, abs-node-subarray-failed, abs-node-aligned-headersize, abs-node-aligned-2headersize, abs-node-abs-node-append-subarray, abs-node-abs-failed, abs-failed-size0, abs-failed-aligned-headersize,
• node-header-size/validtrailer-neq-0 is used by abs-padding-mkbuf0, abs-node-emptybuf,
• node-header-size/validtrailer-size is used by encode-node, decode-node, abs-padding-subarray-failed, abs-padding-size, abs-padding-nospace, abs-padding-aligned-2headersize, abs-padding-abs-failed-append, abs-node-subarray-failed, abs-node-aligned-headersize, abs-node-aligned-2headersize, abs-node-abs-node-append-subarray, abs-node-abs-failed,

Used from specification encoding-node-base

• encoding-node-base/alignedsize is used by encode-node, decode-node, abs-node-subarray-failed, abs-node-abs-node-append-subarray, abs-node-abs-node, abs-node-abs-failed,
• encoding-node-base/is-aligned-2-alignedsize is used by encode-node, abs-node-aligned-2headersize,
• encoding-node-base/is-aligned-alignedsize is used by abs-node-subarray-failed, abs-node-aligned-headersize, abs-node-abs-failed,
• encoding-node-base/is-encoded-empbuf is used by abs-padding-isempty, abs-node-isempty,
• encoding-node-base/node-flash-size is used by encode-node, decode-node,

Used from specification nat

• nat/cancel-01 is used by encode-node,
• nat/elim-sub is used by encode-node, decode-node, abs-padding-subarray-failed, abs-node-subarray-failed, abs-node-abs-node-append-subarray,
• nat/eq-01 is used by encode-node, decode-node,
• nat/fle is used by encode-node, decode-node,
• nat/fle-01 is used by encode-node, decode-node, abs-padding-subarray-failed, abs-node-subarray-failed,
• nat/ge is used by encode-node, abs-padding-subarray-failed, abs-padding-abs-failed-append, abs-node-subarray-failed, abs-node-abs-failed, abs-failed-size0, abs-failed-nospace, abs-failed-aligned-headersize,
• nat/le is used by encode-node,
• nat/le-add is used by abs-padding-abs-failed-append, abs-node-abs-failed,
• nat/le-def is used by encode-node, decode-node, abs-padding-subarray-failed, abs-node-subarray-failed, abs-node-abs-node-append-subarray, abs-failed-size0,
• nat/le-ls-simp is used by encode-node, decode-node,
• nat/lels is used by encode-node, decode-node,
• nat/lels-02 is used by encode-node, decode-node,
• nat/lels-03 is used by encode-node, decode-node, abs-padding-subarray-failed, abs-node-subarray-failed,
• nat/lep is used by encode-node, decode-node, abs-padding-subarray-failed, abs-node-subarray-failed, abs-node-abs-node-append-subarray,
• nat/lep-02 is used by encode-node, decode-node, abs-node-abs-node-append-subarray,
• nat/ler is used by encode-node, decode-node, abs-padding-subarray-failed,
• nat/let is used by encode-node, decode-node, abs-padding-subarray-failed, abs-node-subarray-failed,
• nat/ls-02 is used by encode-node,
• nat/ls-le-simp is used by encode-node, decode-node, abs-failed-nospace,
• nat/sub-ls is used by encode-node,
• nat/zero is used by decode-node,

Used from specification error-class

• error-class/einval is used by decode-node,
• error-class/eio is used by decode-node,
• error-class/not-esuccess is used by encode-node, decode-node,

Used from specification encoding-fixed-size

• encoding-fixed-size/encoding-node-header/is-encoded-size is used by lfw-is-encoded-nodeheader-size,

Used from specification error

• error/disj-66 is used by decode-node,
• error/disj-78 is used by decode-node,

Used from specification encoding

• encoding/encoding-node-headerless/decode-contract is used by decode-node,
• encoding/encoding-node-headerless/encode-contract is used by encode-node,
• encoding/encoding-node-headerless/is-encoded-unique is used by encode-node, abs-node-unique, abs-node-full, abs-node-abs-node-append-subarray, abs-node-abs-node,

Used from specification align

• align/alignup-is-aligned is used by abs-node-subarray-failed,
• align/alignup-is-bigger is used by encode-node,
• align/alignup-is-even-bigger is used by encode-node,
• align/alignup-isnot-smaller is used by encode-node, decode-node, abs-node-subarray-failed,
• align/alignup-le-is-aligned is used by encode-node, abs-node-subarray-failed,
• align/alignup-same is used by encode-node, decode-node, abs-padding-subarray-failed, abs-padding-alignup, abs-padding-abs-failed-append, abs-node-subarray-failed, abs-node-abs-node-append-subarray, abs-node-abs-failed, abs-failed-size0,
• align/is-aligned-add is used by abs-padding-subarray-failed, abs-padding-aligned-2headersize, abs-padding-abs-failed-append, abs-node-subarray-failed, abs-node-aligned-headersize, abs-node-aligned-2headersize, abs-node-abs-failed,
• align/is-aligned-le-eq-zero is used by abs-padding-subarray-failed, abs-padding-abs-failed-append, abs-node-subarray-failed, abs-node-abs-failed, abs-failed-size0, abs-failed-aligned-headersize,
• align/is-aligned-ls-eq-zero is used by abs-padding-subarray-failed, abs-node-subarray-failed, abs-failed-size0,
• align/is-aligned-mod is used by abs-padding-subarray-failed, abs-padding-alignup, abs-padding-abs-failed-append,
• align/is-aligned-multiple-1 is used by abs-padding-subarray-failed, abs-padding-abs-failed-append,
• align/is-aligned-multiplier is used by abs-padding-abs-failed-append, abs-node-abs-failed,
• align/is-aligned-same is used by abs-padding-subarray-failed, abs-padding-aligned-2headersize, abs-node-subarray-failed, abs-node-aligned-headersize, abs-node-aligned-2headersize,
• align/is-aligned-zero is used by abs-padding-subarray-failed, abs-node-subarray-failed,

Used from specification encoding-fixed-size-nonempty

• encoding-fixed-size-nonempty/encoding-node-header/decode-contract is used by decode-node,
• encoding-fixed-size-nonempty/encoding-node-header/encode-contract is used by encode-node,
• encoding-fixed-size-nonempty/encoding-node-header/is-encoded-nonempty is used by lfw-is-encoded-nodeheader-size,
• encoding-fixed-size-nonempty/encoding-node-header/is-encoded-not-garbage-nonempty is used by abs-padding-subarray-failed, abs-padding-abs-failed-append, abs-node-subarray-failed, abs-node-abs-failed, abs-failed-size0,
• encoding-fixed-size-nonempty/encoding-node-header/is-encoded-unique is used by encode-node, decode-node, abs-padding-subarray-failed, abs-padding-size, abs-padding-full, abs-padding-eq, abs-padding-alignup, abs-padding-abs-failed-append, abs-node-unique, abs-node-subarray-failed, abs-node-no-abs-padding, abs-node-full, abs-node-abs-node-append-subarray, abs-node-abs-node, abs-node-abs-failed,

Used from specification array-copy

• array-copy/buffer/at-subarray is used by encode-node,
• array-copy/buffer/subarray-subarray-elim is used by encode-node,
• array-copy/buffer/Fill-zero is used by encode-node,
• array-copy/buffer/at-fill-mkarray is used by encode-node,
• array-copy/buffer/size-copy is used by encode-node,
• array-copy/buffer/size-fill is used by encode-node,
• array-copy/buffer/size-fill-h is used by encode-node,
• array-copy/buffer/size-subarray is used by encode-node, decode-node, abs-padding-subarray-failed, abs-node-subarray-failed,
• array-copy/buffer/subarray-at is used by encode-node,
• array-copy/buffer/subarray-copy-higher is used by encode-node,
• array-copy/buffer/subarray-copy-lower is used by encode-node,
• array-copy/buffer/subarray-elim is used by encode-node, decode-node, abs-node-subarray-failed, abs-node-no-abs-padding, abs-node-emptybuf, abs-node-aligned-2headersize, abs-node-abs-node-append-subarray,
• array-copy/buffer/subarray-zero is used by abs-padding-subarray-failed, abs-node-subarray-failed,

Used from specification abs-node

• abs-node/lfw-is-encoded-nodeheader-size is used by encode-node, decode-node, abs-padding-subarray-failed, abs-padding-size, abs-padding-nospace, abs-padding-isempty, abs-padding-full, abs-padding-eq, abs-padding-alignup, abs-padding-aligned-2headersize, abs-padding-abs-failed-append, abs-node-unique, abs-node-subarray-failed, abs-node-no-abs-padding, abs-node-isempty, abs-node-full, abs-node-aligned-headersize, abs-node-aligned-2headersize, abs-node-abs-node-append-subarray, abs-node-abs-node, abs-node-abs-failed, abs-failed-size0,

Used from specification node-header

• node-header/elim is used by decode-node, abs-padding-abs-failed-append, abs-node-abs-failed,
• node-header/inj is used by abs-padding-size, abs-padding-eq, abs-padding-alignup, abs-padding-abs-failed-append, abs-node-unique, abs-node-no-abs-padding, abs-node-abs-node-append-subarray, abs-node-abs-node, abs-node-abs-failed,
• node-header/sel is used by abs-padding-subarray-failed, abs-node-subarray-failed,

Used from specification nat-mult

• nat-mult/le-05 is used by decode-node,
• nat-mult/ls-08 is used by encode-node, decode-node, abs-node-abs-node-append-subarray,
• nat-mult/mult-a is used by encode-node, decode-node, abs-padding-subarray-failed, abs-padding-size, abs-padding-alignup, abs-padding-aligned-2headersize, abs-padding-abs-failed-append, abs-node-subarray-failed, abs-node-aligned-2headersize, abs-node-abs-node-append-subarray, abs-node-abs-failed, abs-failed-size0,
• nat-mult/mult-c is used by encode-node, decode-node, abs-padding-subarray-failed, abs-padding-size, abs-padding-alignup, abs-padding-aligned-2headersize, abs-padding-abs-failed-append, abs-node-subarray-failed, abs-node-aligned-2headersize, abs-node-abs-node-append-subarray, abs-node-abs-failed, abs-failed-size0,
• nat-mult/numeral-19 is used by encode-node, decode-node, abs-padding-size, abs-node-abs-node-append-subarray,
• nat-mult/numeral-20 is used by encode-node, decode-node, abs-node-abs-node-append-subarray,
• nat-mult/numeral-21 is used by encode-node,
• nat-mult/numeral-24 is used by encode-node, abs-padding-subarray-failed, abs-node-subarray-failed,
• nat-mult/numeral-25 is used by encode-node, abs-node-abs-node-append-subarray,
• nat-mult/numeral-26 is used by decode-node,
• nat-mult/numeral-29 is used by encode-node, decode-node, abs-padding-subarray-failed, abs-node-subarray-failed, abs-node-abs-node-append-subarray,
• nat-mult/numeral-30 is used by encode-node, abs-padding-subarray-failed, abs-node-subarray-failed,
• nat-mult/numeral-33 is used by encode-node, decode-node, abs-node-abs-node-append-subarray,
• nat-mult/numeral-36 is used by encode-node,
• nat-mult/one is used by encode-node, decode-node, abs-padding-subarray-failed, abs-padding-size, abs-node-subarray-failed, abs-node-abs-node-append-subarray,
• nat-mult/two-02 is used by encode-node, decode-node, abs-padding-subarray-failed, abs-padding-aligned-2headersize, abs-padding-abs-failed-append, abs-node-subarray-failed, abs-node-aligned-2headersize, abs-node-abs-failed,
• nat-mult/two-zero-01 is used by encode-node, decode-node, abs-padding-subarray-failed, abs-padding-alignup, abs-padding-aligned-2headersize, abs-padding-abs-failed-append, abs-node-subarray-failed, abs-node-aligned-2headersize, abs-node-abs-node-append-subarray, abs-node-abs-failed, abs-failed-size0,
• nat-mult/twole-02 is used by encode-node,
• nat-mult/twols is used by encode-node,

Used from specification eraseblock

• eraseblock/isempty-elim-right0 is used by abs-padding-isempty, abs-node-isempty,
• eraseblock/isempty-empbuf is used by lfw-is-encoded-nodeheader-size, abs-padding-isempty, abs-node-isempty,

Used from specification array

• array/buffer/Extension is used by encode-node,
• array/buffer/Size-mkarray is used by encode-node, decode-node, buf-size-zero,
• array/buffer/size-0 is used by buf-size-zero,

Used from specification debug

• debug/debug is used by decode-node,