[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 is used by pmon-pia, pmon-pis,
list-last/prefix-nil is used by pmon-pia,
list-last/prefix-one is used by pmon-pis,
list-last/prefix-one-01 is used by pmon-pis,
list-last/prefix-rec-03 is used by pmon-pia, pmon-pis,

Used from specification nat

nat/add-01 is used by pis-inf-simp, pia-inf-simp,
nat/add-num-01 is used by pmon-pia, pmon-pis, inffrag-lim-size-pis-pia,
nat/add-num-03 is used by proj-exec-inf,
nat/elim-pred-c is used by finfrag-pi-step,
nat/le-add is used by proj-exec-inf,
nat/lels is used by proj-exec-inf, inffrag-lim-size-pis-pia,
nat/lep-02 is used by proj-exec-inf,
nat/one-01 is used by proj-exec-inf,
nat/pred-03 is used by pis-inf-simp, pia-inf-simp,
nat/succ-01 is used by inffrag-lim-size-pis-pia,

Used from specification product

product/lrstep-def is used by inffrag-size-pis-pia, pis-mon, proj-exec-fin, pmon-pia, pmon-pis, finfrag-pi-step, inffrag-pis-init, pia-mon, finfrag-pis-init,
product/product-def is used by pis-mon, pia-mon,
product/lrext-def-left is used by productok-lextempty,
product/lrext-def-right is used by productok-rextempty,
product/lrstart-def is used by proj-exec-fin, proj-exec-inf,
product/product-def is used by inffrag-size-pis-pia, proj-exec, projaction-infrec-skipL, projstate-infrec-addR, proj-exec-fin, proj-exec-inf, projstate-infrec-skipL, projaction-infrec-addR, inffrag-pis-lim-init, inffrag-lim-size-pis-pia, projaction-infrec-addboth, projstate-infrec-addboth, finfrag-pi-step, proj-prefix, inffrag-pis-init,

Used from specification IOtrace-lift

IOtrace-lift/frag-is-lift-fragstar is used by lifted-pia, pcont-pia, pcont-pis,
IOtrace-lift/frag-is-lift-fragstar is used by lifted-pis,

Used from specification remtau

remtau/finremtau-empty-equiv is used by productok-lextempty, productok-rextempty,
remtau/remtau-append is used by proj-prefix,

Used from specification list-getput

list-getput/get-zero-01 is used by proj-exec-fin, finfrag-pi-step,

Used from specification nat-basic

nat-basic/a is used by inffrag-size-pis-pia, pis-mon, proj-exec, lifted-pia, projaction-infrec-skipL, lifted-pis, projstate-infrec-addR, proj-exec-fin, proj-exec-inf, projstate-infrec-skipL, projaction-infrec-addR, pmon-pia, pmon-pis, inffrag-pis-lim-init, inffrag-lim-size-pis-pia, projaction-infrec-addboth, pis-inf-simp, projstate-infrec-addboth, pia-inf-simp, mon-pia, finfrag-pi-step, inffrag-pis-init, pia-mon, finfrag-pis-init, mon-pis,
nat-basic/add-base is used by pmon-pia, pmon-pis, pis-inf-simp, pia-inf-simp,
nat-basic/c is used by inffrag-size-pis-pia, pis-mon, proj-exec, lifted-pia, projaction-infrec-skipL, lifted-pis, projstate-infrec-addR, proj-exec-fin, proj-exec-inf, projstate-infrec-skipL, projaction-infrec-addR, pmon-pia, pmon-pis, inffrag-pis-lim-init, inffrag-lim-size-pis-pia, projaction-infrec-addboth, pis-inf-simp, projstate-infrec-addboth, pia-inf-simp, mon-pia, finfrag-pi-step, inffrag-pis-init, pia-mon, finfrag-pis-init, mon-pis,
nat-basic/eq-01 is used by inffrag-size-pis-pia, pis-mon, projaction-infrec-skipL, projstate-infrec-addR, proj-exec-fin, projstate-infrec-skipL, projaction-infrec-addR, pmon-pia, pmon-pis, inffrag-lim-size-pis-pia, projaction-infrec-addboth, projstate-infrec-addboth, pia-mon,
nat-basic/eq-02 is used by inffrag-lim-size-pis-pia,
nat-basic/f is used by productok-lextempty, productok-rextempty, proj-exec-inf, inffrag-lim-size-pis-pia, finfrag-pi-step,
nat-basic/l is used by proj-exec-inf, pmon-pia, pmon-pis, inffrag-lim-size-pis-pia, finfrag-pi-step,
nat-basic/l-01 is used by proj-exec-inf,
nat-basic/l-02 is used by inffrag-lim-size-pis-pia,
nat-basic/l-06 is used by inffrag-lim-size-pis-pia,
nat-basic/less-zero is used by finfrag-pi-step, finfrag-pis-init,
nat-basic/lf-01 is used by proj-exec-inf, inffrag-lim-size-pis-pia,
nat-basic/lf-02 is used by inffrag-lim-size-pis-pia, finfrag-pi-step,
nat-basic/neq-01 is used by inffrag-lim-size-pis-pia,
nat-basic/nls-fst is used by finfrag-pi-step,
nat-basic/one is used by proj-exec-inf,
nat-basic/one-01 is used by finfrag-pi-step,
nat-basic/one-03 is used by inffrag-lim-size-pis-pia,
nat-basic/one-06 is used by inffrag-lim-size-pis-pia,
nat-basic/oz is used by inffrag-lim-size-pis-pia, pis-inf-simp, pia-inf-simp, finfrag-pi-step,
nat-basic/refl-Nat is used by proj-exec-inf, pmon-pia, pmon-pis, inffrag-lim-size-pis-pia,
nat-basic/s-04 is used by proj-exec-inf, pmon-pia, pmon-pis, inffrag-lim-size-pis-pia,
nat-basic/succ is used by inffrag-size-pis-pia, pis-mon, projaction-infrec-skipL, projstate-infrec-addR, proj-exec-fin, proj-exec-inf, projstate-infrec-skipL, projaction-infrec-addR, pmon-pia, pmon-pis, projaction-infrec-addboth, projstate-infrec-addboth, finfrag-pi-step, inffrag-pis-init, pia-mon,
nat-basic/z-01 is used by proj-exec-fin, proj-exec-inf, pmon-pia, pmon-pis, inffrag-lim-size-pis-pia,
nat-basic/zero is used by finfrag-pi-step,

Used from specification list

list/Nil is used by pmon-pia, pmon-pis,
list/a is used by inffrag-size-pis-pia, pis-mon, projaction-rec-addboth-one, projstate-rec-addR-one, projaction-rec-addR-one, projaction-infrec-skipL, projstate-rec-addboth-one, projstate-infrec-addR, proj-exec-fin, projstate-infrec-skipL, projaction-infrec-addR, pmon-pia, pmon-pis, projaction-infrec-addboth, pis-inf-simp, projstate-infrec-addboth, pia-inf-simp, projstate-rec-skipL-one, projaction-rec-skipL-one, finfrag-pi-step, inffrag-pis-init, pia-mon, finfrag-pis-init,
list/app is used by projaction-rec-addboth-one, projstate-rec-addR-one, projaction-rec-addR-one, projaction-infrec-skipL, projstate-rec-addboth-one, projstate-infrec-addR, proj-exec-fin, projstate-infrec-skipL, projaction-infrec-addR, pmon-pia, pmon-pis, projaction-infrec-addboth, projstate-infrec-addboth, projstate-rec-skipL-one, projaction-rec-skipL-one, finfrag-pi-step, finfrag-pis-init,
list/app-02 is used by proj-exec-fin, pmon-pia, pmon-pis, finfrag-pi-step, finfrag-pis-init,
list/c is used by inffrag-size-pis-pia, pis-mon, projaction-rec-addboth-one, projaction-rec-addR-one, proj-exec-fin, projaction-infrec-addR, pmon-pia, pmon-pis, projaction-infrec-addboth, pis-inf-simp, pia-inf-simp, finfrag-pi-step, inffrag-pis-init, pia-mon, finfrag-pis-init,
list/c-03 is used by pmon-pia, pmon-pis,
list/c-08 is used by proj-exec-fin, pmon-pia, pmon-pis, finfrag-pi-step, finfrag-pis-init,
list/e is used by proj-exec-fin, pmon-pia, pmon-pis, finfrag-pi-step, finfrag-pis-init,
list/first is used by finfrag-pis-init,
list/in-14 is used by finfrag-pi-step, finfrag-pis-init,
list/in-rec is used by finfrag-pi-step, finfrag-pis-init,
list/len is used by pmon-pia, pmon-pis,
list/len-01 is used by projaction-infrec-addR, projaction-infrec-addboth, pis-inf-simp, pia-inf-simp,
list/len-02 is used by inffrag-size-pis-pia, pmon-pis, finfrag-pi-step, finfrag-pis-init,
list/len-05 is used by inffrag-size-pis-pia, proj-exec-fin, pmon-pia, pmon-pis, finfrag-pi-step,
list/map-size is used by productok-lextempty, productok-rextempty,

Used from specification contfun-lim

contfun-lim/liftedtr-def is used by lifted-pia, lifted-pis,
contfun-lim/montrl-relative-def is used by pmon-pia, pmon-pis,
contfun-lim/pconttr-lifted is used by pcont-pia, pcont-pis,
contfun-lim/lifttr-fin is used by lifted-pia, lifted-pis,
contfun-lim/lifttr-inf is used by lifted-pia, lifted-pis,

Used from specification IOtrace

IOtrace/finfrag-rec is used by proj-exec-fin, pmon-pia, pmon-pis,
IOtrace/frag is used by pis-mon, proj-exec-inf, finfrag-pi-step, pia-mon, finfrag-pis-init,
IOtrace/frag-rec is used by inffrag-size-pis-pia, finfrag-pi-step, inffrag-pis-init, finfrag-pis-init,
IOtrace/frag-step-zero is used by pis-mon, pia-mon,
IOtrace/exec is used by proj-exec, proj-exec-inf,
IOtrace/finexec is used by proj-exec, proj-exec-fin,
IOtrace/finfrag-one is used by proj-exec-fin, pmon-pis,
IOtrace/finfrag-onlyone is used by pmon-pia, pmon-pis,
IOtrace/frag-finite-sl is used by proj-exec, lifted-pia, lifted-pis,
IOtrace/frag-inf-sl is used by proj-exec, lifted-pia, lifted-pis,
IOtrace/frag-to-inf is used by proj-exec-inf,
IOtrace/fragfin-size is used by proj-exec, lifted-pia, lifted-pis,
IOtrace/fragfin-size-02 is used by proj-exec-fin, finfrag-pi-step, finfrag-pis-init,
IOtrace/infexec is used by proj-exec, proj-exec-inf,
IOtrace/not-finfrag-empty is used by proj-exec-fin,
IOtrace/not-frag-empty is used by finfrag-pi-step, finfrag-pis-init,

Used from specification stream

stream/extensionality is used by proj-exec-inf, inffrag-lim-size-pis-pia,
stream/get-append-ls is used by proj-exec-inf,
stream/hd-inf is used by inffrag-size-pis-pia, inffrag-pis-init,
stream/hd-selzero is used by finfrag-pi-step,
stream/intrace-expand is used by inffrag-size-pis-pia, inffrag-pis-init,
stream/one-inf is used by pis-inf-simp, pia-inf-simp,
stream/prefix-def is used by proj-exec-inf, inffrag-pis-lim-init, inffrag-lim-size-pis-pia, proj-prefix,
stream/to-succ-nf is used by inffrag-size-pis-pia, pis-mon, pis-inf-simp, pia-inf-simp, inffrag-pis-init, pia-mon,
stream/to-succ2-nf is used by inffrag-size-pis-pia, pis-mon, inffrag-pis-init, pia-mon,
stream/to-succ3-nf is used by pis-mon, pia-mon,
stream/append-assoc is used by pis-mon, projaction-infrec-skipL, projstate-infrec-addR, proj-exec-inf, projstate-infrec-skipL, projaction-infrec-addR, inffrag-pis-lim-init, inffrag-lim-size-pis-pia, projaction-infrec-addboth, projstate-infrec-addboth, finfrag-pi-step, proj-prefix, pia-mon, finfrag-pis-init,
stream/append-finfin is used by pis-mon, projstate-infrec-addR, projaction-infrec-addR, projaction-infrec-addboth, projstate-infrec-addboth, finfrag-pi-step, pia-mon, finfrag-pis-init,
stream/appinf-one-to-succ is used by projaction-infrec-skipL, projstate-infrec-addR, projstate-infrec-skipL, projaction-infrec-addR, projaction-infrec-addboth, projstate-infrec-addboth,
stream/appinf-selfun is used by projaction-infrec-skipL, projstate-infrec-addR, projstate-infrec-skipL, projaction-infrec-addR, projaction-infrec-addboth, projstate-infrec-addboth,
stream/cons-append is used by inffrag-size-pis-pia, projaction-infrec-skipL, projstate-infrec-addR, projstate-infrec-skipL, projaction-infrec-addR, projaction-infrec-addboth, projstate-infrec-addboth, inffrag-pis-init,
stream/empty is used by projaction-infrec-skipL, projaction-infrec-addR, projaction-infrec-addboth, finfrag-pi-step, pia-mon, finfrag-pis-init,
stream/eq-stream-to-list-2-1 is used by projstate-infrec-addR, projaction-infrec-addR, projaction-infrec-addboth, projstate-infrec-addboth,
stream/fin-empty is used by finfrag-pi-step,
stream/fin-finlen-tolen is used by inffrag-lim-size-pis-pia,
stream/fun-nonempty is used by pis-mon, proj-exec-inf, inffrag-pis-lim-init, inffrag-lim-size-pis-pia, proj-prefix, pia-mon,
stream/get-append-notls is used by proj-exec-inf,
stream/get-append2-fin is used by inffrag-lim-size-pis-pia,
stream/get-cons-zero is used by inffrag-pis-lim-init,
stream/get-to is used by proj-exec-inf,
stream/hd-fin-lem is used by finfrag-pis-init,
stream/inf-size-to is used by inffrag-lim-size-pis-pia,
stream/infapp-one-to-succ is used by projaction-infrec-skipL, projstate-infrec-addR, projstate-infrec-skipL, projaction-infrec-addR, projaction-infrec-addboth, projstate-infrec-addboth,
stream/infapp-one-to-succ2 is used by projaction-infrec-skipL, projstate-infrec-addR, projstate-infrec-skipL, projaction-infrec-addR, projaction-infrec-addboth, projstate-infrec-addboth,
stream/leq-append-both is used by pis-mon, projstate-infrec-addR, projaction-infrec-addR, projaction-infrec-addboth, projstate-infrec-addboth, pia-mon,
stream/leq-append-right is used by pis-mon, projstate-infrec-addR, projstate-infrec-addboth, proj-prefix,
stream/leq-empty is used by projaction-infrec-skipL, projaction-infrec-addR, projaction-infrec-addboth, pia-mon,
stream/leq-refl is used by pis-mon, projstate-infrec-skipL, inffrag-lim-size-pis-pia,
stream/leq-symm-2 is used by inffrag-lim-size-pis-pia,
stream/prefix-bothfin-listprefix is used by proj-prefix,
stream/sel-fin is used by proj-exec, proj-exec-inf, inffrag-lim-size-pis-pia, finfrag-pi-step,
stream/sel-inf is used by pis-mon, proj-exec, projaction-infrec-skipL, projstate-infrec-addR, proj-exec-inf, projstate-infrec-skipL, projaction-infrec-addR, inffrag-pis-lim-init, inffrag-lim-size-pis-pia, projaction-infrec-addboth, projstate-infrec-addboth, mon-pia, proj-prefix, pia-mon, mon-pis,
stream/size-append is used by proj-exec-inf, inffrag-pis-lim-init, inffrag-lim-size-pis-pia, finfrag-pi-step, finfrag-pis-init,
stream/size-empty is used by finfrag-pi-step, finfrag-pis-init,
stream/size-fin is used by proj-exec-inf, inffrag-pis-lim-init, inffrag-lim-size-pis-pia, finfrag-pi-step, finfrag-pis-init,
stream/size-inf is used by pis-mon, projaction-infrec-skipL, projstate-infrec-addR, proj-exec-inf, projstate-infrec-skipL, projaction-infrec-addR, inffrag-pis-lim-init, inffrag-lim-size-pis-pia, projaction-infrec-addboth, projstate-infrec-addboth, mon-pia, proj-prefix, pia-mon, mon-pis,
stream/size-inf-to is used by inffrag-size-pis-pia, pis-mon, projaction-infrec-skipL, projstate-infrec-addR, projstate-infrec-skipL, projaction-infrec-addR, projaction-infrec-addboth, projstate-infrec-addboth, inffrag-pis-init, pia-mon,
stream/size-succ is used by proj-exec-inf,
stream/size-to is used by proj-exec-inf,
stream/size-to-02 is used by proj-exec-inf,
stream/to-fin is used by inffrag-lim-size-pis-pia,
stream/to-inf is used by inffrag-lim-size-pis-pia,
stream/to-inf-one is used by inffrag-size-pis-pia, pis-mon, inffrag-pis-lim-init, inffrag-pis-init, pia-mon,
stream/to-inf-two is used by pis-mon,
stream/to-zero-nf is used by inffrag-size-pis-pia, pis-mon, projaction-infrec-skipL, projstate-infrec-addR, projstate-infrec-skipL, projaction-infrec-addR, inffrag-pis-lim-init, projaction-infrec-addboth, projstate-infrec-addboth, inffrag-pis-init, pia-mon,

Used from specification IO-Aut-data

IO-Aut-data/sel-IOAut-dotstart is used by proj-exec, proj-exec-fin, proj-exec-inf,

Used from specification nat-inf

nat-inf/add-assoc is used by pis-mon, projaction-infrec-skipL, projstate-infrec-addR, proj-exec-inf, projstate-infrec-skipL, projaction-infrec-addR, inffrag-lim-size-pis-pia, projaction-infrec-addboth, projstate-infrec-addboth, mon-pia, finfrag-pi-step, pia-mon, finfrag-pis-init, mon-pis,
nat-inf/add-cancel-num-01 is used by finfrag-pi-step, finfrag-pis-init,
nat-inf/add-cancel-num-04 is used by proj-exec-inf,
nat-inf/add-comm is used by pis-mon, projaction-infrec-skipL, projstate-infrec-addR, proj-exec-inf, projstate-infrec-skipL, projaction-infrec-addR, inffrag-lim-size-pis-pia, projaction-infrec-addboth, projstate-infrec-addboth, mon-pia, finfrag-pi-step, pia-mon, finfrag-pis-init, mon-pis,
nat-inf/add-fin is used by proj-exec-inf, inffrag-lim-size-pis-pia,
nat-inf/add-inf2 is used by pis-mon, proj-exec-inf, inffrag-lim-size-pis-pia, pia-mon,
nat-inf/add-not-less is used by proj-exec-inf,
nat-inf/addeqinf-cancel is used by projaction-infrec-skipL, projstate-infrec-addR, projstate-infrec-skipL, projaction-infrec-addR, inffrag-lim-size-pis-pia, projaction-infrec-addboth, projstate-infrec-addboth, mon-pia, mon-pis,
nat-inf/disj-rqui-infty is used by projaction-infrec-skipL, projstate-infrec-addR, proj-exec-inf, projstate-infrec-skipL, projaction-infrec-addR, inffrag-lim-size-pis-pia, projaction-infrec-addboth, projstate-infrec-addboth, mon-pia, mon-pis,
nat-inf/eq-natinf-to-nat-2-1 is used by inffrag-lim-size-pis-pia,
nat-inf/eq-natinf-to-nat-3-1 is used by proj-exec-inf, inffrag-lim-size-pis-pia,
nat-inf/eqls-ls-notls is used by proj-exec-inf,
nat-inf/inf-less is used by projaction-infrec-skipL, projstate-infrec-addR, projstate-infrec-skipL, projaction-infrec-addR, projaction-infrec-addboth, projstate-infrec-addboth, mon-pia, mon-pis,
nat-inf/inj-rqui is used by finfrag-pi-step, finfrag-pis-init,
nat-inf/less-fin is used by proj-exec-inf, inffrag-lim-size-pis-pia, finfrag-pi-step, finfrag-pis-init,
nat-inf/less-inf1 is used by inffrag-lim-size-pis-pia,
nat-inf/less-inf2 is used by pis-mon, proj-exec-inf, inffrag-pis-lim-init, inffrag-lim-size-pis-pia, proj-prefix, pia-mon,
nat-inf/less-succ-leq is used by proj-exec-inf,
nat-inf/ls-natinf-to-nat-2-1 is used by proj-exec-inf,
nat-inf/num-add is used by finfrag-pi-step, finfrag-pis-init,
nat-inf/prime-add-fin is used by proj-exec-inf,
nat-inf/sel-rqui-dotn is used by proj-exec-inf,

Used from specification stream-basic

stream-basic/elim-finp-ant is used by proj-exec, lifted-pia, lifted-pis,
stream-basic/elim-finp-suc is used by proj-exec, lifted-pia, lifted-pis,
stream-basic/inj-rqui is used by projaction-infrec-skipL, projstate-infrec-skipL, inffrag-lim-size-pis-pia, pis-inf-simp, pia-inf-simp,
stream-basic/inj-rqui0 is used by projaction-infrec-skipL, pis-inf-simp, pia-inf-simp,
stream-basic/sel-rqui-dotl is used by proj-exec, lifted-pia, lifted-pis,
stream-basic/sel-rqui0-dotf is used by proj-exec,
stream-basic/test-finp-rqui is used by proj-exec,

Used from specification list-data

list-data/elim-add is used by finfrag-pi-step, finfrag-pis-init,
list-data/elim-list-c is used by proj-exec-fin, pmon-pia, pmon-pis,
list-data/l is used by productok-lextempty, productok-rextempty, proj-exec-fin, pmon-pia, pmon-pis, inffrag-lim-size-pis-pia, finfrag-pi-step, finfrag-pis-init,
list-data/lf-01 is used by pmon-pia, pmon-pis,
list-data/size-nil is used by inffrag-size-pis-pia, projaction-rec-addboth-one, projstate-rec-addR-one, projaction-rec-addR-one, projstate-rec-addboth-one, proj-exec-fin, pmon-pia, pmon-pis, projstate-rec-skipL-one, projaction-rec-skipL-one,

Used from specification list-del

list-del/get-append-grt is used by finfrag-pi-step,
list-del/get-succ is used by finfrag-pi-step,
list-del/get-zero is used by proj-exec-fin, finfrag-pi-step, inffrag-pis-init,
list-del/map-get is used by productok-lextempty, productok-rextempty,
list-del/one-03 is used by inffrag-pis-init,

Used from specification streamseq-mon-lim