[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 split-prefix-append-to, from-to-rest,
nat-basic/add-base is used by from-to-rest,
nat-basic/c is used by split-prefix-append-to, from-to-rest,
nat-basic/f is used by tostream-inj, from-to-rest, emptystream-cancel,
nat-basic/l-02 is used by split-prefix-append-to, from-to-rest,
nat-basic/lf is used by from-to-rest,
nat-basic/lf-01 is used by tostream-inj, from-to-rest,
nat-basic/lf-02 is used by from-to-rest,
nat-basic/ls-02 is used by from-to-rest,
nat-basic/ref is used by tostream-to-same, from-empty, emptystream-cancel,
nat-basic/trans is used by from-to-rest,
nat-basic/zero-01 is used by tobuf-empty, from-empty, buf-empty,

Used from specification nat

nat/eq-01 is used by split-prefix-append-to, from-to-rest,
nat/fle is used by from-to-rest,
nat/le-add is used by from-to-rest,
nat/le-def is used by from-to-rest,
nat/le-ls-simp is used by tobuf-rev,
nat/lels is used by tobuf-rev, from-to-rest, from-empty, emptystream-cancel,
nat/ler is used by from-empty, emptystream-cancel,
nat/ls-01 is used by from-to-rest,
nat/ls-le-simp is used by emptystream-cancel,
nat/zero is used by from-empty,

Used from specification stream

stream/buffer-inf/extensionality is used by tostream-to-same, tostream-inj, tobuf-rev, tobuf-disj, split-prefix-append-to, from-to-rest, from-empty, emptystream-cancel, buf-empty,
stream/buffer-inf/fin-size-from is used by from-to-rest,
stream/buffer-inf/fin-size-from2 is used by from-empty,
stream/buffer-inf/get-append-ls is used by split-prefix-append-to, emptystream-cancel,
stream/buffer-inf/get-from is used by split-prefix-append-to,
stream/buffer-inf/size-to is used by from-to-rest,
stream/buffer-inf/append-assoc is used by split-prefix-append-to, emptystream-cancel,
stream/buffer-inf/append-cancel-r-02 is used by emptystream-cancel,
stream/buffer-inf/fin-empty is used by emptystream-cancel,
stream/buffer-inf/finlen-tolen is used by from-to-rest,
stream/buffer-inf/finp-empty is used by tobuf-empty,
stream/buffer-inf/from-inf is used by from-emptystream,
stream/buffer-inf/get-append-notls is used by split-prefix-append-to, emptystream-cancel,
stream/buffer-inf/get-from-inf is used by from-emptystream,
stream/buffer-inf/get-infto is used by emptystream-cancel,
stream/buffer-inf/get-to is used by tostream-to-same,
stream/buffer-inf/inf-size-from is used by split-prefix-append-to,
stream/buffer-inf/inf-size-to is used by emptystream-cancel,
stream/buffer-inf/notfin-sizeinf is used by tobuf-rev, emptystream-cancel,
stream/buffer-inf/sel-fin is used by emptystream-cancel,
stream/buffer-inf/sel-inf is used by emptystream-cancel, at-emptystream,
stream/buffer-inf/size-append is used by split-prefix-append-to, emptystream-cancel,
stream/buffer-inf/size-empty is used by tobuf-empty, from-empty, buf-empty,
stream/buffer-inf/size-empty-equiv is used by from-to-rest, emptystream-cancel,
stream/buffer-inf/size-inf is used by tobuf-disj, emptystream-cancel,
stream/buffer-inf/size-to is used by tostream-to-same, split-prefix-append-to, from-to-rest, emptystream-cancel,
stream/buffer-inf/to-empty-inf is used by emptystream-cancel,
stream/buffer-inf/to-inf is used by emptystream-cancel,
stream/buffer-inf/to-plus-from-simp is used by split-prefix-append-to,

Used from specification stream-basic

stream-basic/buffer-inf/inj-01 is used by from-emptystream,
stream-basic/buffer-inf/stream-fin-forward is used by from-to-rest,
stream-basic/buffer-inf/stream-inf-forward is used by finp-buf,

Used from specification nat-inf

nat-inf/add-assoc is used by split-prefix-append-to, emptystream-cancel,
nat-inf/add-cancel-02 is used by emptystream-cancel,
nat-inf/add-comm is used by split-prefix-append-to, emptystream-cancel,
nat-inf/add-fin is used by split-prefix-append-to,
nat-inf/add-inf2 is used by emptystream-cancel,
nat-inf/add-less-fin-01 is used by emptystream-cancel,
nat-inf/addeqinf-cancel is used by split-prefix-append-to,
nat-inf/disj is used by tobuf-rev, tobuf-disj, split-prefix-append-to, emptystream-cancel,
nat-inf/elim is used by tobuf-rev, emptystream-cancel,
nat-inf/fin-inject-embed is used by tobuf-rev,
nat-inf/inf-less is used by split-prefix-append-to,
nat-inf/inj is used by tostream-to-same, tostream-inj, from-to-rest, from-empty, emptystream-cancel, buf-empty,
nat-inf/less-fin is used by tostream-to-same, tostream-inj, tobuf-rev, tobuf, from-to-rest, from-empty, emptystream-cancel, buf-empty,
nat-inf/less-inf1 is used by split-prefix-append-to, emptystream-cancel,
nat-inf/less-inf2 is used by split-prefix-append-to, emptystream-cancel,
nat-inf/ls-natinf-to-nat-2-1 is used by split-prefix-append-to,
nat-inf/not-less-zero is used by from-to-rest,
nat-inf/sel is used by tobuf-empty, tobuf, split-prefix-append-to, from-to-rest, from-empty,

Used from specification array

array/buffer/Extension is used by tostream-inj, tobuf-empty, tobuf,
array/buffer/Size-mkarray is used by tobuf-empty, buf-empty,