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

list-last/prefix-app-06 is used by repla-mon, repls-mon,
list-last/prefix-rec-03 is used by repla-mon, repls-mon,

Used from specification nat

nat/add-01 is used by replstate-inf, finfrag-repl-frag,
nat/add-num-01 is used by repl-fin-size, finfrag-repl-frag,
nat/add-num-03 is used by repl-frag,
nat/cancel-01 is used by repl-frag,
nat/elim-pred-c is used by repl-frag, repl-size, lift-get, repla-mon, frag-repls-head, finfrag-repls-head, mon-repla-1, repls-infrec-addS, repls-mon, repla-infrec-addS,
nat/elim-sub is used by finfrag-repl-frag,
nat/eq is used by finfrag-repl-frag,
nat/eq-01 is used by finfrag-repl-frag,
nat/eqle-one is used by frag-repla-sametrace, finfrag-repl-frag,
nat/fle is used by finfrag-repl-frag,
nat/le-add is used by repl-frag,
nat/le-def is used by repls-infrec-addS, repla-infrec-addS,
nat/lels is used by repl-frag, lift-get, finfrag-repl-frag,
nat/lep is used by repls-infrec-addS, repla-infrec-addS, finfrag-repl-frag,
nat/lep-02 is used by repl-frag, finfrag-repl-frag,
nat/ler is used by finfrag-repl-frag,
nat/les is used by finfrag-repl-frag,
nat/let is used by finfrag-repl-frag,
nat/lez is used by finfrag-repl-frag,
nat/lez-01 is used by lift-get,
nat/ls-le-simp is used by frag-repla-sametrace, finfrag-repl-frag,
nat/not-zero is used by repls-infrec-addS, repla-infrec-addS,
nat/one-01 is used by repl-frag,
nat/pred-03 is used by replstate-inf,
nat/succ-01 is used by lift-get, finfrag-repl-frag,
nat/zero is used by frag-repla-sametrace, finfrag-repl-frag,

Used from specification funops

funops/cod-def is used by repla-infrec-addboth, product-ok-refine-cext-imp-aext, repls-infrec-addboth, finfrag-repl-frag,
funops/f-in-cod is used by repla-infrec-addboth, product-ok-refine-cext-imp-aext, repls-infrec-addboth, finfrag-repl-frag,
funops/notcod is used by sameshared-notcodc-notcoda, nounsharedextR-notcodren-internal, repla-infrec-addboth, repls-infrec-addboth, finfrag-repl-frag,

Used from specification project-right

project-right/mon-pia is used by repl-frag, repl-size,
project-right/proj-exec is used by refines-product,
project-right/projaction-fin-def is used by repl-frag, repl-size, frag-repls-head, frag-repla-sametrace, repl-fin-size,
project-right/projaction-inf-def is used by repl-frag, repl-size,
project-right/projaction-infrec-addR is used by repla-infrec-skip, repla-mon, frag-repls-head, repls-mon, repls-infrec-skip,
project-right/projaction-infrec-addboth is used by repla-mon, frag-repls-head, repla-infrec-addboth, repls-mon, repls-infrec-addboth,
project-right/projaction-infrec-skipL is used by repla-mon, repls-infrec-addS, repls-mon, repla-infrec-addS,
project-right/productok-rextempty is used by finfrag-repla-sametrace,
project-right/proj-prefix is used by repl-frag, frag-repla-sametrace,
project-right/projaction-base is used by finfrag-repls-head, finfrag-repl-frag,
project-right/projaction-rec-addR is used by finfrag-repla-sametrace, finfrag-repls-head, repl-fin-size, finfrag-repl-frag,
project-right/projaction-rec-addboth is used by finfrag-repla-sametrace, finfrag-repls-head, repl-fin-size, finfrag-repl-frag,
project-right/projaction-rec-skipL is used by finfrag-repla-sametrace, finfrag-repls-head, repl-fin-size, finfrag-repl-frag,

Used from specification product

