[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/l-02 is used by startfin-weakfin-bwinv-is-leqrefine,
list-last/last-01 is used by startfin-weakfin-bwinv-is-leqrefine,
list-last/last-def is used by startfin-weakfin-bwinv-is-leqrefine,
list-last/last-one is used by startfin-weakfin-bwinv-is-leqrefine,

Used from specification nat

nat/add-num-03 is used by startfin-weakfin-bwinv-is-leqrefine,
nat/anti is used by startfin-weakfin-bwinv-is-leqrefine,
nat/elim-pred-c is used by startfin-weakfin-bwinv-is-leqrefine,
nat/fle-01 is used by startfin-weakfin-bwinv-is-leqrefine,
nat/l-num-01 is used by startfin-weakfin-bwinv-is-leqrefine,
nat/le-ls-simp is used by startfin-weakfin-bwinv-is-leqrefine,
nat/lels is used by startfin-weakfin-bwinv-is-leqrefine,
nat/lels-03 is used by startfin-weakfin-bwinv-is-leqrefine,
nat/ler is used by startfin-weakfin-bwinv-is-leqrefine,
nat/zero is used by startfin-weakfin-bwinv-is-leqrefine,

Used from specification infgraph-gen-basic

infgraph-gen-basic/edge-def is used by startfin-weakfin-bwinv-is-leqrefine,
infgraph-gen-basic/dom-def is used by startfin-weakfin-bwinv-is-leqrefine,

Used from specification set-basic

set-basic/In-empty is used by startfin-weakfin-bwinv-is-leqrefine,
set-basic/In-insert is used by startfin-weakfin-bwinv-is-leqrefine,
set-basic/ne-01 is used by startfin-weakfin-bwinv-is-leqrefine,
set-basic/size-zero-01 is used by startfin-weakfin-bwinv-is-leqrefine,

Used from specification list-getput

list-getput/get-zero-01 is used by startfin-weakfin-bwinv-is-leqrefine,

Used from specification nat-basic

nat-basic/a is used by startfin-weakfin-bwinv-is-leqrefine,
nat-basic/c is used by startfin-weakfin-bwinv-is-leqrefine,
nat-basic/eq-01 is used by startfin-weakfin-bwinv-is-leqrefine,
nat-basic/f is used by startfin-weakfin-bwinv-is-leqrefine,
nat-basic/l-02 is used by startfin-weakfin-bwinv-is-leqrefine,
nat-basic/less-zero is used by startfin-weakfin-bwinv-is-leqrefine,
nat-basic/lf-01 is used by startfin-weakfin-bwinv-is-leqrefine,
nat-basic/lf-02 is used by startfin-weakfin-bwinv-is-leqrefine,
nat-basic/ls-02 is used by startfin-weakfin-bwinv-is-leqrefine,
nat-basic/nls-fst is used by startfin-weakfin-bwinv-is-leqrefine,
nat-basic/one-01 is used by startfin-weakfin-bwinv-is-leqrefine,
nat-basic/oz is used by startfin-weakfin-bwinv-is-leqrefine,
nat-basic/refl-Nat is used by startfin-weakfin-bwinv-is-leqrefine,
nat-basic/s-04 is used by startfin-weakfin-bwinv-is-leqrefine,
nat-basic/succ is used by startfin-weakfin-bwinv-is-leqrefine,
nat-basic/zero is used by startfin-weakfin-bwinv-is-leqrefine,

Used from specification list

list/Last is used by startfin-weakfin-bwinv-is-leqrefine,
list/a is used by startfin-weakfin-bwinv-is-leqrefine,
list/app is used by startfin-weakfin-bwinv-is-leqrefine,
list/app-02 is used by startfin-weakfin-bwinv-is-leqrefine,
list/c is used by startfin-weakfin-bwinv-is-leqrefine,
list/c-03 is used by startfin-weakfin-bwinv-is-leqrefine,
list/c-08 is used by startfin-weakfin-bwinv-is-leqrefine,
list/e is used by startfin-weakfin-bwinv-is-leqrefine,
list/first is used by startfin-weakfin-bwinv-is-leqrefine,
list/len-02 is used by startfin-weakfin-bwinv-is-leqrefine,

Used from specification IOtrace

IOtrace/finfrag-rec is used by startfin-weakfin-bwinv-is-leqrefine,
IOtrace/frag-to is used by startfin-weakfin-bwinv-is-leqrefine,
IOtrace/fraginf is used by startfin-weakfin-bwinv-is-leqrefine,
IOtrace/infappend-moves-gen is used by startfin-weakfin-bwinv-is-leqrefine,
IOtrace/inftrace is used by startfin-weakfin-bwinv-is-leqrefine,
IOtrace/finexec is used by startfin-weakfin-bwinv-is-leqrefine,
IOtrace/finfrag-onlyone is used by startfin-weakfin-bwinv-is-leqrefine,
IOtrace/frag-step-inf-inf is used by startfin-weakfin-bwinv-is-leqrefine,
IOtrace/frag-to-inf is used by startfin-weakfin-bwinv-is-leqrefine,
IOtrace/fragomega-def is used by startfin-weakfin-bwinv-is-leqrefine,
IOtrace/infexec is used by startfin-weakfin-bwinv-is-leqrefine,
IOtrace/not-finfrag-empty is used by startfin-weakfin-bwinv-is-leqrefine,
IOtrace/traceomega is used by startfin-weakfin-bwinv-is-leqrefine,
IOtrace/tracestar-def is used by startfin-weakfin-bwinv-is-leqrefine,

Used from specification stream

stream/to-succ2-nf is used by startfin-weakfin-bwinv-is-leqrefine,
stream/to-unwind-end-inf is used by startfin-weakfin-bwinv-is-leqrefine,
stream/append-assoc is used by startfin-weakfin-bwinv-is-leqrefine,
stream/append-finfin is used by startfin-weakfin-bwinv-is-leqrefine,
stream/get-append2-fin is used by startfin-weakfin-bwinv-is-leqrefine,
stream/get-append3-fin is used by startfin-weakfin-bwinv-is-leqrefine,
stream/get-cons-succ is used by startfin-weakfin-bwinv-is-leqrefine,
stream/get-infto is used by startfin-weakfin-bwinv-is-leqrefine,
stream/hd-fin-lem is used by startfin-weakfin-bwinv-is-leqrefine,
stream/sel-fin is used by startfin-weakfin-bwinv-is-leqrefine,
stream/sel-inf is used by startfin-weakfin-bwinv-is-leqrefine,
stream/size-append is used by startfin-weakfin-bwinv-is-leqrefine,
stream/size-fin is used by startfin-weakfin-bwinv-is-leqrefine,
stream/size-inf is used by startfin-weakfin-bwinv-is-leqrefine,
stream/to-inf is used by startfin-weakfin-bwinv-is-leqrefine,

Used from specification IO-Aut-data

IO-Aut-data/sel-IOAut-dotstart is used by startfin-weakfin-bwinv-is-leqrefine,
IO-Aut-data/sel-IOAut-dotstep is used by startfin-weakfin-bwinv-is-leqrefine,

Used from specification nat-inf

nat-inf/add-all-zero is used by startfin-weakfin-bwinv-is-leqrefine,
nat-inf/add-assoc is used by startfin-weakfin-bwinv-is-leqrefine,
nat-inf/add-comm is used by startfin-weakfin-bwinv-is-leqrefine,
nat-inf/add-fin is used by startfin-weakfin-bwinv-is-leqrefine,
nat-inf/add-ls-cancel-num-03 is used by startfin-weakfin-bwinv-is-leqrefine,
nat-inf/add-ls-cancel-num-04 is used by startfin-weakfin-bwinv-is-leqrefine,
nat-inf/addeqinf-cancel is used by startfin-weakfin-bwinv-is-leqrefine,
nat-inf/disj-rqui-infty is used by startfin-weakfin-bwinv-is-leqrefine,
nat-inf/inf-less is used by startfin-weakfin-bwinv-is-leqrefine,
nat-inf/less-fin is used by startfin-weakfin-bwinv-is-leqrefine,
nat-inf/less-inf1 is used by startfin-weakfin-bwinv-is-leqrefine,
nat-inf/less-inf2 is used by startfin-weakfin-bwinv-is-leqrefine,
nat-inf/less-succ-leq is used by startfin-weakfin-bwinv-is-leqrefine,
nat-inf/ls-natinf-to-nat-1-2 is used by startfin-weakfin-bwinv-is-leqrefine,
nat-inf/num-add is used by startfin-weakfin-bwinv-is-leqrefine,

Used from specification list-data

list-data/elim-add is used by startfin-weakfin-bwinv-is-leqrefine,
list-data/l is used by startfin-weakfin-bwinv-is-leqrefine,

Used from specification list-del

list-del/get-append-less is used by startfin-weakfin-bwinv-is-leqrefine,
list-del/get-append-grt is used by startfin-weakfin-bwinv-is-leqrefine,
list-del/get-butlast is used by startfin-weakfin-bwinv-is-leqrefine,
list-del/get-last is used by startfin-weakfin-bwinv-is-leqrefine,
list-del/get-last-04 is used by startfin-weakfin-bwinv-is-leqrefine,
list-del/get-zero is used by startfin-weakfin-bwinv-is-leqrefine,
list-del/one-03 is used by startfin-weakfin-bwinv-is-leqrefine,

Used from specification IObackward-INV

IObackward-INV/backwardsiminv-def is used by startfin-weakfin-bwinv-is-leqrefine,
IObackward-INV/proofobls-backwardsiminv is used by startfin-weakfin-bwinv-is-leqrefine,

Used from specification IOrefine-def

IOrefine-def/leq-def is used by startfin-weakfin-bwinv-is-leqrefine,
IOrefine-def/leqstar-def is used by startfin-weakfin-bwinv-is-leqrefine,

Used from specification IObackward-INV-is-leqstarrefine

IObackward-INV-is-leqstarrefine/bwinv-leqstar is used by startfin-weakfin-bwinv-is-leqrefine,

Used from specification infgraph-gen

infgraph-gen/isroot-def is used by startfin-weakfin-bwinv-is-leqrefine,
infgraph-gen/path-def is used by startfin-weakfin-bwinv-is-leqrefine,
infgraph-gen/pathp-def is used by startfin-weakfin-bwinv-is-leqrefine,

Used from specification Koenigs-Lemma-gen

Koenigs-Lemma-gen/KoenigsLemma is used by startfin-weakfin-bwinv-is-leqrefine,
Koenigs-Lemma-gen/allreachable-def is used by startfin-weakfin-bwinv-is-leqrefine,
Koenigs-Lemma-gen/finout-def is used by startfin-weakfin-bwinv-is-leqrefine,
Koenigs-Lemma-gen/finroot-def is used by startfin-weakfin-bwinv-is-leqrefine,
Koenigs-Lemma-gen/infgraph-def is used by startfin-weakfin-bwinv-is-leqrefine,