[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Used simplifier rules/spec theorems by specification

Used from specification int-basic1

int-basic1/lf-02 is used by fill-one-02,
int-basic1/lf-03 is used by fill-one-02,
int-basic1/ls-01 is used by fill-one-02,

Used from specification nat

nat/prop-01 is used by fill-lastn-03,
nat/add-01 is used by fill-sgn-02, fill-lastn-04, fill-lastn-03, fill-last,
nat/add-num-01 is used by fill-sgn-01,
nat/add-num-03 is used by sgn-length-02, sgn-lastn-01,
nat/elim-pred-c is used by sgn-ex-01, fill-rec, fill-one-02, fill-last,
nat/elim-sub is used by succ-fill, sgn-fill, inv-fill, fill-sgn-01, fill-rec-one, fill-rec-false, fill-rec, fill-lastn-03, fill-fill,
nat/eq-01 is used by succ-fill, inv-fill, fill-sgn, fill-rec-false, fill-rec, fill-fill,
nat/eq-02 is used by fill-length,
nat/fle is used by sgn-length, inv-fill, fill-sgn-01, fill-lastn-05, fill-lastn-04, fill-lastn-03, fill-last, fill-first,
nat/fle-01 is used by sgn-nls, sgn-length-02, inv-fill, fill-lastn-05, fill-lastn-04, fill-last, fill-first,
nat/l-num-04 is used by lastn-fill-sgn,
nat/le is used by fill-lastn-04,
nat/le-ls-simp is used by succ-fill, sgn-lastn-01, fill-lastn-03,
nat/le-num-02 is used by sgn-length-03, sgn-length-02, fill-sgn-01, fill-last,
nat/lels is used by succ-fill, sgn-length-03, sgn-length-02, sgn-length, sgn-lastn-01, lastn-fill-sgn, fix-size, fill-sgn-02, fill-sgn-01, fill-rec-false, fill-rec, fill-lastn-05, fill-lastn-04, fill-lastn-03, fill-last, fill-first,
nat/lels-01 is used by succ-fill, sgn-length-02, sgn-length-01, sgn-lastn-01, sgn-fill, lastn-fill-sgn, inv-fill, fill-size, fill-sgn-02, fill-sgn-01, fill-rec, fill-nls, fill-mklist, fill-length, fill-lastn-04, fill-lastn-03, fill-lastn-02, fill-lastn, fill-last, fill-in, fill-first, fill-fill-01, fill-empty,
nat/lels-03 is used by succ-fill, lastn-fill-sgn, inv-fill, fill-sgn-01, fill-rec, fill-nls, fill-lastn-03, fill-in,
nat/lep is used by sgn-fill, fill-sgn-01, fill-rec-false, fill-lastn-03, fill-last, fill-fill,
nat/lep-01 is used by succ-fill, sgn-length-03, sgn-length-02, fill-rec-false, fill-lastn-04,
nat/lep-02 is used by fill-sgn-03, fill-sgn-02, fill-sgn-01, fill-refill, fill-lastn-04,
nat/ler is used by fill-lastn-04, fill-lastn-03,
nat/let is used by sgn-length-03, sgn-lastn-01, fill-lastn-04, fill-lastn-03,
nat/lez is used by fill-zero, fill-rec-one, fill-last,
nat/lez-01 is used by fill-empty,
nat/ls-01 is used by fill-lastn-04,
nat/ls-03 is used by fill-lastn-03,
nat/pred-03 is used by succ-zeros-02, sgn-ex-01, fill-sgn-02, fill-rec, fill-lastn-04, fill-last, fill-first,
nat/sub-ls is used by fill-lastn-03,
nat/succ-01 is used by fill-sgn-01, fill-rec, fill-length, fill-last,
nat/zero is used by fill-lastn-03,
nat/zero-01 is used by fill-in, fill-empty,

Used from specification int-abs

int-abs/forward-le-05 is used by sgn-true-mklist, sgn-mklist-05,
int-abs/lels is used by fill-one-02,
int-abs/lels-01 is used by fill-one-02,
int-abs/lels-03 is used by fill-one-02,
int-abs/leone is used by fill-one-02,

Used from specification list-last

list-last/bitlista/mk-first is used by sgn-true-mklist,
list-last/bitlista/mk-inj-01 is used by fill-sgn-01,
list-last/bitlista/mk-last is used by succ-zeros-03,
list-last/bitlista/mk-last-02 is used by succ-zeros-02,
list-last/bitlista/mk-plus is used by fill-sgn-01,
list-last/bitlista/mk-succ is used by fill-sgn-01,
list-last/bitlista/b is used by inv-last-03,
list-last/bitlista/bapp is used by inv-last-03,
list-last/bitlista/l is used by inv-last-03, inv-last-02, inv-last-01,
list-last/bitlista/l-02 is used by inv-last-03, inv-last-02, inv-last-01,
list-last/bitlista/last-elim is used by succ-zero-03, succ-rec-02,
list-last/bitlista/mk-elem is used by sgn-mklist-04, sgn-mklist-03, fill-in,
list-last/bitlista/mk-empty is used by sgn-true-mklist, sgn-true, sgn-mklist-03, sgn-mklist, sgn-ex, sgn-2pot, fill-empty,
list-last/bitlista/mk-first is used by sgn-mklist,
list-last/bitlista/mk-in is used by sgn-mklist-03, sgn-ex-01, sgn-ex, fill-sgn, fill-in,
list-last/bitlista/mk-inj-01 is used by fill-lastn-05, fill-lastn-04, fill-lastn-03,
list-last/bitlista/mk-last is used by sgn-mklist-03, sgn-mklist-02, sgn-mklist-01, sgn-mklist, sgn-fill, sgn-ex-01, sgn-ex, inv-mklist, inv-fill, fill-sgn-03, fill-sgn-01, fill-rec-false, fill-rec, fill-one-02, fill-one-01, fill-lastn-05, fill-lastn-04, fill-lastn-03, fill-fill,
list-last/bitlista/mk-len is used by fill-sgn, fill-nls, fill-mklist, fill-length, fill-lastn-04, fill-lastn-03,
list-last/bitlista/mk-plus is used by sgn-mklist-03, sgn-mklist-02, sgn-mklist-01, sgn-mklist, sgn-ex-01, sgn-ex, inv-mklist, inv-last-02, inv-last-01, inv-fill, fill-sgn-03, fill-rec-false, fill-rec, fill-one-02, fill-one-01, fill-lastn-05, fill-lastn-04, fill-lastn-03, fill-fill,
list-last/bitlista/mk-two-01 is used by fill-rec-false,
list-last/bitlista/mk-zero is used by sgn-true-mklist, sgn-mklist-05, sgn-mklist-03, sgn-mklist-02, sgn-mklist-01, sgn-mklist, sgn-ex-01, sgn-2pot, inv-mklist, inv-last-02, inv-last-01, fill-sgn, fill-empty,
list-last/bitlista/mklist-one is used by sgn-mklist-03, sgn-mklist-02, sgn-mklist-01, sgn-mklist, sgn-ex-01, sgn-ex, inv-mklist, inv-last-02, inv-last-01, inv-fill, fill-sgn-03, fill-rec, fill-one-02, fill-one-01, fill-lastn-05, fill-lastn-04, fill-fill,

Used from specification list-data

list-data/bitlista/length-rest is used by fill-lastn-04,
list-data/bitlista/elim-list-c is used by succ-rest, succ-first-01, succ-first, succ-fill, sgn-zeros, sgn-zero, sgn-sgn-01, sgn-sgn, sgn-rec-01, sgn-one-01, sgn-notsame-01, sgn-notsame, sgn-not-empty-01, sgn-not-empty, sgn-mklist-03, sgn-length-02, sgn-length, sgn-lastn-01, sgn-last-diff, sgn-last-04, sgn-last-03, sgn-last-02, sgn-in-01, sgn-first-04, sgn-first-01, sgn-fill, sgn-ex-01, sgn-ex, sgn-base-05, sgn-base-04, sgn-base-03, sgn-append-06, sgn-append-03, sgn-append-02, sgn-append-01, sgn-2pot, lastn-fill-sgn, inv-sgn, inv-rest, inv-rec-01, inv-fill, fill-sgn-03, fill-sgn-02, fill-sgn, fill-rec-false, fill-rec, fill-lastn-03, fill-last, fill-first, fill-fill, bitsinvert-size,
list-data/bitlista/l is used by succ-rec-02, succ-length-01, succ-length, succ-falsein-02, sgn-true, sgn-nls, sgn-length, sgn-fill, sgn-base-05, lastn-fill-sgn, fix-zero, fill-sgn-01, fill-nls, fill-lastn-05, fill-lastn-04, fill-lastn-03, fill-lastn, fill-last, fill-fill-01,
list-data/bitlista/size-01 is used by sgn-length-02, sgn-length, sgn-ex-01, inv-len, inv-last-02, inv-last-01, fill-sgn-02, fill-sgn, fill-rec-one, fill-empty,

Used from specification list

list/bitlista/a is used by sgn-lastn,
list/bitlista/firstoc is used by fill-sgn-01,
list/bitlista/lastdiv is used by succ-zeros-01, succ-zero-01, succ-truein-01, succ-true, succ-succ, succ-prefix, succ-ones, succ-falsein, succ-false, succ-empty-01,
list/bitlista/lastoc-rew is used by succ-len, succ-exinv, succ-ex,
list/bitlista/len-05 is used by fill-sgn,
list/bitlista/split-rest is used by lastn-fill-sgn,
list/bitlista/Last is used by succ-zeros-03, succ-zeros-02, succ-zeros-01, succ-zero-03, succ-zero-01, succ-truein-01, succ-true, succ-succ, succ-rec-02, succ-rec-01, succ-prefix, succ-ones, succ-one-01, succ-one, succ-falsein-02, succ-falsein, succ-false, succ-empty-01, succ-01, fill-last,
list/bitlista/Nil is used by succ-one-01, succ-one, sgn-zeros, sgn-true-mklist, sgn-sgn-01, sgn-mklist-02, sgn-mklist, sgn-last-diff, sgn-last-04, sgn-last, sgn-append-03, sgn-append-02, sgn-append-01, sgn-append, inv-last-03, inv-append,
list/bitlista/Two is used by succ-one-01, succ-first-01,
list/bitlista/a is used by succ-zeros-03, succ-zeros-02, succ-zeros-01, succ-zeros, succ-zero-03, succ-zero-02, succ-zero-01, succ-truein-01, succ-true, succ-succ, succ-rest, succ-rec-02, succ-rec-01, succ-prefix, succ-ones, succ-one-01, succ-one, succ-mklist-01, succ-mklist, succ-length-01, succ-length, succ-len, succ-inv2x, succ-first-01, succ-first, succ-fill, succ-falsein-02, succ-falsein, succ-false, succ-exinv, succ-ex, succ-empty-01, succ-01, sgn-zeros, sgn-zero, sgn-true-mklist, sgn-sgn-01, sgn-sgn, sgn-rec-01-01, sgn-rec-01, sgn-one-01, sgn-notsame-01, sgn-notsame, sgn-not-empty-01, sgn-not-empty, sgn-negint, sgn-mklist-03, sgn-mklist-02, sgn-mklist-01, sgn-mklist, sgn-length-02, sgn-length, sgn-lastn-01, sgn-lastn, sgn-last-same, sgn-last-diff, sgn-last-04, sgn-last-03, sgn-last-02, sgn-last, sgn-in-02, sgn-in-01, sgn-in, sgn-first-04, sgn-first-03, sgn-first-02, sgn-first-01, sgn-first, sgn-fill, sgn-ex-01, sgn-ex, sgn-base-05, sgn-base-04, sgn-base-03, sgn-append-06, sgn-append-03, sgn-append-02, sgn-append-01, sgn-append, sgn-2pot, lastn-fill-sgn, inv-true-01, inv-sgn, inv-rew-01, inv-rew, inv-rest, inv-rec-01, inv-rec, inv-one, inv-mklist, inv-len, inv-last-03, inv-last-02, inv-last-01, inv-last, inv-inv, inv-in, inv-first-01, inv-first, inv-fill, inv-false-01, inv-empty, inv-append, fill-sgn-03, fill-sgn-02, fill-sgn-01, fill-sgn, fill-refill, fill-rec-one, fill-rec-false, fill-rec, fill-one-02, fill-one-01, fill-nls, fill-length, fill-lastn-05, fill-lastn-04, fill-lastn-03, fill-last, fill-in, fill-first, fill-fill, fill-empty, bitsinvert-size,
list/bitlista/app is used by succ-zeros-01, succ-zero-01, succ-succ, succ-prefix, succ-ones, sgn-zero, sgn-true-mklist, sgn-sgn-01, sgn-sgn, sgn-one-01, sgn-notsame-01, sgn-notsame, sgn-not-empty-01, sgn-not-empty, sgn-mklist-03, sgn-mklist-01, sgn-length-02, sgn-length, sgn-lastn-01, sgn-last-04, sgn-last, sgn-in-01, sgn-in, sgn-first, sgn-ex-01, sgn-ex, sgn-base-04, sgn-append-03, sgn-append-02, sgn-append-01, sgn-2pot, inv-sgn, inv-one, inv-last-03, inv-last-02, inv-last-01, fill-sgn-02, fill-rec-one, bitsinvert-size,
list/bitlista/app-01 is used by succ-zeros-03, succ-zeros-02, succ-zeros, succ-zero-03, succ-zero-01, succ-succ, succ-rec-02, succ-rec-01, succ-prefix, succ-mklist-01, succ-mklist, succ-inv2x, succ-fill, succ-01, sgn-sgn-01, sgn-sgn, sgn-negint, sgn-last, sgn-ex-01, sgn-ex, sgn-base-03, sgn-append-02, sgn-append-01, inv-sgn, inv-rew-01, inv-rew, inv-rec-01, inv-rec, inv-mklist, inv-last-03, inv-last, inv-inv, inv-first-01, inv-first, inv-fill, inv-append, fill-sgn-02, fill-rec-false, fill-rec, fill-one-02, fill-one-01, fill-last, fill-fill,
list/bitlista/app-02-ant is used by succ-first-01, succ-empty-01, sgn-zeros, sgn-true-mklist, sgn-one-01, sgn-notsame-01, sgn-notsame, sgn-not-empty-01, sgn-not-empty, sgn-mklist, sgn-lastn-01, sgn-last-same, sgn-last-04, sgn-in-02, sgn-first, sgn-ex-01, sgn-ex, sgn-base-05, sgn-append-03, lastn-fill-sgn, inv-empty, fill-sgn-02, fill-sgn, fill-last, fill-first, fill-empty,
list/bitlista/app-03 is used by succ-zeros-01, succ-zero-01, succ-succ, succ-prefix, succ-ones, sgn-last-diff, sgn-last-04, sgn-ex-01, sgn-ex, sgn-append-06, fill-sgn-01, fill-lastn-03, fill-last,
list/bitlista/app-04 is used by sgn-zero, sgn-last-diff, sgn-last-04, sgn-ex,
list/bitlista/app-05 is used by sgn-last-same, sgn-ex, fill-rec,
list/bitlista/c is used by succ-rest, succ-ones, succ-mklist-01, succ-length-01, succ-length, succ-inv2x, succ-first-01, succ-first, succ-fill, succ-ex, sgn-zeros, sgn-zero, sgn-sgn-01, sgn-sgn, sgn-rec-01, sgn-one-01, sgn-notsame-01, sgn-notsame, sgn-not-empty-01, sgn-not-empty, sgn-negint, sgn-mklist-03, sgn-length-02, sgn-length, sgn-lastn-01, sgn-last-diff, sgn-last-04, sgn-last-03, sgn-last-02, sgn-last, sgn-in-01, sgn-in, sgn-first-04, sgn-first-01, sgn-first, sgn-fill, sgn-ex-01, sgn-ex, sgn-base-05, sgn-base-04, sgn-base-03, sgn-append-06, sgn-append-03, sgn-append-02, sgn-append-01, sgn-append, sgn-2pot, lastn-fill-sgn, inv-true-01, inv-sgn, inv-rew-01, inv-rew, inv-rest, inv-rec-01, inv-rec, inv-one, inv-mklist, inv-len, inv-last-03, inv-last-02, inv-last-01, inv-inv, inv-in, inv-first-01, inv-first, inv-fill, inv-false-01, inv-empty, inv-append, fill-sgn-03, fill-sgn-02, fill-sgn-01, fill-sgn, fill-rec-false, fill-rec, fill-length, fill-lastn-03, fill-last, fill-first, fill-fill, bitsinvert-size,
list/bitlista/c-03 is used by sgn-one-01, sgn-notsame-01, sgn-notsame, sgn-last-04, inv-true-01, inv-false-01,
list/bitlista/c-04 is used by succ-true, succ-ones, succ-false, sgn-zero, sgn-two-01, sgn-two, sgn-true-mklist, sgn-sgn, sgn-one-01, sgn-mklist-03, sgn-mklist-01, sgn-last-same, sgn-last-diff, sgn-last-04, sgn-in, sgn-ex-01, sgn-base-04, sgn-append-03, sgn-2pot, inv-true-01, inv-sgn, inv-one-01, inv-last-03, inv-false-01, inv-false, fill-sgn-02,
list/bitlista/c-05 is used by succ-true, succ-false,
list/bitlista/c-06 is used by succ-first-01, sgn-notsame-01, sgn-notsame, sgn-last-04, sgn-ex-01, inv-last-02, inv-last-01, fill-sgn-03, fill-first, bitsinvert-size,
list/bitlista/c-07 is used by succ-rest, sgn-lastn-01, inv-rest, fill-refill, fill-lastn-05, fill-lastn-04,
list/bitlista/c-08 is used by succ-first, sgn-lastn-01, sgn-last-04, sgn-first-03, sgn-first-02, sgn-first, sgn-ex-01, sgn-ex, sgn-base-05, fill-sgn-02, fill-sgn, fill-last, fill-first,
list/bitlista/e is used by succ-true, succ-empty-01, sgn-zeros, sgn-two-03, sgn-two-02, sgn-two-01, sgn-two, sgn-one-01, sgn-notsame-01, sgn-notsame, sgn-not-empty-01, sgn-not-empty, sgn-mklist-05, sgn-lastn-01, sgn-last-same, sgn-last-diff, sgn-last-04, sgn-last-01, sgn-in-02, sgn-first, sgn-ex-01, sgn-ex, sgn-base-05, lastn-fill-sgn, inv-true-01, inv-false-01, inv-empty, fill-sgn-02, fill-sgn, fill-rec, fill-one-02, fill-last, fill-first,
list/bitlista/e-01 is used by succ-rest, succ-length-01, succ-length, succ-first-01, succ-first, succ-fill, sgn-zero, sgn-sgn-01, sgn-sgn, sgn-rec-01, sgn-one-01, sgn-notsame-01, sgn-notsame, sgn-not-empty-01, sgn-not-empty, sgn-length-02, sgn-length, sgn-lastn-01, sgn-last-diff, sgn-last-04, sgn-last-03, sgn-last-02, sgn-in-01, sgn-first-01, sgn-first, sgn-fill, sgn-ex-01, sgn-ex, sgn-base-05, sgn-base-04, sgn-base-03, sgn-append-06, sgn-append-03, sgn-append-02, sgn-append-01, lastn-fill-sgn, inv-sgn, inv-rest, inv-rec-01, inv-last-03, inv-last-02, inv-last-01, inv-fill, fill-sgn-03, fill-sgn-02, fill-sgn, fill-rec-false, fill-rec, fill-lastn-04, fill-lastn-03, fill-last, fill-first, fill-fill, bitsinvert-size,
list/bitlista/e-02 is used by succ-zeros-01, succ-zero-03, succ-zero-01, succ-truein-01, succ-true, succ-succ, succ-prefix, succ-ones, succ-falsein, succ-false, succ-empty-01, sgn-zeros, sgn-last-same, sgn-last-04,
list/bitlista/e-03 is used by sgn-zeros, lastn-fill-sgn,
list/bitlista/eq-05 is used by bitsinvert-size,
list/bitlista/first is used by sgn-two-03, sgn-two-02, sgn-two-01, sgn-two, sgn-last-diff, sgn-last-01, sgn-first, fill-one-02,
list/bitlista/first-01 is used by sgn-append-03,
list/bitlista/first-02 is used by sgn-zeros,
list/bitlista/in-01 is used by sgn-in-01,
list/bitlista/in-06 is used by succ-falsein, sgn-zeros, sgn-zero, sgn-one-01, sgn-notsame, sgn-last-04, sgn-in-01, sgn-in, sgn-base-04, sgn-append-03, sgn-append-02, sgn-append-01, sgn-append, inv-in,
list/bitlista/in-08 is used by fill-in,
list/bitlista/in-12 is used by fill-in,
list/bitlista/in-13 is used by sgn-notsame-01, sgn-ex-01, fill-sgn-01,
list/bitlista/in-14 is used by succ-first-01, sgn-zeros, sgn-notsame-01, sgn-mklist-03, sgn-last-04, sgn-first-04, sgn-first-03, sgn-first-02, sgn-ex-01, sgn-ex, sgn-append-03, sgn-2pot, inv-first-01, inv-first, fill-sgn-03, fill-sgn-02, fill-sgn, fill-first, bitsinvert-size,
list/bitlista/in-15 is used by succ-zeros-01, succ-zero-01, succ-truein-01, succ-true, succ-succ, succ-prefix, succ-ones, succ-falsein, succ-false, succ-empty-01, sgn-zeros, sgn-notsame, sgn-last-04,
list/bitlista/in-17 is used by succ-zeros-01, succ-zero-01, succ-truein-01, succ-true, succ-succ, succ-prefix, succ-ones, succ-first-01, succ-falsein-02, succ-falsein, succ-false, succ-empty-01, sgn-zeros, sgn-one-01, sgn-notsame-01, sgn-notsame, sgn-last-same, sgn-last-diff, sgn-last-04, sgn-last, sgn-in-01, sgn-first-03, sgn-first-02, sgn-ex-01, sgn-append-06, sgn-append-03, sgn-append-02, sgn-append-01, inv-in, fill-sgn-03, fill-sgn-02, fill-sgn-01, fill-first, bitsinvert-size,
list/bitlista/in-append is used by succ-zeros-01, succ-zero-01, succ-truein-01, succ-true, succ-succ, succ-prefix, succ-ones, succ-first-01, succ-falsein-02, succ-falsein, succ-false, succ-empty-01, sgn-zeros, sgn-one-01, sgn-notsame-01, sgn-notsame, sgn-last-same, sgn-last-diff, sgn-last-04, sgn-last, sgn-in-01, sgn-first-03, sgn-first-02, sgn-ex-01, sgn-ex, sgn-append-06, sgn-append-03, sgn-append-02, sgn-append-01, inv-in, fill-sgn-03, fill-sgn-02, fill-sgn-01, fill-sgn, fill-in, fill-first, bitsinvert-size,
list/bitlista/in-empty is used by succ-zero-01, sgn-zero, sgn-one-01, sgn-last-04, sgn-last, sgn-in-01, sgn-ex-01, sgn-append-03, sgn-append-02, sgn-append-01, inv-in,
list/bitlista/inapp-08 is used by sgn-last-04,
list/bitlista/len is used by succ-zeros-01, succ-zero-01, succ-truein-01, succ-succ, succ-prefix, succ-ones, succ-length-01, succ-length, succ-len, succ-fill, sgn-length-02, sgn-length, sgn-lastn-01, sgn-lastn, sgn-ex-01, sgn-base-05, lastn-fill-sgn, inv-len, inv-last-02, inv-last-01, inv-fill, fill-sgn-03, fill-sgn-02, fill-sgn-01, fill-sgn, fill-refill, fill-rec-false, fill-rec, fill-nls, fill-length, fill-lastn-04, fill-lastn-03, fill-last, fill-first, fill-fill, bitsinvert-size,
list/bitlista/len-02 is used by succ-zeros-01, succ-zero-01, succ-truein-01, succ-succ, succ-prefix, succ-ones, succ-length-01, succ-length, succ-len, succ-fill, sgn-length-02, sgn-length, sgn-lastn-01, sgn-lastn, sgn-ex-01, sgn-base-05, lastn-fill-sgn, inv-len, inv-last-02, inv-last-01, inv-fill, fill-sgn-03, fill-sgn-02, fill-sgn-01, fill-sgn, fill-refill, fill-rec-false, fill-rec, fill-one-02, fill-one, fill-length, fill-lastn-04, fill-lastn-03, fill-last, fill-first, fill-fill, bitsinvert-size,
list/bitlista/neq is used by succ-exinv, succ-ex,
list/bitlista/ni is used by sgn-last-04,

Used from specification nat-basic2

nat-basic2/a is used by succ-zeros-01, succ-zero-01, succ-truein-01, succ-succ, succ-prefix, succ-ones, succ-length-01, succ-length, succ-len, succ-fill, sgn-mklist-03, sgn-mklist-02, sgn-mklist-01, sgn-mklist, sgn-length-03, sgn-length-02, sgn-length, sgn-lastn-01, sgn-lastn, sgn-fill, sgn-ex-01, sgn-ex, sgn-base-05, lastn-fill-sgn, inv-mklist, inv-len, inv-last-02, inv-last-01, inv-fill, fill-sgn-03, fill-sgn-02, fill-sgn-01, fill-sgn, fill-refill, fill-rec-one, fill-rec-false, fill-rec, fill-one-02, fill-one-01, fill-nls, fill-length, fill-lastn-05, fill-lastn-04, fill-lastn-03, fill-lastn-02, fill-last, fill-first, fill-fill, bitsinvert-size,
nat-basic2/c is used by succ-zeros-01, succ-zero-01, succ-truein-01, succ-succ, succ-prefix, succ-ones, succ-length-01, succ-length, succ-len, succ-fill, sgn-mklist-03, sgn-mklist-02, sgn-mklist-01, sgn-mklist, sgn-length-03, sgn-length-02, sgn-length, sgn-lastn-01, sgn-lastn, sgn-fill, sgn-ex-01, sgn-ex, sgn-base-05, lastn-fill-sgn, inv-mklist, inv-len, inv-last-02, inv-last-01, inv-fill, fill-sgn-03, fill-sgn-02, fill-sgn-01, fill-sgn, fill-refill, fill-rec-one, fill-rec-false, fill-rec, fill-one-02, fill-one-01, fill-nls, fill-length, fill-lastn-05, fill-lastn-04, fill-lastn-03, fill-lastn-02, fill-last, fill-first, fill-fill, bitsinvert-size,
nat-basic2/eq is used by lastn-fill-sgn,
nat-basic2/eq-01 is used by succ-len, sgn-lastn, lastn-fill-sgn, inv-len, fill-sgn-01, fill-sgn, bitsinvert-size,
nat-basic2/l is used by succ-length-01, succ-length, succ-fill, sgn-length-02, sgn-length, lastn-fill-sgn, fill-sgn-01, fill-lastn-03, fill-last, fill-first,
nat-basic2/l-01 is used by succ-fill, lastn-fill-sgn, inv-fill, fill-sgn-01, fill-rec, fill-lastn-03,
nat-basic2/l-02 is used by succ-length-01, succ-length, sgn-length, lastn-fill-sgn, inv-fill, fill-rec, fill-nls, fill-lastn-04, fill-lastn-02, fill-last, fill-fill,
nat-basic2/nls-fst is used by succ-fill,
nat-basic2/one is used by sgn-base-05,
nat-basic2/oz is used by sgn-mklist-03, sgn-ex-01, fill-sgn-03, fill-rec, fill-one-01, fill-lastn-04, fill-last,
nat-basic2/pred is used by fill-sgn-03, fill-lastn-05, fill-lastn-04, fill-last,
nat-basic2/s is used by succ-zeros-01, succ-zero-01, succ-truein-01, succ-succ, succ-prefix, succ-ones, lastn-fill-sgn, inv-fill, fill-sgn-03, fill-sgn-01, fill-rec, fill-lastn-05, fill-lastn-04, fill-lastn-03, fill-last, fill-fill,
nat-basic2/succ is used by sgn-mklist-03, sgn-mklist-02, sgn-mklist-01, sgn-mklist, lastn-fill-sgn, inv-mklist, fill-sgn, fill-lastn-03, fill-last, fill-fill-01,
nat-basic2/z is used by fill-rec-one,
nat-basic2/z-01 is used by fill-rec-false,

Used from specification intnat

intnat/abs-zero is used by sgn-true-mklist, sgn-mklist-05, fill-one-02,
intnat/num-i2n-le-02 is used by fill-one-02,

Used from specification nat-basic1

nat-basic1/f is used by succ-length-01, succ-length, succ-fill, sgn-nls, sgn-length-02, sgn-length, sgn-lastn-01, sgn-fill, lastn-fill-sgn, inv-fill, fill-sgn-01, fill-rec, fill-nls, fill-lastn-05, fill-lastn-04, fill-lastn-03, fill-lastn, fill-last, fill-in, fill-first, fill-fill-01, fill-empty,
nat-basic1/less-1 is used by fill-rec,
nat-basic1/lf-01 is used by lastn-fill-sgn,
nat-basic1/ls-02 is used by succ-fill, sgn-fill, lastn-fill-sgn, inv-fill, fill-sgn-01, fill-rec, fill-nls, fill-length, fill-lastn-03, fill-lastn, fill-in, fill-empty,
nat-basic1/one is used by succ-fill, sgn-base-05,
nat-basic1/one-01 is used by fill-sgn-01, fill-lastn-04,
nat-basic1/ref-1 is used by succ-zeros-01, succ-zero-01, succ-truein-01, succ-succ, succ-prefix, succ-ones, sgn-length, inv-fill, fill-size, fill-sgn-02, fill-nls, fill-mklist, fill-lastn-05, fill-lastn-04, fill-last, fill-first, fill-fill-01,
nat-basic1/trans is used by lastn-fill-sgn, fill-lastn-03, fill-fill-01,
nat-basic1/trans-1 is used by lastn-fill-sgn, fill-lastn-03, fill-fill-01,
nat-basic1/z is used by fix-zero, fill-rec-one, fill-one-01,

Used from specification bitlista

bitlista/mklist-intro is used by sgn-true, sgn-ex-01, fill-sgn-01,
bitlista/inmklist is used by sgn-2pot,
bitlista/inmklist-01 is used by succ-mklist-01, succ-mklist, sgn-mklist-04, sgn-ex-01,
bitlista/mklist-intro is used by inv-last-02, inv-last-01,
bitlista/mklist-num is used by sgn-ex-01,
bitlista/mklist-num-01 is used by sgn-ex-01,

Used from specification list-del

list-del/bitlista/lastN-all is used by sgn-lastn, lastn-fill-sgn, fill-lastn-05, fill-lastn-04,
list-del/bitlista/lastN-append is used by sgn-lastn, lastn-fill-sgn,
list-del/bitlista/lastN-append-01 is used by fill-lastn-04,
list-del/bitlista/lastN-rec-02 is used by sgn-lastn-01,
list-del/bitlista/lastn-restn-01 is used by fill-lastn-03,
list-del/bitlista/restN-append is used by fill-lastn-03,
list-del/bitlista/lastN-append-01 is used by fill-lastn-03,
list-del/bitlista/lastN-empty is used by fix-empty,
list-del/bitlista/lastN-zero is used by fix-zero,
list-del/bitlista/lastn-length is used by fix-size,
list-del/bitlista/lastn-mklist-01 is used by fill-lastn-04,
list-del/bitlista/lastn-mklist-03 is used by fill-lastn-05, fill-lastn-04,
list-del/bitlista/rest-mklist-03 is used by fill-lastn-03,
list-del/bitlista/restN-zero is used by fill-lastn-03,