product/lrstep-def is used by repla-infrec-skip, finfrag-repla-sametrace, repla-mon, frag-repls-head, repla-infrec-addboth, finfrag-repls-head, repls-mon, repls-infrec-skip, repls-infrec-addboth, repl-fin-size, finfrag-repl-frag,
product/productok-def is used by product-ok-refine-cext-imp-aext, finfrag-repl-frag,
product/sharingok-def is used by product-ok-refine-cext-imp-aext, finfrag-repl-frag,
product/lrext-def-left is used by same-concrete-abstract,
product/lrext-def-right is used by finfrag-repla-sametrace, nounsharedextR-notcodren-project,
product/lrstart-def is used by repl-exec,
product/product-def is used by repl-frag, repl-size, repl-exec, refines-product, finfrag-repl-frag,
product/productok-injlren is used by finfrag-repl-frag,
product/productok-injrren is used by repla-infrec-skip, repla-infrec-addboth, repls-infrec-skip, repls-infrec-addboth, finfrag-repl-frag,
product/productok-sharedl-not-tau is used by repla-infrec-addboth, product-ok-refine-cext-imp-aext, repls-infrec-addboth, finfrag-repl-frag,
product/productok-sharedr-not-tau is used by repla-infrec-addboth, repls-infrec-addboth, finfrag-repl-frag,

Used from specification remtau

remtau/finremtau-empty-equiv is used by finfrag-repl-frag,
remtau/finremtau-one is used by finfrag-repla-sametrace, same-concrete-abstract, nounsharedextR-notcodren-project, finfrag-repl-frag,
remtau/remtau-append is used by frag-repla-sametrace,
remtau/remtau-split-one is used by finfrag-repla-sametrace, repla-mon, frag-repls-head, finfrag-repls-head, frag-repla-sametrace, repls-mon, repl-fin-size, finfrag-repl-frag,
remtau/remtau_of_to-to_of_rmtau is used by frag-repla-sametrace,
remtau/addopt is used by repla-infrec-skip, repla-mon, frag-repls-head, repla-infrec-addboth, frag-repla-sametrace, repls-mon, repls-infrec-skip, repls-infrec-addboth,
remtau/finremtau-append is used by finfrag-repla-sametrace, finfrag-repls-head, repls-mon, repl-fin-size, finfrag-repl-frag,
remtau/finremtau-def is used by repl-frag, repl-size, finfrag-repla-sametrace, repla-mon, frag-repls-head, repla-infrec-addboth, finfrag-repls-head, frag-repla-sametrace, repls-mon, repls-infrec-addboth, repl-fin-size, finfrag-repl-frag,
remtau/finremtau-empty is used by finfrag-repla-sametrace, finfrag-repls-head, repls-mon, finfrag-repl-frag,
remtau/finremtau-nontau-lem is used by finfrag-repla-sametrace, finfrag-repls-head, repl-fin-size, finfrag-repl-frag,
remtau/one-eq-empty is used by nounsharedextR-notcodren, repls-mon, finfrag-repl-frag,
remtau/remtau-append is used by repl-frag, repl-size, repla-infrec-addboth, frag-repla-sametrace, repls-infrec-addboth,
remtau/remtau-cons is used by repla-infrec-skip, repla-mon, frag-repls-head, repla-infrec-addboth, frag-repla-sametrace, repls-mon, repls-infrec-skip, repls-infrec-addboth,
remtau/remtau-nontau-lem is used by repla-mon, frag-repls-head, repls-mon,

Used from specification list-getput

list-getput/extension is used by frag-repla-sametrace,
list-getput/get-zero-01 is used by finfrag-repl-frag,

Used from specification nat-basic

