[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 purge-idempotent, lemma1-gen,
list/gen-command-list/app-01 is used by purge-idempotent,
list/gen-command-list/c is used by purge-idempotent, lemma1-gen,

Used from specification AccessControlTrans

AccessControlTrans/policy-respects-observe is used by step-eqd,

Used from specification AccessControl

AccessControl/RMA-1 is used by Security-simple, Security,
AccessControl/RMA-2 is used by step1-eqd, step-eqd,
AccessControl/RMA-3 is used by step1-eqd, step-eqd,
AccessControl/alter-observe-respects-policy is used by step1-eqd,
AccessControl/eqd-def is used by step1-eqd, step-eqd, eqd-transitivity, eqd-symmetry, eqd-reflexivity,