[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

list/trace/Nil is used by lemma-5-4-2,
list/trace/a is used by xlrf-property, unwind-BSD-theorem, lemma-5-4-2,
list/trace/app-01 is used by xlrf-property,
list/trace/app-02-ant is used by lemma-5-4-2,
list/trace/app-03 is used by xlrf-property,
list/trace/c is used by xlrf-property, unwind-BSRA-theorem, unwind-BSD-theorem, lemma-5-4-2,
list/trace/c-04 is used by xlrf-property,

Used from specification eventfunsHO

eventfunsHO/enabled-def is used by unwind-BSRA-theorem, unwind-BSD-theorem, lemma-5-4-2,
eventfunsHO/in-trace-def is used by unwind-BSRA-theorem, unwind-BSD-theorem,
eventfunsHO/projection-one-if is used by xlrf-property,
eventfunsHO/reachable-trans is used by unwind-BSRA-theorem,
eventfunsHO/transex-append is used by xlrf-property, unwind-BSRA-theorem, unwind-BSD-theorem, lemma-5-4-2,
eventfunsHO/transex-enabled-intrans is used by unwind-BSRA-theorem,
eventfunsHO/transex-rec is used by xlrf-property, unwind-BSRA-theorem, unwind-BSD-theorem, lemma-5-4-2,
eventfunsHO/validx-def is used by unwind-BSRA-theorem,
eventfunsHO/VCview is used by xlrf-property,
eventfunsHO/Vview is used by xlrf-property,
eventfunsHO/enabled-empty is used by lemma-5-4-2,
eventfunsHO/enabled-transex is used by unwind-BSD-theorem, lemma-5-4-2,
eventfunsHO/projection-VC-C is used by xlrf-property,
eventfunsHO/projection-append is used by xlrf-property, lemma-5-4-2,
eventfunsHO/projection-empty is used by xlrf-property, lemma-5-4-2,
eventfunsHO/projection-one-01 is used by xlrf-property,
eventfunsHO/projection-one-empty is used by lemma-5-4-2,
eventfunsHO/projection-one-empty-01 is used by xlrf-property,
eventfunsHO/reachable-trans is used by xlrf-property, unwind-BSD-theorem, lemma-5-4-2,
eventfunsHO/reachable-transex is used by xlrf-property, lemma-5-4-2,
eventfunsHO/reachable-transex-01 is used by unwind-BSRA-theorem, unwind-BSD-theorem,
eventfunsHO/transex-empty is used by xlrf-property,
eventfunsHO/transex-enabled-intrans is used by unwind-BSD-theorem,

Used from specification view

view/disj-03 is used by xlrf-property,

Used from specification BSPs

BSPs/BSP_BSD-def is used by unwind-BSD-theorem,
BSPs/BSP_BSRA-def is used by unwind-BSRA-theorem,
BSPs/SD-equiv-BSD-N2V is used by unwind-SD-theorem,