nat-basic/a is used by repl-frag, repl-size, repla-infrec-skip, finfrag-repla-sametrace, lift-get, repla-mon, replaction-inf, frag-repls-head, repla-infrec-addboth, finfrag-repls-head, replstate-inf, mon-repla-1, repls-infrec-addS, frag-repla-sametrace, lift-size, repls-mon, repls-infrec-skip, repls-infrec-addboth, repl-fin-size, repla-infrec-addS, finfrag-repl-frag,
nat-basic/add-base is used by finfrag-repla-sametrace, repla-mon, frag-repls-head, repla-infrec-addboth, finfrag-repls-head, replstate-inf, repls-mon, repls-infrec-addboth, repl-fin-size, finfrag-repl-frag,
nat-basic/c is used by repl-frag, repl-size, repla-infrec-skip, finfrag-repla-sametrace, lift-get, repla-mon, replaction-inf, frag-repls-head, repla-infrec-addboth, finfrag-repls-head, replstate-inf, mon-repla-1, repls-infrec-addS, frag-repla-sametrace, lift-size, repls-mon, repls-infrec-skip, repls-infrec-addboth, repl-fin-size, repla-infrec-addS, finfrag-repl-frag,
nat-basic/eq-01 is used by repl-frag, repl-size, finfrag-repla-sametrace, frag-repls-head, finfrag-repls-head, lift-size, repl-fin-size, finfrag-repl-frag,
nat-basic/f is used by repl-frag, lift-get, frag-repla-sametrace, finfrag-repl-frag,
nat-basic/l is used by repl-frag, finfrag-repl-frag,
nat-basic/l-01 is used by repl-frag,
nat-basic/l-02 is used by repl-frag, finfrag-repl-frag,
nat-basic/lf is used by frag-repla-sametrace, finfrag-repl-frag,
nat-basic/lf-01 is used by repl-frag, frag-repla-sametrace, finfrag-repl-frag,
nat-basic/lf-02 is used by finfrag-repl-frag,
nat-basic/one is used by repl-frag,
nat-basic/one-01 is used by repl-frag, repl-size, lift-get, repla-mon, frag-repls-head, finfrag-repls-head, mon-repla-1, repls-infrec-addS, repls-mon, repla-infrec-addS,
nat-basic/oz is used by lift-get, replstate-inf, repls-infrec-addS, repla-infrec-addS, finfrag-repl-frag,
nat-basic/refl-Nat is used by repl-frag, frag-repla-sametrace, finfrag-repl-frag,
nat-basic/s-04 is used by repl-frag, lift-get, frag-repla-sametrace, finfrag-repl-frag,
nat-basic/succ is used by repl-frag, finfrag-repla-sametrace, lift-get, repla-mon, frag-repls-head, repla-infrec-addboth, finfrag-repls-head, lift-size, repls-mon, repls-infrec-addboth, repl-fin-size, finfrag-repl-frag,
nat-basic/trans-Nat is used by frag-repla-sametrace, finfrag-repl-frag,
nat-basic/z-01 is used by repl-frag, finfrag-repla-sametrace, finfrag-repls-head, repl-fin-size, finfrag-repl-frag,

Used from specification list

list/Nil is used by finfrag-repla-sametrace, finfrag-repls-head, repl-fin-size,
list/a is used by repla-infrec-skip, finfrag-repla-sametrace, lift-get, repla-mon, frag-repls-head, repla-infrec-addboth, finfrag-repls-head, replstate-inf, repls-infrec-addS, frag-repla-sametrace, lift-size, repls-mon, repls-infrec-skip, repls-infrec-addboth, repl-fin-size, finfrag-repla-sametrace-1, repla-infrec-addS, finfrag-repl-frag,
list/app is used by finfrag-repla-sametrace, lift-get, repla-mon, frag-repls-head, finfrag-repls-head, repls-infrec-addS, frag-repla-sametrace, repls-mon, repl-fin-size, repla-infrec-addS, finfrag-repl-frag,
list/app-02 is used by lift-get, frag-repls-head, finfrag-repls-head, frag-repla-sametrace, repls-mon, finfrag-repla-sametrace-1, finfrag-repl-frag,
list/app-04 is used by frag-repla-sametrace,
list/c is used by repl-frag, repl-size, repla-infrec-skip, finfrag-repla-sametrace, lift-get, repla-mon, mon-repls, replaction-inf, frag-repls-head, mon-repla, repla-infrec-addboth, finfrag-repls-head, replstate-inf, mon-repla-1, repls-infrec-addS, lift-size, repls-mon, repls-infrec-skip, repls-infrec-addboth, repl-fin-size, finfrag-repla-sametrace-1, repla-infrec-addS, finfrag-repl-frag,
list/c-03 is used by finfrag-repls-head, finfrag-repl-frag,
list/c-04 is used by finfrag-repla-sametrace,
list/c-06 is used by finfrag-repls-head,
list/c-08 is used by finfrag-repla-sametrace, finfrag-repls-head, repl-fin-size, finfrag-repl-frag,
list/e is used by lift-get, frag-repls-head, finfrag-repls-head, frag-repla-sametrace, finfrag-repla-sametrace-1, finfrag-repl-frag,
list/first is used by finfrag-repls-head,
list/first-02 is used by finfrag-repls-head,
list/in-14 is used by frag-repls-head, finfrag-repls-head, frag-repla-sametrace, repls-mon, finfrag-repl-frag,
list/in-15 is used by finfrag-repls-head, repls-mon,
list/in-17 is used by finfrag-repls-head,
list/in-append is used by finfrag-repls-head,
list/in-rec is used by frag-repls-head, finfrag-repls-head, frag-repla-sametrace, finfrag-repl-frag,
list/len is used by repl-fin-size, finfrag-repl-frag,
list/len-01 is used by replstate-inf,
list/len-02 is used by repl-frag, repl-size, finfrag-repla-sametrace, lift-get, repla-mon, frag-repls-head, repla-infrec-addboth, finfrag-repls-head, mon-repla-1, repls-infrec-addS, frag-repla-sametrace, repls-mon, repls-infrec-addboth, repl-fin-size, repla-infrec-addS, finfrag-repl-frag,
list/len-05 is used by finfrag-repla-sametrace, lift-get, frag-repls-head, finfrag-repls-head, lift-size, repls-mon, repl-fin-size, finfrag-repl-frag,
list/len-06 is used by finfrag-repla-sametrace,
list/map-size is used by repl-fin-size, finfrag-repl-frag,

