[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/lapp is used by normedfw-branchingfw-aux,
list-last/l-02 is used by imfiniobackwardinv-implies-leqrefine-aux, normedfw-branchingfw-aux,
list-last/l-in is used by branchingfw-normedfw-aux, triang-fin, normedfw-branchingfw-aux,
list-last/last-01 is used by imfiniobackwardinv-implies-leqrefine-aux, branchinfw-fw-aux,
list-last/last-def is used by branchinfw-fw-aux, normedfw-branchingfw-aux,
list-last/last-elim is used by branchinfw-fw-aux, normedfw-branchingfw-aux,
list-last/last-one is used by imfiniobackwardinv-implies-leqrefine-aux, branchingfw-normedfw-aux, triang-fin, wbw-leqstar, forward-implies-leqrefine, normedfw-branchingfw-aux,
list-last/last-rec is used by branchingfw-normedfw-aux, triang-fin,

Used from specification nat

nat/le-def is used by branchingfw-normedfw-aux,
nat/succ-01 is used by branchingfw-normedfw-aux,
nat/add-num-03 is used by imfiniobackwardinv-implies-leqrefine-aux,
nat/anti is used by imfiniobackwardinv-implies-leqrefine-aux,
nat/elim-pred-c is used by imfiniobackwardinv-implies-leqrefine-aux,
nat/eqle-one is used by normedfw-branchingfw-aux,
nat/fle-01 is used by imfiniobackwardinv-implies-leqrefine-aux,
nat/l-num-01 is used by imfiniobackwardinv-implies-leqrefine-aux,
nat/le-ls-simp is used by imfiniobackwardinv-implies-leqrefine-aux,
nat/lels is used by imfiniobackwardinv-implies-leqrefine-aux, branchingfw-normedfw-aux, normedfw-branchingfw-aux,
nat/lels-03 is used by imfiniobackwardinv-implies-leqrefine-aux,
nat/lep is used by normedfw-branchingfw-aux,
nat/ler is used by imfiniobackwardinv-implies-leqrefine-aux, normedfw-branchingfw-aux,
nat/ls-le-simp is used by normedfw-branchingfw-aux,
nat/succ-01 is used by normedfw-branchingfw-aux,
nat/zero is used by imfiniobackwardinv-implies-leqrefine-aux,

Used from specification remtau

remtau/finremtau-append is used by branchinfw-fw-aux, branchingfw-normedfw-aux, triang-fin, normedfw-branchingfw-aux,
remtau/finremtau-def is used by imfiniobackwardinv-implies-leqrefine-aux, triang-fin, branchingfw-normedfw, forward-implies-leqrefine, normedfw-branchingfw-aux,
remtau/finremtau-empty is used by branchingfw-normedfw-aux, triang-fin,
remtau/finremtau-one is used by imfiniobackwardinv-implies-leqrefine-aux, branchinfw-fw-aux, branchingfw-normedfw-aux, bwinv-leqstar, wbw-leqstar, bwtrueinv-aux, simpleforward-is-forward-aux, forward-lem, forward-implies-leqrefine,
remtau/remtau-one is used by branchinfw-fw-aux,
remtau/remtau-one-03 is used by triang-fin, normedfw-branchingfw-aux,

Used from specification infgraph-gen-basic

infgraph-gen-basic/edge-def is used by imfiniobackwardinv-implies-leqrefine-aux,
infgraph-gen-basic/dom-def is used by imfiniobackwardinv-implies-leqrefine-aux,

Used from specification set-basic

set-basic/In-empty is used by imfiniobackwardinv-implies-leqrefine-aux,
set-basic/In-insert is used by imfiniobackwardinv-implies-leqrefine-aux,
set-basic/ne-01 is used by imfiniobackwardinv-implies-leqrefine-aux,
set-basic/size-zero-01 is used by imfiniobackwardinv-implies-leqrefine-aux,

Used from specification list-getput

list-getput/get-zero-01 is used by forward-implies-leqrefine,
list-getput/get-zero-01 is used by imfiniobackwardinv-implies-leqrefine-aux, normedfw-branchingfw-aux,

Used from specification nat-basic

nat-basic/a is used by imfiniobackwardinv-implies-leqrefine-aux, branchingfw-normedfw-aux, forward-implies-leqrefine, normedfw-branchingfw-aux,
nat-basic/add-base is used by normedfw-branchingfw-aux,
nat-basic/c is used by imfiniobackwardinv-implies-leqrefine-aux, branchingfw-normedfw-aux, forward-implies-leqrefine, normedfw-branchingfw-aux,
nat-basic/eq-01 is used by imfiniobackwardinv-implies-leqrefine-aux, normedfw-branchingfw-aux,
nat-basic/f is used by imfiniobackwardinv-implies-leqrefine-aux, triang-fin, normedfw-branchingfw-aux,
nat-basic/l-02 is used by imfiniobackwardinv-implies-leqrefine-aux, normedfw-branchingfw-aux,
nat-basic/less-zero is used by imfiniobackwardinv-implies-leqrefine-aux,
nat-basic/lf is used by normedfw-branchingfw-aux,
nat-basic/lf-01 is used by imfiniobackwardinv-implies-leqrefine-aux, normedfw-branchingfw-aux,
nat-basic/lf-02 is used by imfiniobackwardinv-implies-leqrefine-aux,
nat-basic/ls-02 is used by imfiniobackwardinv-implies-leqrefine-aux,
nat-basic/nls-fst is used by imfiniobackwardinv-implies-leqrefine-aux, normedfw-branchingfw-aux,
nat-basic/one-01 is used by imfiniobackwardinv-implies-leqrefine-aux,
nat-basic/oz is used by imfiniobackwardinv-implies-leqrefine-aux,
nat-basic/refl-Nat is used by imfiniobackwardinv-implies-leqrefine-aux, normedfw-branchingfw-aux,
nat-basic/s-04 is used by imfiniobackwardinv-implies-leqrefine-aux, normedfw-branchingfw-aux,
nat-basic/succ is used by imfiniobackwardinv-implies-leqrefine-aux, branchingfw-normedfw-aux, forward-implies-leqrefine, normedfw-branchingfw-aux,
nat-basic/trans-Nat is used by normedfw-branchingfw-aux,
nat-basic/z-01 is used by forward-implies-leqrefine, normedfw-branchingfw-aux,
nat-basic/zero is used by imfiniobackwardinv-implies-leqrefine-aux, normedfw-branchingfw-aux,

Used from specification list

list/first-01 is used by normedfw-branchingfw-aux,
list/Last is used by normedfw-branchingfw-aux,
list/Nil is used by triang-fin, normedfw-branchingfw-aux,
list/a is used by imfiniobackwardinv-implies-leqrefine-aux, branchinfw-fw-aux, branchingfw-normedfw-aux, triang-fin, forward-implies-leqrefine, normedfw-branchingfw-aux,
list/app is used by branchingfw-normedfw-aux, normedfw-branchingfw-aux,
list/app-02 is used by imfiniobackwardinv-implies-leqrefine-aux, branchinfw-fw-aux, branchingfw-normedfw-aux, triang-fin, normedfw-branchingfw-aux,
list/c is used by imfiniobackwardinv-implies-leqrefine-aux, branchinfw-fw-aux, branchingfw-normedfw-aux, triang-fin, forward-implies-leqrefine, normedfw-branchingfw-aux,
list/c-03 is used by branchingfw-normedfw-aux,
list/c-05 is used by branchinfw-fw-aux,
list/c-08 is used by imfiniobackwardinv-implies-leqrefine-aux, branchingfw-normedfw-aux, triang-fin,
list/e is used by imfiniobackwardinv-implies-leqrefine-aux, branchinfw-fw-aux, branchingfw-normedfw-aux, triang-fin, forward-implies-leqrefine, normedfw-branchingfw-aux,
list/first is used by imfiniobackwardinv-implies-leqrefine-aux, triang-fin,
list/in-14 is used by branchinfw-fw-aux,
list/in-15 is used by branchinfw-fw-aux,
list/in-17 is used by branchinfw-fw-aux, triang-fin,
list/in-append is used by branchinfw-fw-aux, normedfw-branchingfw-aux,
list/in-empty is used by branchingfw-normedfw-aux,
list/in-rec is used by branchinfw-fw-aux, branchingfw-normedfw-aux, triang-fin, normedfw-branchingfw-aux,
list/len is used by normedfw-branchingfw-aux,
list/len-02 is used by imfiniobackwardinv-implies-leqrefine-aux, normedfw-branchingfw-aux,
list/len-05 is used by branchingfw-normedfw-aux,

Used from specification IOtrace

IOtrace/finfrag-rec is used by branchingfw-normedfw-aux, triang-fin,
IOtrace/finfrag-rec-end is used by branchinfw-fw-aux, normedfw-branchingfw-aux,
IOtrace/finfrag-split is used by normedfw-branchingfw-aux,
IOtrace/fintrace is used by imfiniobackwardinv-implies-leqrefine-aux, bwinv-leqstar, wbw-leqstar, forward-implies-leqrefine,
IOtrace/fraginf is used by forward-implies-leqrefine,
IOtrace/infappend-moves-gen is used by imfiniobackwardinv-implies-leqrefine-aux, forward-implies-leqrefine,
IOtrace/move is used by branchinfw-fw-aux, bwinv-leqstar, wbw-leqstar, forward-implies-leqrefine, normedfw-branchingfw-aux,
IOtrace/move-one is used by simpleforward-is-forward-aux,
IOtrace/preserve-INV is used by imfiniobackwardinv-implies-leqrefine-aux,
IOtrace/preserve-INV-fin is used by bwinv-leqstar,
IOtrace/trace is used by imfiniobackwardinv-implies-leqrefine-aux, forward-implies-leqrefine,
IOtrace/exec is used by imfiniobackwardinv-implies-leqrefine-aux, forward-implies-leqrefine,
IOtrace/finexec is used by imfiniobackwardinv-implies-leqrefine-aux, bwinv-leqstar, wbw-leqstar, forward-lem, forward-implies-leqrefine,
IOtrace/finfrag-one is used by triang-fin, wbw-leqstar,
IOtrace/finfrag-onlyone is used by branchingfw-normedfw-aux,
IOtrace/frag-finite-sl is used by imfiniobackwardinv-implies-leqrefine-aux, forward-implies-leqrefine,
IOtrace/frag-inf-sl is used by imfiniobackwardinv-implies-leqrefine-aux, forward-implies-leqrefine,
IOtrace/frag-step-inf-inf is used by imfiniobackwardinv-implies-leqrefine-aux, forward-implies-leqrefine,
IOtrace/fragfin-size is used by forward-implies-leqrefine, normedfw-branchingfw-aux,
IOtrace/fragfin-size-le1 is used by normedfw-branchingfw-aux,
IOtrace/fragfin-size-ls1 is used by normedfw-branchingfw-aux,
IOtrace/fragfin-size-notls is used by normedfw-branchingfw-aux,
IOtrace/fragomega-def is used by imfiniobackwardinv-implies-leqrefine-aux,
IOtrace/fragstar-def is used by branchingfw-normedfw,
IOtrace/fragstar-onestate is used by branchingfw-normedfw-aux, normedfw-branchingfw-aux,
IOtrace/move-empty is used by branchinfw-fw-aux, simpleforward-is-forward-aux, normedfw-branchingfw-aux,
IOtrace/not-finfrag-empty is used by branchinfw-fw-aux, branchingfw-normedfw-aux, triang-fin, forward-implies-leqrefine, normedfw-branchingfw-aux,
IOtrace/tracestar-def is used by imfiniobackwardinv-implies-leqrefine-aux, forward-implies-leqrefine,

Used from specification stream

stream/fin-finlen-tolen is used by normedfw-branchingfw-aux,
stream/append-assoc is used by imfiniobackwardinv-implies-leqrefine-aux,
stream/append-finfin is used by imfiniobackwardinv-implies-leqrefine-aux,
stream/append-from-size is used by normedfw-branchingfw-aux,
stream/fin-empty is used by triang-fin, branchingfw-normedfw, normedfw-branchingfw-aux,
stream/get-append2-fin is used by imfiniobackwardinv-implies-leqrefine-aux,
stream/get-append3-fin is used by imfiniobackwardinv-implies-leqrefine-aux,
stream/get-cons-succ is used by imfiniobackwardinv-implies-leqrefine-aux,
stream/get-from-01 is used by normedfw-branchingfw-aux,
stream/sel-fin is used by imfiniobackwardinv-implies-leqrefine-aux, forward-implies-leqrefine,
stream/sel-inf is used by imfiniobackwardinv-implies-leqrefine-aux, forward-implies-leqrefine,
stream/size-append is used by imfiniobackwardinv-implies-leqrefine-aux,
stream/size-fin is used by imfiniobackwardinv-implies-leqrefine-aux,
stream/size-inf is used by imfiniobackwardinv-implies-leqrefine-aux,

Used from specification IO-Aut-data

IO-Aut-data/sel-IOAut-dotext is used by branchinfw-fw-aux, bwinv-leqstar, wbw-leqstar, forward-implies-leqrefine, normedfw-branchingfw-aux,
IO-Aut-data/sel-IOAut-dotstart is used by imfiniobackwardinv-implies-leqrefine-aux, bwinv-leqstar, wbw-leqstar, forward-lem, forward-implies-leqrefine,
IO-Aut-data/sel-IOAut-dotstep is used by forward-implies-leqrefine,

Used from specification nat-inf

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

Used from specification stream-basic

stream-basic/elim-finp-ant is used by imfiniobackwardinv-implies-leqrefine-aux, forward-implies-leqrefine,
stream-basic/elim-finp-suc is used by imfiniobackwardinv-implies-leqrefine-aux, forward-implies-leqrefine,
stream-basic/inj-rqui is used by forward-implies-leqrefine,
stream-basic/sel-rqui-dotl is used by imfiniobackwardinv-implies-leqrefine-aux, forward-implies-leqrefine,
stream-basic/sel-rqui0-dotf is used by imfiniobackwardinv-implies-leqrefine-aux, forward-implies-leqrefine,

Used from specification list-data

list-data/elim-add is used by imfiniobackwardinv-implies-leqrefine-aux,
list-data/elim-list-c is used by branchinfw-fw-aux, branchingfw-normedfw-aux, triang-fin, forward-implies-leqrefine, normedfw-branchingfw-aux,
list-data/l is used by imfiniobackwardinv-implies-leqrefine-aux, forward-implies-leqrefine, normedfw-branchingfw-aux,
list-data/size-nil is used by branchingfw-normedfw-aux, forward-implies-leqrefine, normedfw-branchingfw-aux,

Used from specification option

option/disj-Some-None is used by simpleforward-is-forward-aux,
option/elim-Some is used by simpleforward-is-forward-aux,

Used from specification list-del

list-del/first-append-02 is used by normedfw-branchingfw-aux,
list-del/get-append-grt is used by imfiniobackwardinv-implies-leqrefine-aux,
list-del/get-append-less is used by imfiniobackwardinv-implies-leqrefine-aux, normedfw-branchingfw-aux,
list-del/in-get is used by normedfw-branchingfw-aux,
list-del/elim-firstn-restn is used by normedfw-branchingfw-aux,
list-del/firstN-len is used by normedfw-branchingfw-aux,
list-del/get-append-grt is used by imfiniobackwardinv-implies-leqrefine-aux, normedfw-branchingfw-aux,
list-del/get-append-less is used by imfiniobackwardinv-implies-leqrefine-aux,
list-del/get-butlast is used by imfiniobackwardinv-implies-leqrefine-aux,
list-del/get-last is used by imfiniobackwardinv-implies-leqrefine-aux,
list-del/get-last-04 is used by imfiniobackwardinv-implies-leqrefine-aux,
list-del/get-zero is used by branchinfw-fw-aux, forward-implies-leqrefine,
list-del/one-03 is used by imfiniobackwardinv-implies-leqrefine-aux, wbw-leqstar,
list-del/restn-last is used by normedfw-branchingfw-aux,
list-del/restn-prefix is used by normedfw-branchingfw-aux,

Used from specification Unknown

Unknown/Unknown is used by normedfw-branchingfw-aux,

Used from specification IOrefine-def

IOrefine-def/leq-def is used by imfiniobackwardinv-implies-leqrefine-aux, forward-implies-leqrefine,
IOrefine-def/leqstar-def is used by imfiniobackwardinv-implies-leqrefine-aux, bwinv-leqstar, wbw-leqstar,

Used from specification infinite-append

infinite-append/nextl-lemma-butlast is used by forward-implies-leqrefine,

Used from specification infgraph-gen

infgraph-gen/isroot-def is used by imfiniobackwardinv-implies-leqrefine-aux,
infgraph-gen/path-def is used by imfiniobackwardinv-implies-leqrefine-aux,
infgraph-gen/pathp-def is used by imfiniobackwardinv-implies-leqrefine-aux,

Used from specification min-of-Pnat

min-of-Pnat/min-def is used by branchingfw-normedfw-aux,
min-of-Pnat/min-leq-def is used by branchingfw-normedfw-aux,

Used from specification IOrefine-conds

IOrefine-conds/backwardsim-def is used by bwtrueinv,
IOrefine-conds/backwardsiminv-def is used by imfiniobackwardinv-implies-leqrefine-aux, bwinv-leqstar, bwtrueinv,
IOrefine-conds/branchingforwardsim-def is used by branchingfw-normedfw, normedfw-branchingfw, branchinfw-fw,
IOrefine-conds/forwardsim-def is used by branchinfw-fw, simpleforward-is-forward, forward-implies-leqrefine,
IOrefine-conds/fw-frag is used by forward-lem,
IOrefine-conds/imfinbackwardsim-def is used by imfiniobackwardinv-implies-leqrefine,
IOrefine-conds/lemma_3-15 is used by bwinv-leqstar,
IOrefine-conds/normedforwardsim-def is used by branchingfw-normedfw, normedfw-branchingfw,
IOrefine-conds/proofobls-backwardsim is used by bwtrueinv-aux,
IOrefine-conds/proofobls-backwardsiminv is used by imfiniobackwardinv-implies-leqrefine-aux, bwinv-leqstar, bwtrueinv-aux,
IOrefine-conds/proofobls-branchingforwardsim is used by branchinfw-fw-aux, branchingfw-normedfw-aux, normedfw-branchingfw-aux,
IOrefine-conds/proofobls-forwardsim is used by branchinfw-fw-aux, simpleforward-is-forward-aux, forward-lem, forward-implies-leqrefine,
IOrefine-conds/proofobls-imfinbackwardsim is used by imfiniobackwardinv-implies-leqrefine-aux,
IOrefine-conds/proofobls-normedforwardsim is used by branchingfw-normedfw-aux, triang-fin, normedfw-branchingfw-aux,
IOrefine-conds/proofobls-simpleforwardsim is used by simpleforward-is-forward-aux,
IOrefine-conds/proofobls-weakbackwardsim is used by wbw-leqstar,
IOrefine-conds/simpleforwardsim-def is used by simpleforward-is-forward,
IOrefine-conds/weak-lemma_3-15 is used by wbw-leqstar,
IOrefine-conds/weakbackwardsim-def is used by wbw-leqstar,

Used from specification Koenigs-Lemma-gen

Koenigs-Lemma-gen/KoenigsLemma is used by imfiniobackwardinv-implies-leqrefine-aux,
Koenigs-Lemma-gen/allreachable-def is used by imfiniobackwardinv-implies-leqrefine-aux,
Koenigs-Lemma-gen/finout-def is used by imfiniobackwardinv-implies-leqrefine-aux,
Koenigs-Lemma-gen/finroot-def is used by imfiniobackwardinv-implies-leqrefine-aux,
Koenigs-Lemma-gen/infgraph-def is used by imfiniobackwardinv-implies-leqrefine-aux,