[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
Used from specification set-basic
- set-basic/gen-secdomain-set/In-insert
is used by
sources-ipurge,
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/eq
is used by
sources-ipurge,
ipurge-idempotent,
- set-basic/gen-secdomain-set/in-02
is used by
sources-ipurge,
- set-basic/gen-secdomain-set/in-04
is used by
sources-ipurge,
sources-1,
lemma5,
- set-basic/gen-secdomain-set/ne
is used by
sources-ipurge,
lemma3,
ipurge-idempotent,
- set-basic/gen-secdomain-set/ne-01
is used by
sources-ipurge,
sources-1,
lemma5,
lemma4,
lemma3,
ipurge-idempotent,
eqds-trans,
eqds-symm,
eqds-sources-ipurge-01,
- set-basic/gen-secdomain-set/rax
is used by
sources-ipurge,
ipurge-idempotent,
- set-basic/gen-secdomain-set/size-zero
is used by
sources-ipurge,
lemma3,
ipurge-idempotent,
- set-basic/gen-secdomain-set/size-zero-01
is used by
sources-ipurge,
sources-1,
lemma5,
lemma4,
lemma3,
ipurge-idempotent,
eqds-trans,
eqds-symm,
eqds-sources-ipurge-01,
Used from specification nat-basic2
- AccessControl4Vars/RMA-1
is used by
Security-simple-without-initialstate,
Security-strong,
- AccessControl4Vars/RMA-2
is used by
weakly-step-consistent,
- AccessControl4Vars/RMA-3
is used by
weakly-step-consistent,
locally-respects,
- AccessControl4Vars/alter-observe-respects-policy
is used by
locally-respects,
- AccessControl4Vars/eqd-def
is used by
weakly-step-consistent,
locally-respects,
eqd-transitivity,
eqd-symmetry,
eqd-reflexivity,
LanguageBasedNIF-weaker,
eqd-implies-LanguageBasedNIF,
LanguageBasedNIF-run,
LanguageBasedNIF-run-observe,
- AccessControl4Vars/no-read-up
is used by
LanguageBasedNIF-run-observe,
- AccessControl4Vars/obs-is-eqd
is used by
LanguageBasedNIF-weaker,
LanguageBasedNIF-follows,
- AccessControl4Vars/observe-all-names
is used by
locally-respects,