[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 lemma1-gen, inv-run-gen,
list/gen-command-list/c is used by lemma1-gen, inv-run-gen,

Used from specification gen-CongTrans

gen-CongTrans/eqd-refl is used by lemma1,
gen-CongTrans/eqd-symm is used by lemma1-gen,
gen-CongTrans/eqd-trans is used by lemma1-gen,
gen-CongTrans/inv-exec is used by lemma1-gen, inv-run-gen,
gen-CongTrans/inv-init is used by lemma1, inv-run,
gen-CongTrans/locally-respects is used by lemma1-gen,
gen-CongTrans/output-consistent is used by Security,
gen-CongTrans/step-consistent is used by lemma1-gen,