[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/a
is used by
sources-ipurge,
lemma5-2,
lemma3-2,
ipurge-idempotent,
- list/gen-command-list/app-01
is used by
ipurge-idempotent,
- list/gen-command-list/app-03
is used by
ipurge-idempotent,
- list/gen-command-list/c
is used by
sources-ipurge,
sources-1,
lemma5-2,
lemma3-2,
ipurge-idempotent,
- list/gen-command-list/c-04
is used by
ipurge-idempotent,
Used from specification set-basic
- set-basic/gen-secdomain-set/In-insert
is used by
sources-ipurge,
sources-1,
lemma5-2,
lemma4,
lemma3-2,
ipurge-idempotent,
- set-basic/gen-secdomain-set/Size-insert
is used by
sources-ipurge,
ipurge-idempotent,
- set-basic/gen-secdomain-set/eq
is used by
sources-ipurge,
lemma5-2,
- set-basic/gen-secdomain-set/in-02
is used by
sources-ipurge,
- set-basic/gen-secdomain-set/in-03
is used by
sources-ipurge,
ipurge-idempotent,
- set-basic/gen-secdomain-set/in-04
is used by
sources-ipurge,
sources-1,
lemma5-2,
- set-basic/gen-secdomain-set/ne
is used by
sources-ipurge,
lemma5-2,
ipurge-idempotent,
- set-basic/gen-secdomain-set/ne-01
is used by
sources-ipurge,
sources-1,
lemma5-2,
lemma4,
lemma3-2,
ipurge-idempotent,
eqds-trans,
eqds-symm,
- set-basic/gen-secdomain-set/rax
is used by
sources-ipurge,
lemma5-2,
- set-basic/gen-secdomain-set/size-zero
is used by
sources-ipurge,
lemma5-2,
ipurge-idempotent,
- set-basic/gen-secdomain-set/size-zero-01
is used by
sources-ipurge,
sources-1,
lemma5-2,
lemma4,
lemma3-2,
ipurge-idempotent,
eqds-trans,
eqds-symm,
- AccessControlWithState/RMA-2
is used by
weakly-step-consistent2,
eqs-step,
- AccessControlWithState/RMA-3
is used by
weakly-step-consistent2,
locally-respects,
eqs-step,
- AccessControlWithState/alter-observe-respects-policy
is used by
locally-respects,
- AccessControlWithState/eqS-def
is used by
eqs-step,
eqs-reflexivity,
eqs-ipurged,
- AccessControlWithState/eqd-def
is used by
weakly-step-consistent2,
locally-respects2,
locally-respects,
eqd-transitivity,
eqd-symmetry,
eqd-reflexivity,
Security-simple,
Security,
- AccessControlWithState/eqs-step
is used by
lemma5-2,
- AccessControlWithState/extensionality
is used by
Security-simple,
Security,
- AccessControlWithState/obs-other-domain
is used by
Security-simple,
Security,
- AccessControlWithState/ipurged-dom
is used by
sources-ipurge,
- AccessControlWithState/ipurged-id
is used by
ipurge-idempotent,
- AccessControlWithState/ipurged-not
is used by
locally-respects2,
- AccessControlWithState/ipurged-req
is used by
eqs-ipurged,
- AccessControlWithState/obs-in-domain
is used by
Security-simple,
Security,
Used from specification nat-basic2