[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-06 is used by lemma_3-15, weak-lemma_3-15,
list-last/last-01 is used by weakbwsim-implies-bwsiminv-aux,
list-last/last-def is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15,
list-last/last-one is used by weakbwsim-implies-bwsiminv-aux, lemma_3-15, weak-lemma_3-15, bwsiminv-implies-weakbwsim-aux,
list-last/last-rec is used by lemma_3-15, weak-lemma_3-15, bwsiminv-implies-weakbwsim-aux,

Used from specification remtau

remtau/finremtau-append is used by lemma_3-15, weak-lemma_3-15,
remtau/finremtau-def is used by weakbwsim-implies-bwsiminv-aux,
remtau/finremtau-empty is used by lemma_3-15, weak-lemma_3-15,
remtau/finremtau-one is used by weakbwsim-implies-bwsiminv-aux, lemma_3-15, weak-lemma_3-15, bwsim-bwsiminv-aux, bwsiminv-implies-weakbwsim-aux,

Used from specification list-getput

list-getput/get-zero-01 is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15,

Used from specification nat-basic

nat-basic/zero is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15,

Used from specification list

list/Last is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15,
list/a is used by weakbwsim-implies-bwsiminv-aux, lemma_3-15, weak-lemma_3-15, bwsiminv-implies-weakbwsim-aux,
list/app is used by lemma_3-15, weak-lemma_3-15, bwsiminv-implies-weakbwsim-aux,
list/app-02 is used by weakbwsim-implies-bwsiminv-aux, lemma_3-15, weak-lemma_3-15,
list/c is used by weakbwsim-implies-bwsiminv-aux, lemma_3-15, weak-lemma_3-15, bwsiminv-implies-weakbwsim-aux,
list/c-03 is used by lemma_3-15, weak-lemma_3-15, bwsiminv-implies-weakbwsim-aux,
list/c-08 is used by bwsiminv-implies-weakbwsim-aux,
list/e is used by weakbwsim-implies-bwsiminv-aux, lemma_3-15, weak-lemma_3-15,

Used from specification IOtrace

IOtrace/finfrag-rec is used by lemma_3-15, weak-lemma_3-15, bwsiminv-implies-weakbwsim-aux,
IOtrace/finfrag-rec-end is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15,
IOtrace/move is used by weakbwsim-implies-bwsiminv-aux, lemma_3-15, weak-lemma_3-15,
IOtrace/move-trans is used by lemma_3-15, weak-lemma_3-15,
IOtrace/finexec is used by weakbwsim-implies-bwsiminv, weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15, bwsiminv-implies-weakbwsim-aux,
IOtrace/finfrag-one is used by weakbwsim-implies-bwsiminv-aux,
IOtrace/finfrag-onlyone is used by lemma_3-15, weak-lemma_3-15, bwsiminv-implies-weakbwsim-aux,
IOtrace/move-empty is used by lemma_3-15, weak-lemma_3-15,
IOtrace/not-finfrag-empty is used by weakbwsim-implies-bwsiminv-aux, lemma_3-15, weak-lemma_3-15, bwsiminv-implies-weakbwsim-aux,

Used from specification stream

stream/append-assoc is used by bwsiminv-implies-weakbwsim-aux,
stream/append-finfin is used by bwsiminv-implies-weakbwsim-aux,
stream/hd-fin-lem is used by bwsiminv-implies-weakbwsim-aux,

Used from specification IO-Aut-data

IO-Aut-data/sel-IOAut-dotext is used by weakbwsim-implies-bwsiminv-aux, lemma_3-15, weak-lemma_3-15,
IO-Aut-data/sel-IOAut-dotstart is used by weakbwsim-implies-bwsiminv, weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15, bwsiminv-implies-weakbwsim-aux,

Used from specification stream-basic

stream-basic/sel-rqui-dotl is used by weakbwsim-implies-bwsiminv-aux,

Used from specification list-data

list-data/elim-add is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15,
list-data/elim-list-c is used by weakbwsim-implies-bwsiminv-aux, lemma_3-15, weak-lemma_3-15,
list-data/l is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15,

Used from specification list-del

list-del/get-append-less is used by weakbwsim-implies-bwsiminv-aux, weak-lemma_3-15,
list-del/get-zero is used by weakbwsim-implies-bwsiminv-aux, lemma_3-15, weak-lemma_3-15, bwsiminv-implies-weakbwsim-aux,
list-del/one-03 is used by weakbwsim-implies-bwsiminv-aux,