[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
lemma5,
inv-run-gen,
- list/gen-command-list/c
is used by
sources-rec-lem,
sources-equal,
sources-1,
run-rec-lem,
purge-rec-lem,
lemma5,
lemma4,
lemma3,
inv-run-gen,
- gen-CongIntrans/dom-equal
is used by
sources-equal,
- gen-CongIntrans/dom-equiv
is used by
sources-equal,
lemma3,
- gen-CongIntrans/eqd-trans
is used by
lemma3,
- gen-CongIntrans/inv-exec
is used by
inv-run-gen,
- gen-CongIntrans/locally-respects
is used by
lemma5,
lemma4,
lemma3,
- gen-CongIntrans/output-cons
is used by
secure,
- gen-CongIntrans/weakly-step-consistent
is used by
lemma3,
- gen-CongIntrans/eqd-refl
is used by
eqds-refl,
- gen-CongIntrans/eqd-symm-lem
is used by
lemma5,
lemma3,
eqds-symm,
- gen-CongIntrans/eqd-trans-lem
is used by
lemma3,
eqds-trans,
- gen-CongIntrans/inv-exec-lem
is used by
sources-equal,
lemma5,
- gen-CongIntrans/inv-init
is used by
lemma2,
inv-run,
Used from specification pair
- pair/gen-sys-out/elim
is used by
sources-equal,
sources-1,
secure,
lemma5,
lemma4,
lemma3,
inv-run-gen,
- pair/gen-sys-out/sel-02
is used by
sources-equal,
lemma5,
lemma4,
lemma3,
inv-run-gen,
Used from specification set-basic
- set-basic/gen-secdomain-set/In-insert
is used by
sources-1,
lemma5,
lemma4,
lemma3,
- set-basic/gen-secdomain-set/eq-03
is used by
sources-equal,
- set-basic/gen-secdomain-set/in-04
is used by
sources-1,
lemma5,
- set-basic/gen-secdomain-set/ne-01
is used by
sources-equal,
sources-1,
lemma5,
lemma4,
lemma3,
eqds-trans,
eqds-symm,
- set-basic/gen-secdomain-set/rax
is used by
sources-equal,
- set-basic/gen-secdomain-set/size-zero-01
is used by
sources-equal,
sources-1,
lemma5,
lemma4,
lemma3,
eqds-trans,
eqds-symm,