[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/last-one is used by wbw-leqstar,

Used from specification IOtrace

IOtrace/fintrace is used by bwinv-leqstar, wbw-leqstar,
IOtrace/move is used by bwinv-leqstar, wbw-leqstar,
IOtrace/preserve-INV-fin is used by bwinv-leqstar,
IOtrace/finexec is used by bwinv-leqstar, wbw-leqstar,
IOtrace/finfrag-one is used by wbw-leqstar,

Used from specification IO-Aut-data

IO-Aut-data/sel-IOAut-dotext is used by bwinv-leqstar, wbw-leqstar,
IO-Aut-data/sel-IOAut-dotstart is used by bwinv-leqstar, wbw-leqstar,

Used from specification list-del

list-del/one-03 is used by wbw-leqstar,

Used from specification IObackward-INV

IObackward-INV/backwardsim-def is used by bwtrueinv,
IObackward-INV/backwardsiminv-def is used by bwinv-leqstar, bwtrueinv,
IObackward-INV/lemma_3-15 is used by bwinv-leqstar,
IObackward-INV/proofobls-backwardsim is used by bwtrueinv-aux,
IObackward-INV/proofobls-backwardsiminv is used by bwinv-leqstar, bwtrueinv-aux,
IObackward-INV/proofobls-weakbackwardsim is used by wbw-leqstar,
IObackward-INV/weak-lemma_3-15 is used by wbw-leqstar,
IObackward-INV/weakbackwardsim-def is used by wbw-leqstar,

Used from specification IOrefine-def

IOrefine-def/leqstar-def is used by bwinv-leqstar, wbw-leqstar,