[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,
nat-basic/c is used by split-prefix-append-to,
nat-basic/f is used by tostream-inj,
nat-basic/l-02 is used by split-prefix-append-to,
nat-basic/lf-01 is used by tostream-inj,
nat-basic/zero-01 is used by toar-empty, ar-empty,

Used from specification nat

nat/eq-01 is used by split-prefix-append-to,

Used from specification stream

stream/datastream/extensionality is used by tostream-inj, toar-disj, split-prefix-append-to, ar-empty,
stream/datastream/get-append-ls is used by split-prefix-append-to,
stream/datastream/get-from is used by split-prefix-append-to,
stream/datastream/append-assoc is used by split-prefix-append-to,
stream/datastream/finp-empty is used by toar-empty,
stream/datastream/from-inf is used by from-emptystream,
stream/datastream/get-append-notls is used by split-prefix-append-to,
stream/datastream/get-from-inf is used by from-emptystream,
stream/datastream/inf-size-from is used by split-prefix-append-to,
stream/datastream/sel-inf is used by at-emptystream,
stream/datastream/size-append is used by split-prefix-append-to,
stream/datastream/size-empty is used by toar-empty, ar-empty,
stream/datastream/size-inf is used by toar-disj,
stream/datastream/size-to is used by split-prefix-append-to,
stream/datastream/to-plus-from-simp is used by split-prefix-append-to,

Used from specification stream-basic

stream-basic/datastream/inj-01 is used by from-emptystream,
stream-basic/datastream/stream-inf-forward is used by finp-ar,

Used from specification nat-inf

nat-inf/add-assoc is used by split-prefix-append-to,
nat-inf/add-comm is used by split-prefix-append-to,
nat-inf/add-fin is used by split-prefix-append-to,
nat-inf/addeqinf-cancel is used by split-prefix-append-to,
nat-inf/disj is used by toar-disj, split-prefix-append-to,
nat-inf/inf-less is used by split-prefix-append-to,
nat-inf/inj is used by tostream-inj, ar-empty,
nat-inf/less-fin is used by tostream-inj, toar, ar-empty,
nat-inf/less-inf1 is used by split-prefix-append-to,
nat-inf/less-inf2 is used by split-prefix-append-to,
nat-inf/ls-natinf-to-nat-2-1 is used by split-prefix-append-to,
nat-inf/sel is used by toar-empty, toar, split-prefix-append-to,

Used from specification array

array/dataarray/Extension is used by tostream-inj, toar-empty, toar,
array/dataarray/Size-mkarray is used by toar-empty, ar-empty,