Used from specification IOtrace

IOtrace/finfrag-rec is used by finfrag-repla-sametrace, finfrag-repls-head, repl-fin-size, finfrag-repl-frag,
IOtrace/frag is used by repl-frag, finfrag-repla-sametrace, repla-mon, repla-infrec-addboth, repls-mon, repls-infrec-addboth, repl-fin-size, finfrag-repl-frag,
IOtrace/frag-from-1 is used by finfrag-repla-sametrace, repla-mon, repla-infrec-addboth, repls-mon, repls-infrec-addboth, repl-fin-size, finfrag-repl-frag,
IOtrace/frag-step is used by finfrag-repl-frag,
IOtrace/fragstar is used by repl-frag, finfrag-repl-frag,
IOtrace/inffrag-rec is used by repla-infrec-skip, repla-infrec-addboth, repls-infrec-skip, repls-infrec-addboth,
IOtrace/inffrag-rec1 is used by repla-mon, frag-repls-head, repls-mon,
IOtrace/trace is used by refines-product,
IOtrace/exec is used by repl-exec, refines-product,
IOtrace/finfrag-one is used by finfrag-repl-frag,
IOtrace/frag-finite-al is used by frag-repls-head, finfrag-repls-head, finfrag-repl-frag,
IOtrace/frag-finite-sl is used by repl-size, frag-repla-sametrace,
IOtrace/frag-inf-al is used by frag-repls-head,
IOtrace/frag-inf-sl is used by repl-size, frag-repla-sametrace,
IOtrace/frag-onestate is used by finfrag-repls-head,
IOtrace/frag-to-inf is used by repl-frag, repl-size, frag-repla-sametrace,
IOtrace/fragfin-size is used by repl-frag, repl-size, frag-repla-sametrace, repl-fin-size,
IOtrace/fragfin-size-02 is used by finfrag-repla-sametrace, frag-repls-head, finfrag-repls-head, finfrag-repl-frag,
IOtrace/fragomega-def is used by repl-frag, frag-repla-sametrace,
IOtrace/fragstar-def is used by repl-frag,
IOtrace/not-finfrag-empty is used by repl-fin-size, finfrag-repla-sametrace-1, finfrag-repl-frag,
IOtrace/not-frag-empty is used by repl-frag, repl-size, repla-infrec-addboth, repls-infrec-addboth, repl-fin-size, repl-exec, finfrag-repla-sametrace-1, refines-product,
IOtrace/not-frag-fin-inf is used by repl-frag,
IOtrace/not-frag-inf-fin is used by repl-frag,

Used from specification stream

