[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 list

list/references/Cons is used by mkjavavalues-append,
list/bytelist/Last is used by mkjavavalues-byte-lastrec,
list/javavalues/firsteq is used by nonnullrefs-dups-firstoc,
list/javavalues/Last is used by mkjavavalues-byte-lastrec-01, mkjavavalues-byte-lastrec,
list/javavalues/Nil is used by nonnullrefs-in-firstoc, nonnullrefs-dups-firstoc, nonnullrefs-append, mkjavavalues-byte-lastrec-01, mkjavavalues-byte-lastrec, mkjavavalues-append-01, mkjavavalues-append, intvalues-append,
list/bytelist/Nil is used by mkjavavalues-byte-lastrec-01, mkjavavalues-byte-lastrec, mkjavavalues-append-01,
list/intlista/Nil is used by intvalues-append,
list/references/Nil is used by nonnullrefs-append, mkjavavalues-append,
list/bytelist/a is used by vals-at, mkvalues-last, mkvalues-butlast, mkvals-single, mkjavavalues-restn, mkjavavalues-byte-lastrec-01, mkjavavalues-byte-lastrec, mkjavavalues-append-01, mkjavavalues, mkjava-len, mkjava-empty, mkjava-bvs, is_bytes-vals, ints2bytes-one, ints2bytes-len, ints2bytes-empty-01, ints2bytes-butlast, ints2bytes-at, ibbis, bytevalues-one, bytevalues-len, bytevalues-eq, bytevalues-empty-01, bytevals-inj, bytevals-at, bytes2ints-one,
list/references/a is used by nonnullrefs-one, nonnullrefs-ok, nonnullrefs-null, nonnullrefs-in-firstoc, nonnullrefs-in, nonnullrefs-dups-firstoc, nonnullrefs-dups, nonnullrefs-append, mkvalsr-one, mkvalsr-len, mkvalsr-at, mkjavavalues-rec, mkjavavalues-empty, mkjavavalues-append, javavalues-in,
list/intlista/a is used by vals2ints-len, vals2ints-empty-01, vals2int-one, posints-rec-02, posints-rec-01, posints-one, intvalues-put-sw, intvalues-one, intvalues-mklist, intvalues-len, intvalues-empty-01, intvalues-at, intvalues-append, ints2bytes-one, ints2bytes-len, ints2bytes-empty-01, ints2bytes-butlast, ints2bytes-at, ibbis, bytes2ints-one,
list/javavalues/a is used by vals2val-single, vals2ints-len, vals2ints-empty-01, vals2int-one, vals-at, val-inj-01, nonnullrefs-one-no, nonnullrefs-one, nonnullrefs-null, nonnullrefs-in-firstoc, nonnullrefs-in, nonnullrefs-dups-firstoc, nonnullrefs-dups, nonnullrefs-append, mkvalues-last, mkvalues-butlast, mkvalsr-one, mkvalsr-len, mkvalsr-at, mkvals-single, mkjavavalues-restn, mkjavavalues-rec, mkjavavalues-empty, mkjavavalues-byte-lastrec-01, mkjavavalues-byte-lastrec, mkjavavalues-append-01, mkjavavalues-append, mkjavavalues, mkjava-len, mkjava-empty, mkjava-bvs, javavalues-in, isbytelist-all, is_bytes-vals, is_bytelist-one, is_bytelist, intvalues-put-sw, intvalues-one, intvalues-mklist, intvalues-len, intvalues-empty-01, intvalues-at, intvalues-append, bytevalues-one, bytevalues-len, bytevalues-eq, bytevalues-empty-01, bytevals-inj, bytevals-at,
list/bytelist/app is used by mkvalues-last, mkvalues-butlast, mkvals-single, ints2bytes-one, ints2bytes-butlast, bytevalues-one, bytes2ints-one,
list/intlista/app is used by vals2int-one, posints-one, intvalues-one, ints2bytes-one, ints2bytes-butlast, bytes2ints-one,
list/javavalues/app is used by vals2val-single, vals2int-one, nonnullrefs-one-no, mkvalues-last, mkvalues-butlast, mkvalsr-one, mkvals-single, is_bytelist-one, intvalues-one, bytevalues-one,
list/references/app is used by mkvalsr-one,
list/references/app-01 is used by nonnullrefs-ok, nonnullrefs-append,
list/javavalues/app-01 is used by val-inj-01, nonnullrefs-in-firstoc, nonnullrefs-dups-firstoc, mkvalues-butlast, mkjavavalues-restn, mkjavavalues-rec, mkjavavalues-byte-lastrec-01, mkjavavalues-byte-lastrec, mkjavavalues-append-01, mkjavavalues-append, bytevalues-eq, bytevals-inj,
list/bytelist/app-01 is used by mkjava-bvs, ints2bytes-butlast, ibbis,
list/intlista/app-01 is used by intvalues-put-sw, intvalues-append,
list/javavalues/app-02-ant is used by nonnullrefs-in, nonnullrefs-dups-firstoc, nonnullrefs-dups, mkjavavalues-empty, mkjava-empty, intvalues-put-sw,
list/bytelist/app-02-ant is used by ints2bytes-empty-01, bytevalues-eq, bytevalues-empty-01,
list/intlista/app-02-ant is used by vals2ints-empty-01, intvalues-empty-01, intvalues-at,
list/references/app-03 is used by nonnullrefs-one,
list/intlista/app-03 is used by intvalues-mklist,
list/bytelist/c is used by vals-at, mkvalues-last, mkvalues-butlast, mkjavavalues-restn, mkjavavalues-byte-lastrec-01, mkjavavalues-byte-lastrec, mkjavavalues-append-01, mkjavavalues, mkjava-len, mkjava-empty, mkjava-bvs, is_bytes-vals, ibbis, bytevalues-one, bytevalues-len, bytevalues-eq, bytevalues-empty-01, bytevals-inj, bytevals-at,
list/references/c is used by nonnullrefs-one, nonnullrefs-ok, nonnullrefs-in, nonnullrefs-dups-firstoc, nonnullrefs-dups, nonnullrefs-append, mkvalsr-len, mkvalsr-at, mkjavavalues-rec, mkjavavalues-empty, mkjavavalues-append, javavalues-in,
list/javavalues/c is used by vals2ints-len, vals2ints-empty-01, val-inj-01, nonnullrefs-null, nonnullrefs-in-firstoc, nonnullrefs-in, nonnullrefs-dups-firstoc, nonnullrefs-dups, nonnullrefs-append, mkjavavalues-rec, isbytelist-all, intvalues-put-sw, intvalues-len, intvalues-empty-01, intvalues-at, intvalues-append, bytevalues-len, bytevalues-eq, bytevalues-empty-01, bytevals-inj, bytevals-at,
list/intlista/c is used by vals2ints-len, vals2ints-empty-01, vals2int-one, intvalues-put-sw, intvalues-one, intvalues-len, intvalues-empty-01, intvalues-at, intvalues-append, ints2bytes-len, ints2bytes-empty-01, ints2bytes-butlast, ints2bytes-at,
list/references/c-04 is used by nonnullrefs-one-yes,
list/javavalues/c-04 is used by mkjavavalues-byte-lastrec-01, mkjavavalues-byte-lastrec,
list/javavalues/c-06 is used by nonnullrefs-dups-firstoc,
list/bytelist/c-06 is used by bytevalues-eq,
list/bytelist/c-07 is used by mkjavavalues-restn,
list/intlista/c-07 is used by intvalues-at,
list/javavalues/c-07 is used by nonnullrefs-in, nonnullrefs-dups, intvalues-put-sw,
list/javavalues/c-08 is used by intvalues-put-sw,
list/bytelist/e is used by ints2bytes-empty-01, bytevalues-eq, bytevalues-empty-01,
list/javavalues/e is used by nonnullrefs-in, nonnullrefs-dups-firstoc, nonnullrefs-dups, mkjavavalues-empty, mkjava-empty, intvalues-put-sw,
list/intlista/e is used by vals2ints-empty-01, intvalues-empty-01, intvalues-at,
list/javavalues/e-01 is used by nonnullrefs-in, nonnullrefs-dups-firstoc, nonnullrefs-dups, intvalues-put-sw, bytevalues-eq,
list/intlista/e-01 is used by intvalues-at, ints2bytes-butlast, ints2bytes-at,
list/bytelist/e-01 is used by vals-at, mkvalues-last, mkvalues-butlast,
list/references/e-01 is used by mkjavavalues-rec,
list/javavalues/in-01 is used by nonnullrefs-dups-firstoc,
list/javavalues/in-06 is used by nonnullrefs-dups-firstoc, bytevalues-eq,
list/references/in-06 is used by nonnullrefs-in-firstoc, nonnullrefs-dups-firstoc, javavalues-in,
list/javavalues/in-08 is used by nonnullrefs-dups-firstoc,
list/javavalues/in-10 is used by nonnullrefs-in-firstoc, nonnullrefs-dups-firstoc,
list/bytelist/in-14 is used by bytevalues-eq,
list/javavalues/in-14 is used by nonnullrefs-dups-firstoc,
list/references/in-17 is used by nonnullrefs-null, nonnullrefs-in-firstoc, nonnullrefs-in,
list/bytelist/in-17 is used by bytevalues-eq,
list/javavalues/in-17 is used by nonnullrefs-dups-firstoc, mkjavavalues, javavalues-in, isbytelist-all,
list/references/in-append is used by nonnullrefs-null, nonnullrefs-in-firstoc, nonnullrefs-in, nonnullrefs-dups-firstoc,
list/bytelist/in-append is used by bytevalues-eq,
list/javavalues/in-append is used by nonnullrefs-dups-firstoc, mkjavavalues, javavalues-in, isbytelist-all,
list/references/in-empty is used by nonnullrefs-null, nonnullrefs-in-firstoc, nonnullrefs-in, javavalues-in,
list/javavalues/in-empty is used by nonnullrefs-in-firstoc, nonnullrefs-dups-firstoc, mkjavavalues, javavalues-in, isbytelist-all,
list/javavalues/len is used by vals2ints-len, nonnullrefs-in, nonnullrefs-dups, mkvalsr-len, mkjava-len, intvalues-put-sw, intvalues-len, intvalues-at, bytevalues-len, bytevals-at,
list/references/len is used by mkvalsr-len, mkvalsr-at,
list/bytelist/len is used by vals-at, mkjavavalues-restn, mkjava-len, ints2bytes-len, bytevalues-len,
list/intlista/len is used by vals2ints-len, intvalues-len, ints2bytes-len, ints2bytes-at,
list/javavalues/len-02 is used by vals2ints-len, nonnullrefs-in, nonnullrefs-dups, mkvalsr-len, mkjava-len, intvalues-put-sw, intvalues-len, intvalues-at, bytevalues-len, bytevals-at,
list/references/len-02 is used by mkvalsr-len, mkvalsr-at,
list/bytelist/len-02 is used by vals-at, mkjavavalues-restn, mkjava-len, ints2bytes-len, bytevalues-len,
list/intlista/len-02 is used by vals2ints-len, intvalues-len, ints2bytes-len, ints2bytes-at,

Used from specification int-abs

int-abs/lels-01 is used by posints-rec-01, posints-one,
int-abs/lels-04 is used by posints-one,
int-abs/zero-gels-04 is used by posints-rec-02,

Used from specification byte

byte/ibi is used by ibbis,

Used from specification nat-basic1

nat-basic1/f is used by vals-at, nonnullrefs-in, nonnullrefs-dups, mkvalsr-at, intvalues-put-sw, intvalues-at, ints2bytes-at, bytevals-at,
nat-basic1/less-1 is used by nonnullrefs-in, nonnullrefs-dups, mkvalsr-at, intvalues-put-sw, intvalues-at, bytevals-at,
nat-basic1/ref-1 is used by vals-at,
nat-basic1/z is used by mkjavavalues-restn,

Used from specification int-basic1

int-basic1/ls-01 is used by posints-rec-01,

Used from specification javavalue

javavalue/byteval is used by mkjavavalues-byte-lastrec, bytevalues-eq, bytevals-inj,
javavalue/elim-03 is used by mkjavavalues-byte-lastrec-01, mkjavavalues-byte-lastrec, bytevalues-eq,
javavalue/elim-13 is used by nonnullrefs-one-yes, nonnullrefs-in-firstoc, nonnullrefs-in, nonnullrefs-dups-firstoc, nonnullrefs-dups, nonnullrefs-append,
javavalue/elim-refval is used by javavalues-in,
javavalue/inj-03 is used by nonnullrefs-in-firstoc, nonnullrefs-in, nonnullrefs-dups-firstoc, nonnullrefs-dups, mkvalsr-at, javavalues-in,
javavalue/inj-07 is used by vals-at, mkvalues-last,
javavalue/sel-04 is used by intvalues-mklist,
javavalue/sel-08 is used by mkjavavalues-byte-lastrec, mkjava-bvs,
javavalue/sel-09 is used by nonnullrefs-one, nonnullrefs-ok, nonnullrefs-in-firstoc, nonnullrefs-in, nonnullrefs-dups-firstoc, nonnullrefs-dups, javavalues-in,
javavalue/test-19 is used by nonnullrefs-one, nonnullrefs-ok, nonnullrefs-in-firstoc, nonnullrefs-in, nonnullrefs-dups-firstoc, nonnullrefs-dups, nonnullrefs-append, javavalues-in,
javavalue/test-36 is used by mkjavavalues-byte-lastrec-01, mkjavavalues-byte-lastrec, mkjavavalues, is_bytelist, bytevalues-eq,

Used from specification list-dup

list-dup/references/e-01 is used by nonnullrefs-dups-firstoc, nonnullrefs-dups,
list-dup/references/f-01 is used by nonnullrefs-dups-firstoc,
list-dup/references/rec is used by nonnullrefs-dups-firstoc, nonnullrefs-dups,

Used from specification list-data

list-data/javavalues/elim-list-c is used by nonnullrefs-dups-firstoc, bytevalues-eq,
list-data/references/elim-list-c is used by mkjavavalues-rec,
list-data/bytelist/l is used by vals-at,
list-data/javavalues/l is used by nonnullrefs-in, nonnullrefs-dups, intvalues-put-sw, intvalues-at, bytevals-at,
list-data/intlista/l is used by ints2bytes-at,
list-data/references/l is used by mkvalsr-at,
list-data/references/size-01 is used by mkvalsr-len, mkvalsr-at,
list-data/javavalues/size-01 is used by vals2ints-len, nonnullrefs-in, nonnullrefs-dups, mkvalsr-len, mkjava-len, intvalues-put-sw, intvalues-len, intvalues-at, bytevalues-len, bytevals-at,
list-data/intlista/size-01 is used by vals2ints-len, intvalues-len, ints2bytes-len,
list-data/bytelist/size-01 is used by mkjavavalues-restn, mkjava-len, ints2bytes-len, bytevalues-len,

Used from specification list-del

list-del/bytelist/get-numrec is used by vals-at, ints2bytes-at, bytevals-at,
list-del/javavalues/get-numrec is used by nonnullrefs-dups,
list-del/references/get-numrec is used by mkvalsr-at,
list-del/javavalues/get-rec is used by nonnullrefs-in, nonnullrefs-dups,
list-del/intlista/get-rec is used by intvalues-at,
list-del/javavalues/put-rec-01 is used by intvalues-put-sw,
list-del/bytelist/rest-rec is used by mkjavavalues-restn,
list-del/javavalues/get-succ is used by vals-at, nonnullrefs-in, nonnullrefs-dups, mkvalsr-at, intvalues-at, bytevals-at,
list-del/intlista/get-succ is used by ints2bytes-at,
list-del/references/get-zero-01 is used by mkvalsr-at,
list-del/bytelist/get-zero-01 is used by vals-at, ints2bytes-at, bytevals-at,
list-del/javavalues/get-zero-01 is used by vals-at, nonnullrefs-in, nonnullrefs-dups, mkvalsr-at, intvalues-at, bytevals-at,
list-del/intlista/get-zero-01 is used by intvalues-at, ints2bytes-at,
list-del/intlista/put-succ is used by intvalues-put-sw,
list-del/intlista/put-zero is used by intvalues-put-sw,
list-del/javavalues/put-zero is used by intvalues-put-sw,
list-del/bytelist/restN-zero is used by mkjavavalues-restn,
list-del/javavalues/restN-zero is used by mkjavavalues-restn,
list-del/javavalues/weak-restN-rec is used by mkjavavalues-restn,

Used from specification nat

nat/elim-pred-c is used by vals-at, nonnullrefs-in, nonnullrefs-dups, mkvalsr-at, mkjavavalues-restn, intvalues-put-sw, intvalues-at, ints2bytes-at, bytevals-at,
nat/fle is used by vals-at,
nat/fle-01 is used by vals-at,
nat/le-ls-simp is used by mkjavavalues-restn,
nat/lels is used by vals-at, nonnullrefs-in, nonnullrefs-dups, mkvalsr-at, intvalues-put-sw, intvalues-at, ints2bytes-at, bytevals-at,
nat/lels-01 is used by nonnullrefs-in, nonnullrefs-dups, mkjavavalues-restn,
nat/lep-02 is used by mkjavavalues-restn,
nat/lez is used by vals-at, nonnullrefs-in, nonnullrefs-dups,
nat/lez-01 is used by mkjavavalues-restn,
nat/ls-le-simp is used by nonnullrefs-in, nonnullrefs-dups, mkvalsr-at, intvalues-put-sw, intvalues-at, ints2bytes-at, bytevals-at,
nat/pred-03 is used by vals-at, nonnullrefs-dups, mkvalsr-at, mkjavavalues-restn, intvalues-put-sw, ints2bytes-at, bytevals-at,
nat/succ-01 is used by vals-at, nonnullrefs-in, nonnullrefs-dups, mkvalsr-at, intvalues-put-sw, intvalues-at, ints2bytes-at, bytevals-at,

Used from specification list-last

list-last/bytelist/bc is used by ints2bytes-butlast,
list-last/javavalues/bc is used by mkvalues-butlast,
list-last/javavalues/l-02 is used by mkvalues-last,
list-last/javavalues/b is used by mkvalues-butlast,
list-last/intlista/b is used by ints2bytes-butlast,
list-last/bytelist/b is used by mkvalues-butlast, ints2bytes-butlast,
list-last/intlista/bapp is used by ints2bytes-butlast,
list-last/bytelist/bapp is used by mkvalues-butlast,
list-last/javavalues/l is used by mkvalues-last,
list-last/bytelist/l is used by mkvalues-last,
list-last/bytelist/l-02 is used by mkvalues-last,
list-last/intlista/mk-plus is used by intvalues-mklist,
list-last/javavalues/mk-plus is used by intvalues-mklist,
list-last/intlista/mk-zero is used by intvalues-mklist,
list-last/javavalues/mk-zero is used by intvalues-mklist,
list-last/intlista/mklist-one is used by intvalues-mklist,
list-last/javavalues/mklist-one is used by intvalues-mklist,

Used from specification nat-basic2

nat-basic2/a is used by vals2ints-len, vals-at, nonnullrefs-in, nonnullrefs-dups, mkvalsr-len, mkvalsr-at, mkjavavalues-restn, mkjava-len, intvalues-put-sw, intvalues-mklist, intvalues-len, intvalues-at, ints2bytes-len, ints2bytes-at, bytevalues-len, bytevals-at,
nat-basic2/c is used by vals2ints-len, vals-at, nonnullrefs-in, nonnullrefs-dups, mkvalsr-len, mkvalsr-at, mkjavavalues-restn, mkjava-len, intvalues-put-sw, intvalues-mklist, intvalues-len, intvalues-at, ints2bytes-len, ints2bytes-at, bytevalues-len, bytevals-at,
nat-basic2/eq-01 is used by vals2ints-len, nonnullrefs-dups, mkvalsr-len, mkjava-len, intvalues-len, ints2bytes-len, bytevalues-len,
nat-basic2/oz is used by vals-at, nonnullrefs-in, nonnullrefs-dups, mkvalsr-at, mkjavavalues-restn, intvalues-put-sw, intvalues-at, ints2bytes-at, bytevals-at,
nat-basic2/s is used by vals-at, nonnullrefs-in, nonnullrefs-dups, mkvalsr-at, intvalues-put-sw, intvalues-at, ints2bytes-at, bytevals-at,
nat-basic2/succ is used by intvalues-mklist,