Used simplifier rules/spec theorems by specification

Used from specification apeb

• apeb/elim is used by valid-peb0-imp-valid-peb, valid-peb-imp-valid-peb0,
• apeb/sel-04 is used by valid-peb0-write-append, valid-peb0-vidhdr-garbage, valid-peb0-vidhdr-empty, valid-peb0-valid-vidhdr, valid-peb0-invalid-vhdr, valid-peb0-invalid-ehdr, valid-peb-vol, valid-peb-vidhdr-garbage, valid-peb-vidhdr-empty, valid-peb-valid-vidhdr, valid-peb-leb, not-valid-peb2-explicit-0,
• apeb/sel-05 is used by valid-peb0-write-append, valid-peb0-vidhdr-garbage, valid-peb0-vidhdr-empty, valid-peb0-valid-vidhdr, valid-peb0-invalid-vhdr, valid-peb-vol, valid-peb-vidhdr-garbage, valid-peb-vidhdr-empty, valid-peb-valid-vidhdr, valid-peb-leb, not-valid-peb2-explicit-0,
• apeb/sel-06 is used by valid-peb0-write-append, valid-peb0-valid-vidhdr, valid-peb0-invalid-vhdr, valid-peb-vol, valid-peb-valid-vidhdr, valid-peb-leb, not-valid-peb2-explicit-0,
• apeb/sel-07 is used by valid-peb0-write-append,
• apeb/sel-08 is used by valid-peb0-write-append, valid-peb0-vidhdr-garbage, valid-peb0-vidhdr-empty, valid-peb0-valid-vidhdr, valid-peb0-invalid-vhdr, valid-peb0-invalid-ehdr, valid-peb0-bad, valid-peb-vol, valid-peb-vidhdr-garbage, valid-peb-vidhdr-empty, valid-peb-valid-vidhdr, valid-peb-leb, valid-peb-bad, not-valid-peb2-explicit-0,

Used from specification array-splice

• array-splice/buffer/emparray-at is used by valid-peb0-write-append, subarray-add-eq-mkempbuf,
• array-splice/buffer/emparray-len is used by valid-peb0-write-append, subarray-add-eq-mkempbuf,
• array-splice/buffer/mkemparray-eq is used by valid-peb0-write-append,
• array-splice/buffer/subarray-same-ar-eq is used by valid-peb0-write-append,

Used from specification nat-basic

• nat-basic/a is used by valid-peb0-write-append, subarray-add-eq-mkempbuf,
• nat-basic/add-base is used by valid-peb0-write-append,
• nat-basic/c is used by valid-peb0-write-append, subarray-add-eq-mkempbuf,
• nat-basic/eq-01 is used by valid-peb0-write-append,
• nat-basic/eqs is used by valid-peb0-write-append,
• nat-basic/f is used by valid-peb0-write-append, subarray-add-eq-mkempbuf,
• nat-basic/l is used by valid-peb0-write-append,
• nat-basic/l-01 is used by valid-peb0-write-append,
• nat-basic/l-02 is used by valid-peb0-write-append, subarray-add-eq-mkempbuf,
• nat-basic/l-05 is used by valid-peb0-write-append,
• nat-basic/lf is used by valid-peb0-write-append,
• nat-basic/lf-01 is used by valid-peb0-write-append,
• nat-basic/lf-02 is used by valid-peb0-write-append,
• nat-basic/ls-02 is used by valid-peb0-write-append,
• nat-basic/trans is used by valid-peb0-write-append,
• nat-basic/z-01 is used by valid-peb0-write-append,

Used from specification nat

• nat/le-addex is used by valid-peb0-write-append,
• nat/elim-sub is used by valid-peb0-write-append,
• nat/fle is used by valid-peb0-write-append,
• nat/fle-01 is used by valid-peb0-write-append, subarray-add-eq-mkempbuf,
• nat/le-def is used by valid-peb0-write-append,
• nat/le-ls-simp is used by valid-peb0-write-append,
• nat/lels is used by valid-peb0-write-append, subarray-add-eq-mkempbuf,
• nat/lels-02 is used by valid-peb0-write-append,
• nat/lels-03 is used by valid-peb0-write-append,
• nat/ler is used by valid-peb0-write-append,
• nat/let is used by valid-peb0-write-append,

Used from specification avidheader

• avidheader/disj-02 is used by valid-peb0-write-append, valid-peb0-vidhdr-empty, valid-peb-vidhdr-empty,
• avidheader/disj-03 is used by valid-peb0-vidhdr-garbage, valid-peb-vidhdr-garbage,
• avidheader/inj is used by valid-peb0-imp-valid-peb, valid-peb-unique, not-valid-peb2-explicit-0,
• avidheader/sel-06 is used by valid-peb0-imp-valid-peb, valid-peb-vol,
• avidheader/sel-08 is used by valid-peb0-imp-valid-peb, valid-peb-leb,
• avidheader/test-03 is used by valid-peb0-valid-vidhdr, valid-peb0-invalid-vhdr, valid-peb-valid-vidhdr,

Used from specification ubi-io-inv

• ubi-io-inv/peb-inv is used by valid-peb0-write-append,
• ubi-io-inv/peb-inv-size is used by valid-peb0-write-append,

Used from specification array-copy

• array-copy/buffer/size-subarray is used by valid-peb0-write-append, subarray-add-eq-mkempbuf,
• array-copy/buffer/subarray-at is used by valid-peb0-write-append, subarray-add-eq-mkempbuf,
• array-copy/buffer/subarray-elim is used by valid-peb0-write-append,
• array-copy/buffer/subarray-subarray-elim-0 is used by valid-peb0-write-append,

Used from specification datasize

• datasize/datasize is used by valid-peb0-write-append,
• datasize/datasize-add-empty-h is used by valid-peb0-write-append,
• datasize/datasize-append is used by valid-peb0-write-append,
• datasize/datasize-is-smaller-help is used by valid-peb0-write-append,
• datasize/datasize-le-fwd is used by valid-peb0-write-append, not-valid-peb2-explicit-0,
• datasize/datasize-ls-add is used by valid-peb0-write-append,
• datasize/datasize-subarray0 is used by valid-peb0-write-append,

Used from specification eraseblock

• eraseblock/lebsize-neq-zero is used by valid-peb0-write-append,

Used from specification checksum

• checksum/checksum-append-left is used by valid-peb0-write-append,
• checksum/checksum-prefix is used by valid-peb0-write-append,

Used from specification array

• array/buffer/Extension is used by valid-peb0-write-append, subarray-add-eq-mkempbuf,