stream/add-list-fun-def is used by repl-frag, repl-size, repla-mon, frag-repls-head, mon-repla-1, repls-mon,
stream/append-finfin is used by frag-repls-head,
stream/append-fininf is used by frag-repls-head,
stream/append-le-to is used by frag-repla-sametrace,
stream/cons-to-num is used by frag-repls-head,
stream/elim-hd-tl is used by repl-fin-size,
stream/extensionality is used by repl-frag,
stream/extensionality-to is used by frag-repla-sametrace,
stream/from-succ is used by finfrag-repla-sametrace, repla-mon, repla-infrec-addboth, repls-mon, repls-infrec-addboth, finfrag-repl-frag,
stream/get-append-ls is used by repl-frag, finfrag-repl-frag,
stream/get-append-notls is used by finfrag-repls-head, finfrag-repl-frag,
stream/infapp-to-ge is used by repls-infrec-addS, repla-infrec-addS,
stream/intrace-expand is used by repl-frag, repl-size, repla-mon, frag-repls-head, mon-repla-1, repls-mon,
stream/one-inf is used by replstate-inf,
stream/prefix-def is used by repl-frag, repl-size, finfrag-repla-sametrace, repla-mon, frag-repls-head, finfrag-repls-head, frag-repla-sametrace, repls-mon, repl-fin-size, finfrag-repl-frag,
stream/size-append is used by frag-repla-sametrace,
stream/size-to is used by repl-fin-size,
stream/to-plus-from-inf is used by frag-repla-sametrace,
stream/to-succ-nf is used by repl-frag, repl-size, repla-mon, replstate-inf, mon-repla-1, repls-mon,
stream/to-succ2-nf is used by repl-frag, repl-size, repla-mon, mon-repla-1, repls-mon,
stream/append-assoc is used by repl-frag, repl-size, repla-infrec-skip, finfrag-repla-sametrace, repla-mon, replaction-inf, frag-repls-head, repla-infrec-addboth, finfrag-repls-head, repls-infrec-addS, frag-repla-sametrace, repls-mon, repls-infrec-skip, repls-infrec-addboth, repl-fin-size, repl-exec, finfrag-repla-sametrace-1, repla-infrec-addS, refines-product, finfrag-repl-frag,
stream/append-empty is used by finfrag-repls-head, repla-infrec-addS,
stream/append-empty-01 is used by frag-repls-head,
stream/append-finfin is used by finfrag-repla-sametrace, repla-mon, frag-repls-head, repla-infrec-addboth, finfrag-repls-head, repls-infrec-addS, frag-repla-sametrace, repls-mon, repls-infrec-addboth, repl-fin-size, repla-infrec-addS, finfrag-repl-frag,
stream/append-from-addsize-01 is used by finfrag-repla-sametrace, repla-mon, repla-infrec-addboth, repls-mon, repls-infrec-addboth, repl-fin-size, finfrag-repl-frag,
stream/append-gr-to is used by frag-repla-sametrace,
stream/append-split-fin is used by frag-repls-head, repla-infrec-addboth, frag-repla-sametrace, repls-infrec-addboth, repl-fin-size,
stream/append-to-addsize-01 is used by frag-repla-sametrace,
stream/append-two-is-fin is used by frag-repla-sametrace,
stream/appendend-equal is used by frag-repla-sametrace,
stream/appfin-sel is used by frag-repls-head, finfrag-repls-head, frag-repla-sametrace, finfrag-repl-frag,
stream/appfin-sel-01 is used by finfrag-repls-head, frag-repla-sametrace,
stream/appinf-one-to-succ is used by replaction-inf,
stream/appinf-one2-to-succ is used by repla-infrec-skip, repla-infrec-addboth, repls-infrec-addS, repls-infrec-skip, repls-infrec-addboth, repla-infrec-addS,
stream/appinf-sel is used by repla-infrec-skip, frag-repls-head, repla-infrec-addboth, repls-infrec-addS, repls-infrec-skip, repls-infrec-addboth, repla-infrec-addS,
stream/appinf-selfun is used by replaction-inf,
stream/appinf-selfun-01 is used by repla-infrec-skip, repla-infrec-addboth, repls-infrec-addS, repls-infrec-skip, repls-infrec-addboth, repla-infrec-addS,
stream/cons-append is used by repl-frag, repl-size, repla-infrec-skip, finfrag-repla-sametrace, repla-mon, mon-repls, frag-repls-head, mon-repla, repla-infrec-addboth, mon-repla-1, repls-infrec-addS, frag-repla-sametrace, repls-mon, repls-infrec-skip, repls-infrec-addboth, repl-fin-size, repl-exec, finfrag-repla-sametrace-1, repla-infrec-addS, refines-product, finfrag-repl-frag,
stream/cons-empty is used by repl-frag, repl-size, frag-repls-head, repla-infrec-addboth, frag-repla-sametrace, repls-infrec-addboth, repl-fin-size, repl-exec, finfrag-repla-sametrace-1, refines-product,
stream/cons-eq is used by frag-repls-head,
stream/cons-from-addnum is used by finfrag-repla-sametrace, repla-mon, frag-repls-head, repla-infrec-addboth, finfrag-repls-head, repls-mon, repls-infrec-addboth, repl-fin-size, finfrag-repl-frag,
stream/cons-to-addnum is used by finfrag-repls-head, repls-mon, finfrag-repl-frag,
stream/elim-hd-tl is used by repl-frag, repl-size, frag-repls-head, repla-infrec-addboth, frag-repla-sametrace, repls-infrec-addboth, repl-fin-size, repl-exec, finfrag-repla-sametrace-1, refines-product,
stream/empty is used by repla-mon, frag-repls-head, repla-infrec-addboth, finfrag-repls-head, frag-repla-sametrace, repls-mon, repls-infrec-addboth, repla-infrec-addS, finfrag-repl-frag,
stream/empty-append is used by repla-infrec-skip, repla-mon, frag-repls-head, repla-infrec-addboth, frag-repla-sametrace, repls-mon, repls-infrec-skip, repls-infrec-addboth, finfrag-repl-frag,
stream/eq-stream-to-list-2-1 is used by frag-repls-head, frag-repla-sametrace, finfrag-repl-frag,
stream/eq-stream-to-list-3-1 is used by repla-infrec-addboth, finfrag-repls-head, repls-infrec-addboth,
stream/fin-empty is used by finfrag-repla-sametrace, repla-mon, frag-repls-head, repla-infrec-addboth, finfrag-repls-head, frag-repla-sametrace, repls-mon, repls-infrec-addboth, repl-fin-size, finfrag-repl-frag,
stream/fin-finlen-tolen is used by frag-repla-sametrace,
stream/from-cons-one is used by finfrag-repla-sametrace, repla-mon, repla-infrec-addboth, repls-mon, repls-infrec-addboth, repl-fin-size, finfrag-repl-frag,
stream/from-zero is used by frag-repls-head, repls-mon,
stream/fun-nonempty is used by repl-frag, repl-size, frag-repls-head, frag-repla-sametrace,
stream/get-append-ls is used by finfrag-repls-head, finfrag-repl-frag,
stream/get-append-notls is used by repl-frag, finfrag-repl-frag,
stream/get-cons-succ is used by finfrag-repla-sametrace, repla-mon, repls-mon, repl-fin-size, finfrag-repl-frag,
stream/get-cons-zero is used by frag-repls-head, repls-mon, repl-exec, refines-product, finfrag-repl-frag,
stream/get-to is used by repl-frag, frag-repla-sametrace, finfrag-repl-frag,
stream/hd-fin-lem is used by frag-repls-head,
stream/hd-lem is used by frag-repls-head,
stream/infapp-embed is used by repla-infrec-skip, frag-repls-head, repla-infrec-addboth, repls-infrec-addS, repls-mon, repls-infrec-skip, repls-infrec-addboth, repla-infrec-addS,
stream/infapp-one-to-succ is used by repla-infrec-skip, repla-infrec-addboth, repls-infrec-addS, repls-infrec-skip, repls-infrec-addboth, repla-infrec-addS,
stream/infappone-zero is used by repla-infrec-skip, frag-repls-head, repla-infrec-addboth, repls-infrec-skip, repls-infrec-addboth,
stream/leq-append-both is used by repla-mon, repla-infrec-addboth, repls-infrec-addS, repls-mon, repls-infrec-addboth, repla-infrec-addS,
stream/leq-append-right is used by repls-infrec-addS, repls-mon,
stream/leq-empty is used by repla-mon, finfrag-repls-head, repla-infrec-addS, finfrag-repl-frag,
stream/leq-refl is used by repl-frag, frag-repla-sametrace, repls-mon, repl-exec,
stream/neq-fin-inf-01 is used by frag-repls-head, frag-repla-sametrace,
stream/neq-fin-inf-03 is used by frag-repls-head, finfrag-repls-head, finfrag-repl-frag,
stream/prefix-bothfin-listprefix is used by repla-mon, repls-mon,
stream/sel-fin is used by repl-frag, finfrag-repls-head, finfrag-repl-frag,
stream/sel-inf is used by repl-frag, repl-size, mon-repls, frag-repls-head, mon-repla, repla-infrec-addboth, mon-repla-1, repls-infrec-addS, frag-repla-sametrace, repls-infrec-addboth, repla-infrec-addS,
stream/size-append is used by repl-frag, repl-size, finfrag-repla-sametrace, repla-mon, repla-infrec-addboth, frag-repla-sametrace, repls-mon, repls-infrec-addboth, repl-fin-size, finfrag-repl-frag,
stream/size-empty-equiv is used by frag-repla-sametrace, finfrag-repl-frag,
stream/size-fin is used by repl-frag, repl-size, finfrag-repla-sametrace, repla-mon, repla-infrec-addboth, finfrag-repls-head, frag-repla-sametrace, repls-mon, repls-infrec-addboth, repl-fin-size, finfrag-repl-frag,
stream/size-inf is used by repl-frag, repl-size, mon-repls, frag-repls-head, mon-repla, repla-infrec-addboth, mon-repla-1, repls-infrec-addS, frag-repla-sametrace, repls-infrec-addboth, repla-infrec-addS,
stream/size-inf-to is used by repl-frag, repl-size,
stream/size-succ is used by repl-frag, frag-repla-sametrace, finfrag-repl-frag,
stream/size-to is used by repl-frag, frag-repla-sametrace, finfrag-repl-frag,
stream/size-to-02 is used by repl-frag,
stream/to-fin is used by frag-repla-sametrace,
stream/to-inf is used by frag-repla-sametrace,
stream/to-inf-one is used by repla-mon, repls-mon,
stream/to-to-eq is used by frag-repla-sametrace,
stream/to-zero is used by frag-repls-head, finfrag-repls-head, frag-repla-sametrace, repls-mon, finfrag-repl-frag,
stream/to-zero-nf is used by repla-mon, frag-repls-head, repls-infrec-addS, repls-mon, repla-infrec-addS,
stream/toone-cons is used by frag-repla-sametrace,

