[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/gen-command-list/Nil
is used by
sources-app,
- list/gen-command-list/a
is used by
sources-rec-01,
sources-one,
sources-interfere,
sources-app,
lemma5,
ipurge-idempotent,
- list/gen-command-list/app
is used by
sources-one,
- list/gen-command-list/app-01
is used by
ipurge-idempotent,
- list/gen-command-list/c
is used by
sources-rec-01,
sources-not-empty,
sources-ipurge,
sources-interfere,
sources-app,
sources-1,
lemma5,
lemma3,
ipurge-idempotent,
- list/gen-command-list/e-01
is used by
sources-rec-01,
- list/gen-command-list/in-17
is used by
sources-interfere,
- list/gen-command-list/in-append
is used by
sources-interfere,
- list/gen-command-list/in-empty
is used by
sources-interfere,
Used from specification set-basic
- set-basic/gen-secdomain-set/In-insert
is used by
sources-two-transitive,
sources-one-transitive,
sources-ipurge,
sources-interfere,
sources-in-two,
sources-in-one,
sources-1,
lemma5,
lemma4,
lemma3,
ipurge-idempotent,
- set-basic/gen-secdomain-set/Size-insert
is used by
sources-ipurge,
lemma3,
ipurge-idempotent,
- set-basic/gen-secdomain-set/add-01
is used by
sources-two-transitive,
sources-one-transitive,
- set-basic/gen-secdomain-set/eq
is used by
sources-ipurge,
ipurge-idempotent,
- set-basic/gen-secdomain-set/eq-03
is used by
sources-rec-01,
sources-app,
- set-basic/gen-secdomain-set/in-02
is used by
sources-two-transitive,
sources-one-transitive,
sources-ipurge,
sources-in-two,
sources-in-one,
- set-basic/gen-secdomain-set/in-03
is used by
sources-ipurge,
- set-basic/gen-secdomain-set/in-04
is used by
sources-two-transitive,
sources-one-transitive,
sources-one,
sources-not-in,
sources-ipurge,
sources-in-two,
sources-in-one,
sources-1,
lemma5,
- set-basic/gen-secdomain-set/ne
is used by
sources-two-transitive,
sources-one-transitive,
sources-not-empty,
sources-ipurge,
sources-in-two,
lemma3,
ipurge-idempotent,
- set-basic/gen-secdomain-set/ne-01
is used by
sources-two-transitive,
sources-rec-01,
sources-one-transitive,
sources-ipurge,
sources-in-two,
sources-app,
sources-1,
lemma5,
lemma4,
lemma3,
ipurge-idempotent,
eqds-trans,
eqds-symm,
eqds-sources-ipurge,
- set-basic/gen-secdomain-set/rax
is used by
sources-two-transitive,
sources-one-transitive,
sources-ipurge,
sources-in-two,
ipurge-idempotent,
- set-basic/gen-secdomain-set/size-one-01
is used by
sources-two-transitive,
sources-one-transitive,
sources-in-two,
- set-basic/gen-secdomain-set/size-zero
is used by
sources-two-transitive,
sources-one-transitive,
sources-not-empty,
sources-ipurge,
sources-in-two,
lemma3,
ipurge-idempotent,
- set-basic/gen-secdomain-set/size-zero-01
is used by
sources-two-transitive,
sources-one-transitive,
sources-not-empty,
sources-ipurge,
sources-in-two,
sources-1,
lemma5,
lemma4,
lemma3,
ipurge-idempotent,
eqds-trans,
eqds-symm,
eqds-sources-ipurge,
- set-basic/gen-secdomain-set/size-zero-02
is used by
sources-not-empty-01,
- AccessControl/RMA-1
is used by
Security-strong,
Security-simple-without-initialstate,
Security-simple,
- AccessControl/RMA-2
is used by
weakly-step-consistent,
- AccessControl/RMA-3
is used by
weakly-step-consistent,
locally-respects,
- AccessControl/alter-observe-respects-policy
is used by
locally-respects,
- AccessControl/eqd-def
is used by
weakly-step-consistent,
locally-respects,
eqd-transitivity,
eqd-symmetry,
eqd-reflexivity,
Security,
- AccessControl/extensionality
is used by
Security,
- AccessControl/obs-other-domain
is used by
Security,
- AccessControl/obs-in-domain
is used by
Security,
Used from specification list-data
Used from specification nat-basic2