[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

nat/eqle-one is used by pfxclosed-fragstar,
nat/l-num-01 is used by frag-is-lift-fragstar,
nat/le-add is used by frag-is-lift-fragstar,
nat/lels is used by pfxclosed-tracestar, pfxclosed-fragstar, frag-is-lift-fragstar,
nat/lep is used by pfxclosed-tracestar, pfxclosed-fragstar,
nat/let is used by frag-is-lift-fragstar,
nat/ls-le-simp is used by frag-is-lift-fragstar,
nat/succ-01 is used by pfxclosed-tracestar, pfxclosed-fragstar,

Used from specification remtau

remtau/finremtau-split-weak is used by pfxclosed-tracestar,
remtau/remtau-split-weak is used by pfxclosed-trace,
remtau/finremtau-def is used by pfxclosed-trace,

Used from specification list-getput

list-getput/get-zero-01 is used by pfxclosed-tracestar,

Used from specification nat-basic

nat-basic/a is used by exec-is-lift-execstar, pfxclosed-tracestar, pfxclosed-execstar, pfxclosed-fragstar, frag-is-lift-fragstar, pfxclosed-trace,
nat-basic/c is used by exec-is-lift-execstar, pfxclosed-tracestar, pfxclosed-execstar, pfxclosed-fragstar, frag-is-lift-fragstar, pfxclosed-trace,
nat-basic/eq-01 is used by pfxclosed-fragstar, frag-is-lift-fragstar,
nat-basic/f is used by pfxclosed-tracestar, pfxclosed-fragstar, frag-is-lift-fragstar,
nat-basic/l is used by frag-is-lift-fragstar,
nat-basic/l-02 is used by pfxclosed-tracestar, pfxclosed-fragstar,
nat-basic/lf-01 is used by pfxclosed-fragstar,
nat-basic/ls-02 is used by frag-is-lift-fragstar,
nat-basic/oz is used by exec-is-lift-execstar, pfxclosed-trace,
nat-basic/refl-Nat is used by frag-is-lift-fragstar,
nat-basic/s-04 is used by pfxclosed-tracestar, pfxclosed-fragstar, frag-is-lift-fragstar,
nat-basic/succ is used by pfxclosed-tracestar, pfxclosed-fragstar, frag-is-lift-fragstar, pfxclosed-trace,
nat-basic/z-01 is used by pfxclosed-execstar,
nat-basic/zero is used by exec-is-lift-execstar, pfxclosed-execstar, pfxclosed-trace,

Used from specification list

list/a is used by pfxclosed-tracestar, pfxclosed-execstar, pfxclosed-fragstar,
list/app-02 is used by pfxclosed-tracestar,
list/c is used by pfxclosed-tracestar,
list/e is used by pfxclosed-tracestar,
list/len is used by pfxclosed-tracestar, pfxclosed-execstar, pfxclosed-fragstar,
list/len-05 is used by pfxclosed-tracestar,

Used from specification contfun-lim

contfun-lim/pdfclosedtrl-def is used by pfxclosed-execstar, pfxclosed-fragstar,
contfun-lim/pfxclosed-def is used by pfxclosed-trace,
contfun-lim/pfxclosed-lift-tr is used by pfxclosed-frag, pfxclosed-exec,
contfun-lim/pfxclosedl-def is used by pfxclosed-tracestar,
contfun-lim/lift-not-trp-fininf is used by exec-is-lift-execstar, frag-is-lift-fragstar,
contfun-lim/lift-not-trp-inffin is used by exec-is-lift-execstar, frag-is-lift-fragstar,
contfun-lim/lift-trp-fin is used by exec-is-lift-execstar, frag-is-lift-fragstar,
contfun-lim/lift-trp-inf is used by exec-is-lift-execstar, frag-is-lift-fragstar,

Used from specification IOtrace

IOtrace/finfrag-split is used by pfxclosed-tracestar, pfxclosed-fragstar,
IOtrace/fintrace is used by pfxclosed-tracestar, pfxclosed-trace,
IOtrace/frag is used by pfxclosed-trace,
IOtrace/frag-split is used by pfxclosed-trace,
IOtrace/fraginf is used by frag-is-lift-fragstar,
IOtrace/fragstar is used by pfxclosed-tracestar, pfxclosed-fragstar, frag-is-lift-fragstar,
IOtrace/trace is used by pfxclosed-trace,
IOtrace/exec is used by exec-is-lift-execstar, pfxclosed-trace,
IOtrace/finexec is used by exec-is-lift-execstar, pfxclosed-tracestar, pfxclosed-execstar, pfxclosed-trace,
IOtrace/frag-finite-sl is used by frag-is-lift-fragstar,
IOtrace/frag-inf-sl is used by frag-is-lift-fragstar,
IOtrace/fragfin-size is used by pfxclosed-execstar,
IOtrace/traceomega is used by pfxclosed-trace,
IOtrace/tracestar-def is used by pfxclosed-trace,

Used from specification stream

stream/prefix-def is used by pfxclosed-trace,
stream/append-assoc is used by pfxclosed-trace,
stream/append-from-size is used by pfxclosed-tracestar, pfxclosed-fragstar,
stream/append-from-size-01 is used by pfxclosed-trace,
stream/append-to-size-01 is used by pfxclosed-trace,
stream/get-infto is used by exec-is-lift-execstar, frag-is-lift-fragstar,
stream/get-to is used by pfxclosed-trace,
stream/not-prefix-inf-fin is used by pfxclosed-trace,
stream/prefix-inf-inf-equal is used by pfxclosed-trace,
stream/sel-fin is used by exec-is-lift-execstar,
stream/sel-inf is used by exec-is-lift-execstar,
stream/size-append is used by pfxclosed-trace,
stream/size-fin is used by pfxclosed-trace,
stream/size-inf-to is used by frag-is-lift-fragstar,
stream/size-succ is used by pfxclosed-trace,
stream/to-succ-cons-l-lem is used by pfxclosed-tracestar,

Used from specification IO-Aut-data

IO-Aut-data/elim-IOAut is used by exec-is-lift-execstar, pfxclosed-execstar, frag-is-lift-fragstar,
IO-Aut-data/sel-IOAut-dotstart is used by exec-is-lift-execstar, pfxclosed-tracestar, pfxclosed-trace,
IO-Aut-data/sel-IOAut-dotstep is used by pfxclosed-tracestar, pfxclosed-fragstar, frag-is-lift-fragstar,

Used from specification nat-inf

nat-inf/add-assoc is used by pfxclosed-trace,
nat-inf/add-comm is used by pfxclosed-trace,
nat-inf/add-fin is used by pfxclosed-trace,
nat-inf/add-not-less is used by pfxclosed-trace,
nat-inf/less-succ-leq is used by pfxclosed-trace,

Used from specification stream-basic

stream-basic/inj-rqui is used by pfxclosed-trace,
stream-basic/sel-rqui-dotl is used by frag-is-lift-fragstar,
stream-basic/sel-rqui0-dotf is used by frag-is-lift-fragstar,
stream-basic/test-finp-rqui is used by frag-is-lift-fragstar,
stream-basic/test-finp-rqui0 is used by frag-is-lift-fragstar,

Used from specification list-data

list-data/elim-add is used by pfxclosed-tracestar,
list-data/l is used by pfxclosed-tracestar, pfxclosed-execstar,
list-data/size-nil is used by pfxclosed-execstar,

Used from specification list-del

list-del/get-append-less is used by pfxclosed-execstar,
list-del/elim-firstn-restn is used by pfxclosed-tracestar,
list-del/firstN-len is used by pfxclosed-tracestar, pfxclosed-fragstar,
list-del/get-append-grt is used by pfxclosed-execstar,
list-del/get-zero is used by pfxclosed-tracestar,

Used from specification list-last

list-last/prefix is used by pfxclosed-tracestar, pfxclosed-execstar, pfxclosed-fragstar,