Used from specification IO-Aut-data

IO-Aut-data/sel-IOAut-dotstart is used by repl-exec, refines-product,
IO-Aut-data/sel-IOAut-dotstep is used by repl-frag, finfrag-repl-frag,

Used from specification nat-inf

nat-inf/lele-refl is used by frag-repla-sametrace,
nat-inf/add-all-zero is used by repl-size, finfrag-repla-sametrace, repla-mon, repla-infrec-addboth, frag-repla-sametrace, repls-mon, repls-infrec-addboth, repl-fin-size, finfrag-repl-frag,
nat-inf/add-assoc is used by repl-frag, repl-size, finfrag-repla-sametrace, repla-mon, mon-repls, mon-repla, repla-infrec-addboth, mon-repla-1, repls-infrec-addS, frag-repla-sametrace, repls-mon, repls-infrec-addboth, repl-fin-size, repla-infrec-addS, finfrag-repl-frag,
nat-inf/add-cancel-03 is used by frag-repla-sametrace,
nat-inf/add-cancel-num-02 is used by repl-frag,
nat-inf/add-cancel-num-03 is used by repl-size,
nat-inf/add-cancel-num-04 is used by repl-frag, finfrag-repla-sametrace, repla-mon, repls-mon, repl-fin-size, finfrag-repl-frag,
nat-inf/add-comm is used by repl-frag, repl-size, finfrag-repla-sametrace, repla-mon, mon-repls, mon-repla, repla-infrec-addboth, mon-repla-1, repls-infrec-addS, frag-repla-sametrace, repls-mon, repls-infrec-addboth, repl-fin-size, repla-infrec-addS, finfrag-repl-frag,
nat-inf/add-fin is used by repl-frag, repl-size, finfrag-repla-sametrace, repla-mon, repla-infrec-addboth, frag-repla-sametrace, repls-mon, repls-infrec-addboth, repl-fin-size, finfrag-repl-frag,
nat-inf/add-inf2 is used by repl-frag, frag-repla-sametrace,
nat-inf/add-less-fin-01 is used by repl-frag, frag-repla-sametrace,
nat-inf/add-ls-cancel-01 is used by frag-repla-sametrace,
nat-inf/add-ls-cancel-num-04 is used by repl-frag, finfrag-repla-sametrace, repla-mon, repla-infrec-addboth, frag-repla-sametrace, repls-mon, repls-infrec-addboth, repl-fin-size, finfrag-repl-frag,
nat-inf/add-not-less is used by repl-frag, finfrag-repla-sametrace, repla-mon, repla-infrec-addboth, frag-repla-sametrace, repls-mon, repls-infrec-addboth, repl-fin-size, finfrag-repl-frag,
nat-inf/addeqinf-cancel is used by repl-frag, repl-size, mon-repls, mon-repla, repla-infrec-addboth, mon-repla-1, repls-infrec-addS, repls-infrec-addboth, repla-infrec-addS,
nat-inf/disj-rqui-infty is used by repl-frag, repl-size, mon-repls, mon-repla, repla-infrec-addboth, mon-repla-1, repls-infrec-addS, frag-repla-sametrace, repls-infrec-addboth, repla-infrec-addS,
nat-inf/eq-natinf-to-nat-2-1 is used by repl-size, frag-repla-sametrace,
nat-inf/eq-natinf-to-nat-3-1 is used by repl-frag,
nat-inf/inf-less is used by repl-frag, repl-size, mon-repls, mon-repla, repla-infrec-addboth, mon-repla-1, repls-infrec-addS, repls-infrec-addboth, repla-infrec-addS,
nat-inf/inj-rqui is used by repl-size,
nat-inf/less-fin is used by repl-frag, finfrag-repls-head, frag-repla-sametrace, finfrag-repl-frag,
nat-inf/less-inf1 is used by frag-repla-sametrace,
nat-inf/less-inf2 is used by repl-frag, repl-size, frag-repls-head, frag-repla-sametrace,
nat-inf/less-succ-leq is used by repl-frag, finfrag-repla-sametrace, repla-mon, repla-infrec-addboth, repls-mon, repls-infrec-addboth, repl-fin-size, finfrag-repl-frag,
nat-inf/ls-le is used by frag-repla-sametrace,
nat-inf/ls-lsadd is used by finfrag-repl-frag,
nat-inf/ls-natinf-to-nat-2-1 is used by repl-frag, finfrag-repl-frag,
nat-inf/ls-trans is used by finfrag-repl-frag,
nat-inf/lsle-trans is used by finfrag-repl-frag,
nat-inf/num-add is used by finfrag-repla-sametrace, repla-mon, repla-infrec-addboth, repls-mon, repls-infrec-addboth, repl-fin-size, finfrag-repl-frag,
nat-inf/onels-neqzero is used by finfrag-repl-frag,
nat-inf/prime-add-fin is used by repl-frag,
nat-inf/sel-rqui-dotn is used by repl-frag, finfrag-repls-head, finfrag-repl-frag,
nat-inf/sum-zero-fin is used by frag-repla-sametrace,

