[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 nat-basic

nat-basic/a is used by mon-lem,
nat-basic/c is used by mon-lem,
nat-basic/a is used by lim-unique, lim-exists, mon-lem,
nat-basic/add-base is used by lim-exists,
nat-basic/c is used by lim-unique, lim-exists, mon-lem,
nat-basic/eq-02 is used by lim-unique,
nat-basic/f is used by lim-unique, lim-exists,
nat-basic/l is used by lim-exists,
nat-basic/l-01 is used by lim-exists,
nat-basic/l-02 is used by lim-unique, lim-exists, mon-lem,
nat-basic/lf is used by lim-exists,
nat-basic/lf-01 is used by lim-exists,
nat-basic/ls-02 is used by lim-unique, lim-exists,
nat-basic/neq-01 is used by lim-unique,
nat-basic/refl-nat is used by lim-unique, lim-exists,
nat-basic/s-04 is used by lim-exists,
nat-basic/succ is used by lim-exists, mon-lem,
nat-basic/trans-nat is used by lim-exists,

Used from specification nat

nat/cancel-01 is used by lim-exists,
nat/elim-sub is used by lim-exists, mon-lem,
nat/eq-01 is used by lim-exists, mon-lem,
nat/fle is used by lim-exists,
nat/fle-01 is used by lim-exists,
nat/le-def is used by lim-unique, lim-exists,
nat/le-ls-simp is used by lim-exists,
nat/lels is used by lim-unique, lim-exists,
nat/lels-02 is used by lim-exists,
nat/lels-03 is used by lim-exists,
nat/lep is used by lim-exists, mon-lem,
nat/lep-02 is used by lim-exists,
nat/ler is used by lim-unique, mon-lem,
nat/les is used by lim-exists,
nat/let is used by lim-exists,
nat/lez-01 is used by lim-exists,
nat/ls-01 is used by lim-exists,
nat/ls-02 is used by lim-exists,
nat/ls-le-simp is used by lim-exists,
nat/prop-07 is used by lim-exists,
nat/zero-02 is used by lim-exists, mon-lem,

Used from specification list-data

list-data/l is used by lim-exists,
list-data/size-nil is used by lim-exists,

Used from specification stream

stream/append-to-ls is used by lim-unique, lim-exists,
stream/extensionality is used by lim-exists,
stream/extensionality-to is used by lim-unique,
stream/get-append-ls is used by lim-exists,
stream/get-append-notls is used by lim-exists,
stream/size-append is used by lim-unique,
stream/append-assoc is used by lim-unique, lim-exists, prefix-trans, mon-lem,
stream/append-cancel-l-02 is used by lim-exists, mon-lem,
stream/append-cut1 is used by lim-exists,
stream/append-empty is used by lim-exists,
stream/append-inf is used by lim-exists,
stream/empty is used by lim-exists,
stream/eq-stream-to-list-2-1 is used by lim-exists,
stream/fin-empty is used by lim-exists,
stream/finlen-tolen is used by lim-unique,
stream/from-fin is used by lim-exists,
stream/from-inf is used by lim-exists,
stream/get-from-01 is used by lim-exists,
stream/get-from-inf is used by lim-exists,
stream/get-infto is used by lim-exists,
stream/get-to is used by lim-exists,
stream/inf-size-to is used by lim-exists,
stream/length-from is used by lim-exists,
stream/notfin-sizeinf is used by lim-exists,
stream/sel-fin is used by lim-exists,
stream/sel-inf is used by lim-exists,
stream/size-append is used by lim-unique, lim-exists,
stream/stream-of-streams/size-empty-equiv is used by lim-exists,
stream/size-fin is used by lim-exists,
stream/size-inf is used by lim-exists,
stream/size-inf-to is used by lim-exists,
stream/size-succ is used by lim-unique,
stream/size-to is used by lim-unique, lim-exists,
stream/to-empty-inf is used by lim-exists,
stream/to-fin is used by lim-exists,
stream/to-inf is used by lim-exists,
stream/to-plus-from-inf-simp is used by lim-exists,
stream/to-plus-from-simp is used by lim-exists,
stream/to-to-eq is used by lim-unique,
stream/to-zero-l is used by lim-exists,

Used from specification list

list/a is used by lim-exists,
list/len is used by lim-exists,

Used from specification stream-basic

stream-basic/inj-rqui is used by lim-exists,
stream-basic/stream-fin-forward is used by lim-exists,
stream-basic/stream-inf-forward is used by lim-exists,
stream-basic/test-finp-rqui is used by lim-exists,
stream-basic/test-finp-rqui0 is used by lim-exists,

Used from specification nat-inf

nat-inf/notinf-fin is used by lim-unique, lim-exists,
nat-inf/add-all-inf is used by lim-unique, lim-exists,
nat-inf/add-assoc is used by lim-unique, lim-exists, mon-lem,
nat-inf/add-cancel-01 is used by lim-unique, lim-exists,
nat-inf/add-cancel-03 is used by lim-unique,
nat-inf/add-comm is used by lim-unique, lim-exists, mon-lem,
nat-inf/add-fin is used by lim-unique, lim-exists, mon-lem,
nat-inf/add-inf1 is used by lim-unique,
nat-inf/add-ls-cancel-01 is used by lim-exists, mon-lem,
nat-inf/add-not-less is used by lim-unique,
nat-inf/addeqinf-cancel is used by lim-exists,
nat-inf/disj-rqui-infty is used by lim-unique, lim-exists,
nat-inf/eq-natinf-to-nat-2-1 is used by lim-exists,
nat-inf/eq-natinf-to-nat-3-1 is used by lim-unique,
nat-inf/inf-inseq-reduce is used by lim-exists,
nat-inf/inf-less is used by lim-exists,
nat-inf/inj-rqui is used by lim-unique, lim-exists,
nat-inf/less-fin is used by lim-unique, lim-exists,
nat-inf/less-inf1 is used by lim-unique, lim-exists,
nat-inf/less-inf2 is used by lim-unique, lim-exists,
nat-inf/ls-lsadd is used by lim-exists,
nat-inf/ls-natinf-to-nat-1-3 is used by lim-exists,
nat-inf/ls-natinf-to-nat-2-1 is used by lim-exists, mon-lem,
nat-inf/lsle-trans is used by mon-lem,
nat-inf/prime-add-fin is used by lim-exists,
nat-inf/sel-rqui-dotn is used by lim-exists,
nat-inf/sum-zero is used by lim-unique,

Used from specification list-del

list-del/extension is used by lim-exists,
list-del/get-append-less is used by lim-exists,
list-del/get-append-grt is used by lim-exists,

Used from specification infinite-append

infinite-append/infinite-append is used by lim-exists,