[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 AccessControl4Vars

AccessControl4Vars/RMA-1 is used by Security-simple-without-initialstate, Security-without-initialstate, Security-simple, Security,
AccessControl4Vars/RMA-2 is used by step1-eqd, step-eqd,
AccessControl4Vars/RMA-3 is used by step1-eqd, step-eqd,
AccessControl4Vars/alter-observe-respects-policy is used by step1-eqd,
AccessControl4Vars/eqd-def is used by step1-eqd, step-eqd, eqd-transitivity, eqd-symmetry, eqd-reflexivity, LanguageBasedNIF-run, eqd-implies-LanguageBasedNIF,
AccessControl4Vars/extensionality is used by LanguageBasedNIF-follows,
AccessControl4Vars/no-read-up is used by step-eqd,
AccessControl4Vars/observe-all-names is used by step1-eqd, step-eqd, observe-names,
AccessControl4Vars/obs-in-domain is used by LanguageBasedNIF-follows,

Used from specification AccessControl4VarsTrans

AccessControl4VarsTrans/policy-is-reflexive is used by observe-names,
AccessControl4VarsTrans/policy-respects-observe is used by step-eqd,