Used from specification stream-basic

stream-basic/disj-rqui-rqui0 is used by frag-repls-head, finfrag-repls-head, finfrag-repl-frag,
stream-basic/elim-finp-ant is used by repl-size, frag-repls-head, finfrag-repls-head, frag-repla-sametrace, finfrag-repl-frag,
stream-basic/elim-finp-suc is used by repl-size, frag-repls-head, finfrag-repls-head, frag-repla-sametrace, finfrag-repl-frag,
stream-basic/inj-rqui is used by replstate-inf, frag-repla-sametrace,
stream-basic/inj-rqui0 is used by frag-repls-head,
stream-basic/sel-rqui-dotl is used by repl-size, frag-repla-sametrace,
stream-basic/sel-rqui0-dotf is used by repl-size, frag-repla-sametrace,
stream-basic/test-finp-rqui is used by frag-repla-sametrace,

Used from specification list-data

list-data/elim-add is used by frag-repls-head, finfrag-repl-frag,
list-data/elim-list-c is used by finfrag-repls-head, finfrag-repla-sametrace-1,
list-data/l is used by finfrag-repla-sametrace, lift-get, frag-repls-head, finfrag-repls-head, frag-repla-sametrace, repl-fin-size, finfrag-repl-frag,
list-data/lf-01 is used by finfrag-repl-frag,
list-data/size-nil is used by finfrag-repla-sametrace, lift-get, frag-repls-head, finfrag-repls-head, lift-size, repls-mon, repl-fin-size, finfrag-repl-frag,

