[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 eventfuns

eventfuns/enabled-def is used by lemma-5-4-2, BSD-unwind-theorem,
eventfuns/in-trace-def is used by BSD-unwind-theorem,
eventfuns/transex-append is used by lemma-5-4-2, BSD-unwind-theorem,
eventfuns/transex-rec is used by lemma-5-4-2, BSD-unwind-theorem,
eventfuns/enabled-empty is used by lemma-5-4-2,
eventfuns/enabled-transex is used by lemma-5-4-2, BSD-unwind-theorem,
eventfuns/projection-append is used by lemma-5-4-2,
eventfuns/projection-empty is used by lemma-5-4-2,
eventfuns/projection-one-empty is used by lemma-5-4-2,
eventfuns/reachable-trans is used by lemma-5-4-2, BSD-unwind-theorem,
eventfuns/reachable-transex is used by lemma-5-4-2,
eventfuns/reachable-transex-01 is used by BSD-unwind-theorem,
eventfuns/transex-enabled-intrans is used by BSD-unwind-theorem,

Used from specification list

list/trace/Nil is used by lemma-5-4-2,
list/trace/a is used by lemma-5-4-2, BSD-unwind-theorem,
list/trace/app-02-ant is used by lemma-5-4-2,
list/trace/c is used by lemma-5-4-2, BSD-unwind-theorem,

Used from specification MAKS-BSD-unwinding

MAKS-BSD-unwinding/lrf-def is used by BSD-unwind-theorem,
MAKS-BSD-unwinding/osc-def is used by osc-help,