Used from specification option

option/oinj-feq1 is used by product-ok-refine-cext-imp-aext,
option/disj-Some-None is used by repla-mon, product-ok-refine-cext-imp-aext, frag-repla-sametrace, repls-mon,
option/elim-Some is used by finfrag-repla-sametrace, repla-mon, frag-repls-head, finfrag-repls-head, repls-mon, repl-fin-size, finfrag-repl-frag,
option/sel-Some-dotget is used by frag-repla-sametrace,

Used from specification list-del

list-del/get-append-grt is used by lift-get, finfrag-repl-frag,
list-del/get-append-less is used by finfrag-repl-frag,
list-del/get-append-less is used by lift-get,
list-del/get-succ is used by lift-get, finfrag-repl-frag,
list-del/get-zero is used by lift-get, finfrag-repl-frag,
list-del/list-select-not-first is used by finfrag-repl-frag,
list-del/map-get is used by finfrag-repl-frag,
list-del/one-03 is used by repl-frag, repl-size, lift-get, repla-mon, frag-repls-head, finfrag-repls-head, mon-repla-1, repls-mon, finfrag-repl-frag,

Used from specification IOrefine-def

IOrefine-def/leq-def is used by refines-product,

Used from specification IO-Automaton

IO-Automaton/isIOAut-def is used by repl-exec, refines-product,

Used from specification streamseq-mon-lim

streamseq-mon-lim/lim-def is used by repl-frag, repl-size, frag-repls-head, frag-repla-sametrace,
streamseq-mon-lim/lim-extractprefix is used by repla-infrec-addboth, repls-infrec-addS, repls-infrec-addboth, repla-infrec-addS,
streamseq-mon-lim/lim-postfix is used by repla-infrec-skip, repla-infrec-addboth, repls-infrec-addS, repls-infrec-skip, repls-infrec-addboth, repla-infrec-addS,
streamseq-mon-lim/mon-def is used by repl-frag, repl-size, mon-repls, mon-repla, repla-infrec-addboth, mon-repla-1, repls-infrec-addS, repls-infrec-addboth, repla-infrec-addS,
streamseq-mon-lim/two-mon-size is